Empty tactic seq

Stream: lean4

[Patrick Massot]

In my teaching library I have

import Lean

open Lean Meta Elab Command Parser Tactic Term

elab ("Exercise"<|>"Example") str
    "Given:" objs:bracketedBinder*
    "Assume:" hyps:bracketedBinder*
    "Conclusion:" concl:term
    "Proof:" prf:tacticSeq "QED": command => do
  elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := by $prf))

Exercise "Test"
  Given: (n : Nat)
  Assume: (h : n = 0)
  Conclusion: True
Proof:
  sorry
QED

It works well and I can replace the sorry by a proof. But it would be even better if I could remove the sorry and have the elaborator putting it in case the proof is empty. But I was not able to achieve this. Any idea?

[Kyle Miller]

You could make it optional and use docs#Option.getDM to fill it in with sorry when it's missing.

elab ("Exercise"<|>"Example") str
    "Given:" objs:bracketedBinder*
    "Assume:" hyps:bracketedBinder*
    "Conclusion:" concl:term
    "Proof:" prf?:(tacticSeq)? "QED": command => do
  let prf ← prf?.getDM `(tacticSeq| sorry)
  elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := by $prf))

[Patrick Massot]

Nice, thanks!

[Patrick Massot]

Oh no, it doesn't really work. Putting the cursor inside the empty proof shows no goal.

[Kyle Miller]

How about this?

import Lean
import Std.Data.Option.Basic

open Lean Meta Elab Command Parser Tactic Term

elab ("Exercise"<|>"Example") str
    "Given:" objs:bracketedBinder*
    "Assume:" hyps:bracketedBinder*
    "Conclusion:" concl:term
    "Proof:" prf?:(tacticSeq)? tk:"QED" : command => do
  let prf ← prf?.getDM <| withRef tk `(tacticSeq| done)
  elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := by $prf))

Exercise "Test"
  Given: (n : Nat)
  Assume: (h : n = 0)
  Conclusion: True
Proof:

QED

The QED is red and says "unsolved goals"

[Patrick Massot]

It is slightly better but still way too confusing for students.

[Kyle Miller]

There's probably a more elegant way to do this, but I got it to show the goal state by putting some source positions on everything in sight.

import Lean
import Std.Data.Option.Basic

open Lean Meta Elab Command Parser Tactic Term

elab ("Exercise"<|>"Example") str
    "Given:" objs:bracketedBinder*
    "Assume:" hyps:bracketedBinder*
    "Conclusion:" concl:term
    tkp:"Proof:" prf?:(tacticSeq)? tk:"QED" : command => do
  let ref := mkNullNode #[tkp, tk]
  let prf ← prf?.getDM <| withRef ref `(tacticSeq| skip)
  elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := by%$ref
    skip%$ref
    ($prf)
    skip%$ref))

Exercise "Test"
  Given: (n : Nat)
  Assume: (h : n = 0)
  Conclusion: True
Proof:

QED

[Kyle Miller]

I couldn't figure out why it's the first line that gets the "unsolved goals"

[Kyle Miller]

Never mind, it's because the by syntax itself wasn't being assigned a ref. Here's it putting the red squiggle on QED:

import Lean
import Std.Data.Option.Basic

open Lean Meta Elab Command Parser Tactic Term

elab ("Exercise"<|>"Example") str
    "Given:" objs:bracketedBinder*
    "Assume:" hyps:bracketedBinder*
    "Conclusion:" concl:term
    tkp:"Proof:" prf?:(tacticSeq)? tk:"QED" : command => do
  let ref := mkNullNode #[tkp, tk]
  let prf ← prf?.getDM <| withRef ref `(tacticSeq| skip)
  let term ← withRef tk `(by%$ref
    skip%$ref
    ($prf)
    skip%$ref)
  elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := $term))

Exercise "Test"
  Given: (n : Nat)
  Assume: (h : n = 0)
  Conclusion: True
Proof:

QED

[Patrick Massot]

Great!

[Patrick Massot]

Now I need to weave that through the widget panel stuff...

[Eric Wieser]

Are the skip%$refs still needed there?