From 93d05c9703804d9f6da5af4866535d790ffde67a Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Wed, 8 Mar 2023 09:30:01 +0100 Subject: [PATCH] rename [New/Only/Disabled][Tactic/Lemma/Definition] --- server/leanserver/GameServer/Commands.lean | 18 +++++++++--------- .../Levels/Contradiction/L01_Have.lean | 8 ++++---- .../Levels/Contradiction/L02_Suffices.lean | 8 ++++---- .../Levels/Contradiction/L03_ByContra.lean | 2 +- .../Levels/Contradiction/L04_ByContra.lean | 2 +- .../Levels/Contradiction/L05_Contrapose.lean | 6 +++--- .../Levels/Contradiction/L06_Summary.lean | 6 +++--- .../TestGame/Levels/Function/L02_Let.lean | 4 ++-- .../Levels/Function/L03_Composition.lean | 2 +- .../Levels/Function/L06_Piecewise.lean | 4 ++-- .../Levels/Function/L07'_Injective.lean | 4 ++-- .../Levels/Function/L07_Injective.lean | 2 +- .../TestGame/Levels/Implication/L01_Intro.lean | 2 +- .../Levels/Implication/L02_Revert.lean | 2 +- .../TestGame/Levels/Implication/L03_Apply.lean | 2 +- .../TestGame/Levels/Implication/L04_Apply.lean | 2 +- .../TestGame/Levels/Implication/L05_Apply.lean | 2 +- .../TestGame/Levels/Implication/L06_Iff.lean | 2 +- .../TestGame/Levels/Implication/L07_Rw.lean | 2 +- .../TestGame/Levels/Implication/L08_Iff.lean | 2 +- .../TestGame/Levels/Implication/L09_Iff.lean | 2 +- .../TestGame/Levels/Implication/L10_Apply.lean | 4 ++-- .../TestGame/Levels/Implication/L11_Rw.lean | 4 ++-- .../Levels/Implication/L12_Summary.lean | 4 ++-- .../Levels/Induction/L01_Induction.lean | 2 +- .../TestGame/Levels/Inequality/L02_Pos.lean | 4 ++-- .../Levels/Inequality/L03_Linarith.lean | 4 ++-- .../Levels/Inequality/T_Induction.lean | 2 +- .../LeanStuff/L03_ImplicitArguments.lean | 4 ++-- .../LeanStuff/L04_InstanceArguments.lean | 4 ++-- .../TestGame/Levels/LeftOvers/L09_Or.lean | 2 +- .../TestGame/Levels/LeftOvers/L33_Prime.lean | 2 +- .../Levels/LeftOvers/L34_ExistsUnique.lean | 2 +- .../TestGame/Levels/LeftOvers/Lxx_Prime.lean | 2 +- .../Levels/LeftOvers/xx_Functions.lean | 2 +- .../LinearAlgebra/L02_VectorNotation.lean | 2 +- .../LinearAlgebra/L08_GeneratingSet.lean | 2 +- .../TestGame/Levels/Predicate/L01_Ring.lean | 2 +- .../TestGame/Levels/Predicate/L02_Rewrite.lean | 2 +- .../TestGame/Levels/Predicate/L03_Rewrite.lean | 2 +- .../TestGame/Levels/Predicate/L04_Ring.lean | 2 +- .../TestGame/Levels/Predicate/L05_Rfl.lean | 2 +- .../TestGame/Levels/Predicate/L06_Exists.lean | 4 ++-- .../TestGame/Levels/Predicate/L07_Forall.lean | 2 +- .../TestGame/Levels/Predicate/L08_PushNeg.lean | 6 +++--- .../TestGame/Levels/Predicate/L09_Summary.lean | 6 +++--- .../TestGame/Levels/Prime/L04_Prime.lean | 2 +- .../TestGame/Levels/Proposition/L00_Tauto.lean | 2 +- .../TestGame/Levels/Proposition/L01_Rfl.lean | 4 ++-- .../Levels/Proposition/L02_Assumption.lean | 4 ++-- .../Levels/Proposition/L03_Assumption.lean | 4 ++-- .../TestGame/Levels/Proposition/L04_True.lean | 4 ++-- .../TestGame/Levels/Proposition/L05_Not.lean | 4 ++-- .../TestGame/Levels/Proposition/L06_False.lean | 4 ++-- .../Levels/Proposition/L07_ContraNotEq.lean | 4 ++-- .../Levels/Proposition/L08_Contra.lean | 4 ++-- .../TestGame/Levels/Proposition/L09_And.lean | 4 ++-- .../TestGame/Levels/Proposition/L10_And.lean | 4 ++-- .../TestGame/Levels/Proposition/L11_Or.lean | 4 ++-- .../TestGame/Levels/Proposition/L12_Or.lean | 4 ++-- .../Levels/Proposition/L13_Summary.lean | 4 ++-- .../TestGame/Levels/SetTheory/L01_Univ.lean | 2 +- .../TestGame/Levels/SetTheory/L03_Subset.lean | 2 +- .../Levels/SetTheory/L04_SubsetEmpty.lean | 4 ++-- .../TestGame/Levels/SetTheory/L05_Empty.lean | 4 ++-- .../Levels/SetTheory/L06_Nonempty.lean | 4 ++-- .../Levels/SetTheory/L07_UnionInter.lean | 4 ++-- .../Levels/SetTheory/L08_UnionInter.lean | 4 ++-- .../Levels/SetTheory/L09_Complement.lean | 4 ++-- .../TestGame/Levels/SetTheory/L10_Morgan.lean | 4 ++-- .../TestGame/Levels/SetTheory/L11_SSubset.lean | 4 ++-- .../TestGame/Levels/SetTheory/L12_Insert.lean | 4 ++-- .../TestGame/Levels/SetTheory/L13_Insert.lean | 2 +- .../TestGame/Levels/SetTheory/L14_SetOf.lean | 4 ++-- .../Levels/SetTheory/L15_Powerset.lean | 4 ++-- .../Levels/SetTheory/L16_Disjoint.lean | 4 ++-- .../TestGame/Levels/SetTheory/L17_SetOf.lean | 4 ++-- .../TestGame/Levels/SetTheory/L18_SetOf.lean | 4 ++-- .../TestGame/Levels/SetTheory/L19_Subtype.lean | 4 ++-- .../Levels/SetTheory/L20_UnionInter.lean | 4 ++-- .../TestGame/Levels/SetTheory/L21_Summary.lean | 4 ++-- .../TestGame/Levels/SetTheory/T01_Set.lean | 2 +- .../TestGame/Levels/StatementTest.lean | 2 +- .../testgame/TestGame/Levels/Sum/L01_Simp.lean | 2 +- .../testgame/TestGame/Levels/Sum/L02_Sum.lean | 2 +- .../TestGame/Levels/Sum/L03_ArithSum.lean | 4 ++-- .../TestGame/Levels/Sum/L05_SumComm.lean | 2 +- .../TestGame/Levels/Sum/L06_Summary.lean | 2 +- .../TestGame/Levels/Sum/T01_Induction.lean | 2 +- .../TestGame/Levels/Sum/T02_Induction.lean | 2 +- .../TestGame/Levels/Sum/T03__Bernoulli.lean | 2 +- 91 files changed, 155 insertions(+), 155 deletions(-) diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean index b34cda7..4b99dc7 100644 --- a/server/leanserver/GameServer/Commands.lean +++ b/server/leanserver/GameServer/Commands.lean @@ -201,19 +201,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 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 +231,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 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 +264,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 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}} diff --git a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean index d1a9c7e..49db5d7 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L01_Have.lean @@ -63,8 +63,8 @@ have k : ¬ B Conclusion "" -NewTactics «have» -DisabledTactics «suffices» +NewTactic «have» +DisabledTactic «suffices» -NewDefinitions Even Odd -NewLemmas not_even not_odd +NewDefinition Even Odd +NewLemma not_even not_odd diff --git a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean index 166b309..ea7b30e 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L02_Suffices.lean @@ -60,7 +60,7 @@ Hint (A : Prop) (B : Prop) (h : A → ¬ B) (k : A) (f : B) : False => Conclusion "" -NewTactics «suffices» -DisabledTactics «have» -NewDefinitions Even Odd -NewLemmas not_even not_odd +NewTactic «suffices» +DisabledTactic «have» +NewDefinition Even Odd +NewLemma not_even not_odd diff --git a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean index ebd0351..d93a2ef 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L03_ByContra.lean @@ -52,4 +52,4 @@ HiddenHint (A : Prop) (B : Prop) (h : A → B) (b : ¬ B) (a : A) : False => Conclusion "" -NewTactics by_contra contradiction apply assumption +NewTactic by_contra contradiction apply assumption diff --git a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean index c67c016..aac1725 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L04_ByContra.lean @@ -46,4 +46,4 @@ HiddenHint (A : Prop) (B : Prop) : A → B ↔ (¬ B → ¬ A) => Conclusion "" -NewTactics contradiction constructor intro by_contra apply assumption +NewTactic contradiction constructor intro by_contra apply assumption diff --git a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean index eeb5a42..8c4d537 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L05_Contrapose.lean @@ -61,6 +61,6 @@ Hint (n : ℕ) : Even n → ¬Odd (n ^ 2) => Hint (n : ℕ) : Even n → Even (n ^ 2) => "Diese Aussage hast du bereits als Lemma bewiesen, schau mal in der Bibliothek." -NewTactics contrapose rw apply -NewDefinitions Even Odd -NewLemmas not_even not_odd even_square +NewTactic contrapose rw apply +NewDefinition Even Odd +NewLemma not_even not_odd even_square diff --git a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean index abd7c15..6d08b85 100644 --- a/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean +++ b/server/testgame/TestGame/Levels/Contradiction/L06_Summary.lean @@ -71,6 +71,6 @@ 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 +NewTactic contradiction by_contra rw apply assumption -- TODO: suffices, have +NewDefinition Even Odd +NewLemma not_odd not_even even_square diff --git a/server/testgame/TestGame/Levels/Function/L02_Let.lean b/server/testgame/TestGame/Levels/Function/L02_Let.lean index 247c040..ba03a6a 100644 --- a/server/testgame/TestGame/Levels/Function/L02_Let.lean +++ b/server/testgame/TestGame/Levels/Function/L02_Let.lean @@ -58,8 +58,8 @@ show that $f(x) = x^2 + 2x + 1$. unfold f ring -NewTactics «let» -OnlyTactics «let» intro unfold ring +NewTactic «let» +OnlyTactic «let» intro unfold ring HiddenHint : ∀ x, f x = x ^ 2 + 2 * x + 1 => "Fang zuerst wie immer mit `intro x` an." diff --git a/server/testgame/TestGame/Levels/Function/L03_Composition.lean b/server/testgame/TestGame/Levels/Function/L03_Composition.lean index 416e8bb..75510e8 100644 --- a/server/testgame/TestGame/Levels/Function/L03_Composition.lean +++ b/server/testgame/TestGame/Levels/Function/L03_Composition.lean @@ -19,4 +19,4 @@ Statement (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 +NewLemma Function.comp_apply diff --git a/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean b/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean index 97bbfcd..5452fb6 100644 --- a/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean +++ b/server/testgame/TestGame/Levels/Function/L06_Piecewise.lean @@ -57,9 +57,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 => diff --git a/server/testgame/TestGame/Levels/Function/L07'_Injective.lean b/server/testgame/TestGame/Levels/Function/L07'_Injective.lean index 8b2447c..55ee53e 100644 --- a/server/testgame/TestGame/Levels/Function/L07'_Injective.lean +++ b/server/testgame/TestGame/Levels/Function/L07'_Injective.lean @@ -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) => diff --git a/server/testgame/TestGame/Levels/Function/L07_Injective.lean b/server/testgame/TestGame/Levels/Function/L07_Injective.lean index cbc45a5..a06c12d 100644 --- a/server/testgame/TestGame/Levels/Function/L07_Injective.lean +++ b/server/testgame/TestGame/Levels/Function/L07_Injective.lean @@ -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/Implication/L01_Intro.lean b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean index 292005b..9d21ef4 100644 --- a/server/testgame/TestGame/Levels/Implication/L01_Intro.lean +++ b/server/testgame/TestGame/Levels/Implication/L01_Intro.lean @@ -37,4 +37,4 @@ HiddenHint (A : Prop) (B : Prop) (hb : B) : A → (A ∧ B) => Hint (A : Prop) (B : Prop) (ha : A) (hb : B) : (A ∧ B) => "Jetzt kannst du die Taktiken aus dem letzten Kapitel verwenden." -NewTactics intro constructor assumption +NewTactic intro constructor assumption diff --git a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean index 74452a8..e69ba33 100644 --- a/server/testgame/TestGame/Levels/Implication/L02_Revert.lean +++ b/server/testgame/TestGame/Levels/Implication/L02_Revert.lean @@ -39,4 +39,4 @@ dass $B$ wahr ist." 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." -NewTactics revert assumption +NewTactic revert assumption diff --git a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean index 71272b2..bca4093 100644 --- a/server/testgame/TestGame/Levels/Implication/L03_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L03_Apply.lean @@ -32,7 +32,7 @@ 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." -NewTactics apply assumption +NewTactic apply assumption -- 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..b6f2a5e 100644 --- a/server/testgame/TestGame/Levels/Implication/L04_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L04_Apply.lean @@ -32,4 +32,4 @@ HiddenHint (A : Prop) (B : Prop) (C : Prop) (hA : A) (f : A → B) (g : B → C) "Du willst $C$ beweisen. Suche also nach einer Implikation $\\ldots \\Rightarrow C$ und wende diese mit `apply` an." -NewTactics intro apply assumption revert +NewTactic intro apply assumption revert diff --git a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean index 83292a5..900eb37 100644 --- a/server/testgame/TestGame/Levels/Implication/L05_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L05_Apply.lean @@ -48,6 +48,6 @@ Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (E : Prop) (F : Prop) (i : D → E) (k : E → F) (m : C → F) : D => "Sackgasse. Probier doch einen anderen Weg." -NewTactics apply assumption revert intro +NewTactic apply assumption revert intro -- 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..3291e10 100644 --- a/server/testgame/TestGame/Levels/Implication/L06_Iff.lean +++ b/server/testgame/TestGame/Levels/Implication/L06_Iff.lean @@ -38,6 +38,6 @@ aus mehreren Einzelteilen besteht: `⟨A → B, B → A⟩`. Man sagt also Lean, ob das Goal aus solchen Einzelteilen \"konstruiert\" werden kann. " -NewTactics constructor assumption +NewTactic constructor assumption -- 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..0f17917 100644 --- a/server/testgame/TestGame/Levels/Implication/L07_Rw.lean +++ b/server/testgame/TestGame/Levels/Implication/L07_Rw.lean @@ -71,4 +71,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (D : Prop) (h₁ : C ↔ D) (h₂ : D ↔ "Das ist nicht der optimale Weg..." -NewTactics rw assumption +NewTactic rw assumption diff --git a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean index 0bf64f0..0808a39 100644 --- a/server/testgame/TestGame/Levels/Implication/L08_Iff.lean +++ b/server/testgame/TestGame/Levels/Implication/L08_Iff.lean @@ -41,4 +41,4 @@ Hint (A : Prop) (B : Prop) (C : Prop) (h : A ↔ B) (g : B → C) (hA : A) : B = Conclusion "Im nächsten Level findest du die zweite Option." -NewTactics apply assumption +NewTactic apply assumption diff --git a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean index a3c6fe2..4ee0cb8 100644 --- a/server/testgame/TestGame/Levels/Implication/L09_Iff.lean +++ b/server/testgame/TestGame/Levels/Implication/L09_Iff.lean @@ -36,7 +36,7 @@ Conclusion " " -NewTactics intro apply rcases assumption +NewTactic intro apply rcases assumption -- -- 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..2926e69 100644 --- a/server/testgame/TestGame/Levels/Implication/L10_Apply.lean +++ b/server/testgame/TestGame/Levels/Implication/L10_Apply.lean @@ -50,6 +50,6 @@ Conclusion " " -NewTactics apply left right assumption +NewTactic apply left right assumption -NewLemmas not_or_of_imp +NewLemma not_or_of_imp diff --git a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean index 1151fb4..cccdd84 100644 --- a/server/testgame/TestGame/Levels/Implication/L11_Rw.lean +++ b/server/testgame/TestGame/Levels/Implication/L11_Rw.lean @@ -34,6 +34,6 @@ Conclusion `rw` hat automatisch `rfl` ausgeführt und dadurch den Beweis beendet. " -NewTactics rw +NewTactic rw -NewLemmas not_not not_or_of_imp +NewLemma not_not not_or_of_imp diff --git a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean index 7a64ade..ef67410 100644 --- a/server/testgame/TestGame/Levels/Implication/L12_Summary.lean +++ b/server/testgame/TestGame/Levels/Implication/L12_Summary.lean @@ -76,6 +76,6 @@ HiddenHint (A : Prop) (B: Prop) (h : ¬ A ∨ B) (ha : A) : B => HiddenHint (A : Prop) (B: Prop) (ha : A) (ha' : ¬A) : B => "Findest du einen Widerspruch?" -NewTactics rfl assumption trivial left right constructor rcases +NewTactic rfl assumption trivial left right constructor rcases -NewLemmas not_not not_or_of_imp +NewLemma not_not not_or_of_imp 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/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/L01_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean index 52d5908..7a6c6dd 100644 --- a/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean +++ b/server/testgame/TestGame/Levels/Predicate/L01_Ring.lean @@ -39,6 +39,6 @@ Ring zu lösen, funktioniert aber auch auf `ℕ`, auch wenn dieses kein Ring ist (erst `ℤ` ist ein Ring). " -NewTactics ring +NewTactic ring #eval 4 / 6 diff --git a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean index defa2fa..38c3fcb 100644 --- a/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean +++ b/server/testgame/TestGame/Levels/Predicate/L02_Rewrite.lean @@ -67,4 +67,4 @@ Hint (a : ℕ) (b : ℕ) (c : ℕ) (d : ℕ) (h₁ : c = d) (h₂ : d = b) (h₃ Conclusion "Übrigens, mit `rw [h₁, ←h₂]` könnte man mehrere `rw` zusammenfassen." -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..520fe2f 100644 --- a/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean +++ b/server/testgame/TestGame/Levels/Predicate/L03_Rewrite.lean @@ -37,4 +37,4 @@ Hint (a : ℕ) (b : ℕ) (h : a = b) (g : a + a ^ 2 = b + 1) : a + a ^ 2 = a + 1 Conclusion "Übrigens, mit `rw [h] at *` kann man im weiteren `h` in **allen** Annahmen und dem Goal umschreiben." -NewTactics assumption rw +NewTactic assumption rw diff --git a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean index 3d1f19d..29edc30 100644 --- a/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean +++ b/server/testgame/TestGame/Levels/Predicate/L04_Ring.lean @@ -30,4 +30,4 @@ Hint (y : ℕ) : (2 * y + 1) ^ 2 = 4 * y ^ 2 + 3 * y + 1 + y => Conclusion "" -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..ac77ee1 100644 --- a/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean +++ b/server/testgame/TestGame/Levels/Predicate/L05_Rfl.lean @@ -28,4 +28,4 @@ Conclusion aufzurufen, deshalb brauchst du das nur noch selten. " -NewTactics rfl +NewTactic rfl diff --git a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean index 196c372..6e2ae33 100644 --- a/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean +++ b/server/testgame/TestGame/Levels/Predicate/L06_Exists.lean @@ -67,5 +67,5 @@ Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : n ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 => Hint (n : ℕ) (x : ℕ) (hx : n = x + x) : (x + x) ^ 2 = 2 * x ^ 2 + 2 * x ^ 2 => "Die Taktik `ring` löst solche Gleichungen." -NewTactics unfold rcases use rw ring -NewDefinitions Even Odd +NewTactic unfold rcases use rw ring +NewDefinition Even Odd diff --git a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean index 5e1b812..fd493fc 100644 --- a/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean +++ b/server/testgame/TestGame/Levels/Predicate/L07_Forall.lean @@ -50,4 +50,4 @@ Hint (n : ℕ) (hn : Odd n) (h : ∀ (x : ℕ), (Odd x) → Even (x + 1)) : Even Conclusion "Für-alle-Statements, Implikationen und Lemmas/Theoreme verhalten sich alle praktisch gleich. Mehr dazu später." -NewTactics ring intro unfold +NewTactic ring intro unfold diff --git a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean index 3f14063..06f858d 100644 --- a/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean +++ b/server/testgame/TestGame/Levels/Predicate/L08_PushNeg.lean @@ -62,6 +62,6 @@ 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 +NewTactic push_neg intro use rw unfold ring +NewDefinition Even Odd +NewLemma not_even not_odd not_exists not_forall diff --git a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean index 2cb1a6c..9337093 100644 --- a/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean +++ b/server/testgame/TestGame/Levels/Predicate/L09_Summary.lean @@ -50,6 +50,6 @@ Statement Conclusion "" -NewTactics push_neg intro use rw unfold ring -NewDefinitions Even Odd -NewLemmas not_even not_odd not_exists not_forall +NewTactic push_neg intro use rw unfold ring +NewDefinition Even Odd +NewLemma 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 99ca026..400c2f2 100644 --- a/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean +++ b/server/testgame/TestGame/Levels/Proposition/L00_Tauto.lean @@ -47,4 +47,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..74749db 100644 --- a/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean +++ b/server/testgame/TestGame/Levels/Proposition/L01_Rfl.lean @@ -31,5 +31,5 @@ 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..4a6f09f 100644 --- a/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L02_Assumption.lean @@ -41,5 +41,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..9579d2a 100644 --- a/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean +++ b/server/testgame/TestGame/Levels/Proposition/L03_Assumption.lean @@ -34,5 +34,5 @@ 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..88e26aa 100644 --- a/server/testgame/TestGame/Levels/Proposition/L04_True.lean +++ b/server/testgame/TestGame/Levels/Proposition/L04_True.lean @@ -35,5 +35,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..6f2ea13 100644 --- a/server/testgame/TestGame/Levels/Proposition/L05_Not.lean +++ b/server/testgame/TestGame/Levels/Proposition/L05_Not.lean @@ -33,5 +33,5 @@ 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 73c5482..5bcb6e2 100644 --- a/server/testgame/TestGame/Levels/Proposition/L06_False.lean +++ b/server/testgame/TestGame/Levels/Proposition/L06_False.lean @@ -45,5 +45,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 b216517..2d27c5b 100644 --- a/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean +++ b/server/testgame/TestGame/Levels/Proposition/L07_ContraNotEq.lean @@ -39,5 +39,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 4a5feb5..3a0043b 100644 --- a/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean +++ b/server/testgame/TestGame/Levels/Proposition/L08_Contra.lean @@ -33,5 +33,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..6456d35 100644 --- a/server/testgame/TestGame/Levels/Proposition/L09_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L09_And.lean @@ -54,5 +54,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 377e5b7..c2000c0 100644 --- a/server/testgame/TestGame/Levels/Proposition/L10_And.lean +++ b/server/testgame/TestGame/Levels/Proposition/L10_And.lean @@ -47,5 +47,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..712ad00 100644 --- a/server/testgame/TestGame/Levels/Proposition/L11_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L11_Or.lean @@ -44,5 +44,5 @@ 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..9b90569 100644 --- a/server/testgame/TestGame/Levels/Proposition/L12_Or.lean +++ b/server/testgame/TestGame/Levels/Proposition/L12_Or.lean @@ -125,5 +125,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..3be2eba 100644 --- a/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean +++ b/server/testgame/TestGame/Levels/Proposition/L13_Summary.lean @@ -74,5 +74,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/L01_Univ.lean b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean index 90ff1f8..a515da6 100644 --- a/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean +++ b/server/testgame/TestGame/Levels/SetTheory/L01_Univ.lean @@ -39,4 +39,4 @@ Statement mem_univ trivial -- tauto -NewTactics tauto trivial +NewTactic tauto trivial diff --git a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean index eac4906..801ad43 100644 --- a/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean +++ b/server/testgame/TestGame/Levels/SetTheory/L03_Subset.lean @@ -39,7 +39,7 @@ Statement subset_empty_iff intro h hA 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..83e8429 100644 --- a/server/testgame/TestGame/Levels/Sum/L02_Sum.lean +++ b/server/testgame/TestGame/Levels/Sum/L02_Sum.lean @@ -34,7 +34,7 @@ Statement simp ring -NewLemmas Finset.sum_add_distrib add_comm +NewLemma Finset.sum_add_distrib add_comm 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." 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