applying a hypothesis several times

Stream: new members

[Jakob Scholbach]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

@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]

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]

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