proof - 我怎样才能让 Idris 自动证明两个值不相等？

Question

我怎样才能让 Idris 自动证明两个值不相等？

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

我怎样才能让 Idris 自动生成这个证明？ auto似乎无法证明涉及 Not 的陈述.我的最终目标是让 Idris 自动证明向量中的所有元素都是唯一的，并且两个向量是不相交的。

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]

Answer 1

使用 %hint 我让 Idris 自动证明它遇到的任何 NotEq。由于 Not (a = b) 是一个函数(因为 Not a 是 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"]