Natural Number Game

标签：begin rw Natural zero Game Number succ add end

因为用 Verilog 会有颜色显示，所以用的 Verilog。

记录一下 Natural Number Game 的答案，好久以前做的，但没做完。

Tutorial world
Addition world
Multiplication world
Function world
Proposition world
Advanced proposition world
Advanced Addition World
Advanced Multiplication World

Tutorial world

\[\text{example1}:xy+z=xy+z \]

lemma example1 (x y z : mynat) : x * y + z = x * y + z :=
begin
    refl,
end

\[\text{example2}:y=x+1\to2y=2(x+7) \]

lemma example2 (x y : mynat) (h : y = x + 7) : 2 * y = 2 * (x + 7) :=
begin
    rw h,
    refl,
end

\[\text{example3}:\operatorname{succ}(a)=b\to\operatorname{succ}(\operatorname{succ}(a))=\operatorname{succ}(b) \]

lemma example3 (a b : mynat) (h : succ a = b) : succ(succ(a)) = succ(b) :=
begin
    rw h,
    refl,
end

\[\text{add_succ_zero}:a+\operatorname{succ}(0)=\operatorname{succ}(a) \]

lemma add_succ_zero (a : mynat) : a + succ(0) = succ(a) :=
begin
    rw add_succ,
    rw add_zero,
    refl,
end

Addition world

\[\text{zero_add}:0+n=n \]

lemma zero_add (n : mynat) : 0 + n = n :=
begin
    induction n with d m,
    rw add_zero,
    refl,
    rw add_succ,
    rw m,
    refl,
end

\[\text{add_assoc}:(a+b)+c=a+(b+c) \]

lemma add_assoc (a b c : mynat) : (a + b) + c = a + (b + c) :=
begin
    induction c with d hd,
    rw add_zero,
    rw add_zero,
    refl,
    rw add_succ,
    rw add_succ,
    rw add_succ,
    rw hd,
    refl,
end

\[\text{succ_add}:\operatorname{succ}(a)+b=\operatorname{succ}(a+b) \]

lemma succ_add (a b : mynat) : succ a + b = succ (a + b) :=
begin
    induction b with d hd,
    rw add_zero,
    rw add_zero,
    refl,
    rw add_succ,
    rw add_succ,
    rw hd,
    refl,
end

\[\text{add_comm}:a+b=b+a \]

lemma add_comm (a b : mynat) : a + b = b + a :=
begin
    induction b with d hd,
    rw add_zero,
    rw zero_add,
    refl,
    rw succ_add,
    rw add_succ,
    rw hd,
    refl,
end

\[\text{succ_eq_add_one}:\operatorname{succ}(n)=n+1 \]

theorem succ_eq_add_one (n : mynat) : succ n = n + 1 :=
begin
    induction n with d hd,
    rw one_eq_succ_zero,
    rw zero_add,
    refl,
    rw succ_add,
    rw hd,
    refl,
end

\[\text{add_right_comm}:a+b+c=a+c+b \]

lemma add_right_comm (a b c : mynat) : a + b + c = a + c + b :=
begin
    rw add_assoc,
    rw add_assoc,
    induction a with d hd,
    rw zero_add,
    rw zero_add,
    rw add_comm,
    refl,
    rw succ_add,
    rw succ_add,
    rw hd,
    refl,
end

Multiplication world

\[\text{zero_mul}:0\times m=0 \]

lemma zero_mul (m : mynat) : 0 * m = 0 :=
begin
    induction m with d hd,
    rw mul_zero,
    refl,
    rw mul_succ,
    rw add_zero,
    rw nd,
    refl,
end

\[\text{mul_one}:m\times1=m \]

lemma mul_one (m : mynat) : m * 1 = m :=
begin
    induction m with d hd,
    rw zero_mul,
    refl,
    rw one_eq_succ_zero,
    rw mul_succ,
    rw mul_zero,
    rw zero_add,
    refl,
end

\[\text{one_mul}:1\times m=m \]

lemma one_mul (m : mynat) : 1 * m = m :=
begin
    induction m with d hd,
    rw mul_zero,
    refl,
    rw mul_succ,
    rw hd,
    rw succ_eq_add_one,
    refl,
end

\[\text{mul_add}:t(a+b)=ta+tb \]

lemma mul_add (t a b : mynat) : t * (a + b) = t * a + t * b :=
begin
    induction b with d hd,
    rw mul_zero,
    repeat {rw add_zero},
    rw add_succ,
    rw mul_succ,
    rw mul_succ,
    rw hd,
    rw add_assoc,
    refl,
end

\[\text{mul_assoc}:(ab)c=a(bc) \]

lemma mul_assoc (a b c : mynat) : (a * b) * c = a * (b * c) :=
begin
    induction c with d hd,
    repeat {rw mul_zero},
    repeat {rw mul_succ},
    repeat {rw mul_add},
    rw hd,
    refl,
end

\[\text{succ_mul}:\operatorname{succ}(a)\times b=ab+b \]

lemma succ_mul (a b : mynat) : succ a * b = a * b + b :=
begin
    induction b with d hd,
    repeat {rw mul_zero},
    repeat {rw zero_add},
    repeat {rw mul_succ},
    rw hd,
    repeat {rw add_succ},
    rw add_right_comm,
    refl,
end

\[\text{add_mul}:(a+b)\times t=at+bt \]

lemma add_mul (a b t : mynat) : (a + b) * t = a * t + b * t :=
begin
    induction t with d hd,
    repeat {rw mul_zero},
    repeat {rw add_zero},
    repeat {rw mul_succ},
    rw hd,
    simp,
end

\[\text{mul_comm}:a\times b=b\times a \]

lemma mul_comm (a b : mynat) : a * b = b * a :=
begin
    induction b with d hd,
    rw mul_zero,
    rw zero_mul,
    refl,
    rw mul_succ,
    rw succ_mul,
    rw hd,
    refl,
end

\[\text{mul_left_comm}:a(bc)=b(ac) \]

lemma mul_left_comm (a b c : mynat) : a * (b * c) = b * (a * c) :=
begin
    induction b with d hd,
    repeat {rw zero_mul},
    rw mul_zero,
    refl,
    repeat {rw succ_mul},
    rw mul_add,
    rw hd,
    simp,
end

\[\text{zero_pow_zero}:0^0=1 \]

lemma zero_pow_zero : (0 : mynat) ^ (0 : mynat) = 1 :=
begin
    rw pow_zero,
    refl,
end

\[\text{zero_pow_succ}:0^{\operatorname{succ}(m)}=0 \]

lemma zero_pow_succ (m : mynat) : (0 : mynat) ^ (succ m) = 0 :=
begin
    rw pow_succ,
    rw mul_zero,
    refl,
end

\[\text{pow_one}:a^1=a \]

lemma pow_one (a : mynat) : a ^ (1 : mynat) = a :=
begin
    rw one_eq_succ_zero,
    rw pow_succ,
    rw pow_zero,
    rw one_mul,
    refl,
end

\[\text{one_pow}:1^m=1 \]

lemma one_pow (m : mynat) : (1 : mynat) ^ m = 1 :=
begin
    induction m with d hd,
    rw pow_zero,
    refl,
    rw pow_succ,
    rw hd,
    rw one_mul,
    refl,
end

\[\text{pow_add}:a^{m+n}=a^ma^n \]

lemma pow_add (a m n : mynat) : a ^ (m + n) = a ^ m * a ^ n :=
begin
    induction n with d hd,
    rw add_zero,
    rw pow_zero,
    rw mul_one,
    refl,
    rw add_succ,
    repeat {rw pow_succ},
    rw hd,
    simp,
end

\[\text{mul_pow}:(ab)^n=a^nb^n \]

lemma mul_pow (a b n : mynat) : (a * b) ^ n = a ^ n * b ^ n :=
begin
    induction n with d hd,
    repeat {rw pow_zero},
    rw mul_one,
    refl,
    repeat {rw pow_succ},
    rw hd,
    simp,
end

\[\text{pow_pow}:(a^m)^n=a^{mn} \]

lemma pow_pow (a m n : mynat) : (a ^ m) ^ n = a ^ (m * n) :=
begin
    induction n with d hd,
    rw mul_zero,
    repeat {rw pow_zero},
    rw mul_succ,
    repeat {rw pow_succ},
    rw hd,
    rw pow_add,
    refl,
end

\[\text{add_squared}:(a+b)^2=a^2+b^2+2ab \]

lemma add_squared (a b : mynat) :
  (a + b) ^ (2 : mynat) = a ^ (2 : mynat) + b ^ (2 : mynat) + 2 * a * b :=
begin
    rw two_eq_succ_one,
    rw one_eq_succ_zero,
    repeat {rw pow_succ},
    repeat {rw pow_zero},
    repeat {rw one_mul},
    repeat {rw succ_mul},
    rw zero_mul,
    rw zero_add,
    repeat {rw add_mul},
    repeat {rw mul_add},
    simp,
end

Function world

\[\text{example}:\operatorname{exact} \]

example (P Q : Type) (p : P) (h : P → Q) : Q :=
begin
    exact h p,
end

\[\text{example}:\operatorname{intro} \]

example : mynat → mynat :=
begin
    intro n,
    exact n,
end

\[\text{example}:\operatorname{have} \]

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 t : T := j (h p),
    exact l t ,
end

\[\text{example}:\operatorname{apply} \]

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 t : T := j (h p),
    apply l,
    apply t,
end

\[\text{example}:P\to(Q\to P) \]

example (P Q : Type) : P → (Q → P) :=
begin
    intro p,
    intro q,
    exact p,
end

\[\text{example}:(P\to(Q\to R))\to((P\to Q)\to(P\to R)) \]

example (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)) :=
begin
    intros f1 f2 p,
    have q := f2 p,
    apply f1,
    apply p,
    apply q,
end

\[\text{example}:(P\to Q)\to((Q\to F)\to(P\to F)) \]

example (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) :=
begin
    intros f1 f2 p,
    exact f2 (f1 p),
end

\[\text{example}:(P\to Q)\to((Q\to \varnothing)\to(P\to\varnothing)) \]

example (P Q : Type) : (P → Q) → ((Q → empty) → (P → empty)) :=
begin
    intros f1 f2 p,
    exact f2 (f1 p),
end

\[\text{example}:\text{a big maze} \]

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,
    exact f8 (f5 (f2 (f1 a))),
end

Proposition world

\[\text{example}:\begin{cases} P\text{ is true}\\ P\to Q\text{ is true} \end{cases}\to Q\text{ is true} \]

example (P Q : Prop) (p : P) (h : P → Q) : Q :=
begin
    exact h p,
end

\[\text{imp_self}:P\to P \]

lemma imp_self (P : Prop) : P → P :=
begin
    intro p,
    exact p,
end

\[\text{maze}: \]

![diagram](assets/img/Natural Number Game.assets/implies_diag.jpg)

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
    exact l (j (h p)),
end

\[\text{example}:P\to(Q\to P) \]

example (P Q : Prop) : P → (Q → P) :=
begin
    intros p q,
    exact p,
end

\[\text{example}:(P\to(Q\to R))\to((P\to Q)\to(P\to R)) \]

example (P Q R : Prop) : (P → (Q → R)) → ((P → Q) → (P → R)) :=
begin
    intros f1 f2 p,
    have q := f2 p,
    exact f1 p q,
end

\[\text{imp_trans}:\begin{cases} P\to Q\\ Q\to R\\ \end{cases}\to(P\to R)\\ \]

lemma imp_trans (P Q R : Prop) : (P → Q) → ((Q → R) → (P → R)) :=
begin
    intros f1 f2 p,
    exact f2 (f1 p),
end

\[\text{contrapositive}:(P\to Q)\to(\neg Q\to\neg P) \]

lemma contrapositive (P Q : Prop) : (P → Q) → (¬ Q → ¬ P) :=
begin
    repeat {rw not_iff_imp_false},
    intros f nq p,
    exact nq (f p),
end

\[\text{example}:\text{a big maze} \]

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
    intro a,
    exact f15 (f11 (f9 (f8 (f5 (f2 (f1 a)))))),
end

Advanced proposition world

\[\text{example}:\operatorname{split} \]

example (P Q : Prop) (p : P) (q : Q) : P ∧ Q :=
begin
    split,
    exact p,
    exact q,
end

\[\text{and_symm}:P\wedge Q\to Q\wedge P \]

lemma and_symm (P Q : Prop) : P ∧ Q → Q ∧ P :=
begin
    intro h,
    cases h with p q,
    split,
    exact q,
    exact p,
end

\[\text{and_trans}:\begin{cases} P\wedge Q\\ Q\wedge R \end{cases}\to P\wedge R \]

lemma and_trans (P Q R : Prop) : P ∧ Q → Q ∧ R → P ∧ R :=
begin
    intros h1 h2,
    cases h1 with p q,
    cases h2 with q r,
    split,
    exact p,
    exact r,
end

\[\text{iff_trans}:\begin{cases} P\leftrightarrow Q\\ Q\leftrightarrow R \end{cases}\to(P\leftrightarrow R) \]

lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
begin
    intros h1 h2,
    cases h1 with hpq hqp,
    cases h2 with hqr hrq,
    split,
    intro p,
    exact hqr (hpq p),
    intro r,
    exact hqp (hrq r),
end

lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
begin
    intros h1 h2,
    rw h1,
    rw h2,
end

lemma iff_trans (P Q R : Prop) : (P ↔ Q) → (Q ↔ R) → (P ↔ R) :=
begin
    intros h1 h2,
    split,
    intro p,
    exact h2.1 (h1.1 p),
    intro r,
    exact h1.2 (h2.2 r),
end

\[\text{example}:Q\to(P\vee Q) \]

example (P Q : Prop) : Q → (P ∨ Q) :=
begin
    intro q,
    right,
    exact q,
end

\[\text{or_symm}:P\vee Q\to Q\vee P \]

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

\[\text{and_or_distrib_left}:P\wedge(Q\vee R)\leftrightarrow(P\wedge Q)\vee(P\wedge R) \]

lemma and_or_distrib_left (P Q R : Prop) : P ∧ (Q ∨ R) ↔ (P ∧ Q) ∨ (P ∧ R) :=
begin
    split,
    intro h,
    cases h with p or_qr,
    cases or_qr with q r,

    left,
    split,
    exact p,
    exact q,

    right,
    split,
    exact p,
    exact r,

    intro h,
    cases h with and_pq and_pr,

    cases and_pq with p q,
    split,
    exact p,
    left,
    exact q,

    cases and_pr with p r,
    split,
    exact p,
    right,
    exact r,
end

\[\text{contra}:(P\wedge(\neg P))\to Q \]

lemma contra (P Q : Prop) : (P ∧ ¬ P) → Q :=
begin
    intro h,
    rw not_iff_imp_false at h,
    exfalso,
    exact h.2 h.1,
end

\[\text{contrapositive2}:(\neg Q\to\neg P)\to(P\to Q) \]

lemma contrapositive2 (P Q : Prop) : (¬ Q → ¬ P) → (P → Q) :=
begin
    by_cases p: P; by_cases q: Q,
    repeat {cc},
end

Advanced Addition World

\[\text{succ_inj'}:\operatorname{succ}(a)=\operatorname{succ}(b)\to a=b \]

theorem succ_inj' {a b : mynat} (hs : succ(a) = succ(b)) :  a = b := 
begin
    apply succ_inj,
    rw hs,
    refl,
    -- exact succ_inj hs,
end

\[\text{succ_succ_inj}:\operatorname{succ}(\operatorname{succ}(a))=\operatorname{succ}(\operatorname{succ}(b))\to\operatorname{succ}(a)=\operatorname{succ}(b) \]

theorem succ_succ_inj {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
begin
    exact succ_inj (succ_inj h),
end

\[\text{succ_eq_succ_of_eq}:a=b\to\operatorname{succ}(a)=\operatorname{succ}(b) \]

theorem succ_eq_succ_of_eq {a b : mynat} : a = b → succ(a) = succ(b) :=
begin
    intro eq,
    induction b with d hd,
    rw eq,
    refl,
    rw eq,
    refl,
end

\[\text{eq_iff_succ_eq_succ}:a=b\leftrightarrow\operatorname{succ}(a)=\operatorname{succ}(b) \]

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

\[\text{add_right_cancel}:a+t=b+t\to a=b \]

theorem add_right_cancel (a t b : mynat) : a + t = b + t → a = b :=
begin
    intro h,
    induction t with d hd,
    repeat {rw add_zero at h},
    exact h,
    repeat {rw add_succ at h},
    exact hd (succ_inj h),
end

\[\text{add_left_cancel}:t+a=t+b\to a=b \]

theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=
begin
    intro h,
    induction t with d hd,
    repeat {rw zero_add at h},
    exact h,
    repeat {rw succ_add at h},
    exact hd (succ_inj h),
end

theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=
begin
    intro h,
    apply add_right_cancel a t b,
    rw add_comm at h,
    rw h,
    rw add_comm,
    refl,
end

theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=
begin
    intro h,
    apply add_right_cancel a t b,
    simp,
    exact h,
end

theorem add_left_cancel (t a b : mynat) : t + a = t + b → a = b :=
begin
    rw add_comm t a,
    rw add_comm t b,
    exact add_right_cancel a t b,
end

\[\text{add_right_cancel_iff}:a+t=b+t\leftrightarrow a=b \]

theorem add_right_cancel_iff (t a b : mynat) :  a + t = b + t ↔ a = b :=
begin
    split,
    exact add_right_cancel _ _ _,
    intro h,
    rw h,
    refl,
end

\[\text{eq_zero_of_add_right_eq_self}:a+b=a\to b=0 \]

lemma eq_zero_of_add_right_eq_self {a b : mynat} : a + b = a → b = 0 :=
begin
    rw ← add_zero a,
    rw add_assoc,
    rw zero_add b,
    exact add_left_cancel a b 0,
end

\[\text{succ_ne_zero}:\operatorname{succ}(a)\ne0 \]

theorem succ_ne_zero (a : mynat) : succ a ≠ 0 := 
begin
    symmetry,
    exact zero_ne_succ a,
end

\[\text{add_left_eq_zero}:a+b=0\to b=0 \]

lemma add_left_eq_zero {{a b : mynat}} (H : a + b = 0) : b = 0 :=
begin
    cases b with d,
    refl,
    rw add_succ at H,
    exfalso,
    exact succ_ne_zero (a + d) H,
end

\[\text{add_right_eq_zero}:a+b=0\to a=0. \]

lemma add_right_eq_zero {a b : mynat} : a + b = 0 → a = 0 :=
begin
    rw add_comm,
    apply add_left_eq_zero,
end

\[\text{add_one_eq_succ}:d+1=\operatorname{succ}(d) \]

theorem add_one_eq_succ (d : mynat) : d + 1 = succ d :=
begin
    symmetry,
    apply succ_eq_add_one,
end

\[\text{ne_succ_self}:n\ne\operatorname{succ}(n) \]

lemma ne_succ_self (n : mynat) : n ≠ succ n :=
begin
    symmetry,
    rw succ_eq_add_one,
    rw one_eq_succ_zero,
    intro h,
    exact succ_ne_zero 0 (eq_zero_of_add_right_eq_self h),
end

Advanced Multiplication World

\[\text{mul_pos}:a\ne0\to b\ne0\to ab\ne0 \]

theorem mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=
begin
    intros h1 h2,
    cases a with c,
    simp,
    apply h1,
    refl,

    rw succ_mul,
    intro h3,
    apply h2,
    exact add_left_eq_zero h3,
end

theorem mul_pos (a b : mynat) : a ≠ 0 → b ≠ 0 → a * b ≠ 0 :=
begin
    cases a with c; cases b with d,
    simp, simp, simp,
    intros h1 h2 h3,
    rw succ_mul at h3,
    rw add_succ at h3,
    exact succ_ne_zero _ h3,
end

\[\text{eq_zero_or_eq_zero_of_mul_eq_zero}:ab=0\to a=0\vee b=0 \]

theorem eq_zero_or_eq_zero_of_mul_eq_zero (a b : mynat) (h : a * b = 0) :
  a = 0 ∨ b = 0 :=
begin
    cases a with c; cases b with d,
    simp, simp, simp,
    exfalso,
    rw succ_mul at h,
    rw add_succ at h,
    exact succ_ne_zero _ h,
end

\[\text{mul_eq_zero_iff}:ab=0\leftrightarrow a=0\vee b=0 \]

theorem mul_eq_zero_iff (a b : mynat): a * b = 0 ↔ a = 0 ∨ b = 0 :=
begin
    split,
    apply eq_zero_or_eq_zero_of_mul_eq_zero,
    intro h,
    cases h,
    rw h, simp,
    rw h, simp,
end

标签：begin,rw,Natural,zero,Game,Number,succ,add,end
From： https://www.cnblogs.com/violeshnv/p/16831712.html