named Statements are added to context with there specified name
This commit is contained in:
Jon Eugster
@@ -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"
|
||||
|
||||
@@ -1,6 +1,8 @@
|
||||
import Adam.Metadata
|
||||
|
||||
import Adam.ToBePorted
|
||||
import Adam.Levels.Predicate.L06_Exists
|
||||
|
||||
|
||||
Game "Adam"
|
||||
World "Contradiction"
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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
|
||||
@@ -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
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
-- Check that the statement name is a lemma in the doc
|
||||
-- Save the messages before evaluation of the proof.
|
||||
let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
|
||||
|
||||
-- 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 := {} })
|
||||
-- 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)
|
||||
-- let thmStatement' ← match statementName with
|
||||
-- | none => `(lemma $(mkIdent "XX") $sig $val) -- TODO: Make it into an `example`
|
||||
-- | some name => `(lemma $name $sig $val)
|
||||
elabCommand thmStatement
|
||||
let 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
|
||||
|
||||
|
||||
@@ -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
|
||||
|
||||
@@ -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`
|
||||
|
||||
@@ -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]
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user