How does "exact" resolve 2 goals at once?

Stream: new members

[Lars Ericson]

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]

Do you know what ?m_1 means?

[Lars Ericson]

@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]

?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]

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]

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]

@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.