Question on refine

Stream: general

[Filippo A. E. Nuccio]

I understand that refine doesn't accept to change a goal in something else which is not definitionally equal to it. Yet, if my goal is ⊢ ∃ (a : A), P a and I have a hypothesis h : ∃ (a : A), P₀ a, I hoped that saying refine h and then putting appropriate _'s at the right places, it would say something "OK, for the time being you' ve produced a term of type ∃ (a : A), P₀ a: if you cook up a function from ∃ (a : A), P₀ a to ∃ (a : A), P a, then I'll forgive you". Is it the case?

Concretely, in the MWE below, I am sure that my proof is horrible and that it must exist a one-line version of it (actually, if there is a two-line proof using refine I would be even happier, as I still understand this tactic poorly):

example (Q : Prop) (P P₀ : A → Prop) (h : Q → ∃ a : A, P₀ a) (q : Q)
  (H : ∀ a : A, P₀ a → P a) : (∃ a : A, P a) :=
begin
    suffices this : ∃ a : A, P₀ a,
    { intros,
      cases this with a ha,
      use a,
      apply H, exact ha },
    { apply h, use q },
  end

[Johan Commelin]

convert is made for this

[Johan Commelin]

but it will use congr to strip away as much as possible from the two "equal" pieces.

[Johan Commelin]

So you will end up with a goal asking you to prove P = P0.

[Filippo A. E. Nuccio]

The problem with convert is that it asks for equalities

[Filippo A. E. Nuccio]

And I only have P -> P0

[Johan Commelin]

You can restrict how far it strips using convert h using n where n = 1,2,3,4,...

[Johan Commelin]

Does convert h using 0 help you?

[Filippo A. E. Nuccio]

it has the same effect than convert h (and btw it produces two goals, which I don't understand why)

[Kevin Buzzard]

import tactic
variable (A : Type)

example (Q : Prop) (P P₀ : A → Prop) (h : Q → ∃ a : A, P₀ a) (q : Q)
  (H : ∀ a : A, P₀ a → P a) : (∃ a : A, P a) :=
Exists.imp H (h q)

[Kevin Buzzard]

logic.basic is your friend with goals like this.

[Kevin Buzzard]

PS library_search finds this proof.

[Kevin Buzzard]

Your problem is exactly that you want to commute the exists and the imp before you can use apply, and this is a lemma in the library.

[Filippo A. E. Nuccio]

Kevin Buzzard said:

Your problem is exactly that you want to commute the exists and the imp before you can use refine, and this is a lemma in the library.

Yes, indeed!

[Filippo A. E. Nuccio]

But then, actually, you don't even use a refine! Do you think it was overall a bad idea? I can't really figure out its scope...

[Filippo A. E. Nuccio]

At any rate, thanks so much for the Exists.imp, it saves me 5 lines!

[Kevin Buzzard]

refine is just "exact with holes".

[Filippo A. E. Nuccio]

And you basically use when one of the holes wouldn't be a short proof but a long one? Because you can write exact h a b if h a b is a term which finishes the goal... you are saying that if to produce this term you need 10 lines, you prefer to have a new goal asking for this term?

[Kevin Buzzard]

so you need the function giving the complete proof of your goal, except that you don't have some of the inputs, so you use _ and come back to them later.

[Kevin Buzzard]

refine is a really powerful tactic. I often use it instead of apply now, because it makes me fill in the right number of underscores. Yes, the problem is precisely when one or more of the holes isn't just some easy term you can fill in, but something which takes a ten line tactic proof. It's perfect in cases where this tactic proof needs things like rw which are problematic when there is a lot of junk around (e.g. you don't want to rewrite all of the a's, or you are rewriting under a binder etc).

[Kevin Buzzard]

In your original post, you seem to be describing something like the suffices tactic?

[Mario Carneiro]

In theory you could use refine _ h for the example in the original post, but lean doesn't like underscores in function position. You can do revert h to do roughly the same thing

[Mario Carneiro]

that said this usually isn't the kind of move that makes progress, unless you are specifially trying to apply Exists.imp or something along those lines

[Mario Carneiro]

I think the "natural" proof is something like this:

example {A} (Q : Prop) (P P₀ : A → Prop) (h : Q → ∃ a : A, P₀ a) (q : Q)
  (H : ∀ a : A, P₀ a → P a) : (∃ a : A, P a) :=
begin
  rcases h q with ⟨a, h⟩,
  refine ⟨a, _⟩,
  exact H _ h,
end

[Mario Carneiro]

(this is not the golfed version; as Kevin showed this can be compressed to just (h q).imp H)

[Filippo A. E. Nuccio]

Kevin Buzzard said:

refine is a really powerful tactic. I often use it instead of apply now, because it makes me fill in the right number of underscores. Yes, the problem is precisely when one or more of the holes isn't just some easy term you can fill in, but something which takes a ten line tactic proof. It's perfect in cases where this tactic proof needs things like rw which are problematic when there is a lot of junk around (e.g. you don't want to rewrite all of the a's, or you are rewriting under a binder etc).

Thanks!

[Filippo A. E. Nuccio]

Mario Carneiro said:

I think the "natural" proof is something like this:

example {A} (Q : Prop) (P P₀ : A → Prop) (h : Q → ∃ a : A, P₀ a) (q : Q)
  (H : ∀ a : A, P₀ a → P a) : (∃ a : A, P a) :=
begin
  rcases h q with ⟨a, h⟩,
  refine ⟨a, _⟩,
  exact H _ h,
end

Thank you very much, this also helps a lot. It is indeed the proof I was looking for (for self-pedagogical reasons, I agree Kevin's is the best proof). But can you explain the underscore in H _ h? And also how to pass from Exists.imp H ( h q ) to (h q).imp H? I guess that there must be a general rule explaining what it really means "to append a dot", but I ignore it.

[Kevin Buzzard]

The general rule is that if x is a term of type Y (or more generally of type Y a b c) then x.foo means Y.foo x. The backwards E notation is notation, it's not the name of the actual type. The type itself is called Exists .... You can easily tell notation from regular type names, notation is fancy Unicode or LaTeX characters, like $\mathbb{N}$.

[Kevin Buzzard]

This dot thing is a secret, it's not written down anywhere as far as I know

[Kevin Buzzard]

You can replace that last underscore with an a. The reason you don't have to is that when lean sees the type of h it can figure out that the missing input must be a.

[Kevin Buzzard]

If in your theorem statement you had written H : forall {a : A}, ... then you would not need the underscore at all

[Kevin Buzzard]

H is just a function which expects an input and then a proof involving the input (this is what is known as a dependent function, where the type of an input depends on the terms previously inputted) and if lean can see the later inputs explicitly then it might not need to hear the earlier inputs. This is what these {} brackets are all about.

[Mario Carneiro]

I'm almost certain projection notation is described in the reference manual et al

[Kevin Buzzard]

A proof of Fermat's last theorem is a dependent function because the inputs are a,b,c,n and then proofs that n>2 and a^n+b^n=c^n, ie terms of types which depend on a,b,c,n. The output is a proof that abc=0

[Kevin Buzzard]

Maybe it's in the reference manual, it would be nice to know so we can point people there

[Mario Carneiro]

There are two short paragraphs about "dot notation" at https://leanprover.github.io/reference/expressions.html#constructors-projections-and-matching

[Filippo A. E. Nuccio]

Kevin Buzzard said:

H is just a function which expects an input and then a proof involving the input (this is what is known as a dependent function, where the type of an input depends on the terms previously inputted) and if lean can see the later inputs explicitly then it might not need to hear the earlier inputs. This is what these {} brackets are all about.

Oh, this is a nice explanation of many cabbalistic phenomena!

[Filippo A. E. Nuccio]

Mario Carneiro said:

There are two short paragraphs about "dot notation" at https://leanprover.github.io/reference/expressions.html#constructors-projections-and-matching

Thanks!