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

我如何让Idris自动证明两个值不相等？我如何让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]

我将奖励100到应答它允许将所谓的F像它是在q中的奖金（没有指定P1，P2，和P3）。

来源

2017-09-30 2426021684

我认为这可以通过使用默认参数与自定义脚本来找到证明。您必须将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} - >（）'where'prfFinder：Elab（）'。但我不知道prfFinder的价值。 – Gregg54654

使用％提示我得到了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"]

来源

2017-10-10 16:53:11 2426021684

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

回答

相关问题