入职问题

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

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

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.

的东西

我很乐意欢迎任何建议。

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 给自己一个像这样最强大的归纳假设通常没有坏处。这就是为什么它是方程编译器生成归纳假设的默认方式。

入职问题

Induction issue

theorem-proving

lean