# 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 `fact`

s 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