Làm cách nào để Idris tự động chứng minh rằng hai giá trị không bằng nhau?

Question

Làm cách nào để Idris tự động chứng minh rằng hai giá trị không bằng nhau?

p : Not (Int = String) 
p = \Refl impossible 

Làm cách nào để Idris tự động tạo bằng chứng này? auto dường như không có khả năng chứng minh các tuyên bố liên quan đến Not. Mục tiêu cuối cùng của tôi là để Idris tự động chứng minh rằng tất cả các phần tử trong một véc tơ là duy nhất và hai vectơ tách rời nhau.

namespace IsSet 
    data IsSet : List t -> Type where 
     Nil : IsSet [] 
     (::) : All (\a => Not (a = x)) xs -> IsSet xs -> IsSet (x :: xs) 

namespace Disjoint 
    data Disjoint : List t -> List t -> Type where 
     Nil : Disjoint [] ys 
     (::) : All (\a => Not (a = x)) ys -> Disjoint xs ys -> Disjoint (x :: xs) ys 

f : (xs : List Type) -> (ys: List Type) -> {p1 : IsSet xs} -> {p2 : IsSet ys} -> {p3 : Disjoint xs ys} ->() 
f _ _ =() 

q :() 
q = f ['f1, 'f2] ['f3, 'f4] 

Tôi sẽ trao một khoản tiền thưởng 100 cho câu trả lời cho phép f được gọi như trong q (không chỉ định p1, p2 và p3).

Answer 1

Sử dụng% hint Tôi đã nhận Idris để tự động chứng minh bất kỳ NotEq nào nó gặp phải. Vì Not (a = b) là một hàm (vì Not a is -> Void), tôi cần phải tạo NotEq (vì tự động không thể chứng minh các hàm).

module Main 

import Data.Vect 
import Data.Vect.Quantifiers 

%default total 

fromFalse : (d : Dec p) -> {auto isFalse : decAsBool d = False} -> Not p 
fromFalse (Yes _) {isFalse = Refl} impossible 
fromFalse (No contra) = contra 

data NotEq : a -> a -> Type where 
    MkNotEq : {a : t} -> {b : t} -> Not (a = b) -> NotEq a b 

%hint 
notEq : DecEq t => {a : t} -> {b : t} -> {auto isFalse : decAsBool (decEq a b) = False} -> NotEq a b 
notEq = MkNotEq (fromFalse (decEq _ _)) 

NotElem : k -> Vect n k -> Type 
NotElem a xs = All (\x => NotEq a x) xs 

q : (a : lbl) -> (b : Vect n lbl) -> {auto p : NotElem a b} ->() 
q _ _ =() 

w :() 
w = q "a" ["b","c"]