## Stream: new members

### Topic: How does "exact" resolve 2 goals at once?

#### Lars Ericson (Nov 26 2020 at 21:33):

I am working on a proof where I have two subgoals at one point. I apply exact and both are resolved. How does that work? My prior understanding was that tactics only operate on one goal at a time. Here is the example:

example : (∃ x, p x ∧ r) ↔ (∃ x, p x) ∧ r :=
begin
split,
{
intro h,
split,
{
cases h with x pxr,
have px := pxr.left,
constructor, -- two open goals at this point
exact px, -- no goals here
},
sorry,
},
sorry,
end


where the open goals are

2 goals
α : Type u_1,
p : α → Prop,
r : Prop,
x : α,
pxr : p x ∧ r,
px : p x
⊢ p ?m_1

α : Type u_1,
p : α → Prop,
r : Prop,
x : α,
pxr : p x ∧ r,
px : p x
⊢ α


#### Reid Barton (Nov 26 2020 at 21:34):

Do you know what ?m_1 means?

#### Lars Ericson (Nov 26 2020 at 23:25):

@Reid Barton I guess ?m_1 is any member of set α. p ?m_1 is...I don't know, maybe it is a way of denotating any proposition p y where y is in α. I suppose ⊢ p ?m_1 means prove any proposition on all instances of α. I don't what a goal of⊢ α represents, because α is not a proposition. Apparently the proofp x is being applied to both goals in the set, so I suppose if I have a set of goals and a proof, then the rule is that all goals which unify with the exact expression are eliminated. So maybe what I'm seeing here is that p x unifies with p ?m_1 and it unfies with α. These are all guesses, hence the question.

#### Kevin Buzzard (Nov 26 2020 at 23:38):

?m_1 is a metavariable, i.e. Lean doesn't know what it is or even what its name is. It knows its type is alpha though, because p ?m_1 makes sense. That explains the second goal -- Lean is asking for a term of type alpha, and then will instantiate ?m_1 in the first goal with that term. But exact px on the first goal makes Lean figure out that ?m_1 must have been x, so it can now close the second goal as well.

#### Yakov Pechersky (Nov 26 2020 at 23:50):

Lars Ericson said:

I don't what a goal of⊢ α represents, because α is not a proposition.

It's important to understand that, to first principle, anything can be a goal, not just terms p : Prop. That means providing a term a : α where α : Type* can solve a goal of ⊢ α. Could you explain why you thought that only propositions can be goals?

#### Kevin Buzzard (Nov 27 2020 at 01:00):

It's probably true that if you're in tactic mode and your goal isn't a prop then you're doing it wrong -- these things are certainly quite rare. It's also probably true that if your goal contains metavariables then you're doing it wrong, or you're at least being a bit cheeky.

#### Lars Ericson (Nov 27 2020 at 01:01):

@Yakov Pechersky in the context of theorem proving, i.e. expressions like example, lemma and theorem, I assumed that what came after ⊢ would be a Prop. If instead the state of Lean is a stack of goals and anything to be constructed can apply to the right of ⊢ , then I can see how ⊢ α would make sense.

I incorrectly assumed that only one goal at a time could be resolved by a tactic, because initially in filling out the proof I might have something like

sorry,
sorry,


but in the above example, when I fill out the first sorry with the exact, the second sorry becomes redundant.

Last updated: May 10 2021 at 19:16 UTC