From f636a8d83355d3f18285607949a7f2cbcb44831b Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Mon, 3 Apr 2023 11:53:48 +0200 Subject: [PATCH] fix missing lemma docs from statement names --- server/adam/Adam/LemmaDocs.lean | 18 +++++++++++++++++ .../Adam/Levels/Function/L09_Inverse.lean | 3 ++- .../Adam/Levels/Function/L11_Inverse.lean | 4 +++- .../Adam/Levels/LinearAlgebra/L06_Span.lean | 3 ++- .../Adam/Levels/Predicate/L07_Exists.lean | 2 +- .../adam/Adam/Levels/SetTheory/L01_Univ.lean | 2 +- .../adam/Adam/Levels/SetTheory/L02_Empty.lean | 2 +- .../Levels/SetTheory/L04_SubsetEmpty.lean | 2 +- .../adam/Adam/Levels/SetTheory/L05_Empty.lean | 2 +- .../Adam/Levels/SetTheory/L06_Nonempty.lean | 3 +-- .../Adam/Levels/SetTheory/L10_Morgan.lean | 1 - server/adam/Adam/Levels/Sum/L04_SumOdd.lean | 2 +- server/nng/NNG/Doc/Lemmas.lean | 20 +++++++++---------- server/nng/NNG/Levels/Addition/Level_1.lean | 2 +- server/nng/NNG/Levels/Addition/Level_2.lean | 2 +- server/nng/NNG/Levels/Addition/Level_3.lean | 2 +- server/nng/NNG/Levels/Addition/Level_4.lean | 2 +- server/nng/NNG/Levels/Addition/Level_5.lean | 2 +- server/nng/NNG/Levels/Addition/Level_6.lean | 2 +- .../nng/NNG/Levels/AdvAddition/Level_1.lean | 2 +- .../NNG/Levels/AdvProposition/Level_2.lean | 2 +- .../NNG/Levels/AdvProposition/Level_3.lean | 2 +- .../NNG/Levels/AdvProposition/Level_4.lean | 2 +- .../NNG/Levels/AdvProposition/Level_5.lean | 2 +- .../NNG/Levels/AdvProposition/Level_7.lean | 2 +- .../NNG/Levels/AdvProposition/Level_8.lean | 2 +- .../NNG/Levels/AdvProposition/Level_9.lean | 2 +- 27 files changed, 56 insertions(+), 36 deletions(-) diff --git a/server/adam/Adam/LemmaDocs.lean b/server/adam/Adam/LemmaDocs.lean index aa15b23..6381740 100644 --- a/server/adam/Adam/LemmaDocs.lean +++ b/server/adam/Adam/LemmaDocs.lean @@ -464,3 +464,21 @@ LemmaDoc Iff.symm as "Iff.symm" in "Logic" * Mathlib Doc: [#Iff.symm](https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Iff.symm) " + +LemmaDoc not_imp_not as "not_imp_not" in "Logic" +" +`theorem not_imp_not {a : Prop} {b : Prop} : ¬a → ¬b ↔ b → a` + +## Eigenschaften + +* Mathlib Doc: [#not_imp_not](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Logic/Basic.html#not_imp_not) +" + +LemmaDoc Set.nonempty_iff_ne_empty as "nonempty_iff_ne_empty" in "Logic" +" +`theorem Set.nonempty_iff_ne_empty {α : Type u} {s : Set α} : Set.Nonempty s ↔ s ≠ ∅` + +## Eigenschaften + +* Mathlib Doc: [#nonempty_iff_ne_empty](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Basic.html#Set.nonempty_iff_ne_empty) +" diff --git a/server/adam/Adam/Levels/Function/L09_Inverse.lean b/server/adam/Adam/Levels/Function/L09_Inverse.lean index 382f932..76dfe1c 100644 --- a/server/adam/Adam/Levels/Function/L09_Inverse.lean +++ b/server/adam/Adam/Levels/Function/L09_Inverse.lean @@ -20,7 +20,8 @@ aber er möchte, dass du ihm das hier und jetzt nochmals von Grund auf zeigst. open Function --TODO: This is a really hard proof -Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) : +-- bijective_iff_has_inverse +Statement "" {A B : Type} (f : A → B) : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by constructor intro h diff --git a/server/adam/Adam/Levels/Function/L11_Inverse.lean b/server/adam/Adam/Levels/Function/L11_Inverse.lean index be12aaa..adc828f 100644 --- a/server/adam/Adam/Levels/Function/L11_Inverse.lean +++ b/server/adam/Adam/Levels/Function/L11_Inverse.lean @@ -19,7 +19,9 @@ aber er möchte, dass du ihm das hier und jetzt nochmals von Grund auf zeigst. open Function set_option pp.rawOnError true -Statement bijective_iff_has_inverse "" {A B : Type} (f : A → B) : + +-- bijective_iff_has_inverse +Statement {A B : Type} (f : A → B) : Bijective f ↔ ∃ g, LeftInverse g f ∧ RightInverse g f := by Branch exfalso diff --git a/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean b/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean index 8d309d0..9a22ee5 100644 --- a/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean +++ b/server/adam/Adam/Levels/LinearAlgebra/L06_Span.lean @@ -27,7 +27,8 @@ local notation "ℝ²" => Fin 2 → ℝ open Submodule Set Finsupp -Statement mem_span_of_mem +-- mem_span_of_mem +Statement "Zeige, dass $x \\in M$ auch Element von der $K$-linearen Hülle \\langle M \\rangle ist." {V K : Type _} [Field K] [AddCommMonoid V] diff --git a/server/adam/Adam/Levels/Predicate/L07_Exists.lean b/server/adam/Adam/Levels/Predicate/L07_Exists.lean index 3f93edd..59e7309 100644 --- a/server/adam/Adam/Levels/Predicate/L07_Exists.lean +++ b/server/adam/Adam/Levels/Predicate/L07_Exists.lean @@ -19,7 +19,7 @@ Introduction Sofort taucht das nächste Blatt auf. Anscheinend hatten sie sich auf einen Kompromiss geeinigt. " -Statement odd_square (n : ℕ) (h : Odd n) : Odd (n ^ 2) := by +Statement (n : ℕ) (h : Odd n) : Odd (n ^ 2) := by Hint (hidden := true) "**Robo**: mit `rcases h with ⟨r, hr⟩` kannst du wieder das `r` nehmen, das laut Annahme existieren muss. diff --git a/server/adam/Adam/Levels/SetTheory/L01_Univ.lean b/server/adam/Adam/Levels/SetTheory/L01_Univ.lean index f192095..3dbda27 100644 --- a/server/adam/Adam/Levels/SetTheory/L01_Univ.lean +++ b/server/adam/Adam/Levels/SetTheory/L01_Univ.lean @@ -32,7 +32,7 @@ erklärt mir doch folgendes: open Set -Statement mem_univ "" {A : Type} (x : A) : x ∈ (univ : Set A) := by +Statement Set.mem_univ "" {A : Type} (x : A) : x ∈ (univ : Set A) := by Hint "**Du**: Also `A` ist ein `Type`, `x` ist ein Element in `A`… **Robo** … und `univ` ist die Menge aller Elemente in `A`. diff --git a/server/adam/Adam/Levels/SetTheory/L02_Empty.lean b/server/adam/Adam/Levels/SetTheory/L02_Empty.lean index 1840659..bb39525 100644 --- a/server/adam/Adam/Levels/SetTheory/L02_Empty.lean +++ b/server/adam/Adam/Levels/SetTheory/L02_Empty.lean @@ -18,7 +18,7 @@ Ihr zieht also durch die Gegend und redet mit den Leuten. Ein Junge rennt zu euc open Set -Statement not_mem_empty "" {A : Type} (x : A) : +Statement Set.not_mem_empty "" {A : Type} (x : A) : x ∉ (∅ : Set A) := by Hint "**Du**: Kein Element ist in der leeren Menge enthalten? Das ist ja alles tautologisches Zeugs... diff --git a/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean b/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean index 07c6ed5..857140d 100644 --- a/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean +++ b/server/adam/Adam/Levels/SetTheory/L04_SubsetEmpty.lean @@ -31,7 +31,7 @@ aufteilen. open Set Subset -Statement subset_empty_iff {A : Type _} (s : Set A) : +Statement Set.subset_empty_iff {A : Type _} (s : Set A) : s ⊆ ∅ ↔ s = ∅ := by Hint "**Du**: Ja, die einzige Teilmenge der leeren Menge ist die leere Menge. Das ist doch eine Tautologie? diff --git a/server/adam/Adam/Levels/SetTheory/L05_Empty.lean b/server/adam/Adam/Levels/SetTheory/L05_Empty.lean index cc79f4c..af47a66 100644 --- a/server/adam/Adam/Levels/SetTheory/L05_Empty.lean +++ b/server/adam/Adam/Levels/SetTheory/L05_Empty.lean @@ -22,7 +22,7 @@ Zeige folgendes Lemma, welches wir gleich brauchen werden: open Set -Statement eq_empty_iff_forall_not_mem +Statement Set.eq_empty_iff_forall_not_mem "" {A : Type _} (s : Set A) : s = ∅ ↔ ∀ x, x ∉ s := by diff --git a/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean b/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean index 34d3bd8..36e563b 100644 --- a/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean +++ b/server/adam/Adam/Levels/SetTheory/L06_Nonempty.lean @@ -21,8 +21,7 @@ Zeige dass die beiden Ausdrücke äquivalent sind: open Set -Statement nonempty_iff_ne_empty -"" +Statement Set.nonempty_iff_ne_empty {A : Type _} (s : Set A) : s.Nonempty ↔ s ≠ ∅ := by Hint "Am besten fängst du mit `unfold Set.Nonempty` an." diff --git a/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean b/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean index db12481..422dd4a 100644 --- a/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean +++ b/server/adam/Adam/Levels/SetTheory/L10_Morgan.lean @@ -42,7 +42,6 @@ open Set #check mem_compl_iff Statement -"" (A B C : Set ℕ) : (A \ B)ᶜ ∩ (C \ B)ᶜ = ((univ \ A) \ C) ∪ (univ \ Bᶜ) := by rw [←compl_union] rw [←union_diff_distrib] diff --git a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean index b3a6427..17f594f 100644 --- a/server/adam/Adam/Levels/Sum/L04_SumOdd.lean +++ b/server/adam/Adam/Levels/Sum/L04_SumOdd.lean @@ -22,7 +22,7 @@ open Fin open BigOperators -Statement odd_arithmetic_sum +Statement "$\\sum_{i = 0}^n (2n + 1) = n ^ 2$." (n : ℕ) : (∑ i : Fin n, (2 * (i : ℕ) + 1)) = n ^ 2 := by Hint "**Robo**: Das funktioniert genau gleich wie zuvor, viel Glück." diff --git a/server/nng/NNG/Doc/Lemmas.lean b/server/nng/NNG/Doc/Lemmas.lean index f7c4b03..832d773 100644 --- a/server/nng/NNG/Doc/Lemmas.lean +++ b/server/nng/NNG/Doc/Lemmas.lean @@ -1,31 +1,31 @@ import GameServer.Commands LemmaDoc MyNat.add_zero as "add_zero" in "Nat" -"" +"(missing)" LemmaDoc MyNat.add_succ as "add_succ" in "Nat" -"" +"(missing)" LemmaDoc MyNat.zero_add as "zero_add" in "Nat" -"" +"(missing)" LemmaDoc MyNat.add_assoc as "add_assoc" in "Nat" -"" +"(missing)" LemmaDoc MyNat.succ_add as "succ_add" in "Nat" -"" +"(missing)" LemmaDoc MyNat.add_comm as "add_comm" in "Nat" -"" +"(missing)" LemmaDoc MyNat.one_eq_succ_zero as "one_eq_succ_zero" in "Nat" -"" +"(missing)" LemmaDoc not_iff_imp_false as "not_iff_imp_false" in "Prop" -"" +"(missing)" LemmaDoc MyNat.succ_inj as "succ_inj" in "Nat" -"" +"(missing)" LemmaDoc MyNat.zero_ne_succ as "zero_ne_succ" in "Nat" -"" +"(missing)" diff --git a/server/nng/NNG/Levels/Addition/Level_1.lean b/server/nng/NNG/Levels/Addition/Level_1.lean index e6e849c..f9d0cdc 100644 --- a/server/nng/NNG/Levels/Addition/Level_1.lean +++ b/server/nng/NNG/Levels/Addition/Level_1.lean @@ -36,7 +36,7 @@ note that `zero_add` is about zero add something, and `add_zero` is about someth The names of the proofs tell you what the theorems are. Anyway, let's prove `0 + n = n`. " -Statement zero_add +Statement MyNat.zero_add "For all natural numbers $n$, we have $0 + n = n$." (n : ℕ) : 0 + n = n := by Hint "You can start a proof by induction over `n` by typing: diff --git a/server/nng/NNG/Levels/Addition/Level_2.lean b/server/nng/NNG/Levels/Addition/Level_2.lean index d89e00f..d8c3b3f 100644 --- a/server/nng/NNG/Levels/Addition/Level_2.lean +++ b/server/nng/NNG/Levels/Addition/Level_2.lean @@ -30,7 +30,7 @@ that addition, as defined the way we've defined it, is associative. See if you can prove associativity of addition. " -Statement add_assoc +Statement MyNat.add_assoc "On the set of natural numbers, addition is associative. In other words, for all natural numbers $a, b$ and $c$, we have $ (a + b) + c = a + (b + c). $" diff --git a/server/nng/NNG/Levels/Addition/Level_3.lean b/server/nng/NNG/Levels/Addition/Level_3.lean index 06d1fd1..b365655 100644 --- a/server/nng/NNG/Levels/Addition/Level_3.lean +++ b/server/nng/NNG/Levels/Addition/Level_3.lean @@ -42,7 +42,7 @@ that `a + succ(b) = succ(a + b)`. The tactic `rw [add_succ]` just says to Lean \ what the variables are\". " -Statement succ_add +Statement MyNat.succ_add "For all natural numbers $a, b$, we have $ \\operatorname{succ}(a) + b = \\operatorname{succ}(a + b)$." (a b : ℕ) : succ a + b = succ (a + b) := by diff --git a/server/nng/NNG/Levels/Addition/Level_4.lean b/server/nng/NNG/Levels/Addition/Level_4.lean index e729fb7..33329e4 100644 --- a/server/nng/NNG/Levels/Addition/Level_4.lean +++ b/server/nng/NNG/Levels/Addition/Level_4.lean @@ -29,7 +29,7 @@ Look in your inventory to see the proofs you have available. These should be enough. " -Statement add_comm +Statement MyNat.add_comm "On the set of natural numbers, addition is commutative. In other words, for all natural numbers $a$ and $b$, we have $a + b = b + a$." diff --git a/server/nng/NNG/Levels/Addition/Level_5.lean b/server/nng/NNG/Levels/Addition/Level_5.lean index 9c13070..afb74bc 100644 --- a/server/nng/NNG/Levels/Addition/Level_5.lean +++ b/server/nng/NNG/Levels/Addition/Level_5.lean @@ -40,7 +40,7 @@ some theorems about $0$ (`zero_add`, `add_zero`), but, other than `1 = succ 0`, no theorems at all which mention $1$. Let's prove one now. " -Statement succ_eq_add_one +Statement --MyNat.succ_eq_add_one "For any natural number $n$, we have $ \\operatorname{succ}(n) = n+1$ ." (n : ℕ) : succ n = n + 1 := by diff --git a/server/nng/NNG/Levels/Addition/Level_6.lean b/server/nng/NNG/Levels/Addition/Level_6.lean index 29658e1..44d60e7 100644 --- a/server/nng/NNG/Levels/Addition/Level_6.lean +++ b/server/nng/NNG/Levels/Addition/Level_6.lean @@ -35,7 +35,7 @@ additions of the form `a + ?`, and `rw add_comm a b,` will only swap additions of the form `a + b`. " -Statement add_right_comm +Statement --add_right_comm "For all natural numbers $a, b$ and $c$, we have $a + b + c = a + c + b$." (a b c : ℕ) : a + b + c = a + c + b := by diff --git a/server/nng/NNG/Levels/AdvAddition/Level_1.lean b/server/nng/NNG/Levels/AdvAddition/Level_1.lean index ded4dae..411fd7b 100644 --- a/server/nng/NNG/Levels/AdvAddition/Level_1.lean +++ b/server/nng/NNG/Levels/AdvAddition/Level_1.lean @@ -17,7 +17,7 @@ theorem MyNat.succ_inj {a b : ℕ} : succ a = succ b → a = b := by simp only [ theorem MyNat.zero_ne_succ (a : ℕ) : zero ≠ succ a := by simp only [ne_eq, not_false_iff] -Statement succ_inj' +Statement -- MyNat.succ_inj' "" {a b : ℕ} (hs : succ a = succ b) : a = b := by exact succ_inj hs diff --git a/server/nng/NNG/Levels/AdvProposition/Level_2.lean b/server/nng/NNG/Levels/AdvProposition/Level_2.lean index 526e47a..86b3fb5 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_2.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_2.lean @@ -16,7 +16,7 @@ Introduction set_option tactic.hygienic false -Statement and_symm +Statement --and_symm "" (P Q : Prop) : P ∧ Q → Q ∧ P := by intro h diff --git a/server/nng/NNG/Levels/AdvProposition/Level_3.lean b/server/nng/NNG/Levels/AdvProposition/Level_3.lean index 76415ec..93336c1 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_3.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_3.lean @@ -14,7 +14,7 @@ Introduction " -Statement and_trans +Statement --and_trans "" (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R := by intro hpq diff --git a/server/nng/NNG/Levels/AdvProposition/Level_4.lean b/server/nng/NNG/Levels/AdvProposition/Level_4.lean index 023bd22..01a84dd 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_4.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_4.lean @@ -14,7 +14,7 @@ Introduction " -Statement iff_trans +Statement --iff_trans "" (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by intro hpq diff --git a/server/nng/NNG/Levels/AdvProposition/Level_5.lean b/server/nng/NNG/Levels/AdvProposition/Level_5.lean index 26224e6..19e7421 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_5.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_5.lean @@ -14,7 +14,7 @@ Introduction " -Statement iff_trans +Statement --iff_trans "" (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) := by intro hpq hqr diff --git a/server/nng/NNG/Levels/AdvProposition/Level_7.lean b/server/nng/NNG/Levels/AdvProposition/Level_7.lean index abff8e3..d6c77b4 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_7.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_7.lean @@ -15,7 +15,7 @@ Introduction " -Statement or_symm +Statement --or_symm "" (P Q : Prop) : P ∨ Q → Q ∨ P := by intro h diff --git a/server/nng/NNG/Levels/AdvProposition/Level_8.lean b/server/nng/NNG/Levels/AdvProposition/Level_8.lean index fd235cc..983f507 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_8.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_8.lean @@ -15,7 +15,7 @@ Introduction " -Statement and_or_distrib_left +Statement --and_or_distrib_left "" (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) := by constructor diff --git a/server/nng/NNG/Levels/AdvProposition/Level_9.lean b/server/nng/NNG/Levels/AdvProposition/Level_9.lean index d04f314..eb13d75 100644 --- a/server/nng/NNG/Levels/AdvProposition/Level_9.lean +++ b/server/nng/NNG/Levels/AdvProposition/Level_9.lean @@ -17,7 +17,7 @@ Introduction " -Statement contra +Statement --contra "" (P Q : Prop) : (P ∧ ¬ P) → Q := by intro h