Idrisは、2つの値が等しくないことを自動的に証明する方法を教えてください。

Question

Idrisが2つの値が等しくないことを自動的に証明する方法を教えてください。

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

この証明を自動的に生成するにはどうすればよいですか？ autoは、Notを含むステートメントを証明することはできないようです。私の最終目標は、Idrisがベクトルのすべての要素が一意であり、2つのベクトルが互いに素であることを自動的に証明することです。

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] 

私はそれが（P1、P2、P3を指定せずに）のqであるようにfが呼び出されることを可能にする答えに100の恵みを授与します。

Answer 1

％ヒントを使用して、私はIdrisに遭遇したNotEqを自動的に証明するようにしました。 not（a = b）は関数であるから（Not aが - > Voidなので）、NotEqを作る必要があった（autoは関数を証明できないので）。

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"]