Cantor's diagonal argument in Idris 2

cantor.idr

module Main

%default total


data Bijection : Type -> Type -> Type where
  ||| A bijection between two types.
  ||| @ a the first type
  ||| @ b the second type
  ||| @ fwd mapping from first type to the second
  ||| @ bck mapping from second type to the first
  ||| @ fb_producer proof that fwd . bck = id
  ||| @ bf_producer proof that bck . fwd = id
  DoMap : {0 a,b : Type} -> (fwd: a -> b) -> (bck: b -> a)
          -> (fb_producer: (av : a) -> (bck $ fwd av) = av)
          -> (bf_producer: (bv : b) -> (fwd $ bck bv) = bv)
          -> Bijection a b

map_fneq : {0 a,b : Type} -> {f : a->b} -> {g : a->b} -> f = g -> (v:a) -> f v = g v
map_fneq (Refl {x = f}) v = Refl

bool_inv : {v : Bool} -> (v = not v) -> Void
bool_inv {v = True}  prf = uninhabited prf
bool_inv {v = False} prf = uninhabited prf

diagonal : (Bijection Nat (Nat -> Bool)) -> Void
diagonal (DoMap f g _ bf_prf) = bool_inv conflict where
  H : Nat -> Bool
  H i = not $ f i i
  
  h_hi_by_idx : f (g H) (g H) = H (g H)
  h_hi_by_idx = map_fneq (bf_prf H) (g H)
  
  h_hi_by_def : H (g H) = (not $ f (g H) (g H))
  h_hi_by_def = Refl
  
  conflict : f (g H) (g H) = (not $ f (g H) (g H))
  conflict = trans h_hi_by_idx h_hi_by_def


test_bijection : Bijection Nat Nat
test_bijection = DoMap id id (\a => Refl) (\a => Refl)


main : IO ()
main = do putStrLn "Theorems proved"