## Stream: new members

### Topic: applying a hypothesis several times

#### Jakob Scholbach (Jan 28 2021 at 18:58):

I am working through §2 of the mathematics in lean tutorial. I have tried this

import data.real.basic

variables a b c : ℝ

-- BEGIN
example : max a b = max b a :=
begin
apply le_antisymm,
have h : ∀ x y, max x y ≤ max y x,
{
intros x y,
apply max_le,
apply le_max_right,
apply le_max_left,
},
apply h,
apply h
end


but this does not work (the last apply h does not work). I see how to fix it by replacing the proof by

begin
have h : ∀ x y, max x y ≤ max y x,
{
intros x y,
apply max_le,
apply le_max_right,
apply le_max_left,
},
apply le_antisymm,
apply h,
apply h
end


However, I don't understand why the first does not work, while the second does.
Can someone explain that?
Also, is there a way to say "have h ...", prove it, and use this established fact twice?

#### Mario Carneiro (Jan 28 2021 at 19:00):

The have only exists in the first goal when you write it after le_antisymm

#### Mario Carneiro (Jan 28 2021 at 19:01):

the solution is to do the have before both of your goals, as in the second version. That also answers your second question: yes there is a way, you just did it

#### Jakob Scholbach (Jan 28 2021 at 19:08):

What is the overarching rationale / logic behind this dependence of ordering? (Me old-fashioned guy thinking: in a paper proof it would not matter...)

#### Reid Barton (Jan 28 2021 at 19:10):

It "obviously" doesn't matter where you prove h here because the hypotheses are the same for both goals, but if you did something like a case analysis, and you prove a claim in one case, you can't automatically apply it in the other case as well

#### Mario Carneiro (Jan 28 2021 at 20:52):

Also, syntactically there is a scoping consideration; in the first version, after the have you have basically generated a term like

le_antisymm ((\lam h : ∀ x y, max x y ≤ max y x, _) <proof>) _


where the two underscores are the two subgoals, and h is only in scope in the first one (the first subgoal), whereas the second proof is

(\lam h : ∀ x y, max x y ≤ max y x, le_antisymm _ _) <proof>


and now h is in scope for both goals.

#### Johan Commelin (Jan 28 2021 at 21:18):

@Jakob Scholbach another example: suppose you do induction, and you get two goals: the 0 case and the n+1 case. The you might be able to prove have h : bla in the 0 case, but the same proof might not work (or even make sense) in the other case.

#### Kevin Buzzard (Jan 28 2021 at 21:27):

After apply le_antisymm, you have two goals, and are now operating in two completely independent universes which have no way of communicating with each other.

#### Kyle Miller (Jan 28 2021 at 22:56):

Jakob Scholbach said:

What is the overarching rationale / logic behind this dependence of ordering? (Me old-fashioned guy thinking: in a paper proof it would not matter...)

A tactic proof is a sequence of instructions to manipulate the tactic state. It's all fairly low-level -- and for a practitioner it's good if basic tactics don't have too many smarts because then you have a better chance at predicting what they will do.

In principle, someone could probably write a remember h tactic to extract a hypothesis to other parallel goals, but in practice it's easy enough to just reorder things.

Regarding your example, you can apply a tactic proof to all goals simultaneously:

example : max a b = max b a :=
begin
apply le_antisymm,
all_goals
{ have h : ∀ x y, max x y ≤ max y x,
{ intros x y,
apply max_le,
apply le_max_right,
apply le_max_left, },
apply h, },
end


Last updated: May 16 2021 at 21:11 UTC