İdris'in iki değerin eşit olmadığını otomatik olarak nasıl kanıtlayabilirim?

Question

Idris, iki değerin eşit olmadığını otomatik olarak nasıl kanıtlayabilir?

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

nasıl İdris otomatik olarak bu kanıtı üretmek olabilir? auto, Not'u içeren ifadeleri kanıtlayamıyor gibi görünmüyor. Son hedefim, İdris'in bir vektördeki tüm öğelerin benzersiz olduğunu ve iki vektörün ayrıldığını otomatik olarak kanıtlamasıdır.

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] 

I will ödül f o q olduğu gibi çağrılmasına olanak veren bir cevaba 100'lük bir ödül (p1, P2 ve P3 belirtmeden).

Answer 1

% ipucunu kullanarak, kendisiyle karşılaşılan herhangi bir NotEq'i otomatik olarak kanıtlaması için Idris'yu aldım. Not (a = b) bir işlev olduğu için (Not a - a -> Void), NotEq (otomatik olarak işlevleri kanıtlayamadığı için) yapmam gerekiyordu.

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