# Zulip Chat Archive

## 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 proof`p 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