精益中基于简单反射的证明问题（但在Agda中不是）

Question

为了尝试在精益中定义偏斜堆并证明一些结果，我已经定义了树的类型以及融合操作：

inductive tree : Type
| lf : tree
| nd : tree -> nat -> tree -> tree

def fusion : tree -> tree -> tree
| lf t2 := t2
| t1 lf := t1
| (nd l1 x1 r1) (nd l2 x2 r2) :=
    if x1 <= x2
    then nd (fusion r1 (nd l2 x2 r2)) x1 l1
    else nd (fusion (nd l1 x1 l1) r2) x2 l2

然后，即使对于非常简单的结果，例如

theorem fusion_lf : ∀ (t : tree), fusion lf t = t := sorry

我被卡住了。我真的没有线索开始写这个证明。如果我这样开始：

begin
  intro t,
  induction t with g x d,
  refl,
end

对于refl为t的情况，可以使用lf，但如果为nd，则不能使用。

我有点不知所措，因为在阿格达，这真的很容易。如果我定义这个：

data tree : Set where
  lf : tree
  nd : tree -> ℕ -> tree -> tree

fusion : tree -> tree -> tree
fusion lf t2 = t2
fusion t1 lf = t1
fusion (nd l1 x1 r1) (nd l2 x2 r2) with x1 ≤? x2
... | yes _ = nd (fusion r1 (nd l2 x2 r2)) x1 l1
... | no  _ = nd (fusion (nd l1 x1 r1) r2) x2 l2

然后使用refl直接获得先前的结果：

fusion_lf : ∀ t -> fusion lf t ≡ t
fusion_lf t = refl

我错过了什么？

Answer 1

此证明有效。

theorem fusion_lf : ∀ (t : tree), fusion lf t = t := 
λ t, by cases t; simp [fusion]

如果尝试#print fusion.equations._eqn_1或#print fusion.equations._eqn_2等，您会看到simp [fusion]将使用的引理。案例分割与模式匹配中的案例分割不完全相同，因为模式匹配中的案例分割实际上与案例lf lf重复。这就是为什么我需要做cases t。通常，等式引理是定义性的等式，但是这次却不是，并且说实话我不知道为什么。