Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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
 α

view this post on Zulip Reid Barton (Nov 26 2020 at 21:34):

Do you know what ?m_1 means?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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