Proving (x : t) -> (x == x) = True in Idris

1
votes

Given this definition:

data LType : Type where
  TNat : LType
  TFun : LType -> LType -> LType

Eq LType where
  (==) TNat TNat                  = True
  (==) (TFun l0 l1) (TFun r0 r1)  = (l0 == r0) && (l1 == r1)
  (==) _ _                        = False

I am trying to prove the following:

  ltype_eq : (t : LType) -> (t == t) = True

However I am getting stuck in an infinite number of proofs:

ltype_eq : (t : LType) -> (t == t) = True
ltype_eq TNat       = Refl
ltype_eq (TFun x y) = ?ltype_eq_rhs_2

with the type of ?ltype_eq_rhs_2 being:

  x : LType
  y : LType
--------------------------------------
ltype_eq_rhs_2 : Main.LType implementation of Prelude.Interfaces.Eq, method == x
                                                                               x &&
                 Delay (Main.LType implementation of Prelude.Interfaces.Eq, method == y
                                                                                      y) =
                 True

So it is basically a recursive proof. Any ideas on how to prove it?

1
idris

1 Answers

3
votes

I realised how to prove it right after posting. Here is the proof:

ltype_eq : (t : LType) -> (t == t) = True
ltype_eq TNat       = Refl
ltype_eq (TFun x y) =
  rewrite ltype_eq x in
  rewrite ltype_eq y in
  Refl