add let_intros for better experience with levels about functions

doc/create_game.md

@@ -189,8 +189,7 @@ The statement is the exercise of the level. The basics work the same as they wou
 
 #### Name
 
-You can give your exercise a name: `Statement my_first_exercise (n : Nat) ...`. If you do so, it will be added to the inventory and be available in future levels.
-
+You can give your exercise a name: `Statement my_first_exercise (n : Nat) …`. If you do so, it will be added to the inventory and be available in future levels.
 You can but a `Statement` inside namespaces like you would with `theorem`.
 
 #### Doc String / Exercise statement
@@ -203,6 +202,28 @@ Statement ...
   sorry
 ```
 
+#### Local `let` definitions
+
+If you want to make a local definition/notation which only holds for this exercise (e.g.
+a function `f : ℤ → ℤ := fun x ↦ 2 * x`) the recommended way is to use a `let`-statement:
+
+```lean
+Statement (a : ℤ) (h : 0 < a) :
+    let f : ℤ → ℤ := fun x ↦ 2 * x
+    0 < f a := by
+  sorry
+```
+
+The game automatically `intros` such `let`-statements, such that you and the player will see
+the following initial proof state:
+
+```
+a: ℤ
+h: 0 < a
+f: ℤ → ℤ := fun x => 2 * x
+⊢ 0 < f a
+```
+
 #### Attributes
 
 You can add attributes as you would for a `theorem`. Most notably, you can make your named exercise a `simp` lemma:

doc/hints.md

@@ -117,3 +117,5 @@ $$
 \\end{CD}
 $$
 ```
+
+See https://www.jmilne.org/not/Mamscd.pdf

server/GameServer/Commands.lean

@@ -3,6 +3,7 @@ import GameServer.Inventory
 import GameServer.Options
 import GameServer.SaveData
 import GameServer.Hints
+import GameServer.Tactic.LetIntros
 import I18n
 
 open Lean Meta Elab Command
@@ -364,36 +365,38 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     collectUsedInventory proof
   | _ => throwError "expected `:=`"
 
+  -- extract the `tacticSeq` from `val` in order to add `let_intros` in front.
+  -- TODO: don't understand meta-programming enough to avoid having `let_intros`
+  -- duplicated three times below…
+  let tacticStx : TSyntax `Lean.Parser.Tactic.tacticSeq := match val with
+  | `(Parser.Command.declVal| := by $proof) => proof
+  | _ => panic "expected `:= by`"
+
   -- Add theorem to context.
   match statementName with
   | some name =>
     let env ← getEnv
-
     let fullName := (← getCurrNamespace) ++ name.getId
-
     if env.contains fullName then
       let origType := (env.constants.map₁.find! fullName).type
       -- TODO: Check if `origType` agrees with `sig` and output `logInfo` instead of `logWarning`
       -- in that case.
       logWarningAt name (m!"Environment already contains {fullName}! Only the existing " ++
       m!"statement will be available in later levels:\n\n{origType}")
-      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨tacticStx⟩)})
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
-
     else
-      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig $val)
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨tacticStx⟩)})
       elabCommand thmStatement
       -- Check that statement has a docs entry.
       checkInventoryDoc .Lemma name (name := fullName) (template := docContent)
-
   | none =>
-    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig $val)
+    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨tacticStx⟩)})
     elabCommand thmStatement
 
   let msgs := (← get).messages
-
   let mut hints := #[]
   let mut nonHintMsgs := #[]
   for msg in msgs.msgs do

server/GameServer/FileWorker.lean

@@ -4,6 +4,7 @@ import GameServer.Game
 import GameServer.ImportModules
 import GameServer.SaveData
 import GameServer.EnvExtensions
+import GameServer.Tactic.LetIntros
 
 namespace MyModule
 
@@ -258,8 +259,11 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           let tacticStx := (#[skip] ++ tacticStx.getArgs ++ #[done]).map (⟨.⟩)
           let tacticStx := ← `(Lean.Parser.Tactic.tacticSeq| $[$(tacticStx)]*)
 
+          -- Always call `let_intros` to get rid `let` statements in the goal.
+          -- This makes the experience for the user much nicer and allows for local
+          -- definitions in the exercise.
           let cmdStx ← `(command|
-            theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {let_intros; $(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
       cmdCtx cmdStateRef
   let postNew := (← tacticCacheNew.get).post

server/GameServer/Tactic/LetIntros.lean

@@ -0,0 +1,65 @@
+import Lean.Elab.Binders
+import Lean.Elab.Tactic.Basic
+import Lean.Meta.Tactic.Intro
+
+/-!
+# `let_intros` Tactic
+
+`let_intros` is a weaker form of `intros` aimed to only introduce `let` statements,
+but not for example `∀`-binders.
+-/
+
+namespace GameServer
+
+open Lean Meta Elab Parser Tactic
+
+/--
+Copied from `Lean.Meta.getIntrosSize`.
+-/
+private partial def getLetIntrosSize : Expr → Nat
+  -- | .forallE _ _ b _ => getLetIntrosSize b + 1
+  | .letE _ _ _ b _  => getLetIntrosSize b + 1
+  | .mdata _ b       => getLetIntrosSize b
+  | e                =>
+    if let some (_, _, _, b) := e.letFun? then
+      getLetIntrosSize b + 1
+    else
+      0
+
+/--
+Copied and from `Lean.MVarId.intros`.
+-/
+def _root_.Lean.MVarId.letIntros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do
+  let type ← mvarId.getType
+  let type ← instantiateMVars type
+  let n := getLetIntrosSize type
+  if n == 0 then
+    return (#[], mvarId)
+  else
+    -- `introNP` preserves the binder names
+    mvarId.introNP n
+
+/--
+`let_intros` introduces all `let` statements that are preceeding the proof. Concretely
+it does a subset of what `intros` does.
+
+If names are provided, it will introduce as many `let` statements as there are names.
+-/
+syntax (name := letIntros) "let_intros" : tactic
+-- (ppSpace colGt (ident <|> hole))*
+
+#check letIntros
+
+@[tactic letIntros] def evalLetIntros : Tactic := fun stx => do
+  match stx with
+  | `(tactic| let_intros) => liftMetaTactic fun mvarId => do
+    let (_, mvarId) ← mvarId.letIntros
+    return [mvarId]
+  -- | `(tactic| let_intros $ids*) => do
+  --   let fvars ← liftMetaTacticAux fun mvarId => do
+  --     let (fvars, mvarId) ← mvarId.introN ids.size (ids.map getNameOfIdent').toList
+  --     return (fvars, [mvarId])
+  --   withMainContext do
+  --     for stx in ids, fvar in fvars do
+  --       Term.addLocalVarInfo stx (mkFVar fvar)
+  | _ => throwUnsupportedSyntax

server/test/let_intros.lean

@@ -0,0 +1,17 @@
+import GameServer.Tactic.LetIntros
+
+set_option linter.unusedVariables false in
+
+example (f : Nat) :
+    let f := fun x ↦ x + 1
+    let g : Nat → Nat := fun y ↦ y
+    ∀ x : Nat, x ≤ f x := by
+  let_intros
+  /-
+  f✝ : Nat
+  f : Nat → Nat := fun x => x + 1
+  g : Nat → Nat := fun y => y
+  ⊢ ∀ (x : Nat), x ≤ f x
+  -/
+  intro x
+  exact Nat.le_succ x