have with metavariables?

Stream: lean4

[Jason Gross]

Is there a version of have that permits uninferred metavariables?

[Leonardo de Moura]

Jason Gross said:

Is there a version of have that permits uninferred metavariables?

Could you please post an example?

[Jason Gross]

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
-/

[Leonardo de Moura]

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 :)

[Mario Carneiro]

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

[Leonardo de Moura]

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.

[Mario Carneiro]

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

[Leonardo de Moura]

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

[Mario Carneiro]

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

[Leonardo de Moura]

You can still do this.

[Mario Carneiro]

great

[Mario Carneiro]

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

[Leonardo de Moura]

The syntax is ?_ instead of ? though