归纳问题

Question

我已经定义了树的类型，以及如下的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

但是我极度困惑。我想要fusion d1 (nd g2 x2 d2))时，ih处理fusion (nd g1 x1 d1) d2。

我很乐意欢迎您提出任何建议。

Answer 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，通常不会给自己这样强大的归纳假设带来不利影响。这就是为什么它是方程式编译器生成归纳假设的默认方式的原因。