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

如何解决在精益证明的目标中应用函数

有一个树数据结构和一个 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

解决方法

我认为您需要进行归纳而不是案例才能使其起作用。 但这只需 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

,

证明它的几种替代方法

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]