natural-number-game

Solututions to the Natural Number Game

Diffstat

5 files changed, 395 insertions, 0 deletions

diff --git a/README.md b/README.md
@@ -0,0 +1,4 @@
+# Natural Number Game
+
+Solututions to the [Natural Number
+Game](https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/).

diff --git a/advanced-addition.lean b/advanced-addition.lean
@@ -0,0 +1,92 @@
+theorem succ_inj' {a b : mynat} (hs : succ(a) = succ(b)) :  a = b := 
+begin
+  apply succ_inj,
+  exact hs,
+end
+
+theorem succ_succ_inj {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
+begin
+  apply succ_inj,
+  apply succ_inj,
+  exact h,
+end
+
+theorem succ_eq_succ_of_eq {a b : mynat} : a = b → succ(a) = succ(b) :=
+begin
+  intro h,
+  rw h,
+  refl,
+end
+
+theorem succ_eq_succ_iff (a b : mynat) : succ a = succ b ↔ a = b :=
+begin
+  split,
+  exact succ_inj,
+  exact succ_eq_succ_of_eq,
+end
+
+theorem add_right_cancel (a t b : mynat) : a + t = b + t → a = b :=
+begin
+  induction t,
+  intro h,
+  repeat {rw add_zero at h},
+  exact h,
+  intro h,
+  repeat {rw add_succ at h},
+  apply t_ih,
+  exact succ_inj h,
+end
+
+theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=
+begin
+  rw add_comm t,
+  rw add_comm t,
+  exact add_right_cancel a t b,
+end
+
+lemma eq_zero_of_add_right_eq_self {a b : mynat} : a + b = a → b = 0 :=
+begin
+  intro h,
+  rw ← add_zero a at h,
+  rw add_assoc at h,
+  rw zero_add at h,
+  apply add_left_cancel a b 0,
+  exact h,
+end
+
+theorem succ_ne_zero (a : mynat) : succ a ≠ 0 := 
+begin
+  symmetry,
+  exact zero_ne_succ a,
+end
+
+lemma add_left_eq_zero {a b : mynat} (h : a + b = 0) : b = 0 :=
+begin
+  cases b with d,
+  refl,
+  exfalso,
+  rw add_succ at h,
+  apply succ_ne_zero (a + d),
+  exact h,
+end
+
+lemma add_right_eq_zero {a b : mynat} : a + b = 0 → a = 0 :=
+begin
+  rw add_comm,
+  apply add_left_eq_zero,
+end
+
+lemma ne_succ_self (n : mynat) : n ≠ succ n :=
+begin
+  intro h,
+  rw succ_eq_add_one at h,
+  rw ← add_zero n at h,
+  rw add_assoc at h,
+  rw zero_add at h,
+  have p := add_left_cancel n 0 1 h,
+  rw one_eq_succ_zero at p,
+  apply succ_ne_zero 0,
+  symmetry,
+  exact p,
+end
+

diff --git a/advanced-preposition.lean b/advanced-preposition.lean
@@ -0,0 +1,136 @@
+example (P Q : Prop) (p : P) (q : Q) : P ∧ Q :=
+begin
+  split,
+  exact p,
+  exact q,
+end
+
+lemma and_symm (P Q : Prop) : P ∧ Q → Q ∧ P :=
+begin
+  intro h,
+  cases h with p q,
+  split,
+  exact q,
+  exact p,
+end
+
+lemma and_trans (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R :=
+begin
+  intro h1,
+  cases h1 with p _,
+  intro h2,
+  cases h2 with _ r,
+  split,
+  exact p,
+  exact r,
+end
+
+lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
+begin
+  intro p_iff_q,
+  cases p_iff_q with hpq hqp,
+  intro q_iff_r,
+  cases q_iff_r with hqr hrq,
+  split,
+  intro p,
+  apply hqr,
+  apply hpq,
+  exact p,
+  intro r,
+  apply hqp,
+  apply hrq,
+  exact r,
+end
+
+lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
+begin
+  intro p_iff_q,
+  cases p_iff_q with hpq hqp,
+  intro q_iff_r,
+  cases q_iff_r with hqr hrq,
+  split,
+  intro p,
+  apply hqr,
+  apply hpq,
+  exact p,
+  intro r,
+  apply hqp,
+  apply hrq,
+  exact r,
+end
+
+example (P Q : Prop) : Q → (P ∨ Q) :=
+  begin
+  intro q,
+  right,
+  exact q,
+end
+
+lemma or_symm (P Q : Prop) : P ∨ Q → Q ∨ P :=
+begin
+  intro h,
+  cases h with p q,
+  right,
+  exact p,
+  left,
+  exact q,
+end
+
+lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) :=
+begin
+  split,
+  intro h,
+  have p := h.1,
+  cases h.2 with q r,
+  left,
+  split,
+  exact p,
+  exact q,
+  right,
+  split,
+  exact p,
+  exact r,
+  intro h,
+  cases h with p_and_q p_and_r,
+  cases p_and_q with p q,
+  split,
+  exact p,
+  left,
+  exact q,
+  cases p_and_r with p r,
+  split,
+  exact p,
+  right,
+  exact r,
+end
+
+lemma contra (P Q : Prop) : (P ∧ ¬ P) → Q :=
+begin
+  intro h,
+  rw not_iff_imp_false at h,
+  exfalso,
+  apply h.2,
+  exact h.1,
+end
+
+lemma contrapositive2 (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
+begin
+  by_cases p : P; by_cases q : Q,
+  intros _ _,
+  exact q,
+  intro h,
+  have not_p := h q,
+  exfalso,
+  rw not_iff_imp_false at not_p,
+  apply not_p,
+  exact p,
+  intros _ _,
+  exact q,
+  intros h p,
+  have not_p := h q,
+  rw not_iff_imp_false at not_p,
+  exfalso,
+  apply not_p,
+  exact p,
+end
+

diff --git a/function.lean b/function.lean
@@ -0,0 +1,86 @@
+example (P Q : Type) (p : P) (h : P → Q) : Q :=
+begin
+  exact h(p),
+end
+
+example : mynat → mynat :=
+begin
+  intro n,
+  exact 3 * n + 2,
+end
+
+example (P Q R S T U: Type)
+        (p : P)
+        (h : P → Q)
+        (i : Q → R)
+        (j : Q → T)
+        (k : S → T)
+        (l : T → U) : U :=
+begin
+  have q := h(p),
+  have t := j(q),
+  exact l(t),
+end
+
+example (P Q R S T U: Type)
+        (p : P)
+        (h : P → Q)
+        (i : Q → R)
+        (j : Q → T)
+        (k : S → T)
+        (l : T → U) : U :=
+begin
+  have q := h(p),
+  have t := j(q),
+  exact l(t),
+end
+
+example (P Q : Type) : P → (Q → P) :=
+begin
+  intros p q,
+  exact p,
+end
+
+example (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)) :=
+begin
+  intros f g p,
+  apply f,
+  exact p,
+  apply g,
+  exact p,
+end
+
+example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) :=
+  begin
+  intros f g p,
+  apply g,
+  apply f,
+  exact p,
+end
+
+example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) :=
+begin
+  intros f g p,
+  apply g,
+  apply f,
+  exact p,
+end
+
+example (A B C D E F G H I J K L : Type) 
+        ( f1 : A → B) ( f2 : B → E) ( f3 : E → D) 
+        ( f4 : D → A) ( f5 : E → F) ( f6 : F → C)
+        ( f7 : B → C) ( f8 : F → G) ( f9 : G → J) 
+        (f10 : I → J) (f11 : J → I) (f12 : I → H) 
+        (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L :=
+begin
+  intro a,
+  apply f15,
+  apply f11,
+  apply f9,
+  apply f8,
+  apply f5,
+  apply f2,
+  apply f1,
+  exact a,
+end
+

diff --git a/preposition.lean b/preposition.lean
@@ -0,0 +1,77 @@
+example (P Q : Prop) (p : P) (h : P → Q) : Q :=
+begin
+  apply h,
+  exact p,
+end
+
+lemma imp_self (P : Prop) : P → P :=
+begin
+  intro p,
+  exact p,
+end
+
+lemma maze (P Q R S T U: Prop)
+           (p : P)
+           (h : P → Q)
+           (i : Q → R)
+           (j : Q → T)
+           (k : S → T)
+           (l : T → U) : U :=
+begin
+  apply l,
+  apply j,
+  apply h,
+  exact p,
+end
+
+example (P Q : Prop) : P → (Q → P) :=
+begin
+  intros p q,
+  exact p,
+end
+
+example (P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) :=
+begin
+  intros h1 h2 p,
+  apply h1,
+  exact p,
+  apply h2,
+  exact p,
+end
+
+lemma imp_trans (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) :=
+begin
+  intros hpq hqr p,
+  apply hqr,
+  apply hpq,
+  exact p,
+end
+
+lemma contrapositive (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
+begin
+  repeat {rw not_iff_imp_false},
+  intros hpq not_q p,
+  apply not_q,
+  apply hpq,
+  exact p,
+end
+
+example (A B C D E F G H I J K L : Prop)
+        ( f1 : A → B) ( f2 : B → E) ( f3 : E → D) 
+        ( f4 : D → A) ( f5 : E → F) ( f6 : F → C) 
+        ( f7 : B → C) ( f8 : F → G) ( f9 : G → J)
+        (f10 : I → J) (f11 : J → I) (f12 : I → H) 
+        (f13 : E → H) (f14 : H → K) (f15 : I → L) : A → L :=
+begin
+  cc,
+end
+
+
+
+
+
+
+
+
+
+