How can I get Idris to automatically prove that the two values ​​are not equal?

Question

How can I get Idris to automatically prove that the two values ​​are not equal?

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

How can I get Idris to automatically generate this evidence? auto does not seem to be able to prove statements involving Not . My ultimate goal is to force Idris to automatically prove that all elements in the vector are unique and that the two vectors do not intersect.

 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 am rewarded with a prize of 100 for an answer that allows you to call f, as in q (without specifying p1, p2 and p3).

Answer 1

Using% hint, I got Idris to automatically prove the lack of NotEq that it encountered. Since Not (a = b) is a function (since Not a is a → Void), I needed to make NotEq (since the auto cannot prove the function).

 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 ab %hint notEq : DecEq t => {a : t} -> {b : t} -> {auto isFalse : decAsBool (decEq ab) = False} -> NotEq ab notEq = MkNotEq (fromFalse (decEq _ _)) NotElem : k -> Vect nk -> Type NotElem a xs = All (\x => NotEq ax) xs q : (a : lbl) -> (b : Vect n lbl) -> {auto p : NotElem ab} -> () q _ _ = () w : () w = q "a" ["b","c"]