add preample tactic sequence to Statement

server/GameServer/Commands.lean

@@ -341,11 +341,36 @@ elab "LemmaTab"  category:str : command => do
 
 /-! # Exercise Statement -/
 
+/-- You can write `Statement add_comm (preample := simp) .... := by` which
+will automatically execute the given tactic sequence before the exercise
+is handed to the player.
+
+A common example is to use
+
+```
+refine { carrier := M, ?.. }
+```
+
+in exercises, where the statement is a structure, to fill in all the data fields.
+
+For example in "Show that all matrices with first column zero form a submodule",
+you could provide the set of all these matrices as `carrier` and the player will receive
+all the `Prop`-valued fields as goals.
+-/
+syntax preampleArg := atomic(" (preample := " withoutPosition(tacticSeq) ")")
+
 /-- Define the statement of the current level. -/
 elab doc:docComment ? attrs:Parser.Term.attributes ?
-    "Statement" statementName:ident ? sig:declSig val:declVal : command => do
+    "Statement" statementName:ident ? preample:preampleArg ? sig:declSig val:declVal : command => do
   let lvlIdx ← getCurLevelIdx
 
+  -- add an optional tactic sequence that the engine executes before the game starts
+  let preampleSeq : TSyntax `Lean.Parser.Tactic.tacticSeq ← match preample with
+  | none => `(Parser.Tactic.tacticSeq|skip)
+  | some x => match x with
+    | `(preampleArg| (preample := $tac)) => pure tac
+    | _ => `(Parser.Tactic.tacticSeq|skip)
+
   let docContent ← parseDocComment doc
   let docContent ← match docContent with
   | none => pure none
@@ -383,17 +408,17 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
       -- 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 := by {let_intros; $(⟨tacticStx⟩)})
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨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 := by {let_intros; $(⟨tacticStx⟩)})
+      let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $name $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨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 := by {let_intros; $(⟨tacticStx⟩)})
+    let thmStatement ← `(command| $[$doc]? $[$attrs:attributes]? theorem $defaultDeclName $sig := by {let_intros; $(⟨preampleSeq⟩); $(⟨tacticStx⟩)})
     elabCommand thmStatement
 
   let msgs := (← get).messages
@@ -468,6 +493,7 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
   modifyCurLevel fun level => pure { level with
     module := env.header.mainModule
     goal := sig,
+    preample := preampleSeq
     scope := scope,
     descrText := docContent
     statementName := match statementName with
@@ -477,7 +503,8 @@ elab doc:docComment ? attrs:Parser.Term.attributes ?
     hints := hints
     tactics := {level.tactics with used := usedInventory.tactics.toArray}
     definitions := {level.definitions with used := usedInventory.definitions.toArray}
-    lemmas := {level.lemmas with used := usedInventory.lemmas.toArray} }
+    lemmas := {level.lemmas with used := usedInventory.lemmas.toArray}
+    }
 
 /-! # Hints -/
 

server/GameServer/EnvExtensions.lean

@@ -265,6 +265,8 @@ structure GameLevel where
   template: Option String := none
   /-- The image for this level. -/
   image : String := default
+  /-- A sequence of tactics the game automatically executes before the first step. -/
+  preample : TSyntax `Lean.Parser.Tactic.tacticSeq := default
 deriving Inhabited, Repr
 
 /-- Json-encodable version of `GameLevel`

server/GameServer/FileWorker.lean

@@ -263,7 +263,7 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           -- 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 {let_intros; $(⟨tacticStx⟩)} )
+            theorem the_theorem $(level.goal) := by {let_intros; $(⟨level.preample⟩); $(⟨tacticStx⟩)} )
           Elab.Command.elabCommandTopLevel cmdStx)
       cmdCtx cmdStateRef
   let postNew := (← tacticCacheNew.get).post

server/test/test_statement.lean

@@ -73,10 +73,13 @@ theorem xy (n : Nat) : n + 0 = n := by
 
 /-- Doc comment -/
 @[simp]
-Statement My.add_comm (n m : Nat) : n + m = m + n := by
+Statement My.add_assoc (n m x : Nat) : (m + n) + x = m + (n + x) := by
-  rw [Nat.add_comm]
+  rw [Nat.add_assoc]
 
-example (n m : Nat) : n + m = m + n := by
+example (n m : Nat) : (m + n) + x = m + (n + x) := by
   simp
 
-#check My.add_comm
+#check My.add_assoc
+
+Statement My.add_comm (preample := simp [add_comm m n]) (n m : Nat) : n + (m + 0) = m + n := by
+  rw [Nat.add_comm]