+}
function useLevelEditor(worldId: string, levelId: number, codeviewRef, initialCode, onDidChangeContent) {
diff --git a/client/src/components/inventory.css b/client/src/components/inventory.css
index 4f89ca2..07bdb9c 100644
--- a/client/src/components/inventory.css
+++ b/client/src/components/inventory.css
@@ -8,12 +8,6 @@
margin-bottom: .2em;
}
-
-.inventory h2.doc {
- margin-top: 1.5em;
- font-weight: 900;
-}
-
.inventory-list {
display: flex;
gap: .5em;
@@ -58,3 +52,15 @@
color: black;
border-bottom: 0.3em solid var(--clr-primary);
}
+
+
+.doc-panel {
+ padding: 0 1em;
+}
+
+.doc-panel h2 {
+ font-size: 1.5em;
+ margin-top: 1em;
+ margin-bottom: .2em;
+ font-weight: 900;
+}
diff --git a/client/src/components/level.css b/client/src/components/level.css
index b95cf9c..94fce56 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -24,17 +24,11 @@
background-image: url('data:image/png;base64,iVBORw0KGgoAAAANSUhEUgAAAAUAAAAeCAYAAADkftS9AAAAIklEQVQoU2M4c+bMfxAGAgYYmwGrIIiDjrELjpo5aiZeMwF+yNnOs5KSvgAAAABJRU5ErkJggg==');
}
-.side-panel, .exercise-panel, .doc-panel {
+.inventory-panel, .exercise-panel, .doc-panel {
height: 100%;
overflow: auto;
}
-.side-panel {
- display: flex;
- flex-flow: column;
- background-color: #e9f2fb;
-}
-
.introduction-panel, .infoview, .exercise, .conclusion {
padding-top: 1em;
padding-left: 1em;
diff --git a/server/build.sh b/server/build.sh
old mode 100755
new mode 100644
diff --git a/server/leanserver/GameServer/AbstractCtx.lean b/server/leanserver/GameServer/AbstractCtx.lean
new file mode 100644
index 0000000..96d215c
--- /dev/null
+++ b/server/leanserver/GameServer/AbstractCtx.lean
@@ -0,0 +1,26 @@
+import Lean
+
+section AbstractCtx
+open Lean
+open Meta
+
+structure AbstractCtxResult :=
+ (abstractMVarsResult : AbstractMVarsResult)
+
+/-- Abstract LCtx and MCtx to transport an expression into different contexts -/
+def abstractCtx (goal : MVarId) : MetaM AbstractCtxResult := do
+ let goalDecl ← goal.getDecl
+ let fvars := goalDecl.lctx.decls.toArray.filterMap id |> Array.map (mkFVar ·.fvarId)
+ let goal ← mkLambdaFVars (usedLetOnly := false) fvars goalDecl.type
+ let goal ← abstractMVars goal
+ return {
+ abstractMVarsResult := goal
+ }
+
+def openAbstractCtxResult (res : AbstractCtxResult) (k : Array Expr → Expr → MetaM α) : MetaM α := do
+ let (mvars, binderInfo, expr) ← openAbstractMVarsResult res.abstractMVarsResult
+ lambdaLetTelescope (← instantiateMVars expr) k
+ -- TODO: Unfornately, lambdaLetTelescope does not allow us to provide the number of arguments.
+ -- If the goal is a function, this will not work.
+
+end AbstractCtx
diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index b34cda7..fd1044c 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -1,6 +1,7 @@
import Lean
import GameServer.EnvExtensions
+import GameServer.StrInterpolation
open Lean Meta
@@ -61,36 +62,117 @@ partial def reprintCore : Syntax → Option Format
def reprint (stx : Syntax) : Format :=
reprintCore stx |>.getD ""
--- macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
+syntax hintArg := " (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")"
+
+/-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
+see hints. The tactic does not affect the goal state. -/
+elab "Hint" args:hintArg* msg:Lean.Parser.interpolatedStrNoIndent : tactic => do
+ let mut strict := false
+ let mut hidden := false
+
+ for arg in args do
+ match arg with
+ | `(hintArg| (strict := true)) => strict := true
+ | `(hintArg| (strict := false)) => strict := false
+ | `(hintArg| (hidden := true)) => hidden := true
+ | `(hintArg| (hidden := false)) => hidden := false
+ | _ => throwUnsupportedSyntax
+
+ let goal ← Tactic.getMainGoal
+ goal.withContext do
+ -- We construct an expression that can produce the hint text. The difficulty is that we
+ -- want the text to possibly contain quotation of the local variables which might have been
+ -- named differently by the player.
+ let varsName := `vars
+ let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
+ let mut text ← expandInterpolatedStr ⟨msg.raw⟩ (← `(MessageData)) (← `(toMessageData))
+ let goalDecl ← goal.getDecl
+ let decls := goalDecl.lctx.decls.toArray.filterMap id
+ for i in [:decls.size] do
+ text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text)
+ return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize text none
+ let textmvar ← mkFreshExprMVar none
+ guard $ ← isDefEq textmvar text -- Store the text in a mvar.
+ -- The information about the hint is logged as a message using `logInfo` to transfer it to the
+ -- `Statement` command defined below:
+ logInfo $
+ .tagged `Hint $
+ .nest (if strict then 1 else 0) $
+ .nest (if hidden then 1 else 0) $
+ .compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)
+
+/-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
+proof state. We use it to define Hints for alternative proof methods or dead ends. -/
+elab "Branch" t:tacticSeq : tactic => do
+ let b ← saveState
+ Tactic.evalTactic t
+ let msgs ← Core.getMessageLog
+ b.restore
+ Core.setMessageLog msgs
/-- Define the statement of the current level.
Arguments:
- ident: (Optional) The name of the statemtent.
-- descr: The human-readable version of the lemma as string. Accepts Markdown and Mathjax.
+- descr: (Optional) The human-readable version of the lemma as string. Accepts Markdown and Mathjax.
-/
-elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : command => do
+elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
let lvlIdx ← getCurLevelIdx
let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
("level" ++ toString lvlIdx : String)
+
+ -- save the messages before evaluation of the proof
+ let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
+
let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
-- let thmStatement' ← match statementName with
-- | none => `(lemma $(mkIdent "XX") $sig $val) -- TODO: Make it into an `example`
-- | some name => `(lemma $name $sig $val)
+ elabCommand thmStatement
+
+ let msgs := (← get).messages
+
+ let mut hints := #[]
+ let mut nonHintMsgs := #[]
+ for msg in msgs.msgs do
+ -- Look for messages produced by the `Hint` tactic. They are used to pass information about the
+ -- intermediate goal state
+ if let MessageData.withNamingContext _ $ MessageData.withContext ctx $
+ .tagged `Hint $
+ .nest strict $
+ .nest hidden $
+ .compose (.ofGoal text) (.ofGoal goal) := msg.data then
+ let hint ← liftTermElabM $ withMCtx ctx.mctx $ withLCtx ctx.lctx #[] $ withEnv ctx.env do
+ return {
+ goal := ← abstractCtx goal
+ text := ← instantiateMVars (mkMVar text)
+ strict := strict == 1
+ hidden := hidden == 1
+ }
+ hints := hints.push hint
+ else
+ nonHintMsgs := nonHintMsgs.push msg
+
+ -- restore saved messages and non-hint messages
+ modify fun st => { st with
+ messages := initMsgs ++ ⟨nonHintMsgs.toPArray'⟩
+ }
let scope ← getScope
let env ← getEnv
- elabCommand thmStatement
modifyCurLevel fun level => pure {level with
module := env.header.mainModule
goal := sig,
scope := scope,
- descrText := descr.getString,
+ descrText := match descr with
+ | none => ""
+ | some s => s.getString
descrFormat := match statementName with
| none => "example " ++ (toString <| reprint sig.raw) ++ " := by"
| some name => (Format.join ["lemma ", reprint name.raw, " ", reprint sig.raw, " := by"]).pretty 10 -- "lemma " ++ (toString <| reprint name.raw) ++ " " ++ (Format.pretty (reprint sig.raw) 40) ++ " := by"
+ hints := hints
} -- Format.pretty <| format thmStatement.raw }
/-- Define the conclusion of the current game or current level if some
@@ -138,38 +220,40 @@ def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
| (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
| [] => return s
-def elabHint (hidden : Bool) (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder)
- (goal : TSyntax `term) (msg : TSyntax `interpolatedStrKind) :=
-liftTermElabM do withOptions (fun options => options.setBool `linter.unusedVariables false) do
- let (g, decls) ← elabBinders binders fun xs => do
- let g ← mkForallFVars xs $ ← elabTermAndSynthesize goal none
- synthesizeSyntheticMVarsNoPostponing false
- return (← instantiateMVars g, ← xs.mapM (fun x => x.fvarId!.getDecl))
- let varsName := `vars
- let msg ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
- let mut msg ← `(m! $msg)
- for i in [:decls.size] do
- msg ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $msg)
- return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize msg none
-
- if g.hasMVar then throwError m!"Goal contains metavariables: {g}"
-
- modifyCurLevel fun level => pure {level with hints := level.hints.push {
- goal := g,
- intros := decls.size,
- hidden := hidden,
- text := msg }}
+-- def elabHint (hidden : Bool) (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder)
+-- (goal : TSyntax `term) (msg : TSyntax `interpolatedStrKind) :=
+-- liftTermElabM do withOptions (fun options => options.setBool `linter.unusedVariables false) do
+-- let (g, decls) ← elabBinders binders fun xs => do
+-- let g ← mkForallFVars xs $ ← elabTermAndSynthesize goal none
+-- synthesizeSyntheticMVarsNoPostponing false
+-- return (← instantiateMVars g, ← xs.mapM (fun x => x.fvarId!.getDecl))
+-- let varsName := `vars
+-- let msg ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
+-- let mut msg ← `(m! $msg)
+-- for i in [:decls.size] do
+-- msg ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $msg)
+-- return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize msg none
+
+-- if g.hasMVar then throwError m!"Goal contains metavariables: {g}"
+
+ -- modifyCurLevel fun level => pure {level with hints := level.hints.push {
+ -- goal := g,
+ -- intros := decls.size,
+ -- hidden := hidden,
+ -- text := msg }}
/-- Declare a hint. This version doesn't prevent the unused linter variable from running. -/
local elab "Hint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command =>
- elabHint false binders goal msg
+ -- elabHint false binders goal msg
+ pure ()
/--
Declare a hint. This version doesn't prevent the unused linter variable from running.
A hidden hint is only displayed if explicitly requested by the user.
-/
local elab "HiddenHint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
- elabHint true binders goal msg
+ -- elabHint true binders goal msg
+ pure ()
/-- Declare a hint in reaction to a given tactic state in the current level. -/
macro "Hint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
@@ -201,19 +285,19 @@ elab "TacticDoc" name:ident content:str : command =>
content := content.getString })
/-- Declare tactics that are introduced by this level. -/
-elab "NewTactics" args:ident* : command => do
+elab "NewTactic" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Tactic name
modifyCurLevel fun level => pure {level with tactics := {level.tactics with new := names}}
/-- Declare tactics that are temporarily disabled in this level -/
-elab "DisabledTactics" args:ident* : command => do
+elab "DisabledTactic" args:ident* : command => do
let names := args.map (·.getId)
- for name in names do checkInventoryDoc .Tactic name
+ -- for name in names do checkInventoryDoc .Tactic name
modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := names}}
/-- Temporarily disable all tactics except the ones declared here -/
-elab "OnlyTactics" args:ident* : command => do
+elab "OnlyTactic" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Tactic name
modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := names}}
@@ -231,19 +315,19 @@ elab "DefinitionDoc" name:ident content:str : command =>
content := content.getString })
/-- Declare definitions that are introduced by this level. -/
-elab "NewDefinitions" args:ident* : command => do
+elab "NewDefinition" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Definition name
modifyCurLevel fun level => pure {level with definitions := {level.definitions with new := names}}
/-- Declare definitions that are temporarily disabled in this level -/
-elab "DisabledDefinitions" args:ident* : command => do
+elab "DisabledDefinition" args:ident* : command => do
let names := args.map (·.getId)
- for name in names do checkInventoryDoc .Definition name
+ -- for name in names do checkInventoryDoc .Definition name
modifyCurLevel fun level => pure {level with definitions := {level.definitions with disabled := names}}
/-- Temporarily disable all definitions except the ones declared here -/
-elab "OnlyDefinitions" args:ident* : command => do
+elab "OnlyDefinition" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Definition name
modifyCurLevel fun level => pure {level with definitions := {level.definitions with only := names}}
@@ -264,19 +348,19 @@ elab "LemmaDoc" name:ident "as" userName:ident "in" category:str content:str : c
content := content.getString })
/-- Declare lemmas that are introduced by this level. -/
-elab "NewLemmas" args:ident* : command => do
+elab "NewLemma" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Lemma name
modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with new := names}}
/-- Declare lemmas that are temporarily disabled in this level -/
-elab "DisabledLemmas" args:ident* : command => do
+elab "DisabledLemma" args:ident* : command => do
let names := args.map (·.getId)
- for name in names do checkInventoryDoc .Lemma name
+ -- for name in names do checkInventoryDoc .Lemma name
modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with disabled := names}}
/-- Temporarily disable all lemmas except the ones declared here -/
-elab "OnlyLemmas" args:ident* : command => do
+elab "OnlyLemma" args:ident* : command => do
let names := args.map (·.getId)
for name in names do checkInventoryDoc .Lemma name
modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with only := names}}
@@ -347,13 +431,18 @@ elab "MakeGame" : command => do
for item in (level.getInventory inventoryType).new do
let category := (← getInventoryDoc? item inventoryType).get!.category
items := items.insert item {name := item, category, locked := false, disabled := false}
+
+ let mut disabled : HashSet Name := {}
for item in (level.getInventory inventoryType).disabled do
let category := (← getInventoryDoc? item inventoryType).get!.category
- items := items.insert item {name := item, category, locked := false, disabled := true}
+ items := items.insert item {name := item, category, locked := false, disabled := false}
+ -- (we set disabled to false at first because it applies only to the current level)
+ disabled := disabled.insert item
let itemsArray := items.toArray
|>.insertionSort (fun a b => a.1.toString < b.1.toString)
|>.map (·.2)
+ |>.map (fun item => {item with disabled := disabled.contains item.name})
modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
return level.setComputedInventory inventoryType itemsArray
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index 71500af..95a2976 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -1,5 +1,6 @@
import Lean
import GameServer.Graph
+import GameServer.AbstractCtx
/-! # Environment extensions
@@ -16,15 +17,17 @@ open Lean
A hint to help the user with a specific goal state
-/
structure GoalHintEntry where
- goal : Expr
- /-- Number of variables to intro in the beginning of goal -/
- intros : Nat
+ goal : AbstractCtxResult
/-- Text of the hint as an expression of type `Array Expr → MessageData` -/
text : Expr
- /-- If true, then hint should be hidden by default -/
+ /-- If true, then hint should be hidden and only be shown on player's request -/
hidden : Bool := false
- deriving Repr
+ /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
+ strict : Bool := false
+instance : Repr GoalHintEntry := {
+ reprPrec := fun a n => reprPrec a.text n
+}
/-! ## Tactic/Definition/Lemma documentation -/
diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean
index 9176aca..32f3931 100644
--- a/server/leanserver/GameServer/RpcHandlers.lean
+++ b/server/leanserver/GameServer/RpcHandlers.lean
@@ -25,26 +25,83 @@ def getLevelByFileName? [Monad m] [MonadEnv m] (fileName : String) : m (Option G
| return none
return ← getLevel? levelId
-/-- Check if each meta variable in `declMvars` has a matching fvar in `declFvars` -/
-def matchDecls (declMvars : Array Expr) (declFvars : Array Expr) : MetaM Bool := do
+structure FVarBijection :=
+ (forward : HashMap FVarId FVarId)
+ (backward : HashMap FVarId FVarId)
+
+instance : EmptyCollection FVarBijection := ⟨{},{}⟩
+
+def FVarBijection.insert (bij : FVarBijection) (a b : FVarId) : FVarBijection :=
+ ⟨bij.forward.insert a b, bij.backward.insert b a⟩
+
+def FVarBijection.insert? (bij : FVarBijection) (a b : FVarId) : Option FVarBijection :=
+ let a' := bij.forward.find? a
+ let b' := bij.forward.find? b
+ if (a' == none || a' == some b) && (b' == none || b' == some a)
+ then some $ bij.insert a b
+ else none
+
+/-- Checks if `pattern` and `e` are equal up to FVar identities. -/
+partial def matchExpr (pattern : Expr) (e : Expr) (bij : FVarBijection := {}) : Option FVarBijection :=
+ match pattern, e with
+ | .bvar i1, .bvar i2 => if i1 == i2 then bij else none
+ | .fvar i1, .fvar i2 => bij.insert? i1 i2
+ | .mvar _, .mvar _ => bij
+ | .sort u1, .sort u2 => bij -- TODO?
+ | .const n1 ls1, .const n2 ls2 =>
+ if n1 == n2 then bij else none -- && (← (ls1.zip ls2).allM fun (l1, l2) => Meta.isLevelDefEq l1 l2)
+ | .app f1 a1, .app f2 a2 =>
+ some bij
+ |> (Option.bind · (fun bij => matchExpr f1 f2 bij))
+ |> (Option.bind · (fun bij => matchExpr a1 a2 bij))
+ | .lam _ t1 b1 _, .lam _ t2 b2 _ =>
+ some bij
+ |> (Option.bind · (fun bij => matchExpr t1 t2 bij))
+ |> (Option.bind · (fun bij => matchExpr b1 b2 bij))
+ | .forallE _ t1 b1 _, .forallE _ t2 b2 _ =>
+ some bij
+ |> (Option.bind · (fun bij => matchExpr t1 t2 bij))
+ |> (Option.bind · (fun bij => matchExpr b1 b2 bij))
+ | .letE _ t1 v1 b1 _, .letE _ t2 v2 b2 _ =>
+ some bij
+ |> (Option.bind · (fun bij => matchExpr t1 t2 bij))
+ |> (Option.bind · (fun bij => matchExpr v1 v2 bij))
+ |> (Option.bind · (fun bij => matchExpr b1 b2 bij))
+ | .lit l1, .lit l2 =>
+ if l1 == l2 then bij else none
+ | .proj i1 n1 e1, .proj i2 n2 e2 =>
+ if i1 == i2 && n1 == n2 then matchExpr e1 e2 bij else none
+ -- ignore mdata:
+ | .mdata _ pattern', _ =>
+ matchExpr pattern' e bij
+ | _, .mdata _ e' =>
+ matchExpr pattern e' bij
+ | _, _ => none
+
+/-- Check if each fvar in `patterns` has a matching fvar in `fvars` -/
+def matchDecls (patterns : Array Expr) (fvars : Array Expr) (strict := true) (initBij : FVarBijection := {}) : MetaM Bool := do
-- We iterate through the array backwards hoping that this will find us faster results
-- TODO: implement backtracking
- let mut usedFvars := (List.replicate declFvars.size false).toArray
- -- `usedFvars` keeps track of the fvars that were already used to match an mvar.
- for i in [:declMvars.size] do
- let declMvar := declMvars[declMvars.size - i - 1]!
- let mut found := false
- for j in [:declFvars.size] do
- let declFvar := declFvars[declFvars.size - j - 1]!
- let usedFvar := usedFvars[declFvars.size - j - 1]!
- if ¬ usedFvar then
- if ← isDefEq declMvar declFvar then
- usedFvars := usedFvars.set! (declFvars.size - j - 1) true
- found := true
- break
- else
+ let mut bij := initBij
+ for i in [:patterns.size] do
+ let pattern := patterns[patterns.size - i - 1]!
+ if bij.forward.contains pattern.fvarId! then
+ continue
+ for j in [:fvars.size] do
+ let fvar := fvars[fvars.size - j - 1]!
+ if bij.backward.contains fvar.fvarId! then
continue
- if ¬ found then return false
+
+ if let some bij' := matchExpr
+ (← instantiateMVars $ ← inferType pattern)
+ (← instantiateMVars $ ← inferType fvar) bij then
+ -- usedFvars := usedFvars.set! (fvars.size - j - 1) true
+ bij := bij'.insert pattern.fvarId! fvar.fvarId!
+ break
+ if ! bij.forward.contains pattern.fvarId! then return false
+
+ if strict then
+ return fvars.all (fun fvar => bij.backward.contains fvar.fvarId!)
return true
unsafe def evalHintMessageUnsafe : Expr → MetaM (Array Expr → MessageData) :=
@@ -62,19 +119,19 @@ def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array
let some level ← getLevelByFileName? doc.meta.mkInputContext.fileName
| throwError "Level not found: {doc.meta.mkInputContext.fileName}"
let hints ← level.hints.filterMapM fun hint => do
- let (declMvars, binderInfo, hintGoal) ← forallMetaBoundedTelescope hint.goal hint.intros
- -- TODO: Protect mvars in the type of `goal` to be instantiated?
- if ← isDefEq hintGoal (← inferType $ mkMVar goal)
- then
- let lctx ← getLCtx -- Local context of the `goal`
- if ← matchDecls declMvars lctx.getFVars
+ openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
+ if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
then
- let text := (← evalHintMessage hint.text) declMvars
- let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
- let text ← (MessageData.withContext ctx text).toString
- return some { text := text, hidden := hint.hidden }
- else return none
- else return none
+ let lctx := (← goal.getDecl).lctx
+ if ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+ then
+ let text := (← evalHintMessage hint.text) hintFVars
+ let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+ let text ← (MessageData.withContext ctx text).toString
+ return some { text := text, hidden := hint.hidden }
+ else return none
+ else
+ return none
return hints
open RequestM in
diff --git a/server/leanserver/GameServer/StrInterpolation.lean b/server/leanserver/GameServer/StrInterpolation.lean
new file mode 100644
index 0000000..db08b36
--- /dev/null
+++ b/server/leanserver/GameServer/StrInterpolation.lean
@@ -0,0 +1,149 @@
+/- Adapted from `Lean.Parser.StrInterpolation`
+
+This version of interpolated strings deletes any initial spaces from
+new lines. This keeps Markdown from interpreting indented material
+as quotes.
+-/
+import Lean
+namespace Lean.Parser
+
+/-- Push `(Syntax.node tk )` onto syntax stack if parse was successful. -/
+def mkNodeTokenNoWs (n : SyntaxNodeKind) (startPos : String.Pos) : ParserFn := fun c s => Id.run do
+ if s.hasError then
+ return s
+ let input := c.input
+ let stopPos := s.pos
+ let leading := mkEmptySubstringAt input startPos
+ let val := input.extract startPos stopPos
+ let wsStopPos := s.pos
+ let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring }
+ let info := SourceInfo.original leading startPos trailing stopPos
+ s.pushSyntax (Syntax.mkLit n val info)
+
+partial def interpolatedStrNoIndentFn (p : ParserFn) : ParserFn := fun c s =>
+ let input := c.input
+ let stackSize := s.stackSize
+ let rec parse (startPos : String.Pos) (c : ParserContext) (s : ParserState) : ParserState :=
+ let i := s.pos
+ if input.atEnd i then
+ let s := s.pushSyntax Syntax.missing
+ let s := s.mkNode interpolatedStrKind stackSize
+ s.setError "unterminated string literal"
+ else
+ let curr := input.get i
+ let s := s.setPos (input.next i)
+ if curr == '\"' then
+ let s := mkNodeToken interpolatedStrLitKind startPos c s
+ s.mkNode interpolatedStrKind stackSize
+ else if curr == '\n' then
+ -- Ignore initial spaces on a new line
+ let s := mkNodeTokenNoWs interpolatedStrLitKind startPos c s
+ let s := takeWhileFn (fun curr => curr == ' ') c s
+ parse s.pos c s
+ else if curr == '\\' then
+ andthenFn (quotedCharCoreFn isQuotableCharForStrInterpolant) (parse startPos) c s
+ else if curr == '{' then
+ let s := mkNodeToken interpolatedStrLitKind startPos c s
+ let s := p c s
+ if s.hasError then s
+ else
+ let i := s.pos
+ let curr := input.get i
+ if curr == '}' then
+ let s := s.setPos (input.next i)
+ parse i c s
+ else
+ let s := s.pushSyntax Syntax.missing
+ let s := s.mkNode interpolatedStrKind stackSize
+ s.setError "'}'"
+ else
+ parse startPos c s
+ let startPos := s.pos
+ if input.atEnd startPos then
+ s.mkEOIError
+ else
+ let curr := input.get s.pos;
+ if curr != '\"' then
+ s.mkError "interpolated string"
+ else
+ let s := s.next input startPos
+ parse startPos c s
+
+@[inline] def interpolatedStrNoIndentNoAntiquot (p : Parser) : Parser := {
+ fn := interpolatedStrNoIndentFn (withoutPosition p).fn,
+ info := mkAtomicInfo "interpolatedStrNoIndent"
+}
+
+def interpolatedStrNoIndent : Parser :=
+ withAntiquot (mkAntiquot "interpolatedStrNoIndent" interpolatedStrKind) $ interpolatedStrNoIndentNoAntiquot termParser
+
+open Lean.PrettyPrinter
+open Lean.PrettyPrinter.Parenthesizer
+open Lean.PrettyPrinter.Formatter
+
+@[combinator_parenthesizer interpolatedStrNoIndent]
+def interpolatedStrNoIndent.parenthesizer := interpolatedStr.parenthesizer
+
+@[combinator_formatter interpolatedStrNoIndent]
+def interpolatedStrNoIndent.formatter := interpolatedStr.formatter
+
+end Lean.Parser
+
+
+/- Adapted from Init/Meta -/
+open Lean
+
+private def decodeInterpStrQuotedChar (s : String) (i : String.Pos) : Option (Char × String.Pos) := do
+ match Syntax.decodeQuotedChar s i with
+ | some r => some r
+ | none =>
+ let c := s.get i
+ let i := s.next i
+ if c == '{' then pure ('{', i)
+ else none
+
+private partial def decodeInterpStrLit (s : String) : Option String :=
+ let rec loop (i : String.Pos) (acc : String) : Option String :=
+ let c := s.get i
+ let i := s.next i
+ if c == '\"' || c == '{' then
+ pure acc
+ else if c == '\n' then
+ pure (acc.push c)
+ else if s.atEnd i then
+ pure acc
+ else if c == '\\' then do
+ let (c, i) ← decodeInterpStrQuotedChar s i
+ loop i (acc.push c)
+ else
+ loop i (acc.push c)
+ let c := s.get 0
+ if c == '\"' || c == '}' then
+ loop ⟨1⟩ ""
+ else
+ loop ⟨0⟩ ""
+partial def isInterpolatedStrLit? (stx : Syntax) : Option String :=
+ match Syntax.isLit? interpolatedStrLitKind stx with
+ | none => none
+ | some val => decodeInterpStrLit val
+
+open Elab
+
+def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → TermElabM Syntax) (mkElem : Syntax → TermElabM Syntax) : TermElabM Syntax := do
+ let mut i := 0
+ let mut result := Syntax.missing
+ for elem in chunks do
+ let elem ← match isInterpolatedStrLit? elem with
+ | none => mkElem elem
+ | some str => mkElem (Syntax.mkStrLit str)
+ if i == 0 then
+ result := elem
+ else
+ result ← mkAppend result elem
+ i := i+1
+ return result
+
+open TSyntax.Compat in
+def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (toTypeFn : Term) : TermElabM Term := do
+ let r ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a))
+ `(($r : $type))
diff --git a/server/leanserver/lean-toolchain b/server/leanserver/lean-toolchain
index 5bf01da..7f0fd43 100644
--- a/server/leanserver/lean-toolchain
+++ b/server/leanserver/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-10
+leanprover/lean4:nightly-2023-03-09
diff --git a/server/testgame/TestGame.lean b/server/testgame/TestGame.lean
index a6d5646..f48f3f7 100644
--- a/server/testgame/TestGame.lean
+++ b/server/testgame/TestGame.lean
@@ -6,7 +6,7 @@ import TestGame.Levels.Predicate
import TestGame.Levels.Contradiction
import TestGame.Levels.Prime
import TestGame.Levels.Sum
-import TestGame.Levels.Induction
+-- import TestGame.Levels.Induction
import TestGame.Levels.Numbers
import TestGame.Levels.Inequality
@@ -34,8 +34,9 @@ Path Proposition → Implication → Predicate
Path Predicate → Contradiction → Sum → LeanStuff
Path LeanStuff → SetTheory → SetTheory2 → SetFunction
-Path Predicate → Prime → Induction
-Path Sum → Inequality → Induction
+Path Predicate → Prime -- → Induction
+Path Sum → Inequality -- → Induction
+Path Inequality → Function
Path SetTheory2 → Numbers
Path Module → Basis → Module2
diff --git a/server/testgame/TestGame/LemmaDocs.lean b/server/testgame/TestGame/LemmaDocs.lean
index 865cc85..3898ba9 100644
--- a/server/testgame/TestGame/LemmaDocs.lean
+++ b/server/testgame/TestGame/LemmaDocs.lean
@@ -75,40 +75,53 @@ Die Definition kann man mit `unfold odd at *` einsetzen.
DefinitionDoc Injective
"
-`Injective f` ist als
+`Injective f` ist definiert als
```
-∀ {a b : U}, a < b → f a < f b
+∀ a b, f a = f b → a = b
```
definiert.
"
DefinitionDoc Surjective
"
+`Surjective f` ist definiert als
+
+```
+∀ a, (∃ b, f a = b)
+```
"
DefinitionDoc Bijective
"
"
+DefinitionDoc LeftInverse
+"
+"
+
+DefinitionDoc RightInverse
+"
+"
+
DefinitionDoc StrictMono
"
-`StrictMono`
+`StrictMono f` ist definiert als
```
-∀ {a b : U}, f a f b → a = b
+∀ a b, a < b → f a < f b
```
"
-LemmaDoc not_odd as not_odd in "Nat"
-"`¬ (odd n) ↔ even n`"
+LemmaDoc even_iff_not_odd as even_iff_not_odd in "Nat"
+"`Even n ↔ ¬ (Odd n)`"
-LemmaDoc not_even as not_even in "Nat"
-"`¬ (even n) ↔ odd n`"
+LemmaDoc odd_iff_not_even as odd_iff_not_even in "Nat"
+"`Odd n ↔ ¬ (Even n)`"
LemmaDoc even_square as even_square in "Nat"
-"`∀ (n : ℕ), even n → even (n ^ 2)`"
+"`∀ (n : ℕ), Even n → Even (n ^ 2)`"
@@ -178,3 +191,16 @@ LemmaDoc StrictMono.add as StrictMono.add in "Function"
LemmaDoc Odd.strictMono_pow as Odd.strictMono_pow in "Function"
""
+
+LemmaDoc Exists.choose as Exists.choose in "Function"
+""
+
+LemmaDoc Exists.choose_spec as Exists.choose_spec in "Function"
+""
+LemmaDoc congrArg as congrArg in "Function"
+""
+LemmaDoc congrFun as congrFun in "Function"
+""
+
+LemmaDoc Iff.symm as Iff.symm in "Logic"
+""
diff --git a/server/testgame/TestGame/Levels/Contradiction.lean b/server/testgame/TestGame/Levels/Contradiction.lean
index 70e10b5..5805bb1 100644
--- a/server/testgame/TestGame/Levels/Contradiction.lean
+++ b/server/testgame/TestGame/Levels/Contradiction.lean
@@ -8,3 +8,9 @@ import TestGame.Levels.Contradiction.L06_Summary
Game "TestGame"
World "Contradiction"
Title "Widerspruch"
+
+Introduction "
+Ihr begebt euch auf die Suche nach *Oddeus*. Nach etwas rumfragen, kommt ihr tatsächlich an
+eine Dornenfestung und nachdem ihr erklärt habt, wer ihr seit, werdet ihr auf eine Audienz
+gebeten.
+"
diff --git a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
index d1a9c7e..e80a472 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean
@@ -15,56 +15,46 @@ Title "Have"
Introduction
"
-Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein
-Zwischenresultat beweisen, welches wir dann benützen können.
-
-Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen,
-dass man anschliessen beweisen muss.
-
-Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst
-du mit
-```
-have g : ¬ B
-apply h
-assumption
-```
-eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme,
-bevor du dann mit dem Beweis forfährst.
+**Oddeus**: Willkommen Reisende! Ich muss eingestehen ich bin in Gedanken noch
+an etwas, könnt ihr mir bei diesem widersprüchlichen Problem helfen?
"
-Statement
- "Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
- $A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
- (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
- rcases k with ⟨h₁, h₂⟩
- have h₃ : ¬ B
- apply h
- assumption
- contradiction
+-- Manchmal, wollen wir nicht am aktuellen Goal arbeiten, sondern zuerst ein
+-- Zwischenresultat beweisen, welches wir dann benützen können.
-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False =>
-" Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen.
-"
+-- Mit `have [Name] : [Aussage]` kann man ein Zwischenresultat erstellen,
+-- dass man anschliessen beweisen muss.
-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False =>
-"
-Auf Deutsch: \"Als Zwischenresultat haben wir `¬ B`.\"
+-- Wenn du zum Beispiel die Annahmen `(h : A → ¬ B)` und `(ha : A)` hast, kannst
+-- du mit
+-- ```
+-- have g : ¬ B
+-- apply h
+-- assumption
+-- ```
+-- eine neue Annahme `(g : ¬ B)` erstellen. Danach beweist du zuerst diese Annahme,
+-- bevor du dann mit dem Beweis forfährst.
-In Lean :
+Statement (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
+ Hint "**Du**: Also als erstes Teile ich wohl mal das Und (`∧`) auf."
+ rcases k with ⟨h₁, h₂⟩
+ Hint "**Du**: Aber jetzt…
-```
-have k : ¬ B
-[Beweis von k]
-```
-"
+ **Robo**: Du könntest dir ein passendes Zwischenresultat zurechtlegen, das dir hilft:
+ Mach mal `have g : ¬ B`!"
+ have g : ¬ B
+ · Hint "**Du**: Was und jetzt hab ich einfach angenommen das sei richtig?
--- example (n : ℕ) : n.succ + 2 = n + 3 := by
--- ring_nf
+ **Robo**: Ne, jetzt musst du das zuerst beweisen bevor du es dann benützen kannst."
+ Hint (hidden := true) "**Robo**: `apply` scheint passend zu sein."
+ apply h
+ assumption
+ · Hint (hidden := true) "**Du**: Und wie war das nochmals wenn zwei Annahmen sich widersprechen?
-Conclusion ""
+ **Robo**: `contradiction`."
+ contradiction
-NewTactics «have»
-DisabledTactics «suffices»
+NewTactic «have»
+DisabledTactic «suffices»
-NewDefinitions Even Odd
-NewLemmas not_even not_odd
+Conclusion "*Oddeus*: Das stimmt wohl."
diff --git a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
index 166b309..5480fe4 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean
@@ -15,52 +15,49 @@ Title "Suffices"
Introduction
"
-Die Taktik `suffices` funktioniert genau gleich wie `have`,
-vertauscht aber die beiden Beweisblöcke:
+*Oddeus*' Partner meldet sich.
-```
-suffices h : [Aussage]
-[Beweis des Goals (mithilfe von h)]
-[Beweis der Aussage h]
-```
-Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
-\"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"
+**Partner**: Ich habe letzthin was änliches gesehen, aber irgendwie verdreht.
+"
-Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
-dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
-`suffices` schöner gewesen:
+-- Die Taktik `suffices` funktioniert genau gleich wie `have`,
+-- vertauscht aber die beiden Beweisblöcke:
-"
+-- ```
+-- suffices h : [Aussage]
+-- [Beweis des Goals (mithilfe von h)]
+-- [Beweis der Aussage h]
+-- ```
+-- Auf Deutsch entspricht `suffices g : [Aussage]` dem Ausdruck
+-- \"Es genügt zu zeigen, dass `[Aussage]` wahr ist.\"
+
+-- Man kann `have` und `suffices` nach belieben vertauschen. Bevorzugt, wählt man es so,
+-- dass der erste Beweisblock der kürzere ist. Zum Beispiel wäre bei der vorigen Aufgabe
+-- `suffices` schöner gewesen:
Statement
"Angenommen, man hat eine Implikation $A \\Rightarrow \\neg B$ und weiss, dass
$A \\land B$ wahr ist. Zeige, dass dies zu einem Widerspruch führt."
- (A B : Prop) (h : A → ¬ B) (k : A ∧ B) : False := by
- rcases k with ⟨h₁, h₂⟩
- suffices k : ¬ B
+ (A B : Prop) (h : A → ¬ B) (k₁ : A) (k₂ : B) : False := by
+ Hint "**Robo**: Ich weiss was er meint! Anstatt `have` kannst du auch `suffices`
+ brauchen. Das funktioniert genau gleich, aussert dass dann die beiden Goals vertauscht sind.
+
+ **Du**: Also nach `suffices g : ¬B` muss ich dann zuerst zeigen, wie man mit `g` den Beweis
+ abschliesst bevor ich `g` beweise?
+
+ **Robo**: Genau! Verwendende `have` und `suffices` einfach nach gutdünken."
+ suffices g : ¬ B
+ Hint "**Robo**: Also hier beendest du den Beweis angenommen {g} sei wahr."
contradiction
+ Hint "**Robo**: Und hier beweist du das Zwischenresultat."
apply h
assumption
-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A ∧ B) : False =>
-" Fang mal damit an, das UND in den Annahmen mit `rcases` aufzuteilen.
-"
-
-Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False =>
-" Auf Deutsch: \"Es genügt `¬ B` zu zeigen, da dies zu einem direkten Widerspruch führt.\"
-
- In Lean :
+NewTactic «suffices»
+DisabledTactic «have»
- ```
- suffices k : ¬ B
- contradiction
- [...]
- ```
-"
+Conclusion "*Oddeus* nimmt den Brief, schaut ihn an und, rollt ihn zusammen.
-Conclusion ""
+**Oddeus**: Ich verstehe meine Schwester nie. Kommt, vielleicht könnt ihr mir helfen.
-NewTactics «suffices»
-DisabledTactics «have»
-NewDefinitions Even Odd
-NewLemmas not_even not_odd
+Und er führt euch durch seinen Rosengarten."
diff --git a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
index ebd0351..c9e4013 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean
@@ -15,41 +15,51 @@ Level 3
Title "Per Widerspruch"
Introduction
-"
-Eine sehr nützliche Beweismethode ist per Widerspruch.
-
-Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen
-sucht, und damit jegliches beweisen kann.
+"**Oddeus**: Ich verstehe *Evenine* einfach nicht. Ich will euch auch gleich zeigen,
+was sie mir letzthin geschrieben hat, aber zuerst schaut einmal unseren
+wunderschönen Absurda-Tempel an!
-Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle
-Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt.
+Damit kommt ihr vor einen sehr hohen Turm, der ausschliesslich aus Dornenranken gewachsen
+scheint.
-Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung
-steht:
+**Oddeus**: Versteht ihr, was hier über dem Eingang steht?
"
-Statement
-"Angenommen $B$ ist falsch und es gilt $A \\Rightarrow B$. Zeige, dass $A$ falsch sein
-muss."
- (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
- by_contra a
- suffices b : B
- contradiction
- apply g
- assumption
+-- Eine sehr nützliche Beweismethode ist per Widerspruch.
+-- Wir habe schon gesehen, dass `contradiction` einen Widerspruch in den Annahmen
+-- sucht, und damit jegliches beweisen kann.
-HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) : ¬ A =>
-"`by_contra h` nimmt das Gegenteil des Goal als Annahme `(h : A)` und setzt das
-Goal auf `False`."
+-- Um dorthin zu kommen, können wir `by_contra h` brauchen, welches das aktuelle
+-- Goal auf `False` setzt und die Negierung des Goals als Annahme hinzufügt.
-Hint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
-"Jetzt kannst du mit `suffices` oder `have` Fortschritt machen."
+-- Insbesondere braucht man `by_contra h` meistens, wenn im Goal eine Negierung
+-- steht:
-HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False =>
-"Zum Beispiel `suffices hb : B`."
+Statement (A B : Prop) (g : A → B) (b : ¬ B) : ¬ A := by
+ Hint "**Robo**: Ein `¬` im Goal heisst häufig, dass du einen Widerspruchsbeweis führen
+ möchtest.
+ **Du**: Und wie mach ich das? Mit `contradiction`?
+
+ **Robo**: Mit `by_contra h` fängst du einen an. Mit `contradiction` schliesst du ihn dann
+ später ab."
+ by_contra h
+ Hint "**Robo**: Jetzt hast du also eine Annahme `{h} : ¬ {A}`, und damit musst du einen
+ Widerspruch herbeileiten.
+
+ Ein Methode ist, dass du jetzt mit `suffices` sagts, zu was du denn gerne den Widerspruch
+ haben möchtest, zum Beispiel `suffices k : B`
+ "
+ suffices k : B
+ Hint "**Du**: Ah und jetzt kann ich einfach sagen dass sich die Anahmen `{B}` und `¬{B}`
+ widersprechen."
+ contradiction
+ Hint "**Robo**: Und jetzt kannst du noch das Ergebnis zeigen, das zu einem Widerspruch
+ geführt hat."
+ apply g
+ assumption
-Conclusion ""
+NewTactic by_contra
-NewTactics by_contra contradiction apply assumption
+Conclusion "**Oddeus**: Sehr gut, kommt mit hinein!"
diff --git a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
index c67c016..769a4cc 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean
@@ -16,34 +16,36 @@ Title "Per Widerspruch"
Introduction
"
-Als Übung zu `by_contra` und dem bisher gelernten, zeige folgendes Lemma welches
-wir für die Kontraposition brauchen werden:
+*Oddeus* Geht zu einem Regal mit vielen Dokumenten und beginnt zu suchen.
+
+**Oddeus**: Ich hab's gleich. Hier ist eine Notiz meiner Gelehrter, die mir
+mit solchen kryptischen Nachrichten helfen wollten.
+
+Auf dem Pergament steht das ein Lemma mit dem Namen `not_imp_not`:
"
-Statement not_imp_not
-"$A \\Rightarrow B$ ist äquivalent zu $\\neg B \\Rightarrow \\neg A$."
- (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
+Statement not_imp_not (A B : Prop) : A → B ↔ (¬ B → ¬ A) := by
+ Hint "**Du**: Ich glaube, dafür kenn ich das meiste schon."
+ Hint (hidden := true) "**Robo**: Fang doch mal mit `constructor` an."
constructor
intro h b
by_contra a
+ Hint "**Robo**: Zur Erinnerung, hier würde ich mit `suffices g : B` einen Widerspruch
+ herbeiführen."
suffices b : B
contradiction
apply h
assumption
intro h a
+ Hint "**Robo**: Hier würde ich ebenfalls einen Widerspruch anfangen."
by_contra b
+ Hint (hidden := true) "**Robo**: `suffices g : ¬ A` sieht nach einer guten Option aus."
suffices g : ¬ A
contradiction
apply h
assumption
--- TODO: Forbidden Tactics: apply, rw
--- TODO: forbidden Lemma: not_not
-
-HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) =>
-""
-
-
-Conclusion ""
+DisabledTactic rw
+DisabledLemma not_not
-NewTactics contradiction constructor intro by_contra apply assumption
+Conclusion "**Du**: Und wie hilft uns das jetzt, was steht denn in dem Brief?"
diff --git a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
index eeb5a42..6377dec 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean
@@ -14,53 +14,57 @@ Title "Kontraposition"
Introduction
"
-Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
+*Oddeus* reicht euch das Papier.
-```
-lemma not_imp_not (A B : Prop) : (A → B) ↔ (¬ B → ¬ A) := by
- [...]
-```
+**Du**: Da steht etwas über `contrapose` hier…
-Dazu gibt es die Taktik `contrapose`, welche eine Implikation im Goal
-entsprechend umdreht.
+**Oddeus**: Das ist doch klar eine Aggression uns gegenüber!
-Wir erinnern hier an die Taktik `revert h`, die aus der Annahme `h` eine Implikation
-im Goal erstellt.
+**Robo**: Wartet mal, vielleicht wollte euch eure Schwester einfach von ihren neuen
+Endeckungen zeigen. Schaut, darunter ist eine Aufgabe.
+"
-Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen.
-Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)`
-logisch equivalent sind.
+-- Ein Beweis durch Kontraposition benützt im Grunde das eben bewiesene Lemma
-Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
-"
+-- ```
+-- lemma not_imp_not (A B : Prop) : (A → B) ↔ (¬ B → ¬ A) := by
+-- [...]
+-- ```
-Statement
- "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition."
- (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
- revert h
- contrapose
- rw [not_odd]
- rw [not_odd]
- apply even_square
+-- Dazu gibt es die Taktik `contrapose`, welche eine Implikation im Goal
+-- entsprechend umdreht.
-HiddenHint (n : ℕ) (h : Odd (n ^ 2)) : Odd n =>
-"Um `contrapose` anzuwenden, brauchen wir eine Implikation `Odd (n ^ 2) → Odd n` im
-Goal. Benutze `revert h`!"
+-- Wir erinnern hier an die Taktik `revert h`, die aus der Annahme `h` eine Implikation
+-- im Goal erstellt.
-Hint (n : ℕ) : Odd (n ^ 2) → Odd n =>
-"Mit `contrapose` kann man die Implikation zu
-`¬ (Not n) → ¬ (Odd n^2)` umkehren."
+-- Im Gegensatz dazu kann man auch einen Beweis durch Kontraposition führen.
+-- Das ist kein Widerspruch, sondern benützt dass `A → B` und `(¬ B) → (¬ A)`
+-- logisch equivalent sind.
-Hint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Erinnere dich an das Lemma `not_odd`."
+-- Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden.
+open Nat
-HiddenHint (n : ℕ) : ¬Odd n → ¬Odd (n ^ 2) => "Dieses kann mit `rw` gebraucht werden."
+Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
+ Hint "**Oddeus**: Wie soll das den gehen?
-Hint (n : ℕ) : Even n → ¬Odd (n ^ 2) =>
-"rw [not_odd] muss hier zweimal angewendet werden."
+ **Robo**: `contrapose` benutzt das Lemma eurer Gelehrter, `not_imp_not`. Also es wandelt
+ ein Goal `A → B` zu `¬B → ¬A ` um.
+
+ **Du**: Aber das Goal ist doch gar keine Implikation?
+
+ **Robo**: Mit `revert {h}` kannst du die Annahme `{h}` als Implikationsannahme ins Goal
+ schieben."
+ revert h
+ Hint "*Oddeus*: Ob man jetzt wohl dieses `contrapose` benutzen kann?"
+ contrapose
+ Hint (hidden := true) "**Du**: Warte mal, jetzt kann man wohl `even_iff_not_odd` verwenden…"
+ rw [← even_iff_not_odd]
+ rw [← even_iff_not_odd]
+ Hint "**Robo**: Und den Rest hast du bei *Evenine* als Lemma gezeigt!"
+ apply even_square
-Hint (n : ℕ) : Even n → Even (n ^ 2) =>
-"Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek."
+NewTactic contrapose
+DisabledTactic by_contra
-NewTactics contrapose rw apply
-NewDefinitions Even Odd
-NewLemmas not_even not_odd even_square
+Conclusion "**Oddeus**: Ah ich sehe, die Aussage ist, dass wir das nur zusammen lösen konnten.
+Ich danke euch, darauf wäre ich nie gekommen."
diff --git a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
index abd7c15..64693b0 100644
--- a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
+++ b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean
@@ -14,63 +14,43 @@ Title "Contradiction"
Introduction
"
+**Du**: Sag mal Robo, das hätte ich aber auch als Widerspruch anstatt Kontraposition
+beweisen können?
+
+**Robo**: Klar. `contrapose` ist eine Kontraposition, `by_contra` ein Widerspruchsbeweis.
+Probiers doch einfach!
In diesem Kapitel hast du also folgende Taktiken kennengelernt:
-| | Taktik | Beispiel |
-|:------|:----------------|:-------------------------------------------------------|
-| 16 | `have` | Zwischenresultat annehmen. |
-| 17 | `suffices` | Zwischenresultat annehmen. |
-| 18 | `by_contra` | Widerspruch. (startet einen Widerspruch) |
-| *3* | `contradiction` | *(Schliesst einen Widerspruchsbeweis)* |
-| 19 | `contrapose` | Contraposition. |
-| *9* | `revert` | Nützlich um danach `contrapose` anzuwenden. |
Als Vergleich zwischen Beweisen \"per Widerspruch\"
und \"per Kontraposition\", beweise die Gleiche Aufgabe indem
du mit `by_contra` einen Widerspruch suchst.
"
-Statement
- "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch."
- (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
+open Nat
+
+Statement (n : ℕ) (h : Odd (n ^ 2)) : Odd n := by
+ Hint "**Robo**: Fang diesmal mit `by_contra g` an!"
by_contra g
+ Hint "**Robo**: Jetzt würde ich einen Widerspruch zu `Odd (n ^ 2)` führen."
+ Hint "**Robo**: Also `suffices g : ¬ Odd (n ^ 2)`."
suffices d : ¬ Odd (n ^ 2)
contradiction
- rw [not_odd] at *
+ rw [←even_iff_not_odd] at *
apply even_square
assumption
-HiddenHint (n : ℕ) (h : Odd (n^2)) : Odd n =>
-"Schreibe `by_contra h₁` um einen Beweis durch Widerspruch zu starten."
-
-Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : False =>
-"
-Am sinnvollsten ist es, hier einen Widerspruch zu `Odd (n^2)` zu suchen.
-Dafür kannst du
-```
-suffices k : ¬ Odd (n ^ 2)
-contradiction
-```
-benützen.
-"
-
-HiddenHint (n : ℕ) (g : ¬ Odd (n^2)) (h : Odd (n^2)) : False =>
-"Hier brauchst du nur `contradiction`."
+DisabledTactic contrapose revert
-Hint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : ¬ Odd (n^2) =>
-"Das Zwischenresultat `¬Odd (n^2)` muss auch bewiesen werden.
-Hier ist wieder das Lemma `not_Odd` hilfreich."
+Conclusion "**Robo**: Bravo! Hier nochmals ein Überblick, was wir jetzt alles auf diesem
+Mond gelernt haben:
-HiddenHint (n : ℕ) (g : ¬ Odd n) (h : Odd (n^2)) : Even (n^2) =>
-"Mit `rw [not_Odd] at *` kannst du im Goal und allen Annahmen gleichzeitig umschreiben."
-
-Hint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
-"Diese Aussage hast du bereits als Lemma bewiesen."
-
-HiddenHint (n: ℕ) (h : Odd (n ^ 2)) (g : Even n) : Even (n ^ 2) =>
-"Probiers mit `apply ...`"
-
-
-NewTactics contradiction by_contra rw apply assumption -- TODO: suffices, have
-NewDefinitions Even Odd
-NewLemmas not_odd not_even even_square
+| | Taktik | Beispiel |
+|:------|:----------------|:-------------------------------------------------------|
+| 177 | `have` | Zwischenresultat annehmen. |
+| 18 | `suffices` | Zwischenresultat annehmen. |
+| 19 | `by_contra` | Widerspruch. (startet einen Widerspruch) |
+| *3* | `contradiction` | *(Schliesst einen Widerspruchsbeweis)* |
+| 20 | `contrapose` | Kontraposition. |
+| *9* | `revert` | Nützlich um danach `contrapose` anzuwenden. |
+"
diff --git a/server/testgame/TestGame/Levels/Function.lean b/server/testgame/TestGame/Levels/Function.lean
index 6eb4eee..0d2770d 100644
--- a/server/testgame/TestGame/Levels/Function.lean
+++ b/server/testgame/TestGame/Levels/Function.lean
@@ -1,13 +1,24 @@
import TestGame.Levels.Function.L01_Function
import TestGame.Levels.Function.L02_Let
-import TestGame.Levels.Function.L03_Composition
-import TestGame.Levels.Function.L06_Piecewise
-import TestGame.Levels.Function.L07_Injective
-import TestGame.Levels.Function.L07'_Injective
-import TestGame.Levels.Function.L08_Injective
-import TestGame.Levels.Function.L09_Surjective
-import TestGame.Levels.Function.L10_Bijective
+import TestGame.Levels.Function.L03_Piecewise
+import TestGame.Levels.Function.L04_Injective
+import TestGame.Levels.Function.L05_Injective
+import TestGame.Levels.Function.L06_Injective
+import TestGame.Levels.Function.L07_Surjective
+import TestGame.Levels.Function.L08_Bijective
+import TestGame.Levels.Function.L09_Inverse
+import TestGame.Levels.Function.L11_Inverse
Game "TestGame"
World "Function"
Title "Abbildungen"
+
+Introduction "
+Auf der Suche nach dem Buch der Urbilder landet ihr auf einem kleinen Mond, der bis auf
+eine Insel komplett mit Wasser bedeckt zu sein scheint.
+
+Auf der Insel seht ihr verschiedene große und kleine Behausungen, manche aus Stroh und Holz,
+vereinzelte aus Lehm.
+
+Planlos geht ihr zum ersten Haus bei dem jemand vorne außen sitzt.
+"
diff --git a/server/testgame/TestGame/Levels/Function/L01_Function.lean b/server/testgame/TestGame/Levels/Function/L01_Function.lean
index 284136e..1bce9e1 100644
--- a/server/testgame/TestGame/Levels/Function/L01_Function.lean
+++ b/server/testgame/TestGame/Levels/Function/L01_Function.lean
@@ -5,31 +5,59 @@ Game "TestGame"
World "Function"
Level 1
-Title ""
+Title "Anonyme Funktionen"
Introduction
"
-Funktionen werden in Lean mit `ℕ → ℕ` geschrieben (`\\to`), also dem gleichen
-Pfeil wie Implikationen.
+Auf die Frage hin, ob sie von einem Bibliothek wisse, erzählt euch das kleine Mädchen,
+dass es auf der Insel nur einen gäbe, aber sie bedrängt euch so mit einer Frage,
+dass sie euch gar nicht sagt, wo dieser zu finden sei.
+"
+
+Statement "" : ∃ f : ℤ → ℤ, ∀ x, f x < x := by
+ use (fun x ↦ x - 1)
+ simp
+
+Hint : ∃ f : ℤ → ℤ, ∀ x, f x < x =>
+"
+**Robo**: `f : ℤ → ℤ` ist die Notation für eine Funktion und `f x` ist diese Funktion
+angewendet auf ein Element `(x : ℤ)`.
+
+**Du**: War `→` nicht eben noch eine Implikation?
+
+**Robo**: Doch, die brauchen das gleiche Zeichen für beides.
-Eine abstrakte Funktion ist ein entsprechendes Element `(f : ℕ → ℕ)` oder `(g : ℕ → ℝ)`.
-Dies sagt aber gar nichts darüber, wie `f` tatsächlich definiert ist.
+**Du**: Dann ist `f : ℤ → ℤ` also einfach abstrakt irgendeine Funktion,
+wie definier ich aber jetzt konkret eine Abbildungsvorschrift?
-Hat man eine Funktion `(f : A → B)` und ein Element `(x : A)` dann ist `f x` der
-Bildpunkt in `B`. In Lean braucht man also keine Klammern um $f(x)$ zu schreiben.
+**Robo**: Man kennt hier eine Notation für eine anonyme Funktion:
+`fun (x : ℤ) ↦ x ^ 2` ist
-Eplizite, anonyme Funktionen kann man mit dem Syntax `fun (n : ℕ) ↦ n ^ 2` definieren
-(entweder `↦` (`\\map`) oder `=>` als Pfeil in der Mitte).
+$$
+\\begin\{aligned}
+ f : \\mathbb\{ℤ} &\\to \\mathbb\{ℤ} \\\\
+ x &\\mapsto x ^ 2
+\\end\{aligned}
+$$
+
+**Robo**: PS, `↦` ist `\\mapsto`. Aber man kann auch stattdessen `=>` benützen.
"
-Statement
-"Zeige, dass es eine Funktion $\\mathbb{N} \\to \\mathbb{Z}$ gibt, für die $f(x) < x$ gilt."
- : ∃ f : ℕ → ℤ, ∀ x, f x < x := by
- use (fun x ↦ x - 1)
- simp
+HiddenHint : ∃ f : ℕ → ℤ, ∀ x, f x < x =>
+"
+**Du**: Ja aber was mach ich damit?
-Hint : ∃ f : ℕ → ℤ, ∀ x, f x < x =>
+**Robo**: Wie immer gehst du ein `∃` mit `use …` an.
"
-Benütze eine anonyme Funktion `use (fun n ↦ _)` wobei `_` durch einen Ausdruck ersetzt
-werden muss, so dass die Aussage erfüllt wird.
+
+-- TODO: Why does this not show?
+HiddenHint : ∀ (x : ℤ), (fun (y : ℤ) => y - 1) x < x =>
+"**Du**: Zu was sich das wohl vereinfacht?"
+
+HiddenHint (x : ℤ) : (fun y => y - 1) x < x =>
+"**Du**: Zu was sich das wohl vereinfacht?"
+
+Conclusion "Das Mädchen wird kurz ruhig, dann beginnt es zu lächeln und zeigt strahlend
+in eine Richtung. Ihr folgt ihrem Finger und euch fällt in weiter ferne eine pompöse Struktur
+auf einem flachen Hügel auf.
"
diff --git a/server/testgame/TestGame/Levels/Function/L02_Let.lean b/server/testgame/TestGame/Levels/Function/L02_Let.lean
index 247c040..b996425 100644
--- a/server/testgame/TestGame/Levels/Function/L02_Let.lean
+++ b/server/testgame/TestGame/Levels/Function/L02_Let.lean
@@ -5,72 +5,78 @@ Game "TestGame"
World "Function"
Level 2
-Title ""
+Title "let"
Introduction
"
-Ausserhalb eines Beweises kann man Funktionen mit `def`
-(anstatt `lemma`/`example`/`theorem`) definieren:
+Ihr macht euch auf Richtung Bibliothek entlang kleiner Pfade zwischen verschiedenster Behausungen.
-```
-def f (x : ℚ) : ℚ := 1 / (1 + x^2)
+**Du**: Sag mal, ich weiss jetzt dass ich eine Funktion als `fun x ↦ x - 1` definieren kann,
+aber wie kann ich der einen Namen geben?
-def f : ℚ → ℚ := fun x ↦ 1 / (1 + x^2)
-```
+**Robo**: Wenn jemand hier eine Funktion definiert, werden die dir
+`def f (x : ℤ) : ℤ := x - 1` oder `def f : ℤ → ℤ := (fun x ↦ x - 1)` geben.
-(die beiden Varianten sind äquivalent.)
+**Du**: Und das bedeutet beides das gleiche?
-Um eine anonyme Funktion `fun x ↦ 1 / (1 + x^2)` **innerhalb** eines Beweis einem Namen
-zuzuordnen, benützt man `let`:
+**Robo**: Praktisch, ja. Aber! Wenn du eine Funktion in einer Aufgabe benennen willst,
+schreibst du `let f := fun (x : ℤ) ↦ x - 1`!
-```
-let f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
-```
+**Du**: Und was ist der Unterschied?
-`def` und `let` funktionieren also fast gleich wie `lemma`/`example`/`theorem` und `have` mit
-einem wichtigen Unterschied:
+**Robo**: Deines mit `let` ist für innerhalb von einem Beweis, das andere mit `def`
+ist für ausserhalb von einem Beweis. Hier, ich geb dir mal eine Aufgabe:
```
-have f : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
-let f₂ : ℕ → ℕ := fun (n : ℕ) ↦ n ^ 2
+def f (x : ℤ) : ℤ := (x + 4)
```
-
-`have` vergisst sofort den \"Beweis\", das heisst, Lean weiss dann nur, dass es eine
-Funktion `(f : ℕ → ℕ)` gibt, aber nicht, wie diese definiert ist. `let` hingegen speichert
-die Definition der Funktion.
-
-Manchmal muss man Definitionen (von einem `def` oder `let` Statement) mit `unfold` einsetzen.
+und:
"
-def f (x : ℤ) : ℤ := (x + 1) ^ 2
-
-Statement
-"
-Given the function
-```
-def f (x : ℤ) : ℤ := (x + 1) ^ 2
-```
-show that $f(x) = x^2 + 2x + 1$.
+def f (x : ℤ) : ℤ := (x + 4)
-"
- : ∀ x, f x = x ^ 2 + 2 * x + 1 := by
- intro x
+Statement "" (x : ℤ) : ∃ (g : ℤ → ℤ), (g ∘ f) x = x + 1 := by
+ let g := fun (x : ℤ) ↦ x - 3
+ use g
+ simp
unfold f
ring
-NewTactics «let»
-OnlyTactics «let» intro unfold ring
+NewTactic «let»
+NewLemma Function.comp_apply
-HiddenHint : ∀ x, f x = x ^ 2 + 2 * x + 1 =>
-"Fang zuerst wie immer mit `intro x` an."
+Hint (x : ℤ) : ∃ g, (g ∘ f) x = x + 1 =>
+"**Du**: Ist `g ∘ f` Komposition von Funktionen?
-Hint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 =>
-"
-Definitionen muss man manchmal manuell einsetzen um den Taktiken zu helfen.
+**Robo**: Richtig! Das schreibt man mit `\\comp`.
-Das macht man mit `unfold f` (oder alternativ mit `rw [f]`).
-"
+ **Du** Und hier könnte ich also zuerst
+`let g := fun (x : ℤ) ↦ _` definieren, anstatt direkt
+`use fun (x : ℤ) ↦ _`?
-HiddenHint (x : ℤ) : f x = x ^ 2 + 2 * x + 1 =>
+**Robo**: Genau! Das ist zwar praktisch das gleiche, aber kann manchmal nützlich sein.
"
-Nachdem die Definition von `f` eingesetzt ist, übernimmt `ring` den Rest"
+
+-- TODO: Make some hints work here
+Hint (x : ℤ) : ((fun (x : ℤ) ↦ x - 3) ∘ f) x = x + 1 =>
+"**Robo**: Manchmal must du nachhelfen und Funktionen mit `unfold f` öffnen, manchmal nicht.
+Um erlich zu sein, sagt mein Programm nicht genau wann man das machen muss…"
+
+-- TODO : Make this work
+Hint (x : ℤ) (g := (fun (x : ℤ) ↦ x - 3)) : (g ∘ f) x = x + 1 =>
+"**Robo**: `(g ∘ f) x` ist per Definition `g (f x)`, aber mit
+`rw [Function.comp_apply]` kann man das explizit umschreiben, aber `simp` kennt das
+Lemma auch."
+
+Hint (x : ℤ) : f x - 3 = x + 1 =>
+"**Robo**: Manchmal must du nachhelfen und Definitionen mit `unfold f` öffnen, mamchmal klappts
+ohne.
+Um erlich zu sein, sagt mein Programm nicht genau wann man das machen muss…"
+
+-- TODO: Block simp-Lemma
+
+Conclusion "**Du**: Dann verstehst du etwas Mathe?
+
+**Robo**: Ich hatte ja keine Ahnung ob die generierte Aufgabe beweisbar ist…
+
+Und damit erreicht ihr den Hügel mit der Bibliothek."
diff --git a/server/testgame/TestGame/Levels/Function/L03_Composition.lean b/server/testgame/TestGame/Levels/Function/L03_Composition.lean
deleted file mode 100644
index 416e8bb..0000000
--- a/server/testgame/TestGame/Levels/Function/L03_Composition.lean
+++ /dev/null
@@ -1,22 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Function"
-Level 3
-
-Title ""
-
-Introduction
-"
-Komposition von Funktionen kann als `g ∘ f` geschrieben werden.
-
-TODO
-"
-
-Statement
-"TODO: Find an exercise."
- (U T V : Type _) (f : U → V) (g : V → T) (x : U) : (g ∘ f) x = g (f x) := by
- simp only [Function.comp_apply]
-
-NewLemmas Function.comp_apply
diff --git a/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean b/server/testgame/TestGame/Levels/Function/L03_Piecewise.lean
similarity index 89%
rename from server/testgame/TestGame/Levels/Function/L06_Piecewise.lean
rename to server/testgame/TestGame/Levels/Function/L03_Piecewise.lean
index 97bbfcd..8c1615b 100644
--- a/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean
+++ b/server/testgame/TestGame/Levels/Function/L03_Piecewise.lean
@@ -3,13 +3,14 @@ import Mathlib
Game "TestGame"
World "Function"
-Level 4
+Level 3
-Title ""
+Title "Komposition"
Introduction
"
-Du kommst an eine Tür mit zwei Wächtern. Der eine hat ein Schild
+Endlich kommt ihr zur Bibliothek. Komischerweise stehen an der Tür
+zwei Wächtern. Der eine zeigt euch ein Blatt mit
```
def f : ℚ → ℚ := fun x ↦ 5 * x
@@ -21,11 +22,9 @@ der andere eines mit
def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
```
-Auf der Tür steht groß:
+und gibt Dir ein Blatt mit einer einzelnen Zeile am oberen Ende.
"
-example (P : Prop) [Decidable P] (a b : ℕ) (h : P) : ite P a b = a := if_pos h
-
open Set
namespace LevelFunction4
@@ -33,11 +32,6 @@ namespace LevelFunction4
def f : ℚ → ℚ := fun x ↦ 5 * x
def g : ℚ → ℚ := fun x ↦ if 0 ≤ x then 2*x else 0
-
--- #eval (f2 + f2) 2
-
--- #check range f2
-
Statement ""
: f ∘ g = g ∘ f := by
funext x
@@ -57,9 +51,9 @@ Statement ""
unfold f
ring
-NewTactics funext by_cases simp_rw linarith
+NewTactic funext by_cases simp_rw linarith
-NewLemmas not_le if_pos if_neg
+NewLemma not_le if_pos if_neg
Hint : f ∘ g = g ∘ f =>
@@ -72,6 +66,7 @@ Hint : f ∘ g = g ∘ f =>
dann für dieses.
"
+-- TODO : This does not trigger.
-- TODO: These 5 hints should be mutually exclusive. i.e. they should not trigger
-- if a assumption is missing.
Hint (x : ℚ) : (f ∘ g) x = (g ∘ f) x =>
@@ -92,12 +87,15 @@ könnte mit dem Lemma `not_le` zwischen `¬(0 ≤ {x})` und `0 < {x}` wechseln.
Hint (x : ℚ) (h : 0 ≤ x) : f (g x) = g (f x) =>
"
**Robo**: Um das ausrechnen zu können, brauchst du nicht nur `0 ≤ x` sondern auch noch
-eine Annahme `0 ≤ f x`.
+eine neue Annahme `0 ≤ f x`.
+
+**Du**: Also `have h₂ : _`?
"
Hint (x : ℚ) (h : 0 ≤ x) (h₂ : 0 ≤ f x) : f (g x) = g (f x) =>
"
-**Du**: Mit den beiden Annahmen habe ich ja jetzt `(if 0 ≤ x then _)` wobei `0 ≤ x` wahr ist,
+**Du**: Mit den beiden Annahmen sagt die Definition von `g` ja z.B.
+`(if 0 ≤ x then _)` wobei ich weiss dass `0 ≤ x` wahr ist,
kann ich das dann einfach vereinfachen?
**Robo**: Dafür must du zuerst die Definition von `g` öffnen, also `unfold`. Und dann mit
diff --git a/server/testgame/TestGame/Levels/Function/L07_Injective.lean b/server/testgame/TestGame/Levels/Function/L04_Injective.lean
similarity index 87%
rename from server/testgame/TestGame/Levels/Function/L07_Injective.lean
rename to server/testgame/TestGame/Levels/Function/L04_Injective.lean
index cbc45a5..0946ab4 100644
--- a/server/testgame/TestGame/Levels/Function/L07_Injective.lean
+++ b/server/testgame/TestGame/Levels/Function/L04_Injective.lean
@@ -3,13 +3,13 @@ import Mathlib
Game "TestGame"
World "Function"
-Level 5
+Level 4
Title ""
Introduction
"
-Ihr läuft durch verschiedenste Leere Gänge des Funktionentempels.
+Ihr läuft durch verschiedenste Gänge der Bibliothek, allesamt mit Büchern entlang der Wände.
**Du**: Wenn wir wüssten, dass nur ein möglicher Weg hierhin führt, könnten wir
ausschliessen, dass wir im Kreis laufen.
@@ -22,7 +22,7 @@ Statement "" : Injective (fun (n : ℤ) ↦ n + 3) := by
intro a b
simp
-NewDefinitions Injective
+NewDefinition Injective
Hint : Injective (fun (n : ℤ) ↦ n + 3) =>
"**Robo**: `Injective` ist als `∀ \{a b : U}, f a = f b → a = b`
diff --git a/server/testgame/TestGame/Levels/Function/L07'_Injective.lean b/server/testgame/TestGame/Levels/Function/L05_Injective.lean
similarity index 91%
rename from server/testgame/TestGame/Levels/Function/L07'_Injective.lean
rename to server/testgame/TestGame/Levels/Function/L05_Injective.lean
index 8b2447c..48f0172 100644
--- a/server/testgame/TestGame/Levels/Function/L07'_Injective.lean
+++ b/server/testgame/TestGame/Levels/Function/L05_Injective.lean
@@ -5,7 +5,7 @@ set_option tactic.hygienic false
Game "TestGame"
World "Function"
-Level 6
+Level 5
Title ""
@@ -29,8 +29,8 @@ Statement "" : Injective (fun (n : ℤ) ↦ n^3 + (n + 3)) := by
intro a b
simp
-NewDefinitions Injective
-NewLemmas StrictMono.injective StrictMono.add Odd.strictMono_pow
+NewDefinition Injective
+NewLemma StrictMono.injective StrictMono.add Odd.strictMono_pow
Hint : Injective fun (n : ℤ) => n ^ 3 + (n + 3) =>
@@ -76,4 +76,4 @@ Hint (a b : ℤ) (h : a ^ 3 + (a + 3) = b ^ 3 + (b + 3)) : a = b =>
Conclusion "**Du**: Danke vielmals!
-Und ihr läst das Wesen mit im Gang stehen weiter über Injectivität nachdenkend."
+Und damit lässt das Wesen mitten im Gang stehen, wo es weiter über Injektivität nachdenkt."
diff --git a/server/testgame/TestGame/Levels/Function/L08_Injective.lean b/server/testgame/TestGame/Levels/Function/L06_Injective.lean
similarity index 89%
rename from server/testgame/TestGame/Levels/Function/L08_Injective.lean
rename to server/testgame/TestGame/Levels/Function/L06_Injective.lean
index 614ab80..4e61007 100644
--- a/server/testgame/TestGame/Levels/Function/L08_Injective.lean
+++ b/server/testgame/TestGame/Levels/Function/L06_Injective.lean
@@ -3,7 +3,7 @@ import Mathlib
Game "TestGame"
World "Function"
-Level 7
+Level 6
Title "Injektive"
@@ -13,13 +13,13 @@ Weiterirrend kommt ihr an eine Verzweigung.
**Robo**: Sieht beides gleich aus.
-Ein paar Schritte in den linken Korridor hinein seht ihr gekritzel an der Wand:
+Ein paar Schritte in den linken Korridor hinein seht ihr auf dem Boden ein Blatt mit Gekritzel:
```
def f : ℕ → ℕ := fun n ↦ if Even n then n^2 else n+1
```
-**Du**: Hier haben wir eine stückweis definierte Funktion
+**Du**: Hier haben wir wieder eine stückweise Funktion
$$
f(n) = \\begin{cases}
diff --git a/server/testgame/TestGame/Levels/Function/L07_Surjective.lean b/server/testgame/TestGame/Levels/Function/L07_Surjective.lean
new file mode 100644
index 0000000..27906d8
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Function/L07_Surjective.lean
@@ -0,0 +1,37 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 7
+
+Title "Surjektive"
+
+Introduction
+"
+Endlich kommt ihr in einen große, beleuchteten zentralen Raum.
+Alle Wände sind voll mit Büchern und
+in der Mitte sitzt an einem einsamen
+Tisch ein Gelehrter, der tatsächlich das gesuchte Buch zeigen kann.
+
+Bevor er dieses aushändigt, will er aber folgendes wissen:
+"
+
+open Function
+
+Statement "" : Surjective (fun (n : ℤ) ↦ n + 1) := by
+ intro y
+ use y-1
+ simp
+
+NewDefinition Surjective
+
+Hint : Surjective (fun (n : ℤ) ↦ n + 1) =>
+"**Robo**: Die Definition von `Surjective f` ist `∀ y, (∃ x, f x = y)`.
+
+**Du**: Dann kann ich das auch einfach wie Quantifier behandeln?
+
+**Robo**: Schieß drauf los!"
+
+Conclusion
+"Der Gelehrte händigt euch schmunzelnd das Buch aus."
diff --git a/server/testgame/TestGame/Levels/Function/L08_Bijective.lean b/server/testgame/TestGame/Levels/Function/L08_Bijective.lean
new file mode 100644
index 0000000..1fc8135
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Function/L08_Bijective.lean
@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 8
+
+Title ""
+
+Introduction
+"
+**Du**: Ehm, und wie kommen wir da wieder raus?
+
+**Gelehrter**: Gerne zeige ich euch den Weg, nachdem ihr mir auch noch folgendes erklärt:
+"
+
+open Function
+
+Statement "" : Bijective (fun (n : ℤ) ↦ n + 1) := by
+ unfold Bijective
+ constructor
+ intro a b
+ simp
+ intro y
+ use y-1
+ simp
+
+Hint : Bijective (fun (n : ℤ) ↦ n + 1) =>
+"**Robo** *(flüsternd)*: `Bijectve f` ist als `Injective f ∧ Surjective f` definiert.
+
+**Du**: Dann ist das ja ganz simpel!
+"
+
+Conclusion
+"Zufrieden drückt euch der Gelehrte eine neue Fackel in die Hand und
+zeigt euch den Weg nach draussen."
+
+NewDefinition Bijective
diff --git a/server/testgame/TestGame/Levels/Function/L09_Inverse.lean b/server/testgame/TestGame/Levels/Function/L09_Inverse.lean
new file mode 100644
index 0000000..548d01e
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Function/L09_Inverse.lean
@@ -0,0 +1,61 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 9
+
+Title "Inverse"
+
+Introduction
+"
+Eigentlich hast du nur beiläufig Robo gefragt, ob bijektiv nicht auch bedeute, dass
+eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stunde rum
+und der Gelehrte möchte wissen, wie das den genau ginge.
+
+Offensichtlich kennt er diese Aussage als `Function.bijective_iff_has_inverse` aus seinen Büchern,
+aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst.
+"
+
+open Function
+
+--TODO: This is a really hard proof
+Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
+ Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
+ constructor
+ intro h
+ use fun x => (h.2 x).choose
+ constructor
+ · intro x
+ simp
+ apply h.1
+ apply Exists.choose_spec (h.2 (f x))
+ · intro x
+ simp
+ apply Exists.choose_spec (h.2 x)
+ intro ⟨g, h₁, h₂⟩
+ constructor
+ · intro a b hab
+ have h : g (f a) = g (f b)
+ · apply congrArg
+ assumption
+ rw [h₁, h₁] at h
+ assumption
+ · intro x
+ use g x
+ rw [h₂]
+
+NewDefinition LeftInverse RightInverse
+NewLemma Exists.choose Exists.choose_spec congrArg congrFun
+DisabledLemma Function.bijective_iff_has_inverse
+
+Hint {A B : Type} (f : A → B) : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f =>
+"**Du**: Nah da sagt mir so manches nichts, aber ich kann ja mal mit dem `↔` anfangen, das kenn
+ich ja schon."
+
+Conclusion
+"Endlich entkommt ihr der Bibliothek.
+
+**Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!
+
+**Du**: Von wegen Pferden, wie viele PS hat eigentlich unser Raumschiff?"
diff --git a/server/testgame/TestGame/Levels/Function/L09_Surjective.lean b/server/testgame/TestGame/Levels/Function/L09_Surjective.lean
deleted file mode 100644
index dcb6222..0000000
--- a/server/testgame/TestGame/Levels/Function/L09_Surjective.lean
+++ /dev/null
@@ -1,19 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Function"
-Level 8
-
-Title "Surjektive"
-
-Introduction
-"
-"
-
-Statement
-""
-: (fun (n : ℤ) ↦ n + 1).Surjective := by
- intro y
- use y-1
- simp
diff --git a/server/testgame/TestGame/Levels/Function/L10_Bijective.lean b/server/testgame/TestGame/Levels/Function/L10_Bijective.lean
deleted file mode 100644
index 4190785..0000000
--- a/server/testgame/TestGame/Levels/Function/L10_Bijective.lean
+++ /dev/null
@@ -1,23 +0,0 @@
-import TestGame.Metadata
-import Mathlib
-
-Game "TestGame"
-World "Function"
-Level 9
-
-Title ""
-
-Introduction
-"
-"
-
-Statement
-""
- : (fun (n : ℤ) ↦ n + 1).Bijective := by
- constructor
- intro a b hab
- simp at hab
- assumption
- intro y
- use y-1
- simp
diff --git a/server/testgame/TestGame/Levels/Function/L11_Inverse.lean b/server/testgame/TestGame/Levels/Function/L11_Inverse.lean
new file mode 100644
index 0000000..14ac036
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Function/L11_Inverse.lean
@@ -0,0 +1,93 @@
+import TestGame.Metadata
+import Mathlib
+
+Game "TestGame"
+World "Function"
+Level 10
+
+Title "Inverse"
+
+Introduction
+"
+Eigentlich hast du nur beiläufig Robo gefragt, ob bijektiv nicht auch bedeute, dass
+eine Inverse Funktion bestehe. Jetzt steht ihr aber schon seit einer halben Stunde rum
+und der Gelehrte möchte wissen, wie das den genau ginge.
+
+Offensichtlich kennt er diese Aussage als `Function.bijective_iff_has_inverse` aus seinen Büchern,
+aber er möchte, dass Du ihm das hier und jetzt nochmals von Grund auf zeigst.
+"
+
+open Function
+set_option pp.rawOnError true
+Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) :
+ Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by
+ Branch
+ exfalso
+ Hint "Das war eine blöde Idee
+ dd
+
+ ddds
+ "
+ Hint (hidden := true) "constructor"
+ constructor
+ Hint "intro h" -- does not show
+ intro h
+ Hint "rcases h with ⟨h₁, h₂⟩" -- shows too late: 1, 2 after
+ rcases h with ⟨h₁, h₂⟩
+ Hint (strict := true) "let g := fun x => (h₂ x).choose" -- shows correct + 1 after
+ let g := fun x => (h₂ x).choose
+ Hint "use g"
+ use g
+ Hint "constructor" -- does not show
+ constructor
+ Hint "intro x" -- does not show
+ intro x
+ Hint "simp" -- Error updating: Error fetching goals: Rpc error: InternalError: unknown universe metavariable '?_uniq.286465'. Try again.
+ simp
+ Hint "apply h₁"
+ apply h₁
+ Hint "apply Exists.choose_spec (h₂ (f x))"
+ apply Exists.choose_spec (h₂ (f x))
+ Hint "intro y" -- Error updating: Error fetching goals: Rpc error: InternalError: unknown universe metavariable '?_uniq.286465'. Try again.
+ intro y
+ Hint "simp"
+ simp
+ Hint "apply Exists.choose_spec (h₂ y)"
+ apply Exists.choose_spec (h₂ y)
+ Hint "intro ⟨g, h₁, h₂⟩"
+ intro ⟨g, h₁, h₂⟩
+ Hint "constructor"
+ constructor
+ Hint "intro a b hab"
+ intro a b hab
+ Hint (strict := true) "have h : g (f a) = g (f b)"
+ have h : g (f a) = g (f b)
+ Hint "apply congrArg"
+ apply congrArg
+ Hint "assumption"
+ assumption
+ Hint "rw [h₁, h₁] at h"
+ rw [h₁, h₁] at h
+ Hint "assumption"
+ assumption
+ Hint "intro x"
+ intro x
+ Hint "use g x"
+ use g x
+ Hint "rw [h₂]"
+ rw [h₂]
+
+-- NewDefinition LeftInverse RightInverse
+-- NewLemma Exists.choose Exists.choose_spec congrArg congrFun
+-- DisabledLemma Function.bijective_iff_has_inverse
+
+Hint (A B: Type) (f : A → B) (h : Bijective f) :
+ (∃ g, LeftInverse g f ∧ RightInverse g f) → Bijective f =>
+ "Test"
+
+Conclusion
+"Endlich entkommt ihr dem Tempel.
+
+**Robo**: Da würden mich keine zehn Pferde nochmals hineinbringen!
+
+**Du**: Von wegen Pferden, wie viele PS hat eigentlich unser Raumschiff?"
diff --git a/server/testgame/TestGame/Levels/Implication.lean b/server/testgame/TestGame/Levels/Implication.lean
index 4c211af..0d06e71 100644
--- a/server/testgame/TestGame/Levels/Implication.lean
+++ b/server/testgame/TestGame/Levels/Implication.lean
@@ -8,8 +8,9 @@ import TestGame.Levels.Implication.L07_Rw
import TestGame.Levels.Implication.L08_Iff
import TestGame.Levels.Implication.L09_Iff
import TestGame.Levels.Implication.L10_Apply
-import TestGame.Levels.Implication.L11_Rw
-import TestGame.Levels.Implication.L12_Summary
+import TestGame.Levels.Implication.L11_ByCases
+import TestGame.Levels.Implication.L12_Rw
+import TestGame.Levels.Implication.L13_Summary
Game "TestGame"
World "Implication"
@@ -21,10 +22,13 @@ Zurück im Raumschiff macht ihr euch auf den Weg zum einem der beiden Monde, die
beide bewohnt zu sein scheinen.
**Du**: Sag mal Robo, Königin *Logisindes* hat under anderem von Implikationen gesprochen,
-aber niemand von den Einwohnern...
+aber niemand von den Einwohnern wusste was davon...
**Robo**: Auf dem Mond *Implis* den wir gerade ansteuern können sie uns vielleicht mehr
erzählen…
-Und damit leitet Robo den Landeanflug ein.
+Und damit leitet Robo den Landeanflug ein. Implis scheint ein riesiger Tagbau zu sein auf
+dem nach allem möglichen gegraben wird. Überall seht ihr Förderbänder kreuz und queer.
+
+Das Operationsteam begrüsst euch freundlich und lädt zum Essen im Kommandoturm.
"
diff --git a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
index 292005b..7a60817 100644
--- a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
+++ b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean
@@ -1,4 +1,5 @@
import TestGame.Metadata
+import Mathlib.Tactic.Tauto
set_option tactic.hygienic false
@@ -10,31 +11,23 @@ Title "Intro"
Introduction
"
-## Implikationen
-
-In diesem Kapitel lernst du Implikation ($\\Rightarrow$) und Genau-dann-wenn
-($\\Leftrightarrow$) kennen.
-Dazu lernst du, wie man bereits bewiesene Sätze verwendet.
-
-Seien `(A B : Prop)` zwei logische Aussagen. Eine Implikation $A \\Rightarrow B$ schreibt
-man in Lean als `A → B` (`\\to`).
-
-Wenn das Goal eine Implikation $A \\Rightarrow B$ ist, kann man mit
-`intro ha` annehmen, dass $A$ wahr ist. Dann muss man $B$ beweisen.
+**Operationsleiter**: Sagt mal, könnt ihr mir hier weiterhelfen?
"
-Statement
- "Wenn $B$ wahr ist, dann ist die Implikation $A \\Rightarrow (A ∧ B)$ wahr."
- (A B : Prop) (hb : B) : A → (A ∧ B) := by
+Statement (A B : Prop) (hb : B) : A → (A ∧ B) := by
+ Hint "**Du**: Einen Moment, das ist eine Implikation (`\\to`),
+ also `A` impliziert `A und B`, soweit so gut, also eine Tautologie.
+
+ **Robo**: Die scheinen hier `tauto` auch nicht zu verstehen.
+ Implikationen kannst du aber mit `intro h` angehen."
intro hA
+ Hint "**Du**: Jetzt habe ich also angenommen, dass `A` wahr ist und muss `A ∧ B` zeigen,
+ das kennen wir ja schon."
constructor
assumption
assumption
-HiddenHint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) =>
-"Mit `intro ha` kann man annehmen, dass $A$ wahr ist. danach muss man $A \\land B$ zeigen."
-
-Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) =>
-"Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden."
+Conclusion "Der Operationsleiter nickt bedacht."
-NewTactics intro constructor assumption
+NewTactic intro
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
index 74452a8..f05a5c9 100644
--- a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
+++ b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean
@@ -9,34 +9,22 @@ Level 2
Title "Revert"
Introduction
-"
-Mit `intro` kann man also eine Implikation aus dem Goal entfernen, indem man
-die Implikationsprämisse zu den *Annahmen* hinzufügt:
-
-```
-example : A → B :=
- [Beweis]
-```
-
-wird zu
-
-```
-example (ha : A) : B :=
- [Beweis]
-```
-
-Seltener kann auch die andere Richtung nützlich sein. Mit `revert ha` kann man die Annahme
-`ha` entfernen und als Implikationsprämisse vor's Goal hängen.
-"
-
-Statement
-"Angenommen $A$ ist eine wahre Aussage und man hat eine Implikation $A \\Rightarrow B$, zeige
-dass $B$ wahr ist."
- (A B : Prop) (ha : A) (h : A → B) : B := by
+"Jemand aus der Gruppe gibt dir ein Blatt Papier mit einer Zeile Text:"
+
+Statement (A B : Prop) (ha : A) (h : A → B) : B := by
+ Hint "**Robo**: Mit `revert {ha}` kann man die Annahme `ha` als
+ Implikationsprämisse vorne ans Goal anhängen, dann ist das Goal `{A} → {B}`.
+
+ **Du**: Das wirkt etwas unnatürlich.
+
+ **Robo**: Schon, ja. Aber als Tool kann das manchmal nützlich sein."
revert ha
assumption
-HiddenHint (A : Prop) (B : Prop) (ha : A) (h : A → B): B =>
-"Mit `revert ha` kann man die Annahme `ha` als Implikationsprämisse vorne ans Goal anhängen."
+Conclusion "**Du**: Aber das müsste doch auch anders gehen, ich hätte jetzt intuitiv
+die Implikation $A \\Rightarrow B$ angewendet und behauptet, dass es genügt $A$ zu zeigen…
+
+Daraufhin lächelt der Fragende nur vorahnend."
-NewTactics revert assumption
+NewTactic revert
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
index 71272b2..5d917f4 100644
--- a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean
@@ -9,6 +9,8 @@ Title "Apply"
Introduction
"
+Sein Kollege zieht eine Linie unter deinen Beweis, schreibt ein durchgestrichenes ~`revert`~
+hin und gibt dir das Blatt wieder.
`revert` ist aber nur selten der richtige Weg.
Im vorigen Beispiel würde man besser die Implikation $A \\Rightarrow B$ *anwenden*, also
@@ -18,21 +20,20 @@ Wenn man eine Implikation `(g : A → B)` in den Annahmen hat, bei welcher die K
(also $B$) mit dem Goal übereinstimmt, kann man `apply g` genau dies machen.
"
-Statement
- "Seien $A, B$ logische Aussagen, wobei $A$ wahr ist und $A \\Rightarrow B$.
- Zeige, dass $B$ wahr ist."
- (A B : Prop) (hA : A) (g : A → B) : B := by
- apply g
+Statement (A B : Prop) (hA : A) (h : A → B) : B := by
+ Hint "**Robo**: Du hast natürlich recht, normalerweise ist es viel schöner mit
+ `apply {h}` die Implikation anzuwenden."
+ apply h
+ Hint "**Du**: Und jetzt genügt es also `A` zu zeigen."
assumption
-HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : B =>
-"Mit `apply g` kannst du die Implikation `g` anwenden."
+Conclusion "**Robo** Übrigens mit `apply LEMMA` kannst auch jedes Lemma anwenden, dessen
+Aussage mit dem Goal übereinstimmt.
-HiddenHint (A : Prop) (B : Prop) (hA : A) (g : A → B) : A =>
-"Nachdem du die Implikation `A → B` angewendet hast, musst du nur noch $A$ zeigen,
-dafür hast du bereits einen Beweis in den Annahmen."
+Die beiden Fragenden schauen das Blatt an und murmeln zustimmend."
-NewTactics apply assumption
+NewTactic apply
+DisabledTactic revert tauto
-- Katex notes
-- `\\( \\)` or `$ $` for inline
diff --git a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
index e227720..1d4a7a9 100644
--- a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean
@@ -10,26 +10,29 @@ Title "Implikation"
Introduction
"
-Hier eine Übung zu Implikationen.
-Fast immer ist es der richtige Weg, wenn du mit `intro` anfängst.
+**Du** *(zu Robo)*: Testen die uns eigentlich hier?
+
+Ein älteres Gruppenmitglied schiebt ein Tablet über den Tisch und beginnt in leiser
+Stimme zu erklären.
+
+**Mitarbeiterin**: Eines unserer Kontrollelemente ist kaputt und ist verwirrt, wo Sachen hinkommen.
+Gesteuert werden diese über Panels, und hier hab ich das Übungspanel, mit dem wir neue
+Ingeneure ausbilden:
"
-Statement
- "Angenommen man weiss $A \\Rightarrow B \\Rightarrow C$, zeige dass $A \\Rightarrow C$."
- (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
+Statement (A B C : Prop) (f : A → B) (g : B → C) : A → C := by
+ Hint "**Du**: Ich soll Implikationen $A \\Rightarrow B \\Rightarrow C$ zu $A \\Rightarrow C$
+ kombinieren?
+
+ **Robo**: Am besten fängst du mit `intro` an und arbeitest dich dann rückwärts durch."
intro hA
+ Hint (hidden := true) "**Robo**: Das ist wieder eine Anwendung von `apply`."
apply g
apply f
assumption
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (f : A → B) (g : B → C) : A → C =>
-"Mit `intro hA` kann man annehmen, dass $A$ wahr ist. danach muss man $B$ zeigen."
-
-Hint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
-"Jetzt ist es ein altbekanntes Spiel von `apply`-Anwendungen."
+Conclusion "**Du**: Ich hab das Konzept verstanden.
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) : C =>
-"Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende
-diese mit `apply` an."
+Die Mitarbeiterin ist zufrieden und wünscht euch Glück auf der Mission."
-NewTactics intro apply assumption revert
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
index 83292a5..78b48cc 100644
--- a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean
@@ -8,46 +8,46 @@ Title "Implikation"
Introduction
"
-Noch eine Übung: Angenommen man hat folgende Implikationen:
+Selbstsicher folgt ihr den Anweisungen und geht nach draussen zum
+defekten Kontrollelement. Dieses zeigt ein kompliziertes Diagram:
$$
\\begin{CD}
A @>{f}>> B @<{g}<< C \\\\
@. @V{h}VV @V{m}VV \\\\
- D @>{i}>> E @>{k}>> F
+ D @>{i}>> E @>{k}>> F \\\\
+ @A{m}AA @A{n}AA @V{p}VV \\\\
+ G @<{q}<< H @>{r}>> I
\\end{CD}
$$
"
Statement
- "Beweise $A \\Rightarrow F$."
- (A B C D E F : Prop) (f : A → B) (g : C → B) (h : B → E)
- (i : D → E) (k : E → F) (m : C → F) : A → F := by
+ (A B C D E F G H I : Prop)
+ (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : G → D)
+ (n : H → E) (p : F → I) (q : H → G) (r : H → I) : A → I := by
+ Hint "**Du**: Also ich muss einen Pfad von Implikationen $A \\Rightarrow I$ finden.
+
+ **Robo**: Und dann fängst du am besten wieder mit `intro` an."
intro ha
+ Branch
+ apply r
+ Hint "**Robo**: Das sieht nach einer Sackgasse aus…"
+ Hint (hidden := true) "**Robo**: Na wieder `apply`, was sonst."
+ apply p
apply k
apply h
+ Branch
+ apply g
+ Hint "**Robo**: Nah, da stimmt doch was nicht…"
apply f
assumption
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
- (f : A → B) (g : C → B) (h : B → E)
- (i : D → E) (k : E → F) (m : C → F) : A → F =>
-"Wieder ist es schlau, mit `intro` anzufangen."
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
- (hA : A) (f : A → B) (g : C → B) (h : B → E)
- (i : D → E) (k : E → F) (m : C → F) : F =>
-"Versuch mit `apply` den richtigen Weg zu finden."
-
-Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
- (hA : A) (f : A → B) (g : C → B) (h : B → E)
- (i : D → E) (k : E → F) (m : C → F) : C =>
-"Sackgasse. Probier doch einen anderen Weg."
+Conclusion
+"Mit einem lauten Ratteln springen die Förderbänder wieder an.
-Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop)
- (hA : A) (f : A → B) (g : C → B) (h : B → E)
- (i : D → E) (k : E → F) (m : C → F) : D =>
-"Sackgasse. Probier doch einen anderen Weg."
+**Operationsleiter**: Vielen Dank euch! Kommt ich geb euch eine Führung und stell euch den
+Technikern hier vor."
-NewTactics apply assumption revert intro
+DisabledTactic tauto
-- https://www.jmilne.org/not/Mamscd.pdf
diff --git a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
index dee2b57..7f5ea41 100644
--- a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean
@@ -8,36 +8,39 @@ Title "Genau dann wenn"
Introduction
"
-Genau-dann-wenn, $A \\Leftrightarrow B$, wird als `A ↔ B` (`\\iff`) geschrieben.
-`A ↔ B` ist eine Struktur (ähnlich wie das logische UND), die aus zwei Teilen besteht:
+Als erstes kommt ihr in einen kleinen Raum mit ganz vielen Bildschirmen.
-- `mp`: die Implikation $A \\Rightarrow B$.
-- `mpr`: die Implikation $B \\Rightarrow A$.
+Ein junges Wesen dreht sich auf dem Stuhl um, und sagt:
-Hat man ein $\\Leftrightarrow$ im Goal, nimmt man dieses ebenfalls mit der Taktik
-`constructor` auseinander und zeigt dann beide Richtungen einzeln.
+**Mitarbeiter**: Oh hallo! Schaut euch mal das hier an!
"
-Statement
- "Zeige dass `B ↔ C`."
- (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
+Statement (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by
+ Hint "**Robo**: Das ist ein genau-dann-wenn Pfeil: `\\iff`. Er besteht aus zwei Teilen:
+ `A ↔ B` ist als `⟨A → B, B → A⟩` definiert.
+
+ **Du**: Also ganz ähnlich wie das UND, `A ∧ B`?
+
+ **Robo**: Genau. Entsprechend kannst du hier auch mit `constructor` anfangen."
constructor
+ Hint "**Du**: Ah und die beiden hab ich schon in den Annahmen."
assumption
assumption
-HiddenHint (A : Prop) (B : Prop) : A ↔ B =>
-"Eine Struktur wie `A ↔ B` kann man mit `constructor` zerlegen."
-
-HiddenHint (A : Prop) (B : Prop) (h : A → B) : A → B =>
-"Such mal in den Annahmen."
-
Conclusion
"
-Die Taktik `constructor` heisst so, weil `↔` als \"Struktur\" definiert ist, die
-aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean, es soll versuchen,
-ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann.
+**Robo**: Übrigens, bei `(h : A ∧ B)` haben die beiden Teile `h.left` und `h.right` geheissen,
+hier bei `(h : A ↔ B)` heissen sie `h.mp` und `h.mpr`.
+
+**Du**: Also `h.mp` ist `A → B`? Wieso `mp`?
+
+**Operationsleiter**: \"Modulo Ponens\" ist ein lokaler Begriff hier,
+aber das ist doch nicht wichtig.
+
+**Robo**: Und das \"r\" in `mpr` stünde für \"reverse\" weils die Rückrichtung ist.
"
-NewTactics constructor assumption
+NewTactic constructor
+DisabledTactic tauto rw
-- TODO : `case mpr =>` ist mathematisch noch sinnvoll.
diff --git a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
index 17ca7d9..a224432 100644
--- a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
+++ b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean
@@ -11,64 +11,35 @@ Title "Genau dann wenn"
Introduction
"
-Hat man ein `(h : A ↔ B)` in den Annahmen, hat man die gleichen beiden Optionen wie beim
-logischen UND plus noch eine neue:
+Als nächstes begenet ihr jemandem im Flur.
-1. Mit `h.mp` und `h.mpr` (oder `h.1` und `h.2`) kann man die einzelnen Implikationen
- direkt auswählen.
-2. Mit `rcases h with ⟨h₁, h₂⟩` könnte man die Struktur `h` zerlegen und man erhält zwei
- separate Annahmen `(h₁ : A → B)` und `(h₂ : B → A)`
-3. **Mit** `rw [h]` **kann man im Goal `A` durch `B` ersetzen.**
-
-Wir widmen uns zuerst `rw`. Dies steht für \"rewrite\". Da $A$ und $B$ logisch äquivalent
-sind, kann man beliebig das eine mit dem anderen vertauschen.
-`rw [h]` ersetzt $A$ durch $B$.
-Dabei gibt es noch einige Tricks:
-
-- `rw [← h]` ersetzt umgekehrt $B$ durch $A$ (`\\l`, kleines L).
-- `rw [h, g]` ist das gleiche wie `rw [h]` gefolgt von `rw [g]`.
+Dieser hat schon von euch gehört und will sofort wissen, ob ihr ihm helfen könnt:
"
-Statement
- "Zeige dass `B ↔ C`."
- (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
- rw [h₁]
- rw [←h₂]
- assumption
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C =>
-"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
-Probiers doch mit `rw [h₁]`."
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : A ↔ C =>
-"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
-Probiers doch mit `rw [h₁]`."
+Statement (A B C D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ C := by
+ Hint "**Du**: $B \\iff A \\iff D \\iff C$, die sind doch alle äquivalent…
-Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ D) : B ↔ D =>
-"Man kann auch rückwärts umschreiben:
-`rw [←h₂]` ersetzt man im Goal `B` durch `a` (`\\l`, also ein kleines L)"
-
-HiddenHint (A : Prop) (B : Prop) (h : A ↔ B) : A ↔ B =>
-"Schau mal durch die Annahmen durch."
-
-
--- These should not be necessary if they don't use `rw [] at`.
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : A ↔ C) : B ↔ C =>
-"Auch eine Möglichkeit... Kannst du das Goal so umschreiben,
-dass es mit einer Annahme übereinstimmt?"
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : A ↔ B) (h₃ : B ↔ D) : B ↔ C =>
-"Auch eine Möglichkeit.. Kannst du das Goal so umschreiben, dass es mit einer Annahme übereinstimmt?"
+ **Robo**: Ja aber du musst ihm helfen umzuschreiben. Mit `rw [h₁]` kannst du `C` durch `D`
+ ersetzen."
+ rw [h₁]
+ Hint "**Du** Und wenn ich in die andere Richtung umschreiben möchte?
-Hint (A : Prop) (B : Prop) (h : B ↔ A) : A ↔ B =>
-"Naja auch Umwege führen ans Ziel... Wenn du das Goal zu `A ↔ A` umschreibst, kann man es mit
-`rfl` beweisen (rsp. das passiert automatisch.)"
+ **Robo**: Dann schreibst du ein `←` vor den Namen, also `rw [← hₓ]`."
+ Branch
+ rw [← h₃]
+ Hint "**Du**: Ehm, das ist verkehrt.
-Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : D ↔ A) : B ↔ C =>
-"Das ist nicht der optimale Weg..."
+ **Robo**: Andersrum wär's besser gewesen, aber wenn du jetzt einfach weitermachst bis du
+ sowas wie `A ↔ A` kriegst, kann `rfl` das beweisen.
-Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ B) (h₃ : A ↔ D) : B ↔ C =>
-"Das ist nicht der optimale Weg..."
+ **Robo: Da fällt mir ein, `rw` versucht automatisch `rfl` am Ende. Das heisst, du musst
+ das nicht einmal mehr schreiben."
+ rw [h₂]
+ rw [←h₂]
+ assumption
+Conclusion "Ihr geht weiter und der Operationsleiter zeigt euch die Küche."
-NewTactics rw assumption
+NewTactic rw assumption
+DisabledTactic tauto
+-- NewLemma Iff.symm
diff --git a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
index 0bf64f0..8801210 100644
--- a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean
@@ -10,35 +10,35 @@ Title "Genau dann wenn"
Introduction
"
-Nun schauen wir uns Option 1) an, die du schon von UND kennst:
+Der Koch kommt erfreut hinter einem grossen Topf hervor.
-1. Mit `h.mp` und `h.mpr` (oder `h.1` und `h.2`) kann man die einzelnen Implikationen
- direkt auswählen.
-
-`h.mp` und `h.mpr` (oder `h.1` und `h.2`) sind die einzelnen Implikationen, und du kannst
-mit denen ensprechend arbeiten. Insbesondere kannst du mit `apply h.mp` die Implikation
-$A \\Rightarrow B$ anwenden, wenn das Goal $B$ ist.
-
-*(PS: das `.mp` kommt von \"Modus Ponens\", ein Ausdruck as der Logik.)*
+**Koch**: Sagt mal, gestern hat mir jemand was erzählt und es will einfach nicht aus
+meinem Kopf…
"
-Statement
-"Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$."
- (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
+Statement (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by
+ Hint "**Du**: Naja ich kann wohl immerhin mal mit `intro` anfangen und annehmen,
+ dass `{A}` wahr sei…
+
+ **Robo**: und dann schauen wir weiter!"
intro hA
+ Hint "**Robo**: Also eine Implikation wendet man mit apply an…
+
+ **Du**: Weiss ich ja!"
apply g
- apply h.mp
- assumption
+ Hint "**Robo**: …und du kannst die Implikation `{A} → {B}` genau gleich mit
+ `apply {h}.mp` anwenden.
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) : A → C =>
-"Fange wie immer mit `intro` an."
+ **Du**: Aber ich könnte hier auch `rw [← h]` sagen, oder?
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : C =>
-"Wie im Implikationen-Level kannst du nun `apply` verwenden."
+ **Robo**: Klar, aber offenbar versteht der Koch das `rw` nicht.
+ "
+ apply h.mp
+ assumption
-Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B =>
-"Mit `apply h.mp` kannst du nun die Implikation `A → B` anwenden."
+Conclusion "**Koch**: Danke vielmals! Jetzt muss ich aber schauen dass die Suppe nicht verkocht!
-Conclusion "Im nächsten Level findest du die zweite Option."
+Und er eilt davon."
-NewTactics apply assumption
+NewTactic apply assumption
+DisabledTactic tauto rw
diff --git a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
index a3c6fe2..daede52 100644
--- a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
+++ b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean
@@ -10,33 +10,35 @@ Title "Genau dann wenn"
Introduction
"
-Und noch die letzte Option:
+Noch während der Koch wieder zu seiner Suppe geht, kommt sein erster Gehilfe hervor.
-2. Mit `rcases h with ⟨h₁, h₂⟩` könnte man die Struktur `h` zerlegen und man erhält zwei
- separate Annahmen `(h₁ : A → B)` und `(h₂ : B → A)`
-
-Als letzte Option kannst du `rcases h with ⟨h₁, h₂⟩` auch auf eine Annahme `(h : A ↔ B)`
-anwenden, genau wie du dies bei einer Annahme `(h' : A ∧ B)` gemacht hast.
+**Gehilfe**: Ich hab gestern noch was anderes gehört, könnt ihr mir da auch helfen?
+Aber ich versteh nicht ganz was ihr meinem Chef erklärt habt.
"
-Statement
-"Angenommen man hat $A \\iff B$ und $B \\Rightarrow C$, zeige $A \\Rightarrow C$."
- (A B : Prop) : (A ↔ B) → (A → B) := by
+
+Statement (A B : Prop) : (A ↔ B) → (A → B) := by
+ Hint "**Du**: Hmm, mindestens mit der Implikation kann ich anfangen."
+ Hint (hidden := true) "**Robo**: Genau, das war `intro`."
intro h
- rcases h
+ Hint "**Du**: Also ich kenn `rw [h]` und `apply h.mp`, aber das will er wohl nicht hören.
+
+ **Robo**: Was du machen könntest ist mit `rcases h with ⟨mp, mpr⟩` die Annahme in zwei
+ Teile aufteilen."
+ Branch
+ intro a
+ Hint "**Robo**: Hier müsstest du jetzt `rw [←h]` oder `apply h.mp` benützen, aber der
+ Gehilfe will, dass du zwingend eine dritte Variante benützt. Geh doch einen
+ Schritt zurück so dass das Goal `A → B` ist."
+ rcases h with ⟨mp, mpr⟩
+ Hint (hidden := true) "**Du**: Ah und jetzt ist das Resultat in den Annahmen."
assumption
-HiddenHint (A : Prop) (B : Prop) : (A ↔ B) → A → B =>
-"Angefangen mit `intro h` kannst du annehmen, dass `(h : A ↔ B)` wahr ist."
-
-HiddenHint (A : Prop) (B : Prop) (h : A ↔ B) : A → B =>
-"Mit `rcases h with ⟨h₁, h₂⟩` kannst du jetzt die Annahme `(h : A ↔ B)` zerlegen."
-
-
Conclusion
"
+**Gehilfe**: Ah danke! Und jetzt versteh ich auch die Zusammenhänge!
"
-
-NewTactics intro apply rcases assumption
+OnlyTactic intro rcases assumption
+DisabledTactic rw apply tauto
-- -- TODO: The new `cases` works differntly. There is also `cases'`
-- example (A B : Prop) : (A ↔ B) → (A → B) := by
diff --git a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
index 4bea8e4..8905f6f 100644
--- a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
+++ b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean
@@ -11,45 +11,39 @@ Title "Lemmas"
Introduction
"
-Bewiesene Resultate möchte man in späteren Aufgaben als Sätze wieder verwenden.
+Ihr setzt euch hin und der Gehilfe bringt euch allen Suppe. Neben euch sitzt eine Mechanikerin
+über ihre Suppe geneigt.
-In Lean sind das Lemmas und Theoreme (wobei es keinen Unterschied zwischen `lemma` und `theorem`
-gibt).
-
-Links in der Bibliothek findest du bekannte Lemmas. Wenn das Goal mit der Aussage des Lemmas
-übereinstimmt, kannst du es mit `apply [Lemma-Name]` anwenden, wie du das mit Implikationen auch
-machst.
+**Mechanikerin**: Sagt mal, ich hab unten über folgendes tiefgründiges Problem nachgedacht:
+"
-Zum Beispiel gibt es ein Lemma, das sagt, dass wenn
-$A \\Rightarrow B$ dann $(\\neg A \\lor B)$:
+Statement (A : Prop) : ¬A ∨ A := by
+ Hint "**Du**: Das scheint ziemlich offensichtlich.
-```
-lemma not_or_of_imp : (A B : Prop) (h : A → B) :
- ¬A ∨ B := by
- ...
-```
+ **Robo**: Ich glaube, sie will eine detailierte Antwort. Ich kenne ein Lemma
+ `not_or_of_imp`, was sagt `(A → B) → ¬ A ∨ B`. Da das Resultat des Lemmas mit
+ deinem Goal übreinstimmt, kannst du es mit `apply not_or_of_imp` anwenden."
+ Branch
+ right
+ Hint "**Du**: Und jetzt?
-Wenn also dein Goal `¬A ∨ B` ist, kannst du mit `apply not_or_of_imp` dieses
-Lemma anwenden. Danach musst du noch alle Annahmen zeigen.
-"
+ **Robo**: `right/left` funktioniert hier nicht, da du nicht weisst ob `A` wahr oder falsch
+ ist."
+ Branch
+ left
+ Hint "**Du**: Und jetzt?
-Statement
-"Benutze `not_or_of_imp` um zu zeigen, dass $\\neg A \\lor A$ wahr ist."
- (A : Prop) : ¬A ∨ A := by
+ **Robo**: `right/left` funktioniert hier nicht, da du nicht weisst ob `A` wahr oder falsch
+ ist."
apply not_or_of_imp
+ Hint (hidden := true) "**Robo**: Ich würd wieder mit `intro` weitermachen."
intro
assumption
-HiddenHint (A : Prop) : ¬A ∨ A =>
-"Das Lemma wendest du mit `apply not_or_of_imp` an."
-
-HiddenHint (A : Prop) : A → A =>
-"Wie immer, `intro` ist dein Freund."
-
Conclusion
"
+**Mechanikerin**: Danke vielmals, jetzt bin ich schon viel ruhiger.
"
-NewTactics apply left right assumption
-
-NewLemmas not_or_of_imp
+NewLemma not_or_of_imp
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L11_ByCases.lean b/server/testgame/TestGame/Levels/Implication/L11_ByCases.lean
new file mode 100644
index 0000000..7493335
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Implication/L11_ByCases.lean
@@ -0,0 +1,38 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+import Mathlib
+
+Game "TestGame"
+World "Implication"
+Level 11
+
+Title "by_cases"
+
+Introduction
+"
+**Du**: Sagt mal, hätte ich da nicht auch einfach zwei Fälle anschauen können:
+Wenn `A` wahr ist, beweis ich die rechte Seite, sonst die Linke.
+
+**Robo**: Tatsächlich, `by_cases h : A` würde genau das machen!
+"
+
+Statement (A : Prop) : ¬A ∨ A := by
+ Hint (hidden := true) "**Du**: Wie?
+
+ **Robo**: Also `by_cases h : A` erstellt zwei Goals. Im ersten hast Du `(h : A)` zur
+ Verfügung, im zweiten `(h : ¬ A)`."
+ by_cases h : A
+ Hint "**Du**: "
+ right
+ assumption
+ left
+ assumption
+
+Conclusion
+"
+**Du**: Das kann noch ganz nützlich sein.
+"
+
+NewTactic by_cases
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
deleted file mode 100644
index 1151fb4..0000000
--- a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean
+++ /dev/null
@@ -1,39 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Cases
-import Mathlib.Logic.Basic
-
-Game "TestGame"
-World "Implication"
-Level 11
-
-Title "Lemmas"
-
-Introduction
-"
-Wenn die Aussage eines Lemmas eine Äquivalenz ist, kann man dieses auch mit `rw` brauchen,
-wie du es von Äquivalenzen kennst.
-
-Ein wichtiges Lemma ist dass $\\neg(\\neg A))$ und $A$ äquivalent sind:
-
-```
-lemma not_not (A : Prop) : ¬¬A ↔ A := by
- ...
-```
-
-Mit `rw [not_not]` sucht Lean also im Goal ein Term `¬¬(·)` und entfernt dort das `¬¬`.
-"
-
-Statement
-"Zeige, dass $A ∨ (¬¬B) ∧ C$ und $A ∨ B ∧ C$ äquivalent sind."
- (A B C : Prop) : A ∨ (¬¬B) ∧ C ↔ A ∨ B ∧ C := by
- rw [not_not]
-
-Conclusion
-"
-`rw` hat automatisch `rfl` ausgeführt und dadurch den Beweis beendet.
-"
-
-NewTactics rw
-
-NewLemmas not_not not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Implication/L12_Rw.lean b/server/testgame/TestGame/Levels/Implication/L12_Rw.lean
new file mode 100644
index 0000000..ed9683a
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Implication/L12_Rw.lean
@@ -0,0 +1,50 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Cases
+import Mathlib.Logic.Basic
+
+Game "TestGame"
+World "Implication"
+Level 12
+
+Title "Lemmas"
+
+Introduction
+"
+Der Arbeitskollegin der Mechanikerin, der die ganze Zeit gespannt zugehört hat, dreht sich zu
+euch.
+
+Er ist offensichtlich interessiert and existierenden Resultaten zu sein, aber offenbar
+kann er nicht viel mit `apply` anfangen.
+
+Er hat aber folgendes Resultat bereit:
+
+```
+lemma not_not (A : Prop) : ¬¬A ↔ A
+```
+
+und stellt euch folgende Frage:
+"
+
+Statement (A B C : Prop) : (A ∧ (¬¬C)) ∨ (¬¬B) ∧ C ↔ (A ∧ C) ∨ B ∧ (¬¬C) := by
+ Hint "**Robo**: Ein Lemma, das wie `not_not` ein `↔` oder `=` im Statement hat, kann
+ auch mit `rw [not_not]` verwendet werden."
+ rw [not_not]
+ Hint "**Du**: Häh, wieso hat das jetzt 2 von 3 der `¬¬` umgeschrieben?
+
+ **Robo**: `rw` schreibt nur das erste um, das es findet, also `¬¬C`. Aber weil dieses
+ mehrmals vorkommt, werden die alle ersetzt…
+
+ **Du**: Ah, und `¬¬B` ist was anderes, also brauch ich das Lemma nochmals."
+ rw [not_not]
+
+Conclusion
+"
+**Du**: Ah und wir sind fertig…?
+
+**Robo**: Ja, `rw` versucht immer anschliessend `rfl` aufzurufen, und das hat hier
+funktioniert.
+"
+
+DisabledTactic tauto apply
+NewLemma not_not
diff --git a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
deleted file mode 100644
index 7a64ade..0000000
--- a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean
+++ /dev/null
@@ -1,81 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.LeftRight
-import Mathlib
-
-set_option tactic.hygienic false
-
-Game "TestGame"
-World "Implication"
-Level 12
-
-Title "Zusammenfassung"
-
-Introduction
-"
-Damit bist du am Ende der zweiten Lektion angekommen.
-Hier ein Überblick über alles was in diesem Kapitel eingeführt wurde und eine
-Abschlussaufgabe.
-
-## Notationen / Begriffe
-
-| | Beschreibung |
-|:--------------|:---------------------------------------------------------|
-| → | Eine Implikation. |
-| ↔ | Genau-dann-wenn / Äquivalenz. |
-| `lemma` | Ein Resultat mit einem Namen. |
-| `theorem` | Das gleiche wie ein Lemma. |
-| `example` | Wie ein Lemma aber ohne Namen (nicht weiter verwendbar.) |
-
-## Taktiken
-
-| | Taktik | Beispiel |
-|:----|:--------------------------|:-------------------------------------------------------|
-| 8 | `intro` | Für eine Implikation im Goal. |
-| 9 | `revert` | Umkehrung von `intro`. |
-| 10 | `apply` | Wendet eine Implikation auf das Goal an. |
-| 10ᵇ | `apply` | Wendet ein Lemma an. |
-| 11 | `rw` | Umschreiben zweier äquivalenter Aussagen. |
-| 11ᵇ | `rw` | Benutzt ein Lemma, dessen Aussage eine Äquivalenz ist. |
-
-
-Als Abschlussübung kannst du folgende Äquivalenz zeigen:
-"
-
-Statement imp_iff_not_or
-"$A \\Rightarrow B$ ist äquivalent zu $\\neg A \\lor B$."
- (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
- constructor
- apply not_or_of_imp
- intro h ha
- rcases h with h | h
- contradiction
- assumption
-
-HiddenHint (A : Prop) (B: Prop) : (A → B) ↔ ¬ A ∨ B =>
-"Eine Äquivalenz im Goal geht man immer mit `constructor` an."
-
-HiddenHint (A : Prop) (B: Prop) : (A → B) → ¬ A ∨ B =>
-"Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet."
-
-HiddenHint (A : Prop) (B: Prop) (h : A → B) : ¬ A ∨ B =>
-"Diese Aussage hast du vorhin bereits als Lemma kennengelernt und angewendet."
-
-HiddenHint (A : Prop) (B: Prop) : ¬ A ∨ B → (A → B) =>
-"Eine Implikation geht man fast immer mit `intro h` an."
-
-HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) =>
-"Nochmals `intro`."
-
-HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) : (A → B) =>
-"Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen."
-
-HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B =>
-"Das ODER in den Annahmen kannst du mit `rcases h with h | h` aufteilen."
-
-HiddenHint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B =>
-"Findest du einen Widerspruch?"
-
-NewTactics rfl assumption trivial left right constructor rcases
-
-NewLemmas not_not not_or_of_imp
diff --git a/server/testgame/TestGame/Levels/Implication/L13_Summary.lean b/server/testgame/TestGame/Levels/Implication/L13_Summary.lean
new file mode 100644
index 0000000..6de3e35
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Implication/L13_Summary.lean
@@ -0,0 +1,77 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.LeftRight
+import Mathlib
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Implication"
+Level 13
+
+Title "Zusammenfassung"
+
+Introduction
+"
+**Operationsleiter**: Damit endet unsere Führung langsam. Bevor ihr weitergeht
+habe ich noch ein Problem, an dem ich mir die Zähne ausbeisse. Wir haben die
+Herleitung eines unserer Programme `imp_iff_not_or` verloren, und wissen nicht mehr
+ob es einwandfrei funktioniert.
+
+**Du**: Nah gut, mal sehen. Robo, was hab ich denn alles hier gelernt?
+
+**Robo**: Hier ist die Übersicht:
+
+## Notationen / Begriffe
+
+| | Beschreibung |
+|:--------------|:---------------------------------------------------------|
+| → | Eine Implikation. |
+| ↔ | Genau-dann-wenn / Äquivalenz. |
+
+## Taktiken
+
+| | Taktik | Beispiel |
+|:----|:--------------------------|:-------------------------------------------------------|
+| 8 | `intro` | Für eine Implikation im Goal. |
+| 9 | `revert` | Umkehrung von `intro`. |
+| 10 | `apply` | Wendet eine Implikation auf das Goal an. |
+| 10ᵇ | `apply` | Wendet ein Lemma an. |
+| 11 | `by_cases` | Fallunterscheidung `P` und `¬P` |
+| 12 | `rw` | Umschreiben zweier äquivalenter Aussagen. |
+| 12ᵇ | `rw` | Benutzt ein Lemma, dessen Aussage eine Äquivalenz ist. |
+"
+
+Statement imp_iff_not_or (A B : Prop) : (A → B) ↔ ¬ A ∨ B := by
+ constructor
+ Hint "**Du**: Das sieht kompliziert aus…
+
+ **Robo** *(flüsternd)*: Ja, aber die Richtung kennst du ja schon also Lemma,
+ wend doch einfach das an."
+ apply not_or_of_imp
+ Hint "**Du**: Gibt es für die Gegenrichtung auch ein Lemma?
+
+ **Robo**: Leider nicht. Da musst du manuell ran."
+ Hint (hidden := true) "**Robo**: Na Implikationen fangst du immer mit `intro` an."
+ intro h
+ intro ha
+ Hint (hidden := true) "**Robo**: Ich wür mal die Annahme `h` mit `rcases` aufteilen."
+ rcases h with h | h
+ contradiction
+ assumption
+
+DisabledTactic tauto
+
+Conclusion "**Operationsleiter**: Damit gehen unsere Wege auseinander. Da fällt mir ein, seit
+ihr auf dem Weg zu unserem Schwestermond?
+
+**Du**: Könnten wir sein…
+
+**Operationsleiter**: Ich hab hier einen Brief für *Evenine*, könntet ihr diesen mit euch führen?
+
+**Du**: Klar! Robo, halt den mal.
+
+Robo nimmt den Brief und lässt ihn irgendwo in seinem Innern verschwinden. Dabei bemerkt er
+den besorgten Blick des Operationsleiters.
+
+**Robo**: Keine Angst, ich verdaue nichts!"
diff --git a/server/testgame/TestGame/Levels/Induction/L01_Induction.lean b/server/testgame/TestGame/Levels/Induction/L01_Induction.lean
index e113b6f..f2804b9 100644
--- a/server/testgame/TestGame/Levels/Induction/L01_Induction.lean
+++ b/server/testgame/TestGame/Levels/Induction/L01_Induction.lean
@@ -24,7 +24,7 @@ Statement
rw [Nat.pow_succ, Nat.mul_succ, add_assoc, h, mul_comm, ←mul_add]
simp
---NewLemmas Nat.pow_succ, Nat.mul_succ, add_assoc, mul_comm, ←mul_add
+--NewLemma Nat.pow_succ, Nat.mul_succ, add_assoc, mul_comm, ←mul_add
-- example (n : ℕ) : Even (n^2 + n) := by
-- induction n
diff --git a/server/testgame/TestGame/Levels/Inequality/L02_Pos.lean b/server/testgame/TestGame/Levels/Inequality/L02_Pos.lean
index b8555eb..9ebd15c 100644
--- a/server/testgame/TestGame/Levels/Inequality/L02_Pos.lean
+++ b/server/testgame/TestGame/Levels/Inequality/L02_Pos.lean
@@ -34,8 +34,8 @@ Statement Nat.pos_iff_ne_zero
intro
apply Nat.succ_pos
-NewTactics simp
-NewLemmas Nat.succ_pos
+NewTactic simp
+NewLemma Nat.succ_pos
Hint : 0 < Nat.zero ↔ Nat.zero ≠ 0 =>
"Den Induktionsanfang kannst du oft mit `simp` lösen."
diff --git a/server/testgame/TestGame/Levels/Inequality/L03_Linarith.lean b/server/testgame/TestGame/Levels/Inequality/L03_Linarith.lean
index 01203c0..b63fab6 100644
--- a/server/testgame/TestGame/Levels/Inequality/L03_Linarith.lean
+++ b/server/testgame/TestGame/Levels/Inequality/L03_Linarith.lean
@@ -18,6 +18,6 @@ Statement
(n : ℕ) (h : 2 ≤ n) : n ≠ 0 := by
linarith
-NewTactics linarith
+NewTactic linarith
-NewLemmas Nat.pos_iff_ne_zero
+NewLemma Nat.pos_iff_ne_zero
diff --git a/server/testgame/TestGame/Levels/Inequality/T_Induction.lean b/server/testgame/TestGame/Levels/Inequality/T_Induction.lean
index 61fbfff..a393275 100644
--- a/server/testgame/TestGame/Levels/Inequality/T_Induction.lean
+++ b/server/testgame/TestGame/Levels/Inequality/T_Induction.lean
@@ -38,4 +38,4 @@ Hint (P : ℕ → Prop) (m : ℕ) (hi : P m) : P (Nat.succ m) =>
In diesem Beispiel kannst du `apply` benützen."
-NewTactics induction
+NewTactic induction
diff --git a/server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean b/server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean
index e51edc0..1d85c83 100644
--- a/server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean
+++ b/server/testgame/TestGame/Levels/LeanStuff/L03_ImplicitArguments.lean
@@ -43,9 +43,9 @@ Statement
rw [Fin.sum_univ_castSucc (n := m + 1)]
rfl
-OnlyTactics rw rfl
+OnlyTactic rw rfl
-NewLemmas Fin.sum_univ_castSucc
+NewLemma Fin.sum_univ_castSucc
HiddenHint (m : ℕ) :
∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i =>
diff --git a/server/testgame/TestGame/Levels/LeanStuff/L04_InstanceArguments.lean b/server/testgame/TestGame/Levels/LeanStuff/L04_InstanceArguments.lean
index 1522f40..b06d3d2 100644
--- a/server/testgame/TestGame/Levels/LeanStuff/L04_InstanceArguments.lean
+++ b/server/testgame/TestGame/Levels/LeanStuff/L04_InstanceArguments.lean
@@ -49,9 +49,9 @@ Statement
rw [Fin.sum_univ_castSucc (n := m + 1)]
rfl
-OnlyTactics rw rfl
+OnlyTactic rw rfl
-NewLemmas Fin.sum_univ_castSucc
+NewLemma Fin.sum_univ_castSucc
Hint (m : ℕ) :
∑ i : Fin (m + 1), (i : ℕ) + (m + 1) = ∑ i : Fin (Nat.succ m + 1), ↑i =>
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
index e6f93aa..24297d5 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L09_Or.lean
@@ -67,4 +67,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ∧ B) : C ∧ A =>
Hint (A : Prop) (B : Prop) (C : Prop) (h : A → C) : C ∧ A =>
"Ein UND im Goal kann mit `constructor` aufgeteilt werden."
-NewTactics left right assumption constructor rcases
+NewTactic left right assumption constructor rcases
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
index ba06057..1b8393f 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L33_Prime.lean
@@ -20,4 +20,4 @@ Conclusion
"
"
-NewTactics ring
+NewTactic ring
diff --git a/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean b/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
index ce83d69..9abc351 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/L34_ExistsUnique.lean
@@ -20,4 +20,4 @@ Conclusion
"
"
-NewTactics ring
+NewTactic ring
diff --git a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
index 610ec64..be43277 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/Lxx_Prime.lean
@@ -58,4 +58,4 @@ Hint (n : ℕ) (hn : odd n) (h : ∀ (x : ℕ), (odd x) → even (x + 1)) : even
"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
`(x : ℕ) → `"
-NewTactics ring intro unfold
+NewTactic ring intro unfold
diff --git a/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean b/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
index 129c126..061d9a7 100644
--- a/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
+++ b/server/testgame/TestGame/Levels/LeftOvers/xx_Functions.lean
@@ -22,4 +22,4 @@ Statement : ∃ (f : ℕ → ℕ), ∀ (x : ℕ), f x = 0 := by
Conclusion ""
-NewTactics use simp
+NewTactic use simp
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean b/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
index c7fafd9..b471da9 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
+++ b/server/testgame/TestGame/Levels/LinearAlgebra/L01_Module.lean
@@ -62,28 +62,30 @@ Im nachfolgenden beweisen wir die Eigenschaften einzeln.
Statement
"Zeige, dass $\\mathbb{R}$ ein $\\mathbb{Q}$-Modul ist."
- : Module ℚ ℝ :=
- { smul := fun a r ↦ ↑a * r,
- smul_zero := by
- intro a
- rw [smul_zero]
- zero_smul := by
- intro a
- change (0 : ℚ) * a = 0
- simp
- one_smul := by
- intro b
- change (1 : ℚ) * b = b
- rw [Rat.cast_one, one_mul]
- smul_add := by
- intro a x y
- change a * (x + y) = a * x + a * y
- rw [mul_add]
- add_smul := by
- intro r s x
- change (r + s : ℚ) * x = r * x + s * x
- rw [Rat.cast_add, add_mul]
- mul_smul := by
- intro x y b
- change (x * y : ℚ) * b = x * (y * b)
- rw [Rat.cast_mul, mul_assoc]}
+ : Module ℚ ℝ := by
+ refine {
+ smul := fun a r => ↑a * r
+ smul_zero := ?smul_zero
+ zero_smul := ?zero_smul
+ one_smul := ?one_smul
+ smul_add := ?smul_add
+ add_smul := ?add_smul
+ mul_smul := ?mul_smul }
+
+ · intro b
+ change (1 : ℚ) * b = b
+ rw [Rat.cast_one, one_mul]
+ · intro x y b
+ change (x * y : ℚ) * b = x * (y * b)
+ rw [Rat.cast_mul, mul_assoc]
+ · intro a
+ rw [smul_zero]
+ · intro a x y
+ change a * (x + y) = a * x + a * y
+ rw [mul_add]
+ · intro r s x
+ change (r + s : ℚ) * x = r * x + s * x
+ rw [Rat.cast_add, add_mul]
+ · intro a
+ change (0 : ℚ) * a = 0
+ simp
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean b/server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean
index 33848cd..0e77ca7 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean
+++ b/server/testgame/TestGame/Levels/LinearAlgebra/L02_VectorNotation.lean
@@ -72,4 +72,4 @@ Statement
simp <;>
ring
-NewTactics fin_cases funext
+NewTactic fin_cases funext
diff --git a/server/testgame/TestGame/Levels/LinearAlgebra/L08_GeneratingSet.lean b/server/testgame/TestGame/Levels/LinearAlgebra/L08_GeneratingSet.lean
index 46c2cf1..32bc7bd 100644
--- a/server/testgame/TestGame/Levels/LinearAlgebra/L08_GeneratingSet.lean
+++ b/server/testgame/TestGame/Levels/LinearAlgebra/L08_GeneratingSet.lean
@@ -40,4 +40,4 @@ Statement
-- fin_cases i;
-- simp,
---NewLemmas top_le_span_range_iff_forall_exists_fun le_top
+--NewLemma top_le_span_range_iff_forall_exists_fun le_top
diff --git a/server/testgame/TestGame/Levels/Predicate.lean b/server/testgame/TestGame/Levels/Predicate.lean
index c12c91a..d5c4135 100644
--- a/server/testgame/TestGame/Levels/Predicate.lean
+++ b/server/testgame/TestGame/Levels/Predicate.lean
@@ -4,10 +4,24 @@ import TestGame.Levels.Predicate.L03_Rewrite
import TestGame.Levels.Predicate.L04_Ring
import TestGame.Levels.Predicate.L05_Rfl
import TestGame.Levels.Predicate.L06_Exists
-import TestGame.Levels.Predicate.L07_Forall
-import TestGame.Levels.Predicate.L08_PushNeg
-import TestGame.Levels.Predicate.L09_Summary
+import TestGame.Levels.Predicate.L07_Exists
+import TestGame.Levels.Predicate.L08_Forall
+import TestGame.Levels.Predicate.L09_PushNeg
Game "TestGame"
World "Predicate"
Title "Prädikate"
+
+Introduction "Eure Reise geht weiter zum zweiten Mond. Dieser ist etwas grösser und
+komplett mit buschartigen Pflanzen überwachsen. Der Landeanflug sit etwas kniffliger,
+aber offenbar kann Robo nicht nur Lean übersetzen, sondern auch mit maschineller Genauigkeit
+navigieren.
+
+Ihr werdet sofort empfangen und man führt euch zur lokalen Machthaberin.
+Ihr kommt an verschiedensten riesigen Büschen vorbei, die offensichtlich innen Ausgehöhlt sind
+und so als Wände für Behausungen der Wesen hier dienen.
+
+Man führt euch in einen der Büsche. Nun entdecksts du dass das Blätterdach künstlich verstärkt ist,
+offensichtlich um Regen abzuweisen.
+
+Vor euch steht eine Frau, die euch als Machthabering *Evenine* vorgestellt wird."
diff --git a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
index 52d5908..ca8b143 100644
--- a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean
@@ -11,34 +11,26 @@ Title "Natürliche Zahlen"
Introduction
"
-Wir sind den narürlichen Zahlen `ℕ` (`\\N`) schon kurz begegnet.
+**Evenine**: Willkommen Reisende! Wir leben hier in Einklang mit der Natur und allem natürlichen,
+so sagt mir, könnt ihr mit natürlichen Zahlen umgehen?
+"
-Gleichungen, die nur die Operationen `+, -, *, ^` (Addition, Subtraktion, Multiplikation, Potenz)
-und Variablen enthalten, kann Lean mit der Taktik `ring` beweisen.
+Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
+ Hint "**Du**: Das hab ich in der Schule gelernt, man rechnet das einfach aus,
+ indem man die Terme umsortiert.
-Diese Taktik funktioniert nicht nur über den natürlichen Zahlen,
-sondern auch in (kommutativen) Gruppen, Ringen, und Körpern. Sie heisst `ring`, weil sie für Ringe
-entwickelt wurde.
+ **Robo**: Behaupte doch mit `ring`, dass das so ist.
-(Note: Division `/` ignorieren wir hier erst einmal, weil diese auf `ℕ`
-nicht kanonisch definiert ist.)
-"
+ **Du**: Aber `ℕ` ist doch gar kein Ring?
-Statement
- "Zeige $(x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2$."
- (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by
+ **Robo**: `ring` funktioniert schon für Halbringe, aber sie heisst ring, weil sie auf
+ (kommutativen) Ringen am besten funktioniert.
+ "
ring
-HiddenHint (x : ℕ) (y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 =>
-"`ring` übernimmt den ganzen Spaß."
-
Conclusion
"
-Die Taktik heisst übrigens `ring` weil sie dafür entwickelt wurde, Gleichungen in einem abstrakten
-Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist
-(erst `ℤ` ist ein Ring).
+*Evenine: Ja das stimmt schon. Und das genügt uns auf diesem Planet auch als Antwort.*
"
-NewTactics ring
-
-#eval 4 / 6
+NewTactic ring
diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
index defa2fa..a45d6cf 100644
--- a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean
@@ -9,62 +9,31 @@ Title "Rewrite"
Introduction
"
-Wir haben gesehen, dass man mit `rw` Äquivalenzen wie `A ↔ B` brauchen kann, um im Goal
-$A$ durch $B$ zu ersetzen.
+Robo spuckt den Brief aus, den er dabei hatte, und gibt ihn *Evenine*.
-Genau gleich kann man auch Gleichungen `a = b` mit `rw` verwenden.
+**Evenine**: Das verstehe ich nicht, wisst ihr was damit gemeint ist?
+
+Und sie händigt Dir den Brief:
"
-Statement umschreiben
-"Angenommen man hat die Gleichheiten
+Statement (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+ Hint "**Du**: Schau mal, das ist ja fast genau, was wir auf *Implis* gemacht haben,
+ nur jetzt mit Gleichheiten von Zahlen anstatt Genau-Dann-Wenn-Aussagen!
-$$
-\\begin{aligned} a &= b \\\\ a &= d \\\\ c &= d \\end{aligned}
-$$
+ **Robo**: `=` und `↔` kannst du praktisch gleich behandeln wenns um `rw` geht."
+ Hint (hidden := true) "**Du**: Also auch `rw [hₓ]` und `rw [← hₓ]`?
-Zeige dass $b = c$."
-(a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c := by
+ **Robo**: Probiers doch einfach."
rw [h₁]
+ Hint (hidden := true) "**Du**: Wie war das nochmals mit rückwärts umschreiben?
+
+ **Robo**: `←` ist `\\l`. Und dann `rw [← hₓ]`"
rw [←h₂]
assumption
-HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c =>
-"Im Goal kommt `c` vor und `h₁` sagt `c = d`.
-Probiers doch mit `rw [h₁]`."
-
-HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : a = c =>
-"Im Goal kommt `C` vor und `h₁` sagt `C ↔ D`.
-Probiers doch mit `rw [h₁]`."
-
-HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = d =>
-" Man kann auch rückwärts umschreiben: `h₂` sagt `a = b` mit
-`rw [←h₂]` ersetzt man im Goal `b` durch `a` (`\\l`, also ein kleines L)"
-
-HiddenHint (a : ℕ) (b : ℕ) (h : a = b) : a = b =>
-"Schau mal durch die Annahmen durch."
-
-
-
--- These should not be necessary if they don't use `rw [] at`.
-HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = c) : b = c =>
-"Auch eine Möglichkeit... Kannst du das Goal so umschreiben,
-dass es mit einer Annahme übereinstimmt?"
-
-HiddenHint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : b = d) : b = c =>
-"Auch eine Möglichkeit.. Kannst du das Goal so umschreiben, dass es mit einer Annahme übereinstimmt?"
-
-Hint (a : ℕ) (b : ℕ) (h : b = a) : a = b =>
-"Naja auch Umwege führen ans Ziel... Wenn du das Goal zu `a = a` umschreibst, kann man es mit
-`rfl` beweisen (rsp. das passiert automatisch.)"
-
-Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : d = a) : b = c =>
-"das ist nicht der optimale Weg..."
-
-Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ : a = d) : b = c =>
-"das ist nicht der optimale Weg..."
-
-
-
-Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen."
+Conclusion
+"
+**Evenine**: Danke viemals, das hilft uns vermutlich, jetzt Frage ich mich aber…
+"
-NewTactics assumption rw
+NewTactic assumption rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
index 2320b54..be4df47 100644
--- a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean
@@ -9,32 +9,28 @@ Title "Rewrite"
Introduction
"
-Als Übung erinnern wir daran, dass man mit `rw [h] at g` auch in anderen Annahmen umschreiben
-kann:
-
-Wenn `(h : X = Y)` ist, dann ersetzt `rw [h] at g` in der Annahme
-`g` das `X` durch `Y`.
+**Evenine**: Mit diesem neuen Wissen, könnt ihr mir bei folgendem helfen:
"
-Statement umschreiben
-"Angenommen man hat die Gleichheiten
-
+Statement
+"
$$
-\\begin{aligned} a &= b \\\\ a + a ^ 2 &= b + 1 \\end{aligned}
+\\begin{aligned}
+ a &= b \\\\
+ a + a ^ 2 &= b + 1 \\\\
+ \\vdash b + b ^ 2 = b + 1
+\\end{aligned}
$$
-
-Zeige dass $b + b ^ 2 = b + 1$."
+"
(a b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 := by
+ Hint "**Du**: Ah da ersetzt man ja einfach `{a}` durch `{b}` in der anderen Annahme!
+
+ **Robo**: Genau! Das machst du mit `rw [{h}] at {g}`."
rw [h] at g
+ Hint (hidden := true) "**Robo**: Schau mal durch die Annahmen."
assumption
-Hint (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : b + b ^ 2 = b + 1 =>
-"`rw [ ... ] at g` schreibt die Annahme `g` um."
-
-Hint (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1 =>
-"Sackgasse. probiers doch mit `rw [h] at g` stattdessen."
-
-Conclusion "Übrigens, mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
-dem Goal umschreiben."
-
-NewTactics assumption rw
+Conclusion "
+**Robo**: Noch ein Trick: Mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und
+dem Goal umschreiben.
+"
diff --git a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
index 3d1f19d..60291dc 100644
--- a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean
@@ -9,25 +9,27 @@ Title "Natürliche Zahlen"
Introduction
"
-Oft braucht man eine Kombination von `rw` und `ring` um Gleichungen zu lösen.
+*Evenines* Berater meldet sich.
-Zuerst setzt man mit `rw` die vorhandenen Annahmen ein, und sobald die beiden Seiten
-einer Gleichung im Goal rechnerisch gleich sind, kan `ring` dies beweisen.
+**Berater**: Das stimmt wohl, aber das Problem, das uns eigentlich beschäftigt hat, eure
+Natürlichkeit, war folgendes:
"
Statement
- "Angenommen, man hat die Gleichung $x = 2 * y + 1$, zeige
- $x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y$. "
- (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by
- rw [h]
- ring
+ (x y z : ℕ) (h : x = 2 * y + 1) (g : z = 3 * y + 1): x ^ 2 = 4 * y ^ 2 + z + y := by
+ Hint "**Du**: Ich versteh das Pattern. Wenn ich zuerst alles so umschreibe, dass
+ das Goal nur noch rechnen und umsortieren ist, dann kann `ring` den Rest machen!
-Hint (x : ℕ) (y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
- "Die Annahme `h` kannst du mit `rw [h]` benützen."
+ **Robo**: Noch ein Trick: Entweder kannst du zwei Befehle `rw [h₁]` und `rw [h₂]` schreiben,
+ oder du kannst das gleich in einem machen : rw [h₁, h₂]."
+ rw [h, g]
+ ring
-Hint (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y =>
- "Jetzt kann `ring` übernehmen."
-Conclusion ""
+Conclusion
+"
+*Evenine* bedankt sich nochmals für die Botschaft und ihr werdet zu einem kleineren Busch geführt,
+der ein gemütlich warmes Innenleben an den Tag legt.
+"
-NewTactics ring rw
+NewTactic ring rw
diff --git a/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
index 32ecad3..e621f96 100644
--- a/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean
@@ -8,24 +8,29 @@ Title "Definitionally equal"
Introduction
"
-Als kleine Nebenbemerkung:
+Müde ruht ihr euch in eurer Bleibe aus. Du schaust doch eine Lücke in den Blättern vielen
+kleinen Vögeln bei der Nahrungssuche zu.
-Auf Grund der Implementation in Lean brauchst du die Taktik `ring` gar nicht, wenn
-du Gleichungen über `ℕ` hast, die keine Variablen enthalten:
-
-So ist zum Beispiel `2` als `1 + 1` definiert, deshalb kannst du $1 + 1 = 2$ einfach mit
-`rfl` beweisen.
+**Du**: Sag mal Robo, ich hab vorhin ein Kind überhört, dass seinem Spielgefährten erklärt hat,
+folgendes sei mit `rfl` zu beweisen:
"
-Statement
-"Zeige dass $1 + 1$ zwei ist." :
- 1 + 1 = 2 := by
+Statement : 1 + 1 = 2 := by
+ Hint "**Du**: Wieso nicht `ring`?
+
+ **Robo**: Klar, `ring` geht auch und ist intuitiver.
+ Für `rfl` kommt es darauf an, wie die Sachen genau definiert sind: `1 + 1` ist als
+ `(0.succ).succ` definiert und `2` halt ebenfalls.
+ "
rfl
+OnlyTactic rfl
+
Conclusion
"
-**Notiz:** Die meisten anderen Taktiken versuchen am Schluss automatisch `rfl`
-aufzurufen, deshalb brauchst du das nur noch selten.
-"
+**Du**: Dann war das mehr Glück?
+
+**Robo**: Das ist eine Art die Welt zu sehen…
-NewTactics rfl
+Damit fällst du in einen ruhigen Schlaf.
+"
diff --git a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
index 196c372..79fd82b 100644
--- a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
+++ b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean
@@ -6,6 +6,8 @@ import Mathlib.Tactic.Ring
import Mathlib.Algebra.Parity
+set_option tactic.hygienic false
+
Game "TestGame"
World "Predicate"
Level 6
@@ -14,58 +16,58 @@ Title "Gerade/Ungerade"
Introduction
"
-Gerade/ungerade werden in Lean wie folgt definiert:
+Am nächsten Tag erklärt euch *Evenine*, dass es auf dem Mond zwei Gruppierungen gibt,
+ihre und die ihres Halbbruders *Oddeus*. Die Mottos sind
+
```
def Even (n : ℕ) : Prop := ∃ r, n = r + r
-def Odd (n : ℕ) : Prop := ∃ r, n = r + r + 1
```
-Also dadurch, dass ein `(r : ℕ)` existiert sodass `n = r + r (+1)`.
-Beachte das Komma `,` welches die Variablen des `∃` (`\\exists`) von der Aussage trennen.
-
-Hierzu gibt es 3 wichtige Taktiken:
-
-1) Definitionen wie `Even` kann man mit `unfold Even at *` im Infoview einsetzen.
- Das ändert Lean-intern nichts und ist nur für den Benutzer. Man kann auch einen
- Term `(h : Even x)` einfach so behandeln als wäre es ein Term `(h : ∃ r, x = 2 * r)`.
-2) Bei einer Annahme `(h : ∃ r, ...)` kann man mit `rcases h with ⟨y, hy⟩` ein solches `y`
- Auswählen, dass die Annahme `h` erfüllt.
-3) Bei einem `∃` im Goal muss man ein Element `y` angeben, welches diese Aussage erfüllen
- soll. Das macht man mit `use y`
+
+und
+
+```
+def Odd (n : ℕ) : Prop := ∃ r, n = 2 * r + 1
+```
+
+**Evenine**: Hier, ich zeige euch mal etwas was man bei uns machen kann:
"
-Statement even_square
- "Wenn $n$ gerade ist, dann ist $n^2$ gerade."
- (n : ℕ) (h : Even n) : Even (n ^ 2) := by
+Statement even_square (n : ℕ) (h : Even n) : Even (n ^ 2) := by
+ Branch
+ unfold Even
+ Hint "Rob**: Am besten machst du auch noch `unfold Even at h`, damit du verstehst was los ist."
+ Hint "**Robo**: Wie du oben siehst, ist `Even n` dadurch definiert,
+ dass ein `r` existiert so dass `r + r = n`. Am besten
+ öffnest du diese Definition mit `unfold Even at *` einmal, dann siehst du besser, was los ist. "
unfold Even at *
- rcases h with ⟨x, hx⟩
- use 2 * x ^ 2
- rw [hx]
- ring
+ Hint "**Du**: Also von `{h}` weiss ich jetzt dass ein `r` existiert, so dass `r + r = n`…
-Hint (n : ℕ) (h : Even n) : Even (n ^ 2) =>
-"Wenn du die Definition von `Even` nicht kennst, kannst du diese mit `unfold Even` oder
-`unfold Even at *` ersetzen.
-Note: Der Befehl macht erst mal nichts in Lean sondern nur in der Anzeige. Der Beweis funktioniert
-genau gleich, wenn du das `unfold` rauslöscht."
+ **Robo**: Mit `rcases h with ⟨r, hr⟩` kannst du dieses `r` tatsächlich einführen."
+ rcases h with ⟨r, hr⟩
+ Hint "**Du**: Und jetzt muss ich eine passende Zahl finden, so dass `x + x = n^2`?
-Hint (n : ℕ) (h : ∃ r, n = r + r) : ∃ r, n ^ 2 = r + r =>
-"Ein `∃ x, ..` in den Annahmen kann man wieder mit `rcases h with ⟨x, hx⟩` aufteilen, und
-ein `x` erhalten, dass die Aussage erfüllt."
+ **Robo**: Genau. Und mit `use _` gibst du diese Zahl an."
+ Hint (hidden := true) "**Robo**: Also sowas ähnliches wie `use 4 * r ^ 3`, aber ich kann
+ dir leider nicht sagen, welche Zahl passt.
+ "
+ Branch
+ rw [hr]
+ Hint "**Robo**: Das geht auch, jetzt musst du aber wirklich `use` verwenden."
+ use 2 * r ^ 2
+ ring
+ use 2 * r ^ 2
+ Hint "**Du**: Ah und jetzt `ring`!
-Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, n ^ 2 = r + r =>
-"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
-die Aussage erfüllen soll."
-
-Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : ∃ r, (x + x) ^ 2 = r + r =>
-"Bei einem `∃ x, ..` im Goal hingegen, muss man mit `use y` das Element angeben, dass
-die Aussage erfüllen soll."
+ **Robo**: Aber zuerst must du noch mit
+ `rw` `n` durch `r + r` ersetzen, da `ring` das sonst nicht weiss."
+ rw [hr]
+ ring
-Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
-"Prinzipiell löst `ring` simple Gleichungen wie diese. Allerdings musst du zuerst `n` zu
-`x + x` umschreiben..."
+-- TODO: [Comment] For me the expected behaviour of `(strict := true)` would
+-- be that it distinguishes between the defEq states while `(strict := false)`
+-- would show the hint regardless of a `unfold Even`.
-Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 =>
-"Die Taktik `ring` löst solche Gleichungen."
+NewTactic unfold use
+NewDefinition Even Odd
-NewTactics unfold rcases use rw ring
-NewDefinitions Even Odd
+Conclusion "**Evenine**: Seht ihr?"
diff --git a/server/testgame/TestGame/Levels/Predicate/L07_Exists.lean b/server/testgame/TestGame/Levels/Predicate/L07_Exists.lean
new file mode 100644
index 0000000..26bb955
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Predicate/L07_Exists.lean
@@ -0,0 +1,43 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Mathlib.Algebra.Parity
+
+set_option tactic.hygienic false
+
+Game "TestGame"
+World "Predicate"
+Level 7
+
+Title "Gerade/Ungerade"
+
+Introduction
+"
+**Du**: Aber, das sagt doch gar nichts aus, genau das gleiche könnte ich für `Odd`
+auch sagen. Hier seht!
+"
+
+Statement odd_square (n : ℕ) (h : Odd n) : Odd (n ^ 2) := by
+ unfold Odd at *
+ rcases h with ⟨r, hr⟩
+ Hint "**Robo**: Ich hab noch einen Trick auf Lager:
+ Wenn du jetzt herausfinden willst, welche Zahl du einsetzen musst, könntest
+ du schon jetzt mit `rw [{hr}]` weitermachen…"
+ rw [hr]
+ Hint "**Robo**: Wenn du jetzt `ring` benötigst, dann schreibt es einfach alles in
+ Normalform um, das hilft beim vergleichen."
+ ring
+ Hint "**Du**: Was bedeutet `ring_nf`?
+
+ **Robo**: Wenn man `ring` nicht am Schluss benützt, sollte man stattdessen `ring_nf`
+ schreiben, aber die funktionieren praktisch gleich."
+ use 2 * (r + r ^ 2)
+ ring
+
+-- TODO: Allow `ring_nf` as part of `ring`.
+
+Conclusion "**Evenine**: Tatsächlich. Vielleicht sind wir gar nich tso unterschiedlich. Könntet
+ihr mal mit ihm reden gehen?"
diff --git a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
deleted file mode 100644
index 5e1b812..0000000
--- a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean
+++ /dev/null
@@ -1,53 +0,0 @@
-import TestGame.Metadata
-import Std.Tactic.RCases
-import Mathlib.Tactic.Contrapose
-import Mathlib.Tactic.Use
-import Mathlib.Tactic.Ring
-
-import Mathlib.Algebra.Parity
-import Mathlib
-
-Game "TestGame"
-World "Predicate"
-Level 7
-
-Title "Für alle"
-
-Introduction
-"
-Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
-
-Der Syntax ist `∀ (n : ℕ), 0 ≤ n` also wie beim `∃` trennt ein Komma die Annahmen von der Aussage.
-
-Eine `∀`-Aussage in den Annahmen verhält sich so wie ein Lemma. Das heisst man kann
-auch diese mit `apply` und `rw` anwenden, je nachdem was die Aussage nach dem Komma ist.
-
-Also folgende Annahme und Lemma sind genau :
-- `(le_square : ∀ (n : ℕ), n ≤ n^2)`
-- `lemma le_square (n : ℕ) : n ≤ n^2`
-
-Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
-
-
-TODO: 1-2 Aufgaben mehr.
-"
-
-Statement
- " Für alle natürlichen Zahlen $x$ gilt, falls $x$ gerade ist, dann ist $x + 1$
- ungerade." : ∀ (x : ℕ), (Even x) → Odd (1 + x) := by
- intro x h
- unfold Even at h
- unfold Odd
- rcases h with ⟨y, hy⟩
- use y
- rw [hy]
- ring
-
-Hint (n : ℕ) (hn : Odd n) (h : ∀ (x : ℕ), (Odd x) → Even (x + 1)) : Even (n + 1) =>
-"`∀ (x : ℕ), (odd x) → even (x + 1)` ist eigentlich das gleiche wie
-`(x : ℕ) → `"
-
-Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle
-praktisch gleich. Mehr dazu später."
-
-NewTactics ring intro unfold
diff --git a/server/testgame/TestGame/Levels/Predicate/L08_Forall.lean b/server/testgame/TestGame/Levels/Predicate/L08_Forall.lean
new file mode 100644
index 0000000..ff581b2
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Predicate/L08_Forall.lean
@@ -0,0 +1,53 @@
+import TestGame.Metadata
+import Std.Tactic.RCases
+import Mathlib.Tactic.Contrapose
+import Mathlib.Tactic.Use
+import Mathlib.Tactic.Ring
+
+import Mathlib.Algebra.Parity
+import Mathlib
+
+Game "TestGame"
+World "Predicate"
+Level 8
+
+Title "Für alle"
+
+Introduction
+"
+Ihr macht euch also auf den Weg. Unterwegs trefft ihr einen Händler und ihr lässt euch von
+ihm den Weg zeigen, sowie einige Tipps zu den beiden Geschwistern geben.
+
+**Händler**: Also seht, die beiden sind gar nicht so verschieden. Ein altes Sprichwort sagt:
+"
+
+-- Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`).
+
+-- Der Syntax ist `∀ (n : ℕ), 0 ≤ n` also wie beim `∃` trennt ein Komma die Annahmen von der Aussage.
+
+-- Eine `∀`-Aussage in den Annahmen verhält sich so wie ein Lemma. Das heisst man kann
+-- auch diese mit `apply` und `rw` anwenden, je nachdem was die Aussage nach dem Komma ist.
+
+-- Also folgende Annahme und Lemma sind genau :
+-- - `(le_square : ∀ (n : ℕ), n ≤ n^2)`
+-- - `lemma le_square (n : ℕ) : n ≤ n^2`
+
+-- Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`.
+
+
+-- TODO: 1-2 Aufgaben mehr.
+
+Statement : ∀ (x : ℕ), (Even x) → Odd (1 + x) := by
+ Hint "**Du**: Das `∀` heisst sicher \"für alle\".
+
+ **Robo**: Und man schreibt `\\forall`. Ein `∀ x, …` im Goal kannst du wie eine
+ Implikation mit `intro x` angehen."
+ intro x h
+ unfold Even at h
+ unfold Odd
+ rcases h with ⟨y, hy⟩
+ use y
+ rw [hy]
+ ring
+
+Conclusion "**Händler**: Sichere Reise!"
diff --git a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
deleted file mode 100644
index 3f14063..0000000
--- a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean
+++ /dev/null
@@ -1,67 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.PushNeg
-import Mathlib
-
-import Mathlib.Algebra.Parity
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Predicate"
-Level 8
-
-Title "PushNeg"
-
-Introduction
-"
-Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man
-mit `push_neg` das `¬` durch den Quantor hindurchschieben.
-
-Das braucht intern die Lemmas
-
-- `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)`
-- `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)`
-
-(welche man auch mit `rw` explizit benutzen könnte.)
-"
-
-Statement
- "Es existiert keine natürliche Zahl $n$, sodass $n + k$ immer ungerade ist.":
- ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
- push_neg
- intro n
- use n
- rw [not_odd]
- unfold Even
- use n
-
-Hint : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) =>
-"`push_neg` schiebt die Negierung an den Quantoren vorbei."
-
-
-Hint (n : ℕ) : (∃ k, ¬Odd (n + k)) =>
-"An dieser Stelle musst du nun ein `k` angeben, sodass `n + k` gerade ist... Benutze `use`
-mit der richtigen Zahl."
-
-
-HiddenHint (n : ℕ) : ¬Odd (n + n) =>
-"Du kennst ein Lemma um mit `¬odd` umzugehen."
-
--- HiddenHint (n : ℕ) (k : ℕ) : ¬odd (n + k) =>
--- "Du kennst ein Lemma um mit `¬odd` umzugehen."
-
-HiddenHint (n : ℕ) : Even (n + n) =>
-"`unfold even` hilft, anzuschauen, was hinter `even` steckt.
-
-Danach musst du wieder mit `use r` ein `(r : ℕ)` angeben, dass du benützen möchtest."
-
--- HiddenHint (n : ℕ) (k : ℕ) : even (n + k) =>
--- "`unfold even` hilft hier weiter."
-
-Hint (n : ℕ) : n + n = 2 * n => "Recap: `ring` löst Gleichungen in `ℕ`."
-
-Conclusion ""
-
-NewTactics push_neg intro use rw unfold ring
-NewDefinitions Even Odd
-NewLemmas not_even not_odd not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean
new file mode 100644
index 0000000..9eeab66
--- /dev/null
+++ b/server/testgame/TestGame/Levels/Predicate/L09_PushNeg.lean
@@ -0,0 +1,109 @@
+import TestGame.Metadata
+import Mathlib.Tactic.PushNeg
+import Mathlib
+
+import Mathlib.Algebra.Parity
+
+import TestGame.ToBePorted
+
+Game "TestGame"
+World "Predicate"
+Level 9
+
+Title "PushNeg"
+
+Introduction
+"
+Das Dorf von *Oddeus* scheint stärker befestigt zu sein, all jenes von *Evenine*. Ihr kommt
+and eine Wand aus Dornenranken. Beim Eingang steht eine Wache, die auch zuruft:
+
+"
+
+-- Zum Schluss, immer wenn man irgendwo eine Verneinung `¬∃` oder `¬∀` sieht (`\\not`), kann man
+-- mit `push_neg` das `¬` durch den Quantor hindurchschieben.
+
+-- Das braucht intern die Lemmas
+
+-- - `not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)`
+-- - `not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)`
+
+-- (welche man auch mit `rw` explizit benutzen könnte.)
+
+open Nat
+
+Statement : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , Odd (n + k) := by
+ Hint "**Du**: Also ich kann mal das `¬` durch die Quantifier hindurchschieben.
+
+ **Robo**: `push_neg` macht genau das!
+
+ **Robo**: Intern braucht das zwei Lemmas
+
+ ```
+ not_exists (A : Prop) : ¬ (∃ x, A) ↔ ∀x, (¬A)
+ not_forall (A : Prop) : ¬ (∀ x, A) ↔ ∃x, (¬A)
+ ```
+ die du natürlich auch mit `rw` gebrauchen könntest."
+ Branch
+ unfold Odd
+ push_neg
+ Hint "**Robo**: Der Weg ist etwas schwieriger. Ich würde nochmals zurück und schauen,
+ dass du irgendwann `¬Odd` kriegst, was du dann mit `rw [←even_iff_not_odd]`
+ zu `Even` umwandeln.
+ kannst."
+ push_neg
+ intro n
+ Hint "**Robo**: Welche Zahl du jetzt mit `use` brauchst, danach wirst du vermutlich das
+ Lemma `←even_iff_not_odd` brauchen.
+
+ **Du**: Könnte ich jetzt schon `rw [←even_iff_not_odd]` machen?
+
+ **Robo**: Ne, `rw` kann nicht innerhalb von Quantifiern umschreiben.
+
+ **Du**: Aber wie würde ich das machen?
+
+ **Robo**: Zeig ich dir später, die Wache wird schon ganz ungeduldig!
+ Im Moment würde ich zuerst mit `use` eine richtige Zahl angeben, und danach umschreiben."
+ Branch
+ use n + 2
+ Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
+ Branch
+ use n + 4
+ Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
+ use n
+ Hint "**Robo**: Gute Wahl! Jetzt kannst du `←even_iff_not_odd` verwenden."
+ rw [←even_iff_not_odd]
+ unfold Even
+ use n
+ --ring
+
+Conclusion "Damit werdet ihr eingelassen.
+
+**Robo**: Entweder wir suchen direkt diesen *Oddeus*, oder wir schauen uns einmal um. Die Wahl
+ist deine!
+
+**Du**: Kannst du mir nochmals einen Überblick geben, was wir gelernt haben?
+
+**Robo**:
+
+| | Beschreibung |
+|:--------------|:----------------------------|
+| `ℕ` | Die natürlichen Zahlen. |
+| `∃` | Existential-Quantifier |
+| `∀` | Forall-Quantifier |
+| `Even n` | `n` ist gerade |
+| `Odd n` | `n` ist ungerade |
+
+| | Taktik | Beispiel |
+|:------|:--------------------------|:-------------------------------------------------------|
+| *12ᶜ* | `rw` | Umschreiben mit Gleichungen. |
+| 13 | `ring` | Löst Gleichungen mit `+, -, *, ^`. |
+| 14 | `unfold` | Setzt visuell die Bedeutung einer Definition ein. |
+| 15 | `use` | Um ein `∃` im Goal anzugehen. |
+| *7ᶜ* | `rcases h with ⟨x, hx⟩` | Um ein `∃` in den Annahmen zu zerlegen. |
+| *8ᵇ* | `intro` | Um ein `∀` im Goal anzugehen. |
+| 16 | `push_neg` | Für `¬∃` und `¬∀` im Goal. |
+
+"
+
+NewTactic push_neg
+NewLemma even_iff_not_odd odd_iff_not_even not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
deleted file mode 100644
index 2cb1a6c..0000000
--- a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean
+++ /dev/null
@@ -1,55 +0,0 @@
-import TestGame.Metadata
-import Mathlib.Tactic.PushNeg
-import Mathlib
-
-import TestGame.ToBePorted
-
-Game "TestGame"
-World "Predicate"
-Level 9
-
-Title "Zusammenfassung"
-
-Introduction
-"
-Damit bist du am Ende der dritten Lektion angekommen.
-Hier ein Überblick über alles was in diesem Kapitel eingeführt wurde und eine
-Abschlussaufgabe.
-
-## Notationen / Begriffe
-
-| | Beschreibung |
-|:--------------|:----------------------------|
-| `ℕ` | Die natürlichen Zahlen. |
-| `∃` | Existential-Quantifier |
-| `∀` | Forall-Quantifier |
-| `Even n` | `n` ist gerade |
-| `Odd n` | `n` ist ungerade |
-
-
-## Taktiken
-
-| | Taktik | Beispiel |
-|:------|:--------------------------|:-------------------------------------------------------|
-| *11ᶜ* | `rw` | Umschreiben mit Gleichungen. |
-| 12 | `ring` | Löst Gleichungen mit `+, -, *, ^`. |
-| 13 | `unfold` | Setzt visuell die Bedeutung einer Definition ein. |
-| 14 | `use` | Um ein `∃` im Goal anzugehen. |
-| *7ᶜ* | `rcases h with ⟨x, hx⟩` | Um ein `∃` in den Annahmen zu zerlegen. |
-| *8ᵇ* | `intro` | Um ein `∀` im Goal anzugehen. |
-| 15 | `push_neg` | Für `¬∃` und `¬∀` im Goal. |
-
-Als Abschlussübung kannst du folgende Äquivalenz zeigen:
-
-"
-
-Statement
- "TODO":
- True := by
- trivial
-
-Conclusion ""
-
-NewTactics push_neg intro use rw unfold ring
-NewDefinitions Even Odd
-NewLemmas not_even not_odd not_exists not_forall
diff --git a/server/testgame/TestGame/Levels/Prime/L04_Prime.lean b/server/testgame/TestGame/Levels/Prime/L04_Prime.lean
index 0721407..9256544 100644
--- a/server/testgame/TestGame/Levels/Prime/L04_Prime.lean
+++ b/server/testgame/TestGame/Levels/Prime/L04_Prime.lean
@@ -43,4 +43,4 @@ Statement
rcases h with ⟨_, h₂⟩
assumption
-NewLemmas Nat.prime_def_lt''
+NewLemma Nat.prime_def_lt''
diff --git a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
index 81f412d..75a5ec7 100644
--- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean
@@ -21,24 +21,20 @@ Du siehst Robo hilflos an.
Statement ""
(A B C : Prop) :
¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) := by
- tauto
-
-Hint (A B C : Prop) :
- ¬((¬B ∨ ¬ C) ∨ (A → B)) → (¬A ∨ B) ∧ ¬ (B ∧ C) =>
- "**Robo** Das ist ganz einfach. Mit `{A} {B} {C} : Prop` meint sie:
- `{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*).
- Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
+ Hint "**Robo** Das ist ganz einfach. Mit `{A} {B} {C} : Prop` meint sie:
+ `{A}`, `{B}` und `{C}` sind irgendwelche Aussagen (*propositions*).
+ Und mit `→` meint sie ⇒, also “impliziert”. Die anderen Symbole kennst Du, oder?
-**Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
+ **Du** Ehhm, ja. Aber da muss ich jetzt trotzdem erst einmal überlegen.
-**Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
+ **Robo** (flüsternd) Behaupte doch einfach, dass sei eine Tautologie.
-**Du** Ernsthaft?
+ **Du** Ernsthaft?
-**Robo** Ja. Schreib einfach `tauto`.
+ **Robo** Ja. Schreib einfach `tauto`.
-**Robo** Mach schon …
-"
+ **Robo** Mach schon …"
+ tauto
Conclusion
"
@@ -47,4 +43,4 @@ Aber glaubt bloß nicht, dass Ihr damit auf *diesem* Planeten viel weiterkommt!
Meine Untertanen verstehen `tauto` nicht. Da müsst Ihr Euch schon etwas mehr anstrengen.
"
-NewTactics tauto
+NewTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
index 9b723b3..3c56590 100644
--- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean
@@ -19,17 +19,14 @@ Er schreibt es Dir wieder auf.
Statement "" :
42 = 42 := by
+ Hint " **Robo** Ist doch klar. Du musst ihn einfach daran erinnern,
+ dass Gleichheit *reflexiv* ist. Probier mal `rfl`."
rfl
-Hint : 42 = 42 => "
-**Robo** Ist doch klar. Du musst ihn einfach daran erinnern, dass Gleichheit *reflexiv* ist.
-Probier mal `rfl`.
-"
-
Conclusion
"
**Untertan** Ah, richtig. Ja, Sie haben ja so recht. Das vergesse ich immer. Rfl, rfl, rfl …
"
-NewTactics rfl
-DisabledTactics tauto
+NewTactic rfl
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
index c019f3f..e75e141 100644
--- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean
@@ -13,9 +13,7 @@ Während der erste Untertan noch rfl, rfl, rfl murmelt, tritt schon der nächste
Statement ""
(n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n := by
- assumption
-
-Hint (n : ℕ) (h₁ : 10 > n) (h₂ : 1 < n) (h₃ : n ≠ 5) : 1 < n => "
+ Hint "
**Robo** `{n} : ℕ` bedeutet, `{n}` ist eine natürliche Zahl.
**Du** Warum schreibt er dann nicht `{n} ∈ ℕ`??
@@ -32,8 +30,8 @@ für die Annahme `n < 10`, `1 < n` und `n ≠ 5`. Beweisen sollen wir: `1 < n`.
**Du** ???
-**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`.
-"
+**Robo** Du musst ihm das halt explizit sagen. Probiers mal mit `assumption`."
+ assumption
Conclusion
"
@@ -41,5 +39,5 @@ Conclusion
zerbrochen habe!
"
-NewTactics assumption
-DisabledTactics tauto
+NewTactic assumption
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
index 714ca94..7a177eb 100644
--- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean
@@ -14,9 +14,7 @@ Ein dritter Untertan kommt mit folgendem Problem.
Statement ""
(A : Prop) (hA : A) : A := by
- assumption
-
-Hint (A : Prop) (hA : A) : A => "
+ Hint "
**Robo** Hier bedeutet `{A} : Prop` wieder, dass `{A}` irgendeine Aussage ist.
Und `{hA}` ist eine Name für die Annahme, dass `{A}` wahr ist.
@@ -24,15 +22,15 @@ Hint (A : Prop) (hA : A) : A => "
**Robo** Ja. Da kommst Du jetzt selbst drauf, wie das geht, oder?
"
-
-HiddenHint (A : Prop) (hA : A) : A =>
-"Ist doch genau wie eben: die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen.
+ Hint (hidden := true) "Ist doch genau wie eben:
+die Aussage, die zu beweisen ist, gehört selbst zu den Annahmen.
Also wird `asumption` auch wieder funktionieren."
+ assumption
Conclusion
"
**Untertan** Das ging ja schnell. Super! Vielen Dank.
"
-NewTactics assumption
-DisabledTactics tauto
+NewTactic assumption
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L04_True.lean b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
index 97de4d3..0549e7c 100644
--- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean
@@ -11,11 +11,8 @@ Introduction
Der nächste Untertan in der Reihe ist ein Schelm.
"
-Statement "" :
-True := by
- trivial
-
-Hint : True => "
+Statement "" : True := by
+ Hint "
**Robo** Dieses `True` ist eine spezielle Aussage, nämlich die Aussage, die immer und
bedingungslos wahr ist.
@@ -23,6 +20,7 @@ bedingungslos wahr ist.
**Robo** Ich glaube, nichts. Ich glaube, Du kannst einfach `trivial` schreiben.
"
+ trivial
Conclusion
"
@@ -35,5 +33,5 @@ Wie in einer Mathe-Vorlesung?
Das funktioniert nur in einer Handvoll Situationen.
"
-NewTactics trivial
-DisabledTactics tauto
+NewTactic trivial
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
index 3800549..dc1d413 100644
--- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean
@@ -11,27 +11,24 @@ Introduction
Der Schelm hat noch eine Schwester dabei.
"
-Statement "" :
- ¬False := by
- trivial
-
-Hint : ¬False => "
- **Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)`
- wahr ist, dann ist `¬A` falsch, und umgekehrt.
+Statement "" : ¬False := by
+ Hint "
+**Robo** Dieses Zeichen `¬` bedeutet Negation. Also wenn eine Aussage `(A : Prop)`
+wahr ist, dann ist `¬A` falsch, und umgekehrt.
- **Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist?
+**Du** Und `False` ist wahrscheinlich die Aussage, die immer falsch ist?
- **Robo** Ja, richtig.
+**Robo** Ja, richtig.
- **Du** Ist das jetzt nicht doch wieder trivial?
+**Du** Ist das jetzt nicht doch wieder trivial?
- **Robo** Probier mal!
-"
+**Robo** Probier mal!"
+ trivial
Conclusion
"
Die Schwester lacht und eilt ihrem Bruder hinterher.
"
-NewTactics trivial
-DisabledTactics tauto
+NewTactic trivial
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L06_False.lean b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
index 151e025..27d0da1 100644
--- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean
@@ -15,12 +15,8 @@ Als nächstes kommen drei Querulanten. Der erste hat folgendes Problem:
Statement ""
(A : Prop) (h : False) : A := by
- contradiction
-
-Hint (A : Prop) (h : False) : A =>
-"
-**Du** Wenn ich das jetzt richtig lese, ist `{A}` eine Aussage, und wir haben außerdem eine
-Annahme names `{h}`, die besagt …
+ Hint "**Du** Wenn ich das jetzt richtig lese, ist `{A}` eine Aussage,
+und wir haben außerdem eine Annahme names `{h}`, die besagt …
**Robo** … die besagt, dass `False` gilt.
@@ -33,8 +29,8 @@ Insbesondere die gesuchte Aussage `{A}`.
**Du** Und wie erkläre ich das jetzt diesem Formalosophen?
**Robo** Ich glaube, Du musst ihn darauf hinweisen, dass zwischen der allgemeingültigen
-Annahme `True` und seiner Annahme `False` ein Widerspruch besteht. Probier mal `contradiction`.
-"
+Annahme `True` und seiner Annahme `False` ein Widerspruch besteht. Probier mal `contradiction`."
+ contradiction
Conclusion
"Der erste Querulant ist offenbar zufrieden.
@@ -45,5 +41,5 @@ Conclusion
wir haben eine `contradiction` in unserem Annahmen, also folgt jede beliebige Aussage.
"
-NewTactics contradiction
-DisabledTactics tauto
+NewTactic contradiction
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
index f26a6f7..a7193df 100644
--- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean
@@ -17,14 +17,10 @@ Auftritt zweiter Querulant.
Statement ""
(n : ℕ) (h : n ≠ n) : n = 37 := by
- contradiction
-
-Hint (n : ℕ) (h : n ≠ n) : n = 37 =>
-"
-**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch?
+ Hint "**Du** Ist `{n} ≠ {n}` nicht auch ein Widerspruch?
-**Robo** Probiers mal!
-"
+**Robo** Probiers mal!"
+ contradiction
Conclusion
"
@@ -39,5 +35,5 @@ Und gleich 38, und gleich 39, …
**Du** Ok, ok, verstehe.
"
-NewTactics contradiction
-DisabledTactics tauto
+NewTactic contradiction
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
index 7b197fa..296444e 100644
--- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean
@@ -17,14 +17,12 @@ Auftritt dritter Querulant.
Statement ""
(n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 := by
+ Hint "**Du** Wieder ein Widerspruch in den Annahmen?
+
+**Robo** Ich sehe, du hast langsam den Dreh raus."
contradiction
-Hint (n : ℕ) (h : n = 10) (g : n ≠ 10) : n = 42 =>
-"
-**Du** Wieder ein Widerspruch in den Annahmen?
-**Robo** Ich sehe, du hast langsam den Dreh raus.
-"
Conclusion
"
@@ -33,5 +31,5 @@ worin der Widerspruch besteht: Die Annahme `n ≠ 10` ist genau die Negation vo
Man muss `≠` immer als `¬(· = ·)` lesen.
"
-NewTactics contradiction
-DisabledTactics tauto
+NewTactic contradiction
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L09_And.lean b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
index b406dd7..773259e 100644
--- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean
@@ -15,34 +15,46 @@ Der nächste Formalosoph in der Reihe hat seine Frage bereìts mitgebracht.
Er legt sie uns vor, setzt sich hin, und häkelt.
"
Statement "" (A B : Prop) (hA : A) (hB : B) : A ∧ B := by
- constructor
- assumption
- assumption
-
-Hint (A B : Prop) (hA : A) (hB : B) : A ∧ B =>
+ Hint
"
**Du**: Also, wir haben zwei Annahmen: `{A}` gilt, und `{B}` gilt. Auch. Und beweisen sollen wir
dass `{A} und {B}` gilt. Ich glaube, diese Formalospinner treiben mich noch zur Verzweiflung.
Kann ich nicht wieder `trivial` sagen?
-**Robo** Nee, diesmal wird das nicht funktionieren.
+**Robo**: Nee, diesmal wird das nicht funktionieren.
Du musst das Beweisziel einfach in zwei Teile zerlegen. Probier mal `constructor`.
-**Du** Du meinst, `destructor`??
+**Du**: Du meinst, `destructor`??
-**Robo** Nein, `constructor`. Ich weiß das ist verwirrend,
+**Robo**: Nein, `constructor`. Ich weiß das ist verwirrend,
aber die nennen das hier so weil man die Aussage aus mehreren Teilen
konstruieren kann.
"
-
-HiddenHint (A : Prop) (hA : A) : A =>
+ constructor
+ -- TODO: (BUG) Hier werden beide der folgenden Hints angezeigt.
+ -- Das logiste Verhalten wäre, wenn jeder nur am richtigen Ort
+ -- angezeigt würde.
+ -- Ein cooles Feature wäre, wenn man nur diesen ersten Hint schreiben könnte
+ -- und dieser dann automatisch auch beim zweiten Goal angezeigt wird, aber dann mit `B` statt `A`.
+ Hint (hidden := true)
"
-**Robo** Schau mal, das ist Zauberpapier.
+**Robo**: Schau mal, das ist Zauberpapier.
Jetzt haben wir auf einmal zwei Beweisziele.
Hier ist dast Ziel `{A}`.
Ich glaube, Du weißt schon, wie man die jeweils erreicht.
Die Ziele stehen ja jeweils in den *Annahmen*.
"
+ assumption
+ Hint (hidden := true)
+"
+**Robo**: Schau mal, das ist Zauberpapier.
+Jetzt haben wir auf einmal zwei Beweisziele.
+Hier ist dast Ziel `{B}`.
+Ich glaube, Du weißt schon, wie man die jeweils erreicht.
+Die Ziele stehen ja jeweils in den *Annahmen*.
+"
+ assumption
+
Conclusion
"
@@ -54,5 +66,5 @@ Ihm scheinen diese Fragen inzwischen Spaß zu machen.
Oder ist der nur gemalt? Probier mal!
"
-NewTactics constructor
-DisabledTactics tauto
+NewTactic constructor
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L10_And.lean b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
index 4e60cbe..c73dac6 100644
--- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean
@@ -16,10 +16,7 @@ Langsam wird die Schlange kürzer. Die nächste Formalosophin, ebenfalls häkeln
Statement ""
(A B C : Prop) (h : A ∧ (B ∧ C)) : B := by
- rcases h with ⟨_, ⟨g , _⟩⟩
- assumption
-
-Hint (A B C : Prop) (h : A ∧ (B ∧ C)) : B => "
+ Hint "
**Du** Jetzt müssen wir wohl die Annahme de-konstruieren.
**Robo** Ja, genau. Das geht am einfachsten mit `rcases {h} with ⟨h₁, h₂⟩`.
@@ -30,16 +27,12 @@ Hint (A B C : Prop) (h : A ∧ (B ∧ C)) : B => "
Und h₁ schreibst Du einfach als `h\\1`. Aber Du kannst Dir auch einfach andere Namen
für `h₁` und `h₂`, zum Beispiel `rcases {h} with ⟨hA, hBC⟩`
"
-
-Hint (A B C : Prop) (hA : A) (hAB : B ∧ C) : B =>
-"
-**Robo** Das sieht doch schon besser aus! Gleich nochmal!
-"
-
-HiddenHint (A : Prop) (hA : A) : A =>
-"
-**Robo** Du hast einen Beweis dafür in den *Annahmen*.
-"
+ Branch
+ rcases h with ⟨h₁, h₂⟩
+ Hint "**Robo** Das sieht doch schon besser aus! Gleich nochmal!"
+ rcases h with ⟨_, ⟨g , _⟩⟩
+ Hint (hidden := true) "**Robo** Du hast einen Beweis dafür in den *Annahmen*."
+ assumption
Conclusion
"
@@ -47,5 +40,5 @@ Conclusion
`rcases h with ⟨h₁, ⟨h₂ , h₃⟩⟩`.
"
-NewTactics rcases
-DisabledTactics tauto
+NewTactic rcases
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
index 7ed54e8..0c5878b 100644
--- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean
@@ -18,12 +18,7 @@ Der nächste bitte …
Statement
""
(A B : Prop) (hA : A) : A ∨ (¬ B) := by
- left
- assumption
-
-Hint (A B : Prop) (hA : A) : A ∨ (¬ B) =>
-"
-**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
+ Hint "**Du** Muss ich jetzt wieder das Beweisziel de-konstruieren?
**Robo** Nein, viel einfacher. Wenn Du eine Oder-Aussage beweisen sollst, musst Du Dich
einfach entscheiden, ob Du die linke oder rechte Seite beweisen willst.
@@ -31,18 +26,17 @@ einfach entscheiden, ob Du die linke oder rechte Seite beweisen willst.
**Du** Und wie erkläre ich meinem Formalosophen, welche Seite ich gern beweisen würde?
Ich will natürlich `{A}` beweisen!
-**Robo** Mit `left` bzw. `right`. Ist doch logisch, oder?
-"
-
-Hint (A B : Prop) (hA : A) : ¬ B =>
-"
-**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal.
-"
+**Robo** Mit `left` bzw. `right`. Ist doch logisch, oder?"
+ Branch
+ right
+ Hint "**Robo** Wusste gar nicht, dass Du eine Links-Rechts-Schwäche hast. Probier's nochmal."
+ left
+ assumption
Conclusion
"
Auch dieser Formalosoph zieht zufrieden von dannen.
"
-NewTactics left right assumption
-DisabledTactics tauto
+NewTactic left right assumption
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
index 2541f0d..90aa1b1 100644
--- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean
@@ -20,14 +20,7 @@ Der nächste bitte …
Statement ""
(A B : Prop) (h : (A ∧ B) ∨ A) : A := by
- rcases h with h | h
- rcases h with ⟨h₁, h₂⟩
- assumption
- assumption
-
-Hint (A B : Prop) (h :(A ∧ B) ∨ A) : A =>
-"
-**Robo** Schau mal, wenn du mit dem Finger eine Annahme berührst, zeigt es dir,
+ Hint "**Robo** Schau mal, wenn du mit dem Finger eine Annahme berührst, zeigt es dir,
wie die Klammern gesetzt sind. Irre…
**Du** Ah ich sehe, also `({A} ∧ {B}) ∨ {A}`!
@@ -41,34 +34,24 @@ Wir sind ja gleich hier fertig, und können zu einem interessanteren Planeten we
**Du** Also, wieder `rcases …`?
-**Robo** Ja, aber diesmal nicht `rcases {h} with ⟨h₁, h₂⟩`, sondern `rcases {h} with h | h`.
-"
-
--- -- TODO: This also triggers later under the assumptions
--- -- `(A : Prop) (B : Prop) (h₁ : A) (h₂ : B) : A`
--- -- Could we do something about that?
--- Hint (A : Prop) (B : Prop) (h : A) : A =>
--- "
--- **Robo** Jetzt musst Du Dein Ziel zweimal beweisen:
--- Einmal unter Annahme der linken Seite `{A}`,
--- und einmal unter Annahme der rechten Seite `{A} ∨ {B}`. Hier haben nehmen wir an, die linke Seite
--- sei wahr.
--- "
-
-Hint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
-"
-**Robo**
+**Robo** Ja, aber diesmal nicht `rcases {h} with ⟨h₁, h₂⟩`, sondern `rcases {h} with h | h`."
+ rcases h with h | h
+ Hint "**Robo**
Jetzt musst Du Dein Ziel zweimal beweisen:
Einmal unter Annahme der linken Seite `{A} ∨ {B}`,
und einmal unter Annahme der rechten Seite `{A}`.
Hier haben nehmen wir an, die linke Seite
-sei wahr.
-"
-HiddenHint (A : Prop) (B : Prop) (h : A ∧ B) : A =>
-"
-**Robo** Wie man mit einem Und in den Annahmen umgeht, weißt Du doch schon:
-`rcases h with ⟨h₁, h₂⟩`. Zur Erinnerung: Für die Klammern schreibst Du `\\<>`.
-"
+sei wahr."
+ Hint (hidden := true) " **Robo** Wie man mit einem Und in den Annahmen umgeht,
+weißt Du doch schon:
+`rcases h with ⟨h₁, h₂⟩`. Zur Erinnerung: Für die Klammern schreibst Du `\\<>`."
+ rcases h with ⟨h₁, h₂⟩
+ Hint "**Robo** Jetzt musst Du Dein Ziel zweimal beweisen:
+Einmal unter Annahme der linken Seite `{A}`,
+und einmal unter Annahme der rechten Seite `{A} ∨ {B}`. Hier haben nehmen wir an, die linke Seite
+sei wahr."
+ assumption
+ assumption
Conclusion
"**Du** Ok, das scheint ihn zufriedenzustellen. Nur noch eine Seele…
@@ -125,5 +108,5 @@ Die Worte, die Du aktiv gebrauchen musst, heißen zusammengefasst `Taktiken`. H
"
-NewTactics assumption rcases
-DisabledTactics tauto
+NewTactic assumption rcases
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
index eb689d2..6db6c77 100644
--- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
+++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean
@@ -14,7 +14,9 @@ Introduction
"
Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vorherigen.
-**Robo** Wirf einfach alles drauf, was Du gelernt hast. Hier, ich bin sogar so nett und zeig Dir noch einmal die vier wichtigsten Taktiken für diese Situation an.
+**Robo** Wirf einfach alles drauf, was Du gelernt hast.
+Hier, ich bin sogar so nett und zeig Dir noch einmal die vier
+wichtigsten Taktiken für diese Situation an.
| (Übersicht) | Und (`∧`) | Oder (`∨`) |
|-------------|:-------------------------|:------------------------|
@@ -26,46 +28,83 @@ Der letzte Untertan tritt vor. Ihr Anliegen ist etwas komplizierter als die vor
Statement ""
(A B C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) := by
- constructor
- rcases h with h | h
- left
- assumption
- rcases h with ⟨h₁, h₂⟩
- right
- assumption
- rcases h with h | h
- left
- assumption
- rcases h with ⟨h₁, h₂⟩
- right
- assumption
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) =>
-"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) =>
-"**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen."
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
-"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) =>
-"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) =>
-"**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
-
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) =>
-"**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
-
-HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
-"**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
-
--- TODO: Hint nur Anhand der Annahmen?
-
-HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
-"**Robo** `left` oder `right`?"
+ Hint (hidden := true)
+ "**Robo**: Ich würd zuerst die Annahme {h} mit `rcases {h}` aufteilen."
+ Branch
+ constructor
+ · rcases h with h' | h'
+ · left
+ assumption
+ · rcases h' with ⟨h₁, h₂⟩
+ right
+ assumption
+ · rcases h with h' | h'
+ · left
+ assumption
+ · rcases h' with ⟨h₁, h₂⟩
+ right
+ assumption
+ rcases h
+ Hint (hidden := true) "**Robo**: Jetzt kannst Du das `∧` im Goal mit `constructor` angehen."
+ · constructor
+ · left
+ assumption
+ · left
+ assumption
+ · Hint (hidden := true)
+ "**Robo**: Hier würde ich die Annahme {h} nochmals mit `rcases` aufteilen."
+ Branch
+ constructor
+ · Hint "**Robo**: Der Nachteil an der Reihenfolge ist, dass du jetzt in jedem Untergoal
+`rcases h` aufrufen musst."
+ Branch
+ right
+ rcases h with ⟨h₁, h₂⟩
+ assumption
+ rcases h with ⟨h₁, h₂⟩
+ right
+ assumption
+ · Branch
+ right
+ rcases h with ⟨h₁, h₂⟩
+ assumption
+ rcases h with ⟨h₁, h₂⟩
+ right
+ assumption
+ rcases h with ⟨h₁, h₂⟩
+ constructor
+ · right
+ assumption
+ · right
+ assumption
+
+
+-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) ∧ (A ∨ C) =>
+-- "**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
+
+-- HiddenHint (A : Prop) (B : Prop) (C : Prop) : (A ∨ B) ∧ (A ∨ C) =>
+-- "**Robo** Das `∧` im Goal kannst Du mit `constructor` zerlegen."
+
+-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) ∧ (A ∨ C) =>
+-- "**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
+
+-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ B) =>
+-- "**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
+
+-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : A ∨ (B ∧ C)) : (A ∨ C) =>
+-- "**Robo** Das `∨` in der Annahme kannst Du mit `rcases h with h | h` zerlegen."
+
+
+-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ B) =>
+-- "**Robo** Das `∧` in der Annahme kannst Du mit `rcases h with ⟨h₁, h₂⟩` zerlegen."
+
+-- HiddenHint (A : Prop) (B : Prop) (C : Prop) (h : B ∧ C) : (A ∨ C) =>
+-- "**Robo** Das `∧` in der Annahme kannst Du mit `rcases {h} with ⟨h₁, h₂⟩` zerlegen."
+
+-- -- TODO: Hint nur Anhand der Annahmen?
+
+-- HiddenHint (A : Prop) (B : Prop) : A ∨ B =>
+-- "**Robo** `left` oder `right`?"
Conclusion
"
@@ -74,5 +113,5 @@ Conclusion
Königin *Logisinde* ist in der Zwischenzeit eingeschlafen, und ihr stehlt euch heimlich davon.
"
-NewTactics left right assumption constructor rcases rfl contradiction trivial
-DisabledTactics tauto
+NewTactic left right assumption constructor rcases rfl contradiction trivial
+DisabledTactic tauto
diff --git a/server/testgame/TestGame/Levels/SetTheory.lean b/server/testgame/TestGame/Levels/SetTheory.lean
index d1a3ed0..0f9a789 100644
--- a/server/testgame/TestGame/Levels/SetTheory.lean
+++ b/server/testgame/TestGame/Levels/SetTheory.lean
@@ -23,6 +23,21 @@ Game "TestGame"
World "SetTheory"
Title "Mengenlehre"
+Introduction
+"Der größere der beiden Monde sieht dunkelrot und karg aus. Trotzdem sollen dort nomadische
+Gesellschaften wohnen, die sich in der Einöde zurechtfinden.
+
+Ihr steuert einen der wenigen befestigten Standorte am Fusse eines Berges an.
+
+**Robo**: Die Bevölkerung hier lebt so abgekapselt vom Rest des Universums, dass sie sich
+vermutlich noch viel besser mit alter Sprache und Schrift auskennt.
+
+**Du**: Hoffen wir, dass sie uns weiterhelfen können dieses Buch der Urbilder zu entschlüsseln.
+
+Sofort begrüßt euch eine ältere Frau, die sich als *Mengitte*, die Beschützerin des Mondes,
+vorstellt.
+"
+
Game "TestGame"
World "SetTheory2"
Title "Mehr Mengenlehre"
diff --git a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
index 90ff1f8..e46618c 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean
@@ -14,29 +14,47 @@ Title "Mengen"
Introduction
"
-In diesem Kapitel schauen wir uns Mengen an.
+**Mengitte**: Ich würde leider den Inhalt jenes Buches eh nicht verstehen. Aber der beste Weg für
+euch, dieses zu entschlüsseln ist, euch ausgiebig mit der Bevölkerung hier zu unterhalten.
+Lebt mit ihnen, redet mit ihnen und ihr werdet die Sprache automatisch lernen.
-Zuerst ein ganz wichtiger Punkt: Alle Mengen in Lean sind homogen. Das heisst,
-alle Elemente in einer Menge haben den gleichen Typ.
+**Mengitte**: Seit aber vorgewarnt, die Leute hier denken ganz viel über Mengen nach,
+womit sie immer *homogene Mengen* meinen. Eine Menge natürlicher Zahlen `{1, 4, 6}` ist
+verständlich, aber sowas wie eine Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` gibt es hier
+einfach nicht. Punkt.
-Zum Beispiel `{1, 4, 6}` ist eine Menge von natürlichen Zahlen. Aber man kann keine
-Menge `{(2 : ℕ), {3, 1}, \"e\", (1 : ℂ)}` definieren, da die Elemente unterschiedliche Typen haben.
+**Robo**: Als Kontext: Wenn `A` ein beliebiger `Type` ist, dann ist `(U : Set A)` eine Menge
+mit Elementen aus `A`
-Für einen Typen `{X : Type*}` definiert damit also `set X` der Type aller Mengen mit Elementen aus
-`X`. `set.univ` ist dann ganz `X` also Menge betrachtet, und es ist wichtig den Unterschied
-zu kennen: `(univ : set X)` und `(X : Typ*)` haben nicht den gleichen Typ und sind damit auch nicht
-austauschbar!
-
-Um zu beweisen, dass etwas in `univ` ist, kannst du verschiedenste deiner Taktiken anwenden,
-zum Beispiel `tauto`.
+**Mengitte**: Damit ich weiss, dass ihr euch grundsätzlich mit den Leuten austauschen könnt,
+erklärt mir doch folgendes:
"
open Set
-Statement mem_univ
- "4 ist ein Element der Menge aller natürlichen Zahlen." {A : Type _} (x : A) :
- x ∈ (univ : Set A) := by
+Statement mem_univ "" {A : Type} (x : A) : x ∈ (univ : Set A) := by
trivial
- -- tauto
-NewTactics tauto trivial
+Hint (A : Type) (x : A) : x ∈ (univ : Set A) =>
+"**Du**: Also `A` ist ein `Type`, `x` ist ein Element in `A`…
+
+**Robo** … und `univ` ist die Menge aller Elemente in `A`.
+
+**Du** ist das nicht einfach `A` selber?
+
+**Robo** Fast, aber das eine ist ein `Type`, das andere eine Menge, also vom Typ `Set A`.
+
+**Du**: Unlogisch.
+
+**Mengites**: Naja, Typen und Mengen sind halt zwei unterschiedliche Sachen und wenn ihr
+über Mengen sprechen wollt, müssen alles Mengen sein.
+
+**Du**: Na gut. Und wieso `x ∈ univ` und nicht `x : univ` wie bei Typen?
+
+**Robo**: Jedes Element `(x : A)` hat entweder die Eigenschaft `x ∈ U` oder `x ∉ U` für eine
+Menge `(U : Set A)`. (`\\in`, `\\nin`)
+
+**Du**: Also das ist ja dann trivial. Hoffentlich sehen die das hier auch so…
+"
+
+Conclusion "**Mengitte**: Ja das stimmt schon. Dann wünsche ich euch viel Erfolg auf eurer Reise!"
diff --git a/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
index 3c0c548..193a6a6 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L02_Empty.lean
@@ -13,17 +13,22 @@ Title "leere Menge"
Introduction
"
-Gleich wie bei `univ` gibt es leere Mengen `∅` von verschiedenen Typen.
-So ist `(∅ : Set ℕ)` in Lean nicht das gleiche wie `(∅ : Set ℤ)`. (`\\empty`)
-
-Zudem hat die Verneinung `¬ (x ∈ A)` die Notation `x ∉ A` (`\\nin`), gleich wie bei `=` and `≠`.
-
-Um zu zeigen, dass etwas nicht in der leeren Menge ist, kannst du wieder `tauto` verwenden.
+Ihr zieht also durch die Gegend und redet mit den Leuten. Ein Junge rennt zu euch und fragt:
"
open Set
-Statement not_mem_empty
- "Kein Element ist in der leeren Menge enthalten." {A : Type _} (x : A) :
+Statement not_mem_empty "" {A : Type} (x : A) :
x ∉ (∅ : Set A) := by
tauto
+
+NewLemma mem_univ
+
+Hint (A : Type) (x : A) : x ∉ (∅ : Set A) =>
+"**Du**: Kein Element ist in der leeren Menge enthalten? Das ist ja alles tautologisches Zeugs...
+
+**Robo**: Dann behaupte das doch. (`\\empty`)"
+
+Conclusion "Der Junge rennt weiter.
+
+**Du**: So wird das ganze schon angenehmer."
diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
index eac4906..a876537 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean
@@ -28,18 +28,18 @@ namespace MySet
open Set
-theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by
- trivial
+-- theorem mem_univ {A : Type _} (x : A) : x ∈ (univ : Set A) := by
+-- trivial
-theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by
- tauto
+-- theorem not_mem_empty {A : Type _} (x : A) : x ∉ (∅ : Set A) := by
+-- tauto
Statement subset_empty_iff
"." (A : Set ℕ) : A ⊆ univ := by
intro h hA
- apply mem_univ -- or `trivial`.
+ trivial --apply mem_univ -- or `trivial`.
-NewTactics intro trivial apply
+NewTactic intro trivial apply
-- blocked: tauto simp
end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
index 3aeaf5c..d8a6990 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L04_SubsetEmpty.lean
@@ -54,8 +54,8 @@ Statement subset_empty_iff
rcases a with ⟨h₁, h₂⟩
assumption
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
index c9b9908..15f6394 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L05_Empty.lean
@@ -45,8 +45,8 @@ Statement eq_empty_iff_forall_not_mem
rw [←subset_empty_iff]
rfl -- This is quite a miracle :)
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
end MySet
diff --git a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
index 88e28b0..bc69079 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L06_Nonempty.lean
@@ -30,6 +30,6 @@ Statement nonempty_iff_ne_empty
push_neg
rfl
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
index 5a7a792..098ca27 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L07_UnionInter.lean
@@ -26,6 +26,6 @@ Statement
"" (A B : Set ℕ) : (A ∪ ∅) ∩ B = A ∩ (univ ∩ B) := by
simp
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
index af7deeb..906bac4 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L08_UnionInter.lean
@@ -30,6 +30,6 @@ Statement
rw [←union_diff_distrib]
rw [univ_union]
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
index b48d09b..f454337 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L09_Complement.lean
@@ -30,6 +30,6 @@ Statement
rw [←not_mem_compl_iff]
exact h4
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean b/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
index e61fcd3..76b6900 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L10_Morgan.lean
@@ -22,7 +22,7 @@ man die de-Morganschen Regeln einfach selber beweisen könnten.
Die meisten Aufgaben über Mengen sind eine Kombination von `rw` und `simp_rw` verschiedenster
-NewLemmas in `import Mathlib.Data.Set`.
+NewLemma in `import Mathlib.Data.Set`.
Die Taktik `simp_rw` funktioniert ähnlich wie `rw`, aber sie versucht jedes Lemma so oft
wie möglich anzuwenden. Wir kennen also 4 etwas verwandte Optionen um Lemmas und Theoreme zu
@@ -52,7 +52,7 @@ Statement
rw [diff_eq_compl_inter]
rw [inter_comm]
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-- TODOs
-- Lemmas compl_union compl_inter mem_compl_iff
diff --git a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
index 652584a..6dd11f4 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L11_SSubset.lean
@@ -33,6 +33,6 @@ Statement
rw [Set.mem_diff]
exact hx
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
index 6b03d1b..40c786d 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L12_Insert.lean
@@ -32,6 +32,6 @@ Statement
({4, 9} : Set ℕ) = Set.insert 4 {9} := by
rfl
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean b/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
index daf6062..cb32a1a 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L13_Insert.lean
@@ -35,5 +35,5 @@ Statement
simp_rw [mem_insert_iff, mem_singleton_iff] at *
tauto
-NewTactics simp_rw intro tauto rw
+NewTactic simp_rw intro tauto rw
--Lemmas Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
index bc6e273..50a1e18 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L14_SetOf.lean
@@ -32,6 +32,6 @@ Statement
use 1
ring
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
index 768f341..7162728 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L15_Powerset.lean
@@ -37,6 +37,6 @@ Statement
assumption
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
index 20ff5b7..df5d23e 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L16_Disjoint.lean
@@ -36,6 +36,6 @@ Statement
ring
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
index 0887e21..94d3ae8 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L17_SetOf.lean
@@ -34,6 +34,6 @@ Statement
ring
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
index e98dd28..5d81257 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L18_SetOf.lean
@@ -28,6 +28,6 @@ Statement
{ x ∈ (S : Set ℤ) | 0 ≤ x} ⊆ S := by
library_search
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
index 2824f96..93569fb 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L19_Subtype.lean
@@ -23,6 +23,6 @@ Statement
use 1
ring
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
index dfd5380..7a9d10e 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L20_UnionInter.lean
@@ -22,6 +22,6 @@ open Set
Statement
"" : True := sorry
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
index 7c384ad..52d376c 100644
--- a/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/L21_Summary.lean
@@ -23,6 +23,6 @@ Statement
use 1
ring
-NewTactics constructor intro rw assumption rcases simp tauto trivial
+NewTactic constructor intro rw assumption rcases simp tauto trivial
-NewLemmas Subset.antisymm_iff empty_subset
+NewLemma Subset.antisymm_iff empty_subset
diff --git a/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean b/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
index 9b6e875..f8ac55d 100644
--- a/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
+++ b/server/testgame/TestGame/Levels/SetTheory/T01_Set.lean
@@ -54,7 +54,7 @@ Statement
rw [←Set.union_diff_distrib]
rw [Set.univ_union]
-NewTactics rw
+NewTactic rw
example : 4 ∈ (univ : Set ℕ) := by
trivial
diff --git a/server/testgame/TestGame/Levels/StatementTest.lean b/server/testgame/TestGame/Levels/StatementTest.lean
index a9d47e1..2d00bb9 100644
--- a/server/testgame/TestGame/Levels/StatementTest.lean
+++ b/server/testgame/TestGame/Levels/StatementTest.lean
@@ -35,4 +35,4 @@ lemma asdf (a b c d : ℕ) (h₁ : c = d) (h₂ : a = b) (h₃ : a = d) : b = c
Conclusion ""
-NewTactics assumption
+NewTactic assumption
diff --git a/server/testgame/TestGame/Levels/Sum/L01_Simp.lean b/server/testgame/TestGame/Levels/Sum/L01_Simp.lean
index 829249a..d7970de 100644
--- a/server/testgame/TestGame/Levels/Sum/L01_Simp.lean
+++ b/server/testgame/TestGame/Levels/Sum/L01_Simp.lean
@@ -44,4 +44,4 @@ Statement
(n : ℕ) : (∑ i : Fin n, (0 + 0)) = 0 := by
simp
-NewTactics simp
+NewTactic simp
diff --git a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
index 176bf81..218187a 100644
--- a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
+++ b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean
@@ -31,15 +31,11 @@ Statement
"Zeige dass $\\sum_{i=0}^{n-1} (i + 1) = n + \\sum_{i=0}^{n-1} i$."
(n : ℕ) : ∑ i : Fin n, ((i : ℕ) + 1) = n + (∑ i : Fin n, (i : ℕ)) := by
rw [Finset.sum_add_distrib]
+ Hint "Die zweite Summe `∑ x : Fin n, 1` kann `simp` zu `n` vereinfacht werden."
simp
- ring
-
-NewLemmas Finset.sum_add_distrib add_comm
+ Hint "Bis auf Umordnung sind jetzt beide Seiten gleich, darum kann `ring` das Goal schließen.
-Hint (n : ℕ) : ∑ x : Fin n, ↑x + ∑ x : Fin n, 1 = n + ∑ i : Fin n, ↑i =>
-"Die zweite Summe `∑ x : Fin n, 1` kann `simp` zu `n` vereinfacht werden."
-
-Hint (n : ℕ) : ∑ x : Fin n, ↑x + n = n + ∑ x : Fin n, ↑x =>
-"Bis auf Umordnung sind jetzt beide Seiten gleich, darum kann `ring` das Goal schließen.
+ Alternativ kann man auch mit `rw [add_comm]` dies explizit umordnen."
+ ring
-Alternativ kann man auch mit `rw [add_comm]` dies explizit umordnen."
+NewLemma Finset.sum_add_distrib add_comm
diff --git a/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean b/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
index e648aad..fde2614 100644
--- a/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
+++ b/server/testgame/TestGame/Levels/Sum/L03_ArithSum.lean
@@ -52,8 +52,8 @@ Statement arithmetic_sum
rw [Nat.succ_eq_add_one]
ring
-NewTactics induction
-NewLemmas Fin.sum_univ_castSucc Nat.succ_eq_add_one mul_add add_mul
+NewTactic induction
+NewLemma Fin.sum_univ_castSucc Nat.succ_eq_add_one mul_add add_mul
Hint (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) =>
"Als Erinnerung, einen Induktionsbeweis startet man mit `induction n`."
diff --git a/server/testgame/TestGame/Levels/Sum/L05_SumComm.lean b/server/testgame/TestGame/Levels/Sum/L05_SumComm.lean
index 406f007..957104e 100644
--- a/server/testgame/TestGame/Levels/Sum/L05_SumComm.lean
+++ b/server/testgame/TestGame/Levels/Sum/L05_SumComm.lean
@@ -33,4 +33,4 @@ $\\sum_{i=0}^n\\sum_{j=0}^m 2^i (1 + j) = \\sum_{j=0}^m\\sum_{i=0}^n 2^i (1 +
∑ j : Fin m, ∑ i : Fin n, ( 2^i * (1 + j) : ℕ) := by
rw [Finset.sum_comm]
-NewLemmas Finset.sum_comm
+NewLemma Finset.sum_comm
diff --git a/server/testgame/TestGame/Levels/Sum/L06_Summary.lean b/server/testgame/TestGame/Levels/Sum/L06_Summary.lean
index bc6f4e3..7657785 100644
--- a/server/testgame/TestGame/Levels/Sum/L06_Summary.lean
+++ b/server/testgame/TestGame/Levels/Sum/L06_Summary.lean
@@ -57,7 +57,7 @@ Statement
rw [arithmetic_sum]
ring
-NewLemmas arithmetic_sum add_pow_two
+NewLemma arithmetic_sum add_pow_two
HiddenHint (m : ℕ) : ∑ i : Fin (m + 1), (i : ℕ) ^ 3 = (∑ i : Fin (m + 1), ↑i) ^ 2 =>
"Führe auch hier einen Induktionsbeweis."
diff --git a/server/testgame/TestGame/Levels/Sum/T01_Induction.lean b/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
index b31adfa..1e2c033 100644
--- a/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
+++ b/server/testgame/TestGame/Levels/Sum/T01_Induction.lean
@@ -37,4 +37,4 @@ example (n : ℕ) (h : 5 ≤ n) : n^2 < 2 ^ n
sorry
| n + 5 => by sorry
-NewTactics rw simp ring
+NewTactic rw simp ring
diff --git a/server/testgame/TestGame/Levels/Sum/T02_Induction.lean b/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
index 89d2ac9..aa25628 100644
--- a/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
+++ b/server/testgame/TestGame/Levels/Sum/T02_Induction.lean
@@ -32,4 +32,4 @@ Statement
-- ring
-- rw [Nat.succ_eq_one_add]
-- rw []
-NewTactics rw simp ring
+NewTactic rw simp ring
diff --git a/server/testgame/TestGame/Levels/Sum/T03__Bernoulli.lean b/server/testgame/TestGame/Levels/Sum/T03__Bernoulli.lean
index 8d461dd..003a584 100644
--- a/server/testgame/TestGame/Levels/Sum/T03__Bernoulli.lean
+++ b/server/testgame/TestGame/Levels/Sum/T03__Bernoulli.lean
@@ -46,4 +46,4 @@ Statement
-- rw [mul_add, hn]
-- ring
-NewTactics ring
+NewTactic ring
diff --git a/server/testgame/TestGame/ToBePorted.lean b/server/testgame/TestGame/ToBePorted.lean
index 564a4a3..9e01935 100644
--- a/server/testgame/TestGame/ToBePorted.lean
+++ b/server/testgame/TestGame/ToBePorted.lean
@@ -1,10 +1,10 @@
import Mathlib
-lemma not_odd {n : ℕ} : ¬ Odd n ↔ Even n := by
- sorry
+-- lemma not_odd {n : ℕ} : ¬ Odd n ↔ Even n := by
+-- sorry
-lemma not_even {n : ℕ} : ¬ Even n ↔ Odd n := by
- sorry
+-- lemma not_even {n : ℕ} : ¬ Even n ↔ Odd n := by
+-- sorry
lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by
intro ⟨x, hx⟩
@@ -13,72 +13,58 @@ lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by
rw [hx]
ring
-section powerset
-
-open Set
-
-namespace Finset
-
-theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) :
- Finset.powerset {x} = {∅, {x}} := by
- ext y
- rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton]
-
-end Finset
-
-/- The powerset of a singleton contains only `∅` and the singleton. -/
-theorem powerset_singleton {U : Type _} (x : U) :
- 𝒫 ({x} : Set U) = {∅, {x}} := by
- ext y
- rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff]
-
-theorem subset_insert_iff_of_not_mem {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s)
- : s ⊆ insert a t ↔ s ⊆ t := by
- constructor
- · intro g y hy
- specialize g hy
- rw [mem_insert_iff] at g
- rcases g with g | g
- · rw [g] at hy
- contradiction
- · assumption
- · intro g y hy
- specialize g hy
- exact mem_insert_of_mem _ g
-
-theorem subset_insert_iff_of_not_mem' {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s)
- (g : s ⊆ t) : s ⊆ insert a t := by
- intro y hy
- specialize g hy
- exact mem_insert_of_mem _ g
-
-lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) :
- S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by
- simp_rw [mem_powerset_iff]
- constructor
- · intro h
- by_cases hs : x ∈ S
- · right
- use S \ {x}
- rw [insert_diff_singleton, insert_eq_of_mem hs, diff_singleton_subset_iff]
- exact ⟨h, rfl⟩
- · left
- exact (subset_insert_iff_of_not_mem hs).mp h
- · intro h
- rcases h with h | ⟨B, h₁, h₂⟩
- · exact le_trans h (subset_insert x A)
- · rw [←h₂]
- exact insert_subset_insert h₁
-
-lemma mem_powerset_insert_iff' {U : Type _} (A S : Set U) (x : U) :
- S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by
- rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff]
-
-lemma powerset_insert {U : Type _} (A : Set U) (x : U) :
- 𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by
- ext y
- rw [mem_powerset_insert_iff, mem_union, mem_image]
-
-
-
-end powerset
+-- section powerset
+
+-- open Set
+
+-- namespace Finset
+
+-- theorem powerset_singleton {U : Type _} [DecidableEq U] (x : U) :
+-- Finset.powerset {x} = {∅, {x}} := by
+-- ext y
+-- rw [mem_powerset, subset_singleton_iff, mem_insert, mem_singleton]
+
+-- end Finset
+
+-- /- The powerset of a singleton contains only `∅` and the singleton. -/
+-- theorem powerset_singleton {U : Type _} (x : U) :
+-- 𝒫 ({x} : Set U) = {∅, {x}} := by
+-- ext y
+-- rw [mem_powerset_iff, subset_singleton_iff_eq, mem_insert_iff, mem_singleton_iff]
+
+-- theorem subset_insert_iff_of_not_mem' {U : Type _ } {s t : Set U} {a : U} (h : a ∉ s)
+-- (g : s ⊆ t) : s ⊆ insert a t := by
+-- intro y hy
+-- specialize g hy
+-- exact mem_insert_of_mem _ g
+
+-- lemma mem_powerset_insert_iff {U : Type _} (A S : Set U) (x : U) :
+-- S ∈ 𝒫 (insert x A) ↔ S ∈ 𝒫 A ∨ ∃ B ∈ 𝒫 A , insert x B = S := by
+-- simp_rw [mem_powerset_iff]
+-- constructor
+-- · intro h
+-- by_cases hs : x ∈ S
+-- · right
+-- use S \ {x}
+-- rw [insert_diff_singleton, insert_eq_of_mem hs, diff_singleton_subset_iff]
+-- exact ⟨h, rfl⟩
+-- · left
+-- exact (subset_insert_iff_of_not_mem hs).mp h
+-- · intro h
+-- rcases h with h | ⟨B, h₁, h₂⟩
+-- · exact le_trans h (subset_insert x A)
+-- · rw [←h₂]
+-- exact insert_subset_insert h₁
+
+-- lemma mem_powerset_insert_iff' {U : Type _} (A S : Set U) (x : U) :
+-- S ∈ 𝒫 (insert x A) ↔ S \ {x} ∈ 𝒫 A := by
+-- rw [mem_powerset_iff, mem_powerset_iff, diff_singleton_subset_iff]
+
+-- lemma powerset_insert {U : Type _} (A : Set U) (x : U) :
+-- 𝒫 (insert x A) = A.powerset ∪ A.powerset.image (insert x) := by
+-- ext y
+-- rw [mem_powerset_insert_iff, mem_union, mem_image]
+
+
+
+-- end powerset
diff --git a/server/testgame/gameserver b/server/testgame/gameserver
old mode 100755
new mode 100644
diff --git a/server/testgame/lake-manifest.json b/server/testgame/lake-manifest.json
index ad627d9..0856666 100644
--- a/server/testgame/lake-manifest.json
+++ b/server/testgame/lake-manifest.json
@@ -4,25 +4,25 @@
[{"git":
{"url": "https://github.com/leanprover-community/mathlib4.git",
"subDir?": null,
- "rev": "c8bff08cf815e8881e95967259910524100adfb0",
+ "rev": "fc4a489c2af75f687338fe85c8901335360f8541",
"name": "mathlib",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/gebner/quote4",
"subDir?": null,
- "rev": "7ac99aa3fac487bec1d5860e751b99c7418298cf",
+ "rev": "cc915afc9526e904a7b61f660d330170f9d60dd7",
"name": "Qq",
"inputRev?": "master"}},
{"git":
{"url": "https://github.com/JLimperg/aesop",
"subDir?": null,
- "rev": "ba61f7fec6174d8c7d2796457da5a8d0b0da44c6",
+ "rev": "071464ac36e339afb7a87640aa1f8121f707a59a",
"name": "aesop",
"inputRev?": "master"}},
{"path": {"name": "GameServer", "dir": "./../leanserver"}},
{"git":
{"url": "https://github.com/leanprover/std4",
"subDir?": null,
- "rev": "de7e2a79905a3f87cad1ad5bf57045206f9738c7",
+ "rev": "44a92d84c31a88b9af9329a441890ad449d8cd5f",
"name": "std",
"inputRev?": "main"}}]}
diff --git a/server/testgame/lean-toolchain b/server/testgame/lean-toolchain
index 5bf01da..7f0fd43 100644
--- a/server/testgame/lean-toolchain
+++ b/server/testgame/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-02-10
+leanprover/lean4:nightly-2023-03-09