Add Support for lemma statement.

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<HTMLDivElement>(null)
   const infoviewRef = useRef<HTMLDivElement>(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() {
         <div ref={messagePanelRef} className="message-panel">
           <MathJax><ReactMarkdown>{introduction}</ReactMarkdown></MathJax>
         </div>
+        <p><b>Aufgabe:</b></p>
+        <div><MathJax><ReactMarkdown>{description}</ReactMarkdown></MathJax></div>
+        {/* <div className="statement"><code>{ppStatement}</code></div>
+          NOTE(TODO): currently this looks bad, so I disabled it. Maybe have a drop-down for it of Syntax highlighting... */}
         <div ref={codeviewRef} className="codeview">
           {/* <InputZone index={index} history={history} messageOpen={messageOpen} setMessageOpen={setMessageOpen} completed={completed} sendTactic={sendTactic} nbLevels={nbLevels} loadNextLevel={loadNextLevel}
             errors={errors} lastTactic={lastTactic} undo={undo} finishGame={finishGame} /> */}

client/src/components/TacticState.tsx

@@ -42,11 +42,12 @@ function Goal({ goal }) {
       <Typography>Prove:</Typography>
       <Typography color="primary" sx={{ ml: 2 }}>{goal.goal}</Typography>
       {goal.messages.map((message) => <Alert severity="info" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert>)}
-      <FormControlLabel
+      {hasHints &&
-        control={<Switch checked={showHints} onChange={handleHintsChange} />}
+        <FormControlLabel
-        label="Help"
+          control={<Switch checked={showHints} onChange={handleHintsChange} />}
-      />
+          label="Help"
-      {goal.hints.map((message) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{message}</ReactMarkdown></MathJax></Alert></Collapse>)}
+        />}
+        {goal.hints.map((hint) => <Collapse in={showHints}><Alert severity="warning" sx={{ mt: 1 }}><MathJax><ReactMarkdown>{hint}</ReactMarkdown></MathJax></Alert></Collapse>)}
     </Box>)
 }
 

client/src/components/Welcome.tsx

@@ -92,7 +92,7 @@ function Welcome() {
         </Typography>
       </Box>
       <Box textAlign='center' sx={{ m: 5 }}>
-        <Button component={RouterLink} to="/world/TestWorld/level/1" variant="contained">Start rescue mission</Button>
+        <Button component={RouterLink} to="/world/Logic/level/1" variant="contained">Start rescue mission</Button>
       </Box>
       <div ref={worldsRef} style={{"width": "100%","height": "50em"}} />
     </div>

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. -/
+-- TODO: Instead of this, it would be nice to have a proper syntax parser that enables
-elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
+-- 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)
+  let defaultDeclName : Name := (← getCurGame).name ++ (← getCurWorld).name ++
-  elabCommand (← `(theorem $(mkIdent declName) $sig $val))
+    ("level" ++ toString lvlIdx : String)
-  modifyCurLevel fun level => pure {level with goal := sig}
+  let thmStatement ← `(theorem $(mkIdent defaultDeclName) $sig $val)
--- TODO: Do something with the lemma name.
+  -- 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. -/

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 -/

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

server/leanserver/GameServer/RpcHandlers.lean

@@ -24,8 +24,8 @@ structure GameGoal where
 deriving FromJson, ToJson
 
 
-def Lean.MVarId.toGameGoal (goal : MVarId) (messages : Array String)
+def Lean.MVarId.toGameGoal (goal : MVarId)
-    (hints : Array String) : MetaM GameGoal := do
+    (messages : Array String) (hints : Array String) : MetaM GameGoal := do
 match (← getMCtx).findDecl? goal with
 | none          => throwError "unknown goal"
 | some mvarDecl => do

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."

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
 

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
 

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

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]

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 =>

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 sei `hA` ein Beweis für $A$.
-    Sei `A` eine logische Aussage und angenommen man hat einen Beweis für `A`.
+    Zeige, dass $ A $ wahr ist."
-    Zeige, dass `A` wahr ist.
-    "
     (A : Prop) (hA : A) : A := by
   assumption
 

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`.
-    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist."
-    Zeige, dass `B` wahr ist.
-    "
     (A B : Prop) (hA : A) (g : A → B) : B := by
   apply g
   assumption

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`.
-    Seien `A`, `B` logische Aussagen, wobei `A` wahr ist und `A` impliziert `B`.
+    Zeige, dass `B` wahr ist."
-    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

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

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₂]

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

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

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

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

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
 

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

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

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

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
 

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

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

server/testgame/TestGame/Levels/Naturals/L31_Sum.lean

@@ -13,7 +13,7 @@ TODO: Summe
 
 "
 
-Statement : True := by
+Statement "" : True := by
   trivial
 
 Conclusion

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

server/testgame/TestGame/Levels/Naturals/L33_Prime.lean

@@ -13,7 +13,7 @@ TODO: Primzahl
 
 "
 
-Statement : True := by
+Statement "" : True := by
   trivial
 
 Conclusion

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

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
 

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
 

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."
+    "Ein Widerspruch impliziert alles."
-  (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by
+    (n : ℕ) (h₁ : even n) (h₂ : odd n) : n = 128 := by
   rw [← not_even] at h₂
   contradiction
 

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

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]
 

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

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]

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

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."
+    "Es existiert keine natürliche Zahl, die grösser als alle anderen.":
-  : ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
+    ¬ ∃ (n : ℕ), ∀ (k : ℕ) , odd (n + k) := by
   push_neg
   intro n
   use 3*n + 6