2

我定义了一种树，以及fusion如下操作：

open nat

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

open tree

def fusion : tree -> tree -> tree
| lf t2 := t2
| (nd l1 x1 r1) lf := (nd l1 x1 r1)
| (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 r1) r2) x2 l2

然后，我有一个计数函数，它返回给定整数在树中出现的次数：

def occ : nat -> tree -> nat
| _ lf := 0
| y (nd g x d) := (occ y g) + (occ y d) + (if x = y then 1 else 0)

我想证明(occ x (fusion t1 t2)) = (occ x t1) + (occ x t2)，但在证明过程中，我遇到了一个问题，因为我不知道如何处理给定的归纳假设。

到目前为止，我已经想到了这个：

theorem q5 : ∀ (x : ℕ) (t1 t2 : tree),
    (occ x (fusion t1 t2)) = (occ x t1) + (occ x t2) :=
begin
    intros x t1 t2,
    induction t1 with g1 x1 d1 _ ih1,
    simp [fusion, occ],
    induction t2 with g2 x2 d2 _ ih2,
    simp [fusion, occ],
    by_cases x1 <= x2,
    simp [fusion, h, occ],
    rw ih1,
    simp [occ, fusion, h],
    simp [occ, fusion, h],
end

但我拼命地卡住了。ih 处理fusion d1 (nd g2 x2 d2))我想要的东西fusion (nd g1 x1 d1) d2。

我很乐意欢迎任何建议。

4

1 回答 1

1

解决这个问题的最简单方法是使用您定义函数的相同模式匹配来证明使用方程编译fusion器

theorem q5 (x : ℕ) : ∀ (t1 t2 : tree),
    (occ x (fusion t1 t2)) = (occ x t1) + (occ x t2)
| lf t2 := by simp [fusion, occ]
| (nd l1 x1 r1) lf := by simp [fusion, occ]
| (nd l1 x1 r1) (nd l2 x2 r2) := 
begin
  simp only [fusion, occ],
  by_cases hx12 : x1 ≤ x2,
  { rw [if_pos hx12],
    simp only [fusion, occ],
    rw q5,
    simp [occ] },
  { rw if_neg hx12,
    simp only [fusion, occ],
    rw q5,
    simp [occ] }
end

另一种方法是

theorem q5 : ∀ (x : ℕ) (t1 t2 : tree),
    (occ x (fusion t1 t2)) = (occ x t1) + (occ x t2) :=
begin
  intros x t1,
  induction t1 with g1 x1 d1 _ ih1,
  { simp [fusion, occ] },
  { assume t2,
    induction t2 with g2 x2 d2 _ ih2,
    simp [fusion, occ],
    by_cases x1 <= x2,
    { simp [fusion, h, occ, ih1] },
    { simp [occ, fusion, h, ih2] } },
end

您的方法的问题在于，rw ih2在您的证明结束时可能会产生两个难以证明的子目标，因为归纳假设之前的假设。

解决这个问题的方法是改变第一个归纳假设。在我的第二个证明中没有intro t2归纳之前。这样，第一次归纳的归纳假设更强，因为从∀ t2.

每当您对变量进行归纳时t2，提及的每个假设t2都会自动作为假设添加到您的归纳假设之前。

在您的情况下，第一个归纳的归纳假设提到t2了 ，因此您最终得到了第二个假设的尴尬归纳假设。

但是，我对第一次归纳的归纳假设以 开头∀ t2，因此它们与我的局部常数无关t2，因此它们没有添加到第二次归纳的归纳假设中，因此我有一个更有用的归纳假设。

通过概括它，给自己这样最有力的归纳假设通常没有缺点∀ t2。这就是为什么它是方程编译器生成归纳假设的默认方式。

于 2019-12-20T05:02:00.727 回答