From b1dc4d71b362cce008a79a2db3b057155f63a730 Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 14 Apr 2023 10:48:46 +0200
Subject: [PATCH] named Statements are added to context with there specified
 name

---
 .../Levels/Contradiction/L05_Contrapose.lean  |  2 +-
 .../Levels/Contradiction/L06_Summary.lean     |  2 +
 server/adam/Adam/Levels/Sum/L04_SumOdd.lean   |  2 +
 server/adam/Adam/Levels/Sum/L05_SumComm.lean  |  2 +-
 server/adam/Adam/Levels/Sum/L06_Summary.lean  |  4 +-
 server/adam/Adam/Options/ArithSum.lean        | 13 ------
 server/adam/Adam/ToBePorted.lean              |  6 ---
 server/leanserver/GameServer/Commands.lean    | 42 +++++++++++++------
 server/nng/NNG/Levels/Addition/Level_2.lean   |  8 ----
 server/nng/NNG/Levels/Addition/Level_3.lean   | 11 -----
 server/nng/NNG/Levels/Addition/Level_4.lean   | 10 -----
 server/nng/NNG/Levels/Addition/Level_5.lean   | 10 -----
 12 files changed, 38 insertions(+), 74 deletions(-)
 delete mode 100644 server/adam/Adam/Options/ArithSum.lean

diff --git a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean
index 33b9308..ca0e523 100644
--- a/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean
+++ b/server/adam/Adam/Levels/Contradiction/L05_Contrapose.lean
@@ -2,6 +2,7 @@ import Adam.Metadata
 import Std.Tactic.RCases
 
 import Adam.ToBePorted
+import Adam.Levels.Predicate.L06_Exists
 
 Game "Adam"
 World "Contradiction"
@@ -53,7 +54,6 @@ Statement (n : ℕ) (h : Odd (n ^ 2)): Odd n := by
   `even_square` anwenden!"
   apply even_square
 
-NewLemma even_square
 NewTactic contrapose
 DisabledTactic by_contra
 LemmaTab "Nat"
diff --git a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean
index 3acae7a..f22927c 100644
--- a/server/adam/Adam/Levels/Contradiction/L06_Summary.lean
+++ b/server/adam/Adam/Levels/Contradiction/L06_Summary.lean
@@ -1,6 +1,8 @@
 import Adam.Metadata
 
 import Adam.ToBePorted
+import Adam.Levels.Predicate.L06_Exists
+
 
 Game "Adam"
 World "Contradiction"
diff --git a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean
index 93cf12e..b2692bd 100644
--- a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean
+++ b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean
@@ -3,6 +3,8 @@ import Adam.Metadata
 import Adam.ToBePorted
 import Adam.Options.MathlibPart
 
+import Adam.Levels.Sum.L03_ArithSum
+
 Game "Adam"
 World "Sum"
 Level 4
diff --git a/server/adam/Adam/Levels/Sum/L05_SumComm.lean b/server/adam/Adam/Levels/Sum/L05_SumComm.lean
index c6d4f2a..eddf617 100644
--- a/server/adam/Adam/Levels/Sum/L05_SumComm.lean
+++ b/server/adam/Adam/Levels/Sum/L05_SumComm.lean
@@ -3,7 +3,7 @@ import Adam.Metadata
 import Adam.ToBePorted
 import Adam.Options.MathlibPart
 
-import Adam.Options.ArithSum
+import Adam.Levels.Sum.L04_SumOdd
 
 set_option tactic.hygienic false
 
diff --git a/server/adam/Adam/Levels/Sum/L06_Summary.lean b/server/adam/Adam/Levels/Sum/L06_Summary.lean
index 7c68f7b..8bbd9c2 100644
--- a/server/adam/Adam/Levels/Sum/L06_Summary.lean
+++ b/server/adam/Adam/Levels/Sum/L06_Summary.lean
@@ -3,7 +3,7 @@ import Adam.Metadata
 import Adam.ToBePorted
 import Adam.Options.MathlibPart
 
-import Adam.Options.ArithSum
+import Adam.Levels.Sum.L05_SumComm
 
 Game "Adam"
 World "Sum"
@@ -82,7 +82,7 @@ Statement (m : ℕ) : (∑ i : Fin (m + 1), (i : ℕ)^3) = (∑ i : Fin (m + 1),
   Hint "**Du**: Jetzt sollten es eigentlich nur noch arithmetische Operationen sein."
   ring
 
-NewLemma arithmetic_sum add_pow_two
+NewLemma add_pow_two
 LemmaTab "Sum"
 
 Conclusion "Der Golem denkt ganz lange nach, und ihr bekommt das Gefühl, dass er gar nie
diff --git a/server/adam/Adam/Options/ArithSum.lean b/server/adam/Adam/Options/ArithSum.lean
deleted file mode 100644
index 6019a33..0000000
--- a/server/adam/Adam/Options/ArithSum.lean
+++ /dev/null
@@ -1,13 +0,0 @@
-import Adam.Options.MathlibPart
-
-open BigOperators
-
-lemma arithmetic_sum (n : ℕ) : 2 * (∑ i : Fin (n + 1), ↑i) = n * (n + 1) := by
-  induction' n with n hn
-  simp
-  rw [Fin.sum_univ_castSucc]
-  rw [mul_add]
-  simp
-  rw [mul_add, hn]
-  simp_rw [Nat.succ_eq_one_add]
-  ring
diff --git a/server/adam/Adam/ToBePorted.lean b/server/adam/Adam/ToBePorted.lean
index 4fa6321..5e6ef93 100644
--- a/server/adam/Adam/ToBePorted.lean
+++ b/server/adam/Adam/ToBePorted.lean
@@ -29,12 +29,6 @@ def delabFinsetSum : Delab := do
 -- lemma not_even {n : ℕ} : ¬ Even n ↔ Odd n := by
 --   sorry
 
-lemma even_square (n : ℕ) : Even n → Even (n ^ 2) := by
-  intro ⟨x, hx⟩
-  unfold Even at *
-  use 2 * x ^ 2
-  rw [hx]
-  ring
 
 -- section powerset
 
diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 86e449f..996e505 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -204,8 +204,6 @@ If omitted, the current tab will remain open. -/
 elab "LemmaTab"  category:str : command =>
   modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
 
-
-
 /-! # Exercise Statement -/
 
 -- TODO: Instead of this, it would be nice to have a proper syntax parser that enables
@@ -226,24 +224,44 @@ def reprint (stx : Syntax) : Format :=
 
 /-- Define the statement of the current level. -/
 elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
+  let lvlIdx ← getCurLevelIdx
+
+  -- Save the messages before evaluation of the proof.
+  let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
 
-  -- Check that the statement name is a lemma in the doc
+  -- Check that statement has a docs entry.
   match statementName with
   | some name => checkInventoryDoc .Lemma name.getId
   | none => pure ()
 
-  let lvlIdx ← getCurLevelIdx
+  -- The default name of the statement is `[Game].[World].level[no.]`, e.g. `NNG.Addition.level1`
+  -- However, this should not be used when designing the game.
   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
+  -- Add theorem to context.
+  match statementName with
+  | some name =>
+    let env ← getEnv
+    if env.contains name.getId then
+      logWarningAt name s!"Environment already contains {name.getId}! Only the existing statement will be available in later levels."
+      -- TODO: Check if the two agree. turn into `logInfo` in that case.
+      -- let origType := (env.constants.map₁.find! name.getId).type
+      -- -- let newType := (env.constants.map₁.find! defaultDeclName).type
+      -- dbg_trace sig
+      -- dbg_trace origType
+      --dbg_trace (env.constants.map₁.find! name.getId).value! -- that's the proof
+      --let newType := Lean.Elab.Term.elabTerm sig none
+
+      let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
+      dbg_trace thmStatement
+      elabCommand thmStatement
+    else
+      let thmStatement ← `(theorem $(mkIdent name.getId) $sig $val)
+      elabCommand thmStatement
+  | none =>
+    let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
+    elabCommand thmStatement
 
   let msgs := (← get).messages
 
diff --git a/server/nng/NNG/Levels/Addition/Level_2.lean b/server/nng/NNG/Levels/Addition/Level_2.lean
index 00a379a..b220ee6 100644
--- a/server/nng/NNG/Levels/Addition/Level_2.lean
+++ b/server/nng/NNG/Levels/Addition/Level_2.lean
@@ -8,14 +8,6 @@ Title "add_assoc (associativity of addition)"
 
 open MyNat
 
-theorem MyNat.zero_add (n : ℕ) : 0 + n = n := by
-  induction n with n hn
-  · rw [add_zero]
-    rfl
-  · rw [add_succ]
-    rw [hn]
-    rfl
-
 Introduction
 "
 It's well-known that $(1 + 2) + 3 = 1 + (2 + 3)$; if we have three numbers
diff --git a/server/nng/NNG/Levels/Addition/Level_3.lean b/server/nng/NNG/Levels/Addition/Level_3.lean
index 7e63a68..7e63ed4 100644
--- a/server/nng/NNG/Levels/Addition/Level_3.lean
+++ b/server/nng/NNG/Levels/Addition/Level_3.lean
@@ -8,17 +8,6 @@ Title "succ_add"
 
 open MyNat
 
-theorem MyNat.add_assoc (a b c : ℕ) : (a + b) + c = a + (b + c)  := by
-  induction c with c hc
-  · rw [add_zero]
-    rw [add_zero]
-    rfl
-  · rw [add_succ]
-    rw [add_succ]
-    rw [add_succ]
-    rw [hc]
-    rfl
-
 Introduction
 "
 Oh no! On the way to `add_comm`, a wild `succ_add` appears. `succ_add`
diff --git a/server/nng/NNG/Levels/Addition/Level_4.lean b/server/nng/NNG/Levels/Addition/Level_4.lean
index 0d0a659..267ae1e 100644
--- a/server/nng/NNG/Levels/Addition/Level_4.lean
+++ b/server/nng/NNG/Levels/Addition/Level_4.lean
@@ -8,16 +8,6 @@ Title "`add_comm` (boss level)"
 
 open MyNat
 
-theorem MyNat.succ_add (a b : ℕ) : succ a + b = succ (a + b)  := by
-  induction b with d hd
-  · rw [add_zero]
-    rw [add_zero]
-    rfl
-  · rw [add_succ]
-    rw [hd]
-    rw [add_succ]
-    rfl
-
 Introduction
 "
 [boss battle music]
diff --git a/server/nng/NNG/Levels/Addition/Level_5.lean b/server/nng/NNG/Levels/Addition/Level_5.lean
index 1e39660..bfa30eb 100644
--- a/server/nng/NNG/Levels/Addition/Level_5.lean
+++ b/server/nng/NNG/Levels/Addition/Level_5.lean
@@ -9,16 +9,6 @@ Title "succ_eq_add_one"
 
 open MyNat
 
-theorem MyNat.add_comm (a b : ℕ) : a + b = b + a := by
-  induction b with d hd
-  · rw [zero_add]
-    rw [add_zero]
-    rfl
-  · rw [add_succ]
-    rw [hd]
-    rw [succ_add]
-    rfl
-
 theorem one_eq_succ_zero : (1 : ℕ) = succ 0 := by simp only
 
 NewLemma MyNat.one_eq_succ_zero