如何让 Idris 自动证明两个值不相等？答案

【问题标题】：How can I have Idris automatically prove that two values are not equal?如何让 Idris 自动证明两个值不相等？
【发布时间】：2017-09-30 22:45:16
【问题描述】：

如何让 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]

【问题讨论】：

我认为可以通过使用带有自定义脚本的默认参数来查找证明。您必须将 f 的类型写为f: (xs: List Type) -> (ys: List Type) -> {default (%runElab prfFinder) p1: IsSet xs} -> {default (%runElab prfFinder) p2: IsSet ys} -> {default (%runElab prfFinder) p3: Disjoint xs ys} -> ()，其中prfFinder: Elab ()。但是不知道prfFinder的值怎么看。

标签： proof idris

【解决方案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"]

【讨论】：