CODEWITHSUNDEEP
proofidris
michaelmesser
michaelmesser

Reputation: 3726

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

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

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]

Upvotes: 8

Views: 867

Answers (1)

michaelmesser
michaelmesser

Reputation: 3726

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

Upvotes: 2

Related Questions