natural-number-game

Solututions to the Natural Number Game

NameSizeMode
..
advanced-addition.lean 1760B -rw-r--r--
01
02
03
04
05
06
07
08
09
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
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