Zulip Chat Archive

Stream: general

Topic: global have


Johan Commelin (Feb 13 2019 at 15:37):

I'm playing a bit with automation. Somehow I want to tell Lean some facts that it should use, and then it should blast its way through to the finish line.
So I would like to write

have fact₁ : foo,
  apply key_lemma,
have fact₂ : bar,
have fact₃ : xyzzy,
all_goals {some_auto}

The natural order (for mathematicians) would be to state these facts in such an order that the proof of fact₃ may depend on fact₁ and fact₂. All these facts together will be used to prove the main goal.
However, Lean doesn't like that order. Because now the have fact₃ claim is nested in the proof of fact₂, which is nested in the proof of fact₁. And so these facts aren't actually available when trying to prove the main goal.

To some extent suffices makes the "correct" order available. However, then you can't say apply key_lemma right after stating some claim.

So what I would like is global_have, which adds a claim to the global scope, instead of nested in the proof of a subgoal. Is something like that possible?

Reid Barton (Feb 13 2019 at 15:39):

I'm a little confused--do you intend to prove these facts yourself?

Reid Barton (Feb 13 2019 at 15:40):

because after have fact₂ : bar, say, you should be giving the proof of fact₂

Johan Commelin (Feb 13 2019 at 15:40):

No. Not really. They are just to guide the automation.

Johan Commelin (Feb 13 2019 at 15:41):

It should be able to prove these subgoals. And once it knows these facts, go on to prove the main goal.

Reid Barton (Feb 13 2019 at 15:41):

Okay, so basically you want to continue working on the main goal first. Then you can use swap, or possibly have fact₂ : bar := _,

Reid Barton (Feb 13 2019 at 15:41):

It should be able to prove these subgoals. And once it knows these facts, go on to prove the main goal.

If you want to do it in that order, then you should put your prove-everything tactic after each have

Johan Commelin (Feb 13 2019 at 15:42):

I see, so I want a swap_have :grinning_face_with_smiling_eyes:

Johan Commelin (Feb 13 2019 at 15:42):

I don't want my prove-everything tactic after each have. That doesn't look nice.

Reid Barton (Feb 13 2019 at 15:43):

I tested and := _ does work, and it's the same number of characters as swap_

Johan Commelin (Feb 13 2019 at 15:47):

I want swap_to_main_goal.

Johan Commelin (Feb 13 2019 at 15:48):

Is that possible?

Johan Commelin (Feb 13 2019 at 15:55):

Ok, I now have this

theorem Euclid (n : ) :  p  n, prime p :=
begin
  let N := n.fact + 1,
  let p := min_fac N,
  use_this p,
  have p_is_prime : prime p := min_fac_prime _,
  split,
    by_contradiction,
    have key_fact : p  n.fact := dvd_fact _ _,
    have oops : p  1,
  all_goals { auto },
end

where auto is a wrapper around solve_by_elim and tidy. I'm reasonably happy with this.

Johan Commelin (Feb 13 2019 at 15:55):

Thanks for the tips @Reid Barton

Reid Barton (Feb 13 2019 at 15:58):

I feel like I no longer know why this theorem is true

Johan Commelin (Feb 13 2019 at 15:59):

You think mathlib's version is more readable?

Reid Barton (Feb 13 2019 at 16:05):

I think it's that phenomenon where you see a word so many times that it stops looking like a word.

Reid Barton (Feb 13 2019 at 16:05):

But maybe it would help to have p < n appear somewhere in the proof (I guess it would show up in the tactic state at least)

Edward Ayers (Feb 13 2019 at 16:06):

https://en.wikipedia.org/wiki/Semantic_satiation

Reid Barton (Feb 13 2019 at 16:08):

did the auto tactic figure out to prove p <= n from p < n?

Johan Commelin (Feb 13 2019 at 16:13):

Auto is just chaining solve_by_elim (with a suitable set of lemmas) and tidy.
I know this is cheating... but we don't have a proper back yet, and I want to show that it is not unreasonable to hope that Lean will be able to figure out the trivial proof obligations.

Mario Carneiro (Feb 13 2019 at 17:38):

by the way swap_have is called suffices

Johan Commelin (Feb 13 2019 at 17:40):

suffices does not suffice... see above. But I think the "main goal" is not always well-defined. So I've come to the conclusion that I probably can't have exactly what I want. However, Reid's approach solved it for me.


Last updated: Dec 20 2023 at 11:08 UTC