From 9bc0a3de46737442e38379ec0bbb629f72af6b8f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 15 Mar 2024 17:06:43 +0100 Subject: [PATCH] add let_intros for better experience with levels about functions --- doc/create_game.md | 25 +++++++++- doc/hints.md | 2 + server/GameServer/Commands.lean | 19 +++++--- server/GameServer/FileWorker.lean | 6 ++- server/GameServer/Tactic/LetIntros.lean | 65 +++++++++++++++++++++++++ server/test/let_intros.lean | 17 +++++++ 6 files changed, 123 insertions(+), 11 deletions(-) create mode 100644 server/GameServer/Tactic/LetIntros.lean create mode 100644 server/test/let_intros.lean diff --git a/doc/create_game.md b/doc/create_game.md index 0fc347f..ddea86b 100644 --- a/doc/create_game.md +++ b/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: diff --git a/doc/hints.md b/doc/hints.md index d050505..170031d 100644 --- a/doc/hints.md +++ b/doc/hints.md @@ -117,3 +117,5 @@ $$ \\end{CD} $$ ``` + +See https://www.jmilne.org/not/Mamscd.pdf diff --git a/server/GameServer/Commands.lean b/server/GameServer/Commands.lean index b6aeb41..6909bd1 100644 --- a/server/GameServer/Commands.lean +++ b/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 diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index e65fa7c..ccecae9 100644 --- a/server/GameServer/FileWorker.lean +++ b/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 diff --git a/server/GameServer/Tactic/LetIntros.lean b/server/GameServer/Tactic/LetIntros.lean new file mode 100644 index 0000000..914e38b --- /dev/null +++ b/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 diff --git a/server/test/let_intros.lean b/server/test/let_intros.lean new file mode 100644 index 0000000..6de61da --- /dev/null +++ b/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