proof - 在精益证明的目标中应用函数

Question

有一个树数据结构和一个flip方法。我想写一个证明，如果你申请flip方法到一棵树两次你得到初始树。我有一个目标

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

我想更换 flip_mytree (mytree.branch t_ᾰ t_ᾰ_1 t_ᾰ_2)结果为 flip_mytree .我该怎么做？或者怎么拉 (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

Answer 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