Jak mogę pozwolić Idrisowi automatycznie dowieść, że dwie wartości nie są równe?

Question

Jak mogę pozwolić Idrysowi automatycznie dowieść, że dwie wartości nie są równe?

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

Jak mogę automatycznie wygenerować ten dowód przez Idris? auto nie wydaje się być w stanie udowodnić oświadczenia z udziałem Not. Moim końcowym celem jest sprawdzenie, czy Idrys automatycznie udowodni, że wszystkie elementy w wektorze są unikalne i że dwa wektory są rozłączne.

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] 

będę przyznać nagród od 100 do odpowiedzi, która pozwala f nazywać tak jak to jest w q (bez podawania P1, P2 i P3).

Answer 1

Korzystanie z podpowiedzi% Mam Idrisa do automatycznego udowodnienia każdego napotkanego NotEq. Ponieważ Not (a = b) jest funkcją (ponieważ Not a jest -> Void), musiałem zrobić NotEq (ponieważ auto nie może udowodnić funkcji).

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