expand `have` capabilities

Stream: mathlib4

[Arthur Paulino]

I wanna try to implement unstructured have but I will need some guidance.

I have this:

elab "have " id:ident " : " t:term " dont_wanna_do_this " p:term : tactic => do
  let t ← elabTerm t none
  let p ← elabTermEnsuringType p t
  liftMetaTactic fun mvarId => do
    let mvarIdNew ← assert mvarId id.getId t p
    let (_, mvarIdNew) ← intro1P mvarIdNew
    return [mvarIdNew]

example : true := by
  have h : Nat dont_wanna_do_this 5
  simp

Instead of providing a term of the given type, I want to turn that type into a new goal (and add it to the list of goals).

So I have two questions:

• How can I add h : Nat to the context without relying on assert (nor on a given term of Nat)?
• How can I add ⊢ Nat as a new goal?

[Mario Carneiro]

(aside: I object to the term "unstructured", since all uses of this tactic in mathlib are quite structured)

[Mario Carneiro]

it's a version of have that keeps the proof inside the same tactic block

[Arthur Paulino]

Yeah I don't understand why "unstructured" either. I'm just mimicking what's on the Mathport/Syntax.lean file

[Mario Carneiro]

I'm confused why you have the dont_wanna_do_this part

[Mario Carneiro]

why aren't you just using the syntax as is?

[Arthur Paulino]

I just want to be explicit that I don't want to rely on p. With my current knowledge, the only way that I know how to add h : Nat to the context is through assert. And it relies on a term of the given type

[Mario Carneiro]

You can use assert, you just create a new metavariable with the desired type and pass it to assert and also put it in the goal list

[Arthur Paulino]

/--
  Convert the given goal `Ctx |- target` into `Ctx |- type -> target`.
  It assumes `val` has type `type` -/
def assert (mvarId : MVarId) (name : Name) (type : Expr) (val : Expr) : MetaM MVarId

How can I create an Expr of type type at this point? Isn't this the whole theorem proving challenge?

[Arthur Paulino]

(I'm talking about the 4th argument val)

[Arthur Paulino]

I would appreciate a hint without much spoiling, if possible :)

[Arthur Paulino]

Huh, wait, something clicked in my head. Let me try something

[Arthur Paulino]

Alright, I think I got it:

elab "have " id:ident " : " t:term : tactic => do
  let t ← elabTerm t none
  let p ← mkFreshExprMVar t
  liftMetaTactic fun mvarId => do
    let mvarIdNew ← assert mvarId id.getId t p
    let (_, mvarIdNew) ← intro1P mvarIdNew
    return [p.mvarId!, mvarIdNew]
  let goals ← getUnsolvedGoals

example : Nat := by
  have h : Nat
  · exact 5
  exact h

Please let me know if this is too naive (of course I still need to generalize an optional identifier if the user wants to store on this)

[Arthur Paulino]

I don't see a clear advantage of this except for being able to change the goals order as in:

example : Nat := by
  have h : Nat
  swap
  exact h
  exact 5

Are there other benefits? I thought about being able to add tags to the subgoals. Maybe that can be useful to make proofs more organized with case <tag> => tacSeq?

[Mario Carneiro]

you want the first two lines to be in the liftMetaTactic block, that also sets the context

[Mario Carneiro]

the version that changes goals order is already a thing, that's suffices

[Mario Carneiro]

you should name the subgoals as well, I think it makes sense for the mvar to be named the same as the identifier

[Arthur Paulino]

Mario Carneiro said:

you want the first two lines to be in the liftMetaTactic block, that also sets the context

I can do this:

elab "have " id:ident " : " t:term : tactic => do
  let t ← elabTerm t none
  liftMetaTactic fun mvarId => do
    let p ← mkFreshExprMVar t
    let mvarIdNew ← assert mvarId id.getId t p
    let (_, mvarIdNew) ← intro1P mvarIdNew
    return [p.mvarId!, mvarIdNew]

But elabTerm can't be executed in MetaM. Unless I'm doing something wrong

[Mario Carneiro]

At least in lean 3, opening another tactic block via have : foo := by { } instead of have : foo, { } meant that the two blocks could not share metavariables - everything has to be solved in the nested block

[Arthur Paulino]

This is already happening:

example : Nat := by
  have h : Nat
  · let q := 5
    exact 5
  let a := q -- unknown identifier 'q'
  exact h

[Mario Carneiro]

what are you showing?

[Mario Carneiro]

I'm not sure if withMainContext needs to be called before the elabTerm; to test that you should try referencing a variable in another goal..?

[Mario Carneiro]

but also, you should be using the original syntax with haveIdLhs instead of "have " ident " : " term

[Mario Carneiro]

those produce different syntax trees

[Arthur Paulino]

Mario Carneiro said:

I'm not sure if withMainContext needs to be called before the elabTerm; to test that you should try referencing a variable in another goal..?

The variables don't seem to be shared among goals:

example : true ∧ true := by
  constructor
  have h : Nat
  have w : String
  /-
  ⊢ String
  w : String
  ⊢ ℕ
  case left
  h : ℕ
  ⊢ true = true
  case right
  ⊢ true = true
  -/
  simp
  simp

[Arthur Paulino]

I think I am misunderstanding what you're saying

[Mario Carneiro]

The question is whether the elaboration of the type is occurring in the right context, because tactics operate on a bunch of goals and different goals have different variables in them and hence elaborate terms differently

[Arthur Paulino]

Hmm, even with withMainContext it's still possible to do:

elab "have " id:ident " : " t:term : tactic => do
  withMainContext do
    let t ← elabTerm t none
    let name := id.getId
    liftMetaTactic fun mvarId => do
      let p ← mkFreshExprMVar (userName := name) t
      let mvarIdNew ← assert mvarId name t p
      let (_, mvarIdNew) ← intro1P mvarIdNew
      return [p.mvarId!, mvarIdNew]

example : true ∧ true := by
  constructor
  have h1 : String
  have h2 : String
  case h1 =>
    exact h2 -- this works, but is it desired?
  case h2 =>
    exact ""
  simp
  simp

[Arthur Paulino]

I will upgrade the syntax to haveIdLhs after I get this POC working nicely

[Mario Carneiro]

That all seems to be working as intended

[Mario Carneiro]

withMainContext doesn't seem to make a difference

[Mario Carneiro]

the question is about free variables in t and where they come from

[Mario Carneiro]

so you need an example with a dependent type instead of just String

[Mario Carneiro]

like this

import Lean
open Lean Meta Elab Tactic

elab "have " id:ident " : " t:term : tactic => do
  -- withMainContext do
    let t ← elabTerm t none
    let name := id.getId
    liftMetaTactic fun mvarId => do
      let p ← mkFreshExprMVar (userName := name) t
      let mvarIdNew ← assert mvarId name t p
      let (_, mvarIdNew) ← intro1P mvarIdNew
      return [p.mvarId!, mvarIdNew]

example : True := by
  have h1 : String := sorry
  have h2 : h1 = h1 -- fail

[Arthur Paulino]

More progress:

syntax "have " (ident)? " this "? " : " term (" as " ident)? : tactic

private def haveDef (name : Name) (t : Syntax) (i? : Option Syntax) : TacticM Unit :=
  withMainContext do
    let t ← elabTerm t none
    let caseName := match i? with
      | none   => name
      | some i => i.getId
    liftMetaTactic fun mvarId => do
      let p ← mkFreshExprMVar (userName := caseName) t
      let mvarIdNew ← assert mvarId name t p
      let (_, mvarIdNew) ← intro1P mvarIdNew
      return [p.mvarId!, mvarIdNew]

elab_rules : tactic
  | `(tactic|have $h:ident : $t:term $[as $i:ident]?) => haveDef h.getId t i
  | `(tactic|have $[this]? : $t:term $[as $i:ident]?) => haveDef `this   t i

example {a b : Nat} (h : a = b) : 2 * a + b = a + (2 * b) := by
  rw [h]
  have : 2 * b = b + b as h_two_mul
  on_goal -1     => rw [this, Nat.add_assoc] -- targeting the final goal
  case h_two_mul => ring

With this syntax it's possible to name the subgoals with as <name>

[Mario Carneiro]

:thinking: Seems like have h this : foo is legal syntax

[Mario Carneiro]

I don't think the as thing is necessary, people won't be using the case name in most cases and the given identifier seems as good a name as any

[Mario Carneiro]

not to mention that it's not entirely clear if it will play well with the haveIdLhs parser

[Arthur Paulino]

Btw I'm having some troubles with the haveIdLhs parser

[Mario Carneiro]

care to share?

[Arthur Paulino]

Apparently it's not allowed to say have this : Nat with it

[Mario Carneiro]

that's true, although it's not obvious we need to do anything about it

[Mario Carneiro]

you can just write have : instead

[Mario Carneiro]

If you want to make this acceptable in that position then probably it should be a lean core change

[Mario Carneiro]

I'm not really sure why this became a keyword in the first place, besides perhaps some tactic that forgot to use &"this" instead of "this" in the syntax. @Sebastian Ullrich do you know?

[Arthur Paulino]

Alright, this works:

syntax "have " Parser.Term.haveIdLhs : tactic

private def haveDef (name : Name) (t : Syntax) : TacticM Unit :=
  withMainContext do
    let t ← elabTerm t none
    liftMetaTactic fun mvarId => do
      let p ← mkFreshExprMVar (userName := name) t
      let mvarIdNew ← assert mvarId name t p
      let (_, mvarIdNew) ← intro1P mvarIdNew
      return [p.mvarId!, mvarIdNew]

elab_rules : tactic
  | `(tactic|have $[$h?:ident]? : $t:term) =>
    match h? with
    | none   => haveDef `this t
    | some h => haveDef h.getId t

example {a b : Nat} (h : a = b) : 2 * a + b = a + (2 * b) := by
  rw [h]
  have h' : 2 * b = b + b
  on_goal -1 => rw [h', Nat.add_assoc] -- targeting the final goal
  case h'    => ring

Is that elab_rule enough?

[Mario Carneiro]

you aren't covering the have $[$h?:ident]? case

[Arthur Paulino]

Without expliciting a type?

[Mario Carneiro]

right

[Arthur Paulino]

What is supposed to happen in this case?

[Mario Carneiro]

the type is a metavariable (not added as a goal)

[Mario Carneiro]

example : true :=
begin
  have h,
  -- 2 goals
  -- ⊢ ?m_1

  -- h : ?m_1
  -- ⊢ true
end

[Mario Carneiro]

the lean 4 syntax also allows binders between the identifier and the colon, although it is lower priority since lean 3 doesn't support this

[Arthur Paulino]

How come it's not added as a goal? I see "2 goals" in your example after have h

[Arthur Paulino]

This seems to work, but for some reason I'm being required to put a semicolon after have:
https://github.com/leanprover-community/mathlib4/pull/232

Help is appreciated :pray:

[Mario Carneiro]

FYI you can match both cases of have at once using | `(tactic|have $[$n:ident]? $[: $t:term]?) => haveDef n t

[Arthur Paulino]

I tried that, but it gave me an error

[Arthur Paulino]

I think it's related to the semicolon issue. The syntax tree might have some issue

[Arthur Paulino]

We might need a way to say "no line break allowed". Something similar to noWs, which forbids spaces

[Mario Carneiro]

Most parsers use colGt when parsing trailing idents for exactly this reason. This fixes the issue:

import Lean

def Lean.Parser.Term.haveIdLhs' :=
  optional (ident >> many (ppSpace >>
    checkColGt "expected to be indented" >>
    (simpleBinderWithoutType <|> bracketedBinder))) >> optType

namespace Mathlib.Tactic

open Lean Elab.Tactic Meta Parser.Term

syntax "have " haveIdLhs' : tactic

elab_rules : tactic
| `(tactic|have $[$n:ident]? $[: $t:term]?) =>
  withMainContext do
    let name : Name := match n with
      | none   => `this
      | some n => n.getId
    let t ← match t with
    | none   => mkFreshTypeMVar
    | some t => elabTerm t none
    liftMetaTactic fun mvarId => do
      let p ← mkFreshExprMVar (userName := name) t
      let mvarIdNew ← assert mvarId name t p
      let (_, mvarIdNew) ← intro1P mvarIdNew
      return [p.mvarId!, mvarIdNew]

example : True := by
  have h
  exact 5
  simp

[Arthur Paulino]

Hmm, I don't understand it yet but I'm glad it solved the issue!
Will adjust the PR tomorrow

[Arthur Paulino]

Thank you :D

[Mario Carneiro]

The problem is that

example : True := by
  have h
    simp

is interpreted as

example : True := by
  have h (simp : _) : _

[Mario Carneiro]

and without the indentation fix,

example : True := by
  have h
  simp

is also interpreted that way

[Arthur Paulino]

Can't we just forbid linebreaks after haveIdLhs?

[Arthur Paulino]

(is it even possible to do so?)

[Arthur Paulino]

This way we wouldn't need to redefine the whole syntax

[Mario Carneiro]

well, this is arguably an issue in core

[Mario Carneiro]

it's also not a good idea to forbid linebreaks generally because not all uses fit on a line

[Sebastian Ullrich]

Mario Carneiro said:

I'm not really sure why this became a keyword in the first place, besides perhaps some tactic that forgot to use &"this" instead of "this" in the syntax. Sebastian Ullrich do you know?

I don't think you can use & in leading position. But it also looks like a bad idea, since it would make it easy to introduce a variable this that then can't be referenced.

[Mario Carneiro]

@Sebastian Ullrich I can't understand your comment. Why is this not like any other ident name? You should be able to just use it like this + 2.

[Sebastian Ullrich]

https://github.com/leanprover/lean4/issues/821

[Sebastian Ullrich]

In short, because this bindings are not regular, it cannot be a regular identifier

[Arthur Paulino]

I remember times in which the well-behaved metavariable names helped me make sense of what was going on:

example : true :=
begin
  have h,
  -- 2 goals
  -- ⊢ ?m_1

  -- h : ?m_1
  -- ⊢ true
end

But with this implementation in Lean 4, they are named after some "arbitrarily" high number:

example : True := by
  have h
  /-
  case h
  ⊢ ?m.2156
  h : ?m.2156
  ⊢ True
  -/

Should I worry about this?

[Mario Carneiro]

Sebastian Ullrich said:

In short, because this bindings are not regular, it cannot be a regular identifier

I don't really understand the hygiene system, but can't have := ...; this be treated exactly like have this := ...; this? That is, the have introduces an invisible this token suitably marked up with hygiene stuff so that the second this resolves

[Mario Carneiro]

@Arthur Paulino No, that's a general issue with mvar printing not related to have

[Sebastian Ullrich]

Mario Carneiro said:

Sebastian Ullrich said:

In short, because this bindings are not regular, it cannot be a regular identifier

I don't really understand the hygiene system, but can't have := ...; this be treated exactly like have this := ...; this? That is, the have introduces an invisible this token suitably marked up with hygiene stuff so that the second this resolves

Hygiene happens when the quotation is evaluated, i.e. when the syntax tree is constructed. The this binding does not exist at that point in any form.

[Mario Carneiro]

I think there are other tactics that want to have this "invisible this" behavior for other names too

[Mario Carneiro]

The have exists though, can't it be marked up somehow?

[Mario Carneiro]

that is, we are syntactically at a point where we know it is have and that it needs a this

[Sebastian Ullrich]

Well, this is a specific property of the Lean hygiene algorithm that is different in e.g. Racket: only identifiers are annotated with hygiene information, so we can't just say "introduce this with the same scope as the have keyword"

[Sebastian Ullrich]

I'm relatively happy with the this design so far, it makes it completely clear that it does not follow the standard identifier scoping

[Mario Carneiro]

I'm not sure the original issue is all that important though. Is there a reason I should care if I don't write things like that in syntax quotations? i.e. as a regular user how does this affect me?

[Mario Carneiro]

let this := 1 is a syntax error. This makes me unhappy as a user

[Mario Carneiro]

and there are lots of other places that accept every ident but not this

[Sebastian Ullrich]

let this is not a syntax error

[Mario Carneiro]

I thought it was, perhaps fun this => ...?

[Arthur Paulino]

Mario Carneiro said:

let this := 1 is a syntax error. This makes me unhappy as a user

I had made it possible with a custom syntax for the replace tactic: link

[Mario Carneiro]

#check fun this => 1 results in a weird error

[Sebastian Ullrich]

Hah, that should probably be a special case in the match elaborator. We shouldn't even elaborate a match in this case.

[Sebastian Ullrich]

But going back to the question of why you should care about the fix: in Lean 3 you assume that you can lift arbitrary tactic snippets into a helper tactic, no? In Lean 4 that would involve a syntax quotation, so the fix makes sure this still works in the helper.

[Sebastian Ullrich]

Now Lean 4 actually doesn't let you lift arbitrary snippets exactly because of hygiene, but without the fix, using this even completely internal to the helper would not work.

[Mario Carneiro]

I find that using identifiers of any kinds in syntax quotations does the wrong thing and I always use $(mkIdent `foo)

[Mario Carneiro]

which probably makes me a bad person

[Sebastian Ullrich]

I guess you don't perceive them as separate scopes then. Which makes sense coming from Lean 3, but I'd hope that's not the natural assumption to make without that background.

[Mario Carneiro]

I don't really know what that means. I want a foo in my expression

[Mario Carneiro]

and writing foo doesn't give me that

[Sebastian Ullrich]

Such that it is visible to the outside?

[Mario Carneiro]

such that the identifier is called foo

[Mario Carneiro]

my model of identifiers is probably not hygienic, I just think of them as names and everything else scares me

[Mario Carneiro]

(I exaggerate, but hygienic identifiers are significantly more complex to deal with as a tactic author)

[Mario Carneiro]

I think that hygiene is most important for macro tactics and other "simple" expansions where you aren't doing anything except shuffling syntax around and using syntax quotations

[Sebastian Ullrich]

I can't say much without a specific example. But the whole point of hygiene is to make scoping in metaprograms behave like you would expect in regular programs. If a variable reference in a helper function doesn't bind to a variable of that name in the caller, then the same should be true for a helper tactic.

[Mario Carneiro]

I am usually writing elab tactics where very little is done using syntax quotations, and there it seems that hygiene is only an interference

[Mario Carneiro]

An example might be Arthur's have tactic above; what does it need to do to handle this correctly?

[Arthur Paulino]

Mario Carneiro said:

An example might be Arthur's have tactic above; what does it need to do to handle this correctly?

This code did it. But it relied on that custom syntax

[Mario Carneiro]

Here's a proposal: an invisibleThis parser that parses nothing and yields a hygienic this ident

[Mario Carneiro]

then have and friends can use "have" (ident <|> invisibleThis) ...

[Mario Carneiro]

(or better yet, invisible(`this) since that way you can use other names too)

[Mario Carneiro]

That would make have := 1; this and have this := 1; this produce the exact same Syntax

[Mario Carneiro]

(which is not currently the case btw, the second one adds a match)

[Arthur Paulino]

implicit(`this) also works as a name

[Sebastian Ullrich]

You can use (ident <|> Lean.termThis), though perhaps you had something different in mind

[Mario Carneiro]

I'm talking about making the binder special and making this a regular identifier again

[Mario Carneiro]

The reason have := 1; this doesn't work is because the second this gets marked up with hygiene information local to the scope and the first one doesn't, because it doesn't exist. To fix this we can have a parser that inserts a this token exactly as though the extra characters this were present in the original string

[Sebastian Ullrich]

The one fundamental rule of the parser is that the token sequence in the returned syntax tree is identical to the input

[Mario Carneiro]

Okay, then it's not a proper token but instead a node Parser.implicit._0.metadata #[] or something

[Mario Carneiro]

it's your choice where you want to stuff the metadata

[Sebastian Ullrich]

That would work for the parser, but we would have to adjust the hygiene algorithm. It sounds a bit messy.

[Sebastian Ullrich]

For what it's worth, it would be nice if the desired tactic could be implemented purely as a macro. This comes close, but the case with the missing type adds it as an additional goal.

syntax "have " (colGt term)? (" : " colGt term)? : tactic
macro_rules
  | `(tactic| have $[$id:ident]?) => `(tactic| have $[$id:ident]? : ?_ := ?_)
  | `(tactic| have : $h) => `(tactic| have : $h := ?_)
  | `(tactic| have $e:term $[: $h]?) => `(tactic| have $e:term $[: $h]? := ?_)

[Arthur Paulino]

Sebastian Ullrich said:

but the case with the missing type adds it as an additional goal

How come? Even if I provide the term? I would like Lean to elaborate the type for me in that case

[Sebastian Ullrich]

No, only if it can't be inferred

[Sebastian Ullrich]

Wait, I thought the point of the tactic was that you don't provide the term :upside_down:

[Arthur Paulino]

This no longer works :thinking:

example : True := by
  have h
  exact 5 -- invalid universe level, ?u.2348 is not greater than 0
  simp

[Sebastian Ullrich]

Ah, the goals are in the wrong order

[Gabriel Ebner]

(deleted)

[Arthur Paulino]

Let's bring the discussion here.
What should I do with the syntax?

[Mario Carneiro]

Do you know how to support the binders?

[Arthur Paulino]

I still don't know what binders are :sweat_smile:

[Mario Carneiro]

if you can support the entire tactic that would be ideal

[Mario Carneiro]

The idea is that have foo x := x + 1 should define a function like have foo := fun x => x + 1

[Mario Carneiro]

have foo x : x < x + 1 would produce a proof of foo : (x : Nat) -> x < x + 1 on one branch and a proof obligation x : nat |- x < x + 1 on the other (note that x is already introduced)

[Arthur Paulino]

So If i have more than one identifier it will always define a function?

[Arthur Paulino]

(using the first identifier as the function name and the others as parameters)

[Mario Carneiro]

yes, the syntax is an ident followed by a list of x or (x) or (x : ty)

[Arthur Paulino]

1 ident => current behavior
2+ ident => function

[Arthur Paulino]

I can do that

[Mario Carneiro]

it's not a separate case, really

[Mario Carneiro]

the haveIdLhs parser gives you the list of binders and the name separately

[Arthur Paulino]

have foo := x + 1
have foo x := x + 1
Are those the same case?

[Mario Carneiro]

yes, the first one has binders [] and the second has binders [x]

[Mario Carneiro]

and have foo x y would have binders [x, y]

[Mario Carneiro]

and have (x : ty) would have binders [(x : ty)] and no ident (i.e. this)

[Mario Carneiro]

the parser handles all this already

[Arthur Paulino]

I will try it later

[Arthur Paulino]

is there an example of these binders handling?

[Mario Carneiro]

intro tactic, or let

[Mario Carneiro]

you might just be able to delegate to regular have

[Arthur Paulino]

delegating to regular have has the same issue from Sebastian's macro

[Arthur Paulino]

@Mario Carneiro I'm not sure I fully understood what you meant in the lean4 stream. This is my current code:

import Lean

def Lean.Parser.Term.haveIdLhs' : Parser :=
  optional (ident >> many (ppSpace >>
    checkColGt "expected to be indented" >>
    (simpleBinderWithoutType <|> bracketedBinder))) >> optType

def Lean.Parser.Term.letIdLhs' : Parser :=
  ident >> notFollowedBy (checkNoWsBefore "" >> "[")
    "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >>
      many (ppSpace >> checkColGt "expected to be indented" >>
        (simpleBinderWithoutType <|> bracketedBinder)) >> optType

namespace Mathlib.Tactic

open Lean Elab.Tactic Meta

syntax "have " Parser.Term.haveIdLhs' : tactic
syntax "let "  Parser.Term.letIdLhs'  : tactic

private def addToContext (name : Name) (t : Expr) (keepTerm : Bool) : TacticM Unit :=
  let declFn := if keepTerm then define else assert
  liftMetaTactic fun mvarId => do
    let p ← mkFreshExprMVar (userName := name) t
    let mvarIdNew ← declFn mvarId name t p
    let (_, mvarIdNew) ← intro1P mvarIdNew
    return [p.mvarId!, mvarIdNew]

private def elabType (t : Option Syntax) : Elab.TermElabM Expr :=
  match t with
  | none   => mkFreshTypeMVar
  | some t => elabTerm t none

elab_rules : tactic
| `(tactic|have $[$n:ident]? $[: $t:term]?)  => withMainContext do
  let name := match n with
    | none   => `this
    | some n => n.getId
  addToContext name (← elabType t) false
| `(tactic|have $n:ident $bs* $[: $t:term]?) => withMainContext do
    let e ← Elab.Term.elabBinders bs $
      fun es => do mkForallFVars es (← elabType t)
    addToContext n.getId e false
| `(tactic|let $n:ident $[: $t:term]?)       => withMainContext do
  addToContext n.getId (← elabType t) true
| `(tactic|let $n:ident $bs* $[: $t:term]?)  => withMainContext do
    let e ← Elab.Term.elabBinders bs $
      fun es => do mkForallFVars es (← elabType t)
    addToContext n.getId e true

[Arthur Paulino]

I'm tackling let and have in the same file because there's a lot of code that can be reused

[Mario Carneiro]

have f (x : Nat) : x < x + 1

should produce goals

case f
x : Nat
|- x < x + 1

f : (x : Nat) -> x < x + 1
|- goal

[Mario Carneiro]

I think that means that you have to inline addToContext and move some things around

[Arthur Paulino]

Alright. Another question: is there another elab_rule I am missing?

[Mario Carneiro]

IIRC the behavior is different if you put more than one symtax node in the same elab_rules

[Mario Carneiro]

so I think you want have and let to be separate

[Mario Carneiro]

also I think you should be matching (tactic| have $[$n:ident $bs*]? $[: $t:term]?)

[Mario Carneiro]

which is the only case

[Arthur Paulino]

Nice, tyvm :+1:

[Arthur Paulino]

Mario Carneiro said:

have f (x : Nat) : x < x + 1

should produce goals

case f
x : Nat
|- x < x + 1

f : (x : Nat) -> x < x + 1
|- goal

I don't know how to make it possible. I thought about a hacky solution performing intro x multiple times (depending on the number of binders and their types)

[Arthur Paulino]

Hmm, maybe not "hacky", but kinda inefficient

[Arthur Paulino]

Okay I think it turned out pretty good actually: mathlib4#232