Apply function in goal in lean proof

Question

There are a tree data structure and a flip method for it. I want to write a proof that if you apply the flip method to a tree twice you get initial tree. I've got a goal

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

and I want to replace flip_mytree (mytree.branch t_ᾰ t_ᾰ_1 t_ᾰ_2) with result of flip_mytree. How may I do that? Or how can I pull (mytree.branch a l r) := mytree.branch a (flip_mytree r) (flip_mytree l) hypothesis from the flip_mytree function definition into my theorem context?

I've read about rw, apply and have tactics but they seems to be useless here.

A whole example is down below.

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

Not sure how much you've learnt; have you come across `simp`? — It'sNotALie., Apr 21 '21 at 16:09

score 2 · Accepted Answer · answered Apr 21 '21 at 16:25

2

I think you need to do induction rather than cases for this to work. But this is doable with just induction and rw as follows

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

answered Apr 21 '21 at 16:25

Alex J Best

306
1
6

You may pass to `rw` tactic not only `a = b` expression but a function too. So `rw flip_mytree` is what I am looking for. – osseum Apr 22 '21 at 14:59
@osseum yes, what is really happening is that lean generates auxiliary equation lemmas for your function. Which you can see with `#print prefix flip_mytree`. These include `flip_mytree.equations._eqn_1 : ∀ {A : Type u} (_x : A), flip_mytree (mytree.leaf _x) = mytree.leaf _x` so when you do `rw flip_mytree` this equation is what is being rewritten. You could even do this by hand with `rw [flip_mytree.equations._eqn_1]` for the first `rw` and use `_eqn_2` for the second one, but this is just adding more characters for no reason! – Alex J Best Apr 22 '21 at 21:17

score 1 · Answer 2 · answered Apr 21 '21 at 19:37

A couple of alternative ways of proving it

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]

Apply function in goal in lean proof

2 Answers2