Test.idr

{-- THIS IS AN EXAMPLE OF UNSOUND PROOF -- IT IS THE PRODUCT OF A CONFUSED MIND --}

data Bin = O Nat Bin | BNil 

{-
total aNEBMeansNotEqual : (a : Nat) -> (b : Nat) -> (v : Bin) -> Dec (a = b) -> Dec (O a v = O b v) 
aNEBMeansNotEqual a b v (Yes prf) = rewrite prf in Yes Refl 
aNEBMeansNotEqual a b v (No contra) = No ?contraHell
-}

data TypeHolder a = Holder 
 
extractContra : (a -> Void) -> (TypeHolder a)
extractContra contra = Holder

extractFromHolder : TypeHolder a -> a
extractFromHolder t = idris_crash "lol-extract"

{- Given a DecEq contra , extract the "proof" -} 
contraProof : (a -> Void) -> a
contraProof = extractFromHolder . extractContra
 
isImpossible_ : a -> a -> Void 
isImpossible_ a = idris_crash "lol-impossible"
{- Given a proof, construct its antiproof -}
isImpossible : a -> a -> Void 
isImpossible a = isImpossible_ (extractFromHolder Holder)

total aNEBMeansNotEqual : (a : Nat) -> (b : Nat) -> (v : Bin) -> Dec (a = b) -> Dec (O a v = O b v)
aNEBMeansNotEqual a b v (Yes prf) = rewrite prf in Yes Refl
aNEBMeansNotEqual a b v (No contra) =
  let prf = contraProof contra in
  rewrite prf in No (isImpossible Refl)