From 17792e1a0172ce4043ab0b7589fb3cc40e77032b Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 12 Dec 2022 20:08:28 +0100 Subject: [PATCH] Add Support for lemma statement. --- client/src/components/Level.tsx | 10 +++- client/src/components/TacticState.tsx | 11 +++-- client/src/components/Welcome.tsx | 2 +- server/leanserver/GameServer/Commands.lean | 46 ++++++++++++++++--- .../leanserver/GameServer/EnvExtensions.lean | 12 +++++ server/leanserver/GameServer/Game.lean | 10 ++++ server/leanserver/GameServer/RpcHandlers.lean | 4 +- server/testgame/TestGame/Levels/Level1.lean | 2 +- server/testgame/TestGame/Levels/Level2.lean | 2 +- server/testgame/TestGame/Levels/Level3.lean | 2 +- server/testgame/TestGame/Levels/Level4.lean | 2 +- server/testgame/TestGame/Levels/Level5.lean | 2 +- .../TestGame/Levels/Logic/L01_Rfl.lean | 2 +- .../Levels/Logic/L03b_Assumption.lean | 6 +-- .../TestGame/Levels/Logic/L05_Apply.lean | 6 +-- .../TestGame/Levels/Logic/L05b_Apply.lean | 6 +-- .../TestGame/Levels/Logic/L05c_Apply.lean | 1 + .../TestGame/Levels/Logic/L06_Iff.lean | 4 +- .../TestGame/Levels/Logic/L06b_Iff.lean | 4 +- .../TestGame/Levels/Logic/L06c_Iff.lean | 1 + .../TestGame/Levels/Logic/L06d_Iff.lean | 4 +- .../TestGame/Levels/Logic/L07_And.lean | 1 + .../TestGame/Levels/Logic/L08_Or.lean | 2 +- .../TestGame/Levels/Logic/L08b_Or.lean | 1 + .../TestGame/Levels/Logic/L08c_Or.lean | 2 +- .../TestGame/Levels/Naturals/L01_Ring.lean | 2 +- .../TestGame/Levels/Naturals/L02_Ring.lean | 2 +- .../TestGame/Levels/Naturals/L03_Exists.lean | 2 +- .../TestGame/Levels/Naturals/L04_Forall.lean | 2 +- .../TestGame/Levels/Naturals/L31_Sum.lean | 2 +- .../Levels/Naturals/L32_Induction.lean | 2 +- .../TestGame/Levels/Naturals/L33_Prime.lean | 2 +- .../Levels/Naturals/L34_ExistsUnique.lean | 2 +- .../TestGame/Levels/Negation/L01_False.lean | 2 +- .../TestGame/Levels/Negation/L02_Contra.lean | 2 +- .../TestGame/Levels/Negation/L03_Contra.lean | 4 +- .../TestGame/Levels/Negation/L04_Contra.lean | 2 +- .../TestGame/Levels/Negation/L05_Not.lean | 1 + .../Levels/Negation/L06_ByContra.lean | 2 +- .../Levels/Negation/L07_Contrapose.lean | 2 +- .../Levels/Negation/L08_Contrapose.lean | 2 +- .../TestGame/Levels/Negation/L09_PushNeg.lean | 4 +- 42 files changed, 120 insertions(+), 62 deletions(-) diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index e094771..f42efcc 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -41,10 +41,12 @@ function Level() { const [expertInfoview, setExpertInfoview] = useState(false) - const [leanData, setLeanData] = useState({goals: []}) + const [leanData, setLeanData] = useState({goals: [], description: "Loading..."}) const [history, setHistory] = useState([]) const [lastTactic, setLastTactic] = useState("") const [introduction, setIntroduction] = useState("") + const [description, setDescription] = useState("Loading...") + const [ppStatement, setPPStatement] = useState("") const [errors, setErrors] = useState([]) const codeviewRef = useRef(null) const infoviewRef = useRef(null) @@ -129,6 +131,8 @@ function Level() { setTacticDocs(res["tactics"]) setLemmaDocs(res["lemmas"]) setIntroduction(res["introduction"]) + setDescription(res["description"]) + setPPStatement(res["ppStatement"]) processResponse(res) }); @@ -153,6 +157,10 @@ function Level() {
{introduction}
+

Aufgabe:

+
{description}
+ {/*
{ppStatement}
+ NOTE(TODO): currently this looks bad, so I disabled it. Maybe have a drop-down for it of Syntax highlighting... */}
{/* */} diff --git a/client/src/components/TacticState.tsx b/client/src/components/TacticState.tsx index ebebad7..2ec2428 100644 --- a/client/src/components/TacticState.tsx +++ b/client/src/components/TacticState.tsx @@ -42,11 +42,12 @@ function Goal({ goal }) { Prove: {goal.goal} {goal.messages.map((message) => {message})} - } - label="Help" - /> - {goal.hints.map((message) => {message})} + {hasHints && + } + label="Help" + />} + {goal.hints.map((hint) => {hint})} ) } diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx index fe9f79c..7966c56 100644 --- a/client/src/components/Welcome.tsx +++ b/client/src/components/Welcome.tsx @@ -92,7 +92,7 @@ function Welcome() { - +
diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index efb4fa1..0b8718e 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -46,13 +46,47 @@ elab "Introduction" t:str : command => do | .World => modifyCurWorld fun world => pure {world with introduction := t.getString} | .Game => modifyCurGame fun game => pure {game with introduction := t.getString} -/-- Define the statement of the current level. -/ -elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do +-- TODO: Instead of this, it would be nice to have a proper syntax parser that enables +-- us highlighting on the client side. +partial def reprintCore : Syntax → Option Format + | Syntax.missing => none + | Syntax.atom _ val => val.trim + | Syntax.ident _ rawVal _ _ => rawVal.toString + | Syntax.node _ kind args => + match args.toList.filterMap reprintCore with + | [] => none + | [arg] => arg + | args => Format.group <| Format.nest 2 <| Format.joinSep args " " + +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) + +/-- 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. +-/ +elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : command => do + let lvlIdx ← getCurLevelIdx - let declName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ ("level" ++ toString lvlIdx : String) - elabCommand (← `(theorem $(mkIdent declName) $sig $val)) - modifyCurLevel fun level => pure {level with goal := sig} --- TODO: Do something with the lemma name. + let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++ + ("level" ++ toString lvlIdx : String) + 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 + modifyCurLevel fun level => pure {level with + goal := sig, + description := descr.getString, + ppStatement := 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" + } -- Format.pretty <| format thmStatement.raw } /-- Define the conclusion of the current game or current level if some building a level. -/ diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean index a437ee6..70ead1d 100644 --- a/server/leanserver/GameServer/EnvExtensions.lean +++ b/server/leanserver/GameServer/EnvExtensions.lean @@ -182,15 +182,27 @@ deriving Inhabited def getCurLevelId [MonadError m] : m LevelId := do return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx} +/-- + + +Fields: +- TODO +- introduction: Theory block shown all the time. +- description: The mathematical statemtent in mathematician-readable form. +- goal: The statement in Lean. +- conclusion: Displayed when level is completed. +-/ structure GameLevel where index: Nat title: String := default introduction: String := default + description: String := default conclusion: String := default tactics: Array TacticDocEntry := default lemmas: Array LemmaDocEntry := default messages: Array GoalMessageEntry := default goal : TSyntax `Lean.Parser.Command.declSig := default + ppStatement : String := default deriving Inhabited, Repr /-! ## World -/ diff --git a/server/leanserver/GameServer/Game.lean b/server/leanserver/GameServer/Game.lean index 0043f3e..d0170be 100644 --- a/server/leanserver/GameServer/Game.lean +++ b/server/leanserver/GameServer/Game.lean @@ -29,12 +29,20 @@ def getGame (game : Name): GameServerM Game := do | throwServerError "Game not found" return game +/-- + +Fields: +- description: Lemma in mathematical language. +- descriptionGoal: Lemma printed as Lean-Code. +-/ structure LevelInfo where index : Nat title : String tactics: Array TacticDocEntry lemmas: Array LemmaDocEntry introduction : String + description : String + ppStatement : String deriving ToJson structure LoadLevelParams where @@ -62,6 +70,8 @@ partial def handleServerEvent (ev : ServerEvent) : GameServerM Bool := do title := lvl.title, tactics := lvl.tactics, lemmas := lvl.lemmas, + description := lvl.description, + ppStatement := lvl.ppStatement --toExpr <| format (lvl.goal.raw) --toString <| Syntax.formatStx (lvl.goal.raw) --Syntax.formatStx (lvl.goal.raw) , -- TODO introduction := lvl.introduction } c.hOut.writeLspResponse ⟨id, ToJson.toJson levelInfo⟩ return true diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean index 97b7f74..3b78810 100644 --- a/server/leanserver/GameServer/RpcHandlers.lean +++ b/server/leanserver/GameServer/RpcHandlers.lean @@ -24,8 +24,8 @@ structure GameGoal where deriving FromJson, ToJson -def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array String) - (hints : Array String) : MetaM GameGoal := do +def Lean.MVarId.toGameGoal (goal : MVarId) + (messages : Array String) (hints : Array String) : MetaM GameGoal := do match (← getMCtx).findDecl? goal with | none => throwError "unknown goal" | some mvarDecl => do diff --git a/server/testgame/TestGame/Levels/Level1.lean b/server/testgame/TestGame/Levels/Level1.lean index f1cf148..6ec5eac 100644 --- a/server/testgame/TestGame/Levels/Level1.lean +++ b/server/testgame/TestGame/Levels/Level1.lean @@ -20,7 +20,7 @@ After closing this message, type rfl in the invocation zone and hit Enter or cli the \"Cast spell\" button. " -Statement (x y z : ℕ) : x * y + z = x * y + z := by +Statement "" (x y z : ℕ) : x * y + z = x * y + z := by rfl Conclusion "Congratulations for completing your first level! You can now click on the *Go to next level* button." diff --git a/server/testgame/TestGame/Levels/Level2.lean b/server/testgame/TestGame/Levels/Level2.lean index 9201d72..9fd39b1 100644 --- a/server/testgame/TestGame/Levels/Level2.lean +++ b/server/testgame/TestGame/Levels/Level2.lean @@ -26,7 +26,7 @@ this substitution using the `rewrite` spell. This spell takes a list of equaliti or equivalences so you can cast `rewrite [h]`. " -Statement (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by +Statement "" (x y : ℕ) (h : y = x + 7) : 2 * y = 2 * (x + 7) := by rewrite [h] rfl diff --git a/server/testgame/TestGame/Levels/Level3.lean b/server/testgame/TestGame/Levels/Level3.lean index 74f3018..7318367 100644 --- a/server/testgame/TestGame/Levels/Level3.lean +++ b/server/testgame/TestGame/Levels/Level3.lean @@ -56,7 +56,7 @@ the *right* hand side. Try and figure out how the goal will change, and then try it. " -Statement (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by +Statement "" (a b : ℕ) (h : succ a = b) : succ (succ a) = succ b := by rewrite [h] rfl diff --git a/server/testgame/TestGame/Levels/Level4.lean b/server/testgame/TestGame/Levels/Level4.lean index ccad6c9..81ac34e 100644 --- a/server/testgame/TestGame/Levels/Level4.lean +++ b/server/testgame/TestGame/Levels/Level4.lean @@ -43,7 +43,7 @@ Observe that the goal mentions `... + succ ...`. So type and hit enter; see the goal change. " -Statement (a : ℕ ) : a + succ 0 = succ a := by +Statement "" (a : ℕ ) : a + succ 0 = succ a := by rewrite [add_succ] rewrite [add_zero] rfl diff --git a/server/testgame/TestGame/Levels/Level5.lean b/server/testgame/TestGame/Levels/Level5.lean index d302491..c919ea7 100644 --- a/server/testgame/TestGame/Levels/Level5.lean +++ b/server/testgame/TestGame/Levels/Level5.lean @@ -64,7 +64,7 @@ The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + Start by casting `induction_on n`. " -Statement (n : ℕ) : 0 + n = n := by +Statement "" (n : ℕ) : 0 + n = n := by sorry -- induction_on n -- rewrite [add_zero] diff --git a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean index 8593cf9..4ed4443 100644 --- a/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Logic/L01_Rfl.lean @@ -21,7 +21,7 @@ ersten offenen Goal zu machen. Wenn der Beweis komplett ist, erscheint \"goals accomplished\". " -Statement "Zeige `42 = 42`." : 42 = 42 := by +Statement "Zeige $ 42 = 42 $." : 42 = 42 := by rfl Message : 42 = 42 => diff --git a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean index c5a7e89..d693c49 100644 --- a/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean +++ b/server/testgame/TestGame/Levels/Logic/L03b_Assumption.lean @@ -16,10 +16,8 @@ ob die Aussage `A` wahr oder falsch ist. Mit einer Annahme `(hA : A)` nimmt man -- TODO: Macht es Sinn mehrere Aufgaben auf einer Seite zu haben? Statement mehr_triviales - " - Sei `A` eine logische Aussage und angenommen man hat einen Beweis für `A`. - Zeige, dass `A` wahr ist. - " + "Sei $ A $ eine logische Aussage und sei `hA` ein Beweis für $A$. + Zeige, dass $ A $ wahr ist." (A : Prop) (hA : A) : A := by assumption diff --git a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean index a565449..8291fae 100644 --- a/server/testgame/TestGame/Levels/Logic/L05_Apply.lean +++ b/server/testgame/TestGame/Levels/Logic/L05_Apply.lean @@ -22,10 +22,8 @@ Auf Papier würde man schreiben, \"es genügt zu zeigen, dass `A` stimmt, denn ` " Statement - " - Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`. - Zeige, dass `B` wahr ist. - " + "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`. + Zeige, dass `B` wahr ist." (A B : Prop) (hA : A) (g : A → B) : B := by apply g assumption diff --git a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean index cd04ddf..398de77 100644 --- a/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean +++ b/server/testgame/TestGame/Levels/Logic/L05b_Apply.lean @@ -18,10 +18,8 @@ Beweise Aussage `F`. " Statement - " - Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`. - Zeige, dass `B` wahr ist. - " + "Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`. + Zeige, dass `B` wahr ist." (A B C D E F : Prop) (hA : A) (f : A → B) (g : C → B) (h : B → E) (i : D → E) (k : E → F) (m : C → F) : F := by apply k diff --git a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean index 8c79b34..d184925 100644 --- a/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean +++ b/server/testgame/TestGame/Levels/Logic/L05c_Apply.lean @@ -16,6 +16,7 @@ und das Goal wird zu `B`. " Statement + "" (A B C : Prop) (f : A → B) (g : B → C) : A → C := by intro hA apply g diff --git a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean index 423f6f6..ab4e558 100644 --- a/server/testgame/TestGame/Levels/Logic/L06_Iff.lean +++ b/server/testgame/TestGame/Levels/Logic/L06_Iff.lean @@ -21,9 +21,7 @@ Gleichungen von natürlichen Zahlen. " Statement - " - Zeige dass `B ↔ C`. - " + "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₂] diff --git a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean index f2bebfb..0c91995 100644 --- a/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean +++ b/server/testgame/TestGame/Levels/Logic/L06b_Iff.lean @@ -17,9 +17,7 @@ Wenn das Goal `A ↔ B` ist, kann man mit der `constructor` Taktik, dieses in di " Statement - " - Zeige dass `B ↔ C`. - " + "Zeige dass `B ↔ C`." (A B : Prop) (mp : A → B) (mpr : B → A) : A ↔ B := by constructor assumption diff --git a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean index 12568f5..a3a0394 100644 --- a/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean +++ b/server/testgame/TestGame/Levels/Logic/L06c_Iff.lean @@ -20,6 +20,7 @@ man explizit an, wie die neuen Annahmen heissen sollen, die Klammern sind `\\<` " Statement + "" (A B : Prop) : (A ↔ B) → (A → B) := by intro h rcases h diff --git a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean b/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean index 76365ef..b986b1f 100644 --- a/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean +++ b/server/testgame/TestGame/Levels/Logic/L06d_Iff.lean @@ -17,9 +17,7 @@ Implikation `A → B` auf ein Goal `B` anwenden. " Statement - " - Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen. - " + "Benütze nur `apply` und `assumption` um das gleiche Resultat zu zeigen." (A B C : Prop) (h : A ↔ B) (g : B → C) : A → C := by intro hA apply g diff --git a/server/testgame/TestGame/Levels/Logic/L07_And.lean b/server/testgame/TestGame/Levels/Logic/L07_And.lean index a5681b3..1af28d7 100644 --- a/server/testgame/TestGame/Levels/Logic/L07_And.lean +++ b/server/testgame/TestGame/Levels/Logic/L07_And.lean @@ -20,6 +20,7 @@ Man can also genau gleich `constructor` und `rcases` anwenden, ebenso kann man " Statement + "" (A B : Prop) : (A ∧ (A → B)) ↔ (A ∧ B) := by constructor intro h diff --git a/server/testgame/TestGame/Levels/Logic/L08_Or.lean b/server/testgame/TestGame/Levels/Logic/L08_Or.lean index b573a12..e4e6cb1 100644 --- a/server/testgame/TestGame/Levels/Logic/L08_Or.lean +++ b/server/testgame/TestGame/Levels/Logic/L08_Or.lean @@ -18,7 +18,7 @@ Wenn das Goal ein `∨` ist kann man mit `left` oder `right` entscheiden, welche Seite man beweisen möchte. " -Statement (A B : Prop) (hA : A) : A ∨ (¬ B) := by +Statement "" (A B : Prop) (hA : A) : A ∨ (¬ B) := by left assumption diff --git a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean index 7d3c3ca..6923ff6 100644 --- a/server/testgame/TestGame/Levels/Logic/L08b_Or.lean +++ b/server/testgame/TestGame/Levels/Logic/L08b_Or.lean @@ -25,6 +25,7 @@ Diese Annahme benennt man dann mit `rcases h with hA | hB`. " Statement + "" (A B C D : Prop) (h : (A ∧ B) ∨ (D ∨ C)) : (A ∧ B) ∨ (C ∨ D) := by rcases h with ⟨ha, hb⟩ | (h | h) left diff --git a/server/testgame/TestGame/Levels/Logic/L08c_Or.lean b/server/testgame/TestGame/Levels/Logic/L08c_Or.lean index 5fda4e2..a8fa8b0 100644 --- a/server/testgame/TestGame/Levels/Logic/L08c_Or.lean +++ b/server/testgame/TestGame/Levels/Logic/L08c_Or.lean @@ -16,7 +16,7 @@ Introduction " Statement and_or_imp - "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen." + "Benutze alle vier Methoden mit UND und ODER umzugehen um folgende Aussage zu beweisen." (A B C : Prop) (h : (A ∧ B) ∨ (A → C)) (hA : A) : (B ∨ (C ∧ A)) := by rcases h with h₁ | h₂ left diff --git a/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean b/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean index 599ae11..c0bd94b 100644 --- a/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean +++ b/server/testgame/TestGame/Levels/Naturals/L01_Ring.lean @@ -18,7 +18,7 @@ bereits mit `rfl` bewiesen werden können. Algemeinere Gleichungen mit Variablen kann man mit der Taktik `ring` lösen. " -Statement (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by +Statement "" (x y : ℕ) : (x + y) ^ 2 = x ^ 2 + 2 * x * y + y ^ 2 := by ring Conclusion diff --git a/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean b/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean index 3993c56..421393b 100644 --- a/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean +++ b/server/testgame/TestGame/Levels/Naturals/L02_Ring.lean @@ -12,7 +12,7 @@ Introduction Ring setzt aber nicht selbständig Annahmen ein, diese muss man zuerst manuell mit `rw` verwenden. " -Statement (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by +Statement "" (x y : ℕ) (h : x = 2 * y + 1) : x ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y := by rw [h] ring diff --git a/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean b/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean index df0b272..0ec946f 100644 --- a/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean +++ b/server/testgame/TestGame/Levels/Naturals/L03_Exists.lean @@ -33,7 +33,7 @@ Hierzu gibt es 3 wichtige Taktiken: soll. Das macht man mit `use y` " -Statement even_square (n : ℕ) (h : even n) : even (n ^ 2) := by +Statement even_square "" (n : ℕ) (h : even n) : even (n ^ 2) := by unfold even at * rcases h with ⟨x, hx⟩ use 2 * x ^ 2 diff --git a/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean b/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean index 7175f1d..9fb619e 100644 --- a/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean +++ b/server/testgame/TestGame/Levels/Naturals/L04_Forall.lean @@ -19,7 +19,7 @@ Zum `∃` gehört auch das \"für alle\" `∀` (`\\forall`). Ein `∀` im Goal kann man mit `intro` angehen, genau wie bei einer Implikation `→`. " -Statement : ∀ (x : ℕ), (even x) → odd (1 + x) := by +Statement "" : ∀ (x : ℕ), (even x) → odd (1 + x) := by intro x h unfold even at h unfold odd diff --git a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean b/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean index ad47fb0..90f0417 100644 --- a/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean +++ b/server/testgame/TestGame/Levels/Naturals/L31_Sum.lean @@ -13,7 +13,7 @@ TODO: Summe " -Statement : True := by +Statement "" : True := by trivial Conclusion diff --git a/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean b/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean index 9314c64..2e4ce58 100644 --- a/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean +++ b/server/testgame/TestGame/Levels/Naturals/L32_Induction.lean @@ -13,7 +13,7 @@ TODO: Induktion (& induktion vs rcases) " -Statement : True := by +Statement "" : True := by trivial Conclusion diff --git a/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean b/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean index 06592b4..acce168 100644 --- a/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean +++ b/server/testgame/TestGame/Levels/Naturals/L33_Prime.lean @@ -13,7 +13,7 @@ TODO: Primzahl " -Statement : True := by +Statement "" : True := by trivial Conclusion diff --git a/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean b/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean index f669cf2..de45f47 100644 --- a/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean +++ b/server/testgame/TestGame/Levels/Naturals/L34_ExistsUnique.lean @@ -13,7 +13,7 @@ TODO: Es existiert genau eine gerade Primzahl. " -Statement : True := by +Statement "" : True := by trivial Conclusion diff --git a/server/testgame/TestGame/Levels/Negation/L01_False.lean b/server/testgame/TestGame/Levels/Negation/L01_False.lean index a2ca589..814307c 100644 --- a/server/testgame/TestGame/Levels/Negation/L01_False.lean +++ b/server/testgame/TestGame/Levels/Negation/L01_False.lean @@ -22,7 +22,7 @@ Der einfachste Widerspruch ist wenn man einen Beweis von `false` hat: " Statement - "Ein Widerspruch impliziert alles." + "Ein Widerspruch impliziert alles." (A : Prop) (h : false) : A := by contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L02_Contra.lean b/server/testgame/TestGame/Levels/Negation/L02_Contra.lean index 6a844ea..fa5b14e 100644 --- a/server/testgame/TestGame/Levels/Negation/L02_Contra.lean +++ b/server/testgame/TestGame/Levels/Negation/L02_Contra.lean @@ -17,7 +17,7 @@ also `(h : A)` und `(g : ¬ A)`. (`\\not`) " Statement - "Ein Widerspruch impliziert alles." + "Ein Widerspruch impliziert alles." (n : ℕ) (h : even n) (g : ¬ (even n)) : n = 128 := by contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L03_Contra.lean b/server/testgame/TestGame/Levels/Negation/L03_Contra.lean index a7ad661..a7c7e8e 100644 --- a/server/testgame/TestGame/Levels/Negation/L03_Contra.lean +++ b/server/testgame/TestGame/Levels/Negation/L03_Contra.lean @@ -22,8 +22,8 @@ Hier musst du zuerst eines der Lemmas `not_odd : ¬ odd n ↔ even n` oder " Statement - "Ein Widerspruch impliziert alles." - (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by + "Ein Widerspruch impliziert alles." + (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by rw [← not_even] at h₂ contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L04_Contra.lean b/server/testgame/TestGame/Levels/Negation/L04_Contra.lean index 992f977..d22ba56 100644 --- a/server/testgame/TestGame/Levels/Negation/L04_Contra.lean +++ b/server/testgame/TestGame/Levels/Negation/L04_Contra.lean @@ -16,7 +16,7 @@ oder auch Annahmen der Form `A ≠ A` (`\\ne`). " Statement - "Ein Widerspruch impliziert alles." + "Ein Widerspruch impliziert alles." (A : Prop) (a b c : ℕ) (g₁ : a = b) (g₂ : b = c) (h : a ≠ c) : A := by rw [g₁] at h contradiction diff --git a/server/testgame/TestGame/Levels/Negation/L05_Not.lean b/server/testgame/TestGame/Levels/Negation/L05_Not.lean index bf1012d..b5abba9 100644 --- a/server/testgame/TestGame/Levels/Negation/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Negation/L05_Not.lean @@ -15,6 +15,7 @@ wie im nächsten Level dann gezeigt wird. Manchmal aber hat man Terme der Form " Statement + "" (A : Prop) : ¬ (¬ A) ↔ A := by rw [not_not] diff --git a/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean b/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean index 4cfd4e2..b8d1962 100644 --- a/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean +++ b/server/testgame/TestGame/Levels/Negation/L06_ByContra.lean @@ -19,7 +19,7 @@ dass das Gegenteil des Goals wahr sei, und dann einen Widerspruch erzeugen. " Statement - "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch." + "Ist n² ungerade, so ist auch n ungerade. Beweise durch Widerspruch." (n : ℕ) (h : odd (n ^ 2)) : odd n := by by_contra g rw [not_odd] at g diff --git a/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean b/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean index f273736..b3db2af 100644 --- a/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean +++ b/server/testgame/TestGame/Levels/Negation/L07_Contrapose.lean @@ -22,7 +22,7 @@ Wenn das Goal eine Implikation ist, kann man `contrapose` anwenden. " Statement - "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition." + "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition." (n : ℕ) : odd (n ^ 2) → odd n := by contrapose rw [not_odd] diff --git a/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean b/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean index 50b458f..c08166e 100644 --- a/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean +++ b/server/testgame/TestGame/Levels/Negation/L08_Contrapose.lean @@ -20,7 +20,7 @@ Implikationsannahme ins Goal schreiben. " Statement - "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition." + "Ist n² ungerade, so ist auch n ungerade. Beweise durch Kontraposition." (n : ℕ) (h : odd (n ^ 2)): odd n := by revert h contrapose diff --git a/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean b/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean index c759ba1..3a8f8dd 100644 --- a/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean +++ b/server/testgame/TestGame/Levels/Negation/L09_PushNeg.lean @@ -17,8 +17,8 @@ mit `push_neg` das `¬` durch den Quantor hindurchschieben. " Statement - "Es existiert keine natürliche Zahl, die grösser als alle anderen." - : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by + "Es existiert keine natürliche Zahl, die grösser als alle anderen.": + ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by push_neg intro n use 3*n + 6