How can I have Idris automatically prove that two values are not equal?

Question

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

How can I have Idris automatically generate this proof? auto does not appear to be capable of proving statements involving Not. My end goal is to have Idris automatically prove that all elements in a vector are unique and that two vectors are disjoint.

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 think it may be possible by using default arguments with a custom script to find the proofs. You'd have to write the type of f as 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 (). But I don't know how the value of prfFinder looks. — Gregg54654

michaelmesser michaelmesser · Accepted Answer · 2017-10-10T16:53:11

Using %hint I got Idris to auto prove any NotEq it encountered. Since Not (a = b) is a function (since Not a is a -> Void), I needed to make NotEq (since auto cannot prove functions).

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

How can I have Idris automatically prove that two values are not equal?

1 Answers