Allow naming exercises

Also factor out statements code
PatrickMassot · Mar 14, 2024 · ca9e614 · ca9e614
1 parent 9ceb74f
commit ca9e614
Show file tree

Hide file tree

Showing 3 changed files with 44 additions and 34 deletions.
diff --git a/Verbose/English/Statements.lean b/Verbose/English/Statements.lean
@@ -1,4 +1,5 @@
 import Verbose.Infrastructure.Initialize
+import Verbose.Tactics.Statements
 import Verbose.English.Widget
 
 import ProofWidgets.Demos.Macro
@@ -7,24 +8,14 @@ open Lean Meta Elab Command Parser Tactic
 
 open Lean.Parser.Term (bracketedBinder)
 
-/- **TODO**  Allow empty Given of Assume. -/
+endpoint (lang := en) mkProof (prf : TSyntax ``tacticSeq) : CoreM (TSyntax `tactic) :=
+Lean.TSyntax.mkInfoCanonical <$> `(tactic| with_suggestions $prf)
 
-elab ("Exercise"<|>"Example") str
+/- **TODO**  Allow omitting Given or Assume. -/
+
+elab name?:(ident)? ("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)
-  if (← getOptions).getBool `verbose.suggestion_widget then
-    let tac : TSyntax `tactic ←
-    Lean.TSyntax.mkInfoCanonical <$>
-      `(tactic| with_suggestions
-                  $prf)
-    elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := by {$tac}))
-  else
-    elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := $term))
+    tkp:"Proof:" prf?:(tacticSeq)? tkq:"QED" : command => do
+  mkExercise name? objs hyps concl prf? tkp tkq
diff --git a/Verbose/French/Statements.lean b/Verbose/French/Statements.lean
@@ -1,4 +1,5 @@
 import Verbose.Infrastructure.Initialize
+import Verbose.Tactics.Statements
 import Verbose.French.Widget
 
 import ProofWidgets.Demos.Macro
@@ -7,24 +8,14 @@ open Lean Meta Elab Command Parser Tactic
 
 open Lean.Parser.Term (bracketedBinder)
 
-/- **TODO**  Allow empty Given of Assume. -/
+endpoint (lang := fr) mkProof (prf : TSyntax ``tacticSeq) : CoreM (TSyntax `tactic) :=
+Lean.TSyntax.mkInfoCanonical <$> `(tactic| with_suggestions $prf)
 
-elab ("Exercice"<|>"Exemple") str
+/- **TODO**  Allow omitting Données or Hypothèses. -/
+
+elab name?:(ident)? ("Exercice"<|>"Exemple") str
     "Données :" objs:bracketedBinder*
     "Hypothèses :" hyps:bracketedBinder*
     "Conclusion :" concl:term
-    tkp:"Démonstration :" 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)
-  if (← getOptions).getBool `verbose.suggestion_widget then
-    let tac : TSyntax `tactic ←
-    Lean.TSyntax.mkInfoCanonical <$>
-      `(tactic| with_suggestions
-                  $prf)
-    elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := by {$tac}))
-  else
-    elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := $term))
+    tkp:"Démonstration :" prf?:(tacticSeq)? tkq:"QED" : command => do
+  mkExercise name? objs hyps concl prf? tkp tkq
diff --git a/Verbose/Tactics/Statements.lean b/Verbose/Tactics/Statements.lean
@@ -0,0 +1,28 @@
+import Mathlib.Tactic.Lemma
+import Verbose.Infrastructure.Multilingual
+
+open Lean Meta Elab Command Parser Tactic
+
+open Lean.Parser.Term (bracketedBinder)
+
+endpoint mkProof (prf : TSyntax ``tacticSeq) : CoreM (TSyntax `tactic)
+
+def mkExercise (name? : Option Ident) (objs hyps : TSyntaxArray ``bracketedBinder) (concl: Term)
+    (prf?: Option (TSyntax ``tacticSeq)) (tkp tkq : Syntax) : CommandElabM Unit := do
+  let ref := mkNullNode #[tkp, tkq]
+  let prf ← prf?.getDM <| withRef ref `(tacticSeq| skip)
+  let term ← withRef tkq `(by%$ref
+    skip%$ref
+    ($prf)
+    skip%$ref)
+  if (← getOptions).getBool `verbose.suggestion_widget then
+    let tac : TSyntax `tactic ← liftCoreM <| mkProof prf
+    if let some name := name? then
+      elabCommand (← `(command|lemma $name $(objs ++ hyps):bracketedBinder* : $concl := by {$tac}))
+    else
+      elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := by {$tac}))
+  else
+    if let some name := name? then
+      elabCommand (← `(command|lemma $name $(objs ++ hyps):bracketedBinder* : $concl := $term))
+    else
+      elabCommand (← `(command|example $(objs ++ hyps):bracketedBinder* : $concl := $term))