global have

Stream: general

[Johan Commelin]

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]

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

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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]

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]

I see, so I want a swap_have :grinning_face_with_smiling_eyes:

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

I want swap_to_main_goal.

[Johan Commelin]

Is that possible?

[Johan Commelin]

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]

Thanks for the tips @Reid Barton

[Reid Barton]

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

[Johan Commelin]

You think mathlib's version is more readable?

[Reid Barton]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Johan Commelin]

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]

by the way swap_have is called suffices

[Johan Commelin]

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.