2

为了在 Lean 中定义倾斜堆并证明一些结果，我定义了一种树类型以及一个融合操作：

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用于 where tis的情况lf，但如果它是 a 则不能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

那么前面的结果直接用 a 得到refl：

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

我错过了什么？

4

1 回答 1

4

这个证明有效。

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]将使用的引理。case 拆分与模式匹配中的 case 拆分并不完全相同，因为模式匹配中的 case 拆分实际上复制了 case lf lf。这就是为什么我需要这样做cases t。通常方程引理是定义等式，但这次不是，老实说我不知道​​为什么。

于 2019-12-02T15:03:31.603 回答