Zulip Chat Archive

Stream: lean4

Topic: have with metavariables?


view this post on Zulip Jason Gross (Mar 11 2021 at 22:06):

Is there a version of have that permits uninferred metavariables?

view this post on Zulip Leonardo de Moura (Mar 12 2021 at 20:38):

Jason Gross said:

Is there a version of have that permits uninferred metavariables?

Could you please post an example?

view this post on Zulip Jason Gross (Mar 12 2021 at 20:43):

I think this should go through:

def goal : 1 + 1 = 1 + 1 := by
  have h := 1
  have h' := (rfl : _ + 1 = _ + 1)
  refine h'
  done
/-
Goals (1)
h : Nat
h' : ?m.721 + 1 = ?m.721 + 1
⊢ 1 + 1 = 1 + 1

Messages (4)
3:14:
don't know how to synthesize implicit argument
  @rfl Nat (?m.721 + 1)
context:
h : Nat
⊢ Nat
3:28:
don't know how to synthesize placeholder
context:
h : Nat
⊢ Nat
3:20:
don't know how to synthesize placeholder
context:
h : Nat
⊢ Nat
3:2:
failed to infer 'let' declaration type
-/

view this post on Zulip Leonardo de Moura (Mar 13 2021 at 02:32):

We are trying to promote structured tactic scripts in Lean 4. So, have/let/sufficies will reject problems with unresolved holes.
Note that they do accept "synthetic" named holes (e.g., ?h1). This kind of hole is useful for missing proofs only since they cannot be "filled" by unification. We fill them using tactics such as case <hole-name> => <tactic>.
That being said, I acknowledge that the feature you are asking for is useful in some circumstances.
We already had refine! (renamed to refine' today), and I added have' and let'. They transform all unresolved holes into new goals.
These are just macros defined here https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean#L270-L288
So, we can now write

def goal : 1 + 1 = 1 + 1 := by
  have h := 1
  have' h' := (rfl : _ + 1 = _ + 1)
  refine h'
  done

BTW, have' is not being highlighted. We stopped manually marking the builtin keywords since we will soon have
https://github.com/leanprover/lean4/pull/344
Your example also exposed other problems that have been fixed today :)

view this post on Zulip Mario Carneiro (Mar 13 2021 at 02:52):

What's the difference between refine without ' and exact then?

view this post on Zulip Leonardo de Moura (Mar 13 2021 at 03:00):

Mario Carneiro said:

What's the difference between refine without ' and exact then?

You can use synthetic holes with refine and create many subgoals. exact must not produce any subgoal.

view this post on Zulip Mario Carneiro (Mar 13 2021 at 03:01):

Is there syntax for a hole with no name? Does ? work?

view this post on Zulip Leonardo de Moura (Mar 13 2021 at 03:02):

Here is an example

theorem simple6 (x y z : Nat) : y = z  x = x  x = y  x = z :=
  intro h1 _ h3
  refine Eq.trans ?pre h1;
  case pre => assumption

view this post on Zulip Mario Carneiro (Mar 13 2021 at 03:03):

The lean 3 version would do something like:

theorem ex (x y z : Nat) : y = z  x = x  x = y  x = z := by
  intro h1 _ h3
  refine Eq.trans ? ?
  { exact h1 }
  { exact h3 }

It would be nice to have something like this where there are structured subgoals but they are simply ordered instead of named

view this post on Zulip Leonardo de Moura (Mar 13 2021 at 03:04):

You can still do this.

view this post on Zulip Mario Carneiro (Mar 13 2021 at 03:05):

great

view this post on Zulip Mario Carneiro (Mar 13 2021 at 03:05):

(I think that most of the time refine is used there aren't very interesting names to give these holes)

view this post on Zulip Leonardo de Moura (Mar 13 2021 at 03:06):

The syntax is ?_ instead of ? though


Last updated: May 07 2021 at 13:21 UTC