theorem-proving - 感应问题
问题描述
我定义了一种树,以及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
。
我很乐意欢迎任何建议。
解决方案
解决这个问题的最简单方法是使用您定义函数的相同模式匹配来证明使用方程编译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
。这就是为什么它是方程编译器生成归纳假设的默认方式。
推荐阅读
- java - RMI 服务运行类似于套接字
- angular - 上传文件时有没有办法获得确切的文件路径?
- android - 在 xhdpi 设备上使用 xxhdpi
- python - 有没有办法创建关系熊猫数据框?
- javascript - 使用 angular primeng 根据搜索值显示来自 api 的用户数据
- reactjs - 如何在 react-app 中重用自定义 Material-ui 按钮?
- ios - 从其他表格 DidSelect 方法更新表格单元格数据
- wso2 - 将服务提供者中的 NameID 重新映射到 office365 身份提供者的 Alias 属性
- c++ - 为什么这个函数不打印所有的 char 数组呢?
- python - 如何将 html 列表添加到破折号布局