Zulip Chat Archive

Stream: new members

Topic: applying a hypothesis several times


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Jan 28 2021 at 19:00):

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

view this post on Zulip 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

view this post on Zulip 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...)

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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