在Idris中证明（x：t） - >（x == x）= True

Question

鉴于此定义：

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

我想证明以下内容：

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

然而，我陷入了无数的证据：

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

类型为？ltype_eq_rhs_2为：

  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

所以它基本上是一个递归证明。关于如何证明它的任何想法？

Answer 1

我意识到如何在发布后立即证明这一点。这是证明：

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