在精益证明的目标中应用函数答案

【问题标题】：Apply function in goal in lean proof在精益证明的目标中应用函数
【发布时间】：2021-04-21 15:51:47
【问题描述】：

有一个树数据结构和一个flip 方法。我想写一个证明，如果您将flip 方法应用于一棵树两次，您将获得初始树。我有一个目标

⊢ flip_mytree (flip_mytree (mytree.branch t_ᾰ t_ᾰ_1 t_ᾰ_2)) = mytree.branch t_ᾰ t_ᾰ_1 t_ᾰ_2

我想用flip_mytree 的结果替换flip_mytree (mytree.branch t_ᾰ t_ᾰ_1 t_ᾰ_2)。我该怎么做？或者如何将(mytree.branch a l r) := mytree.branch a (flip_mytree r) (flip_mytree l) 假设从flip_mytree 函数定义中提取到我的定理上下文中？

我读过rw、apply 和have 战术，但它们在这里似乎没用。

下面是一个完整的例子。

universes u

inductive mytree (A : Type u) : Type u
| leaf : A → mytree
| branch : A → mytree → mytree → mytree

def flip_mytree {A : Type u} : mytree A → mytree A
| t@(mytree.leaf _)     := t
| (mytree.branch a l r) := mytree.branch a (flip_mytree r) (flip_mytree l)


theorem flip_flip {A : Type u} {t : mytree A} : flip_mytree (flip_mytree t) = t :=
begin
  cases t,
  

end

【问题讨论】：

不确定你学到了多少；你遇到过simp吗？

标签： proof theorem-proving lean

【解决方案1】：

我认为您需要进行归纳而不是案例才能使其起作用。但这仅使用induction 和rw 是可行的，如下所示

universes u

inductive mytree (A : Type u) : Type u
| leaf : A → mytree
| branch : A → mytree → mytree → mytree

def flip_mytree {A : Type u} : mytree A → mytree A
| t@(mytree.leaf _)     := t
| (mytree.branch a l r) := mytree.branch a (flip_mytree r) (flip_mytree l)


theorem flip_flip {A : Type u} {t : mytree A} : flip_mytree (flip_mytree t) = t :=
begin
  induction t with l a b₁ b₂ ih₁ ih₂,
  rw [flip_mytree],
  refl,
  
  rw [flip_mytree, flip_mytree],
  rw [ih₁, ih₂],
end

【讨论】：

您可以传递给rw 策略，不仅可以传递a = b 表达式，还可以传递一个函数。所以rw flip_mytree 就是我要找的。span>
@osseum 是的，真正发生的是精益为您的函数生成辅助方程引理。您可以使用#print prefix flip_mytree 查看。其中包括flip_mytree.equations._eqn_1 : ∀ {A : Type u} (_x : A), flip_mytree (mytree.leaf _x) = mytree.leaf _x，所以当您执行rw flip_mytree 时，这个等式就是被重写的内容。您甚至可以手动使用rw [flip_mytree.equations._eqn_1] 作为第一个rw 并使用_eqn_2 作为第二个，但这只是无缘无故地添加更多字符！

【解决方案2】：

证明它的几种替代方法

theorem flip_flip {A : Type u} : ∀ {t : mytree A}, flip_mytree (flip_mytree t) = t
| t@(mytree.leaf _)     := rfl
| (mytree.branch a l r) := by rw [flip_mytree, flip_mytree, flip_flip, flip_flip]

theorem flip_flip' {A : Type u} {t : mytree A} : flip_mytree (flip_mytree t) = t :=
by induction t; simp [*, flip_mytree]

【讨论】：