lean4-example/Lean4Example.lean at main · durant42040/lean4-example · GitHub

1
2
3
4
5
6
7
8
9
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
theorem my_add_comm (n m : Nat) : n + m = m + n := by
  rw [Nat.add_comm]

theorem succ_add_succ (a b : Nat) : Nat.succ a + Nat.succ b = Nat.succ (Nat.succ (a + b)) := by
  simp [Nat.succ_eq_add_one, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]

theorem mul_assoc_my : ∀ a b c : Nat, (a * b) * c = a * (b * c) := by
  intro a b c
  simp [Nat.mul_comm]
  simp [Nat.mul_comm, Nat.mul_left_comm]

theorem my_and_comm : ∀ {p q : Prop}, And p q → And q p := by
  simp
  intro p q hp hq
  exact ⟨hq, hp⟩

theorem my_add_comm_1 (n m : Nat) : n + m = m + n := by
  rw [Nat.add_comm]

theorem succ_add_succ_1 (a b : Nat) : Nat.succ a + Nat.succ b = Nat.succ (Nat.succ (a + b)) := by
  rw [Nat.succ_add, Nat.add_succ]

theorem mul_assoc_my_1 : ∀ a b c : Nat, (a * b) * c = a * (b * c) := by
  intro a b c
  simp [Nat.mul_comm]
  simp [Nat.mul_comm, Nat.mul_left_comm]

theorem my_and_comm_1 : ∀ {p q : Prop}, And p q → And q p := by
  simp
  intro p q hp hq
  exact ⟨hq, hp⟩

theorem my_add_comm_2 (n m : Nat) : n + m = m + n := by
  rw [Nat.add_comm]

theorem succ_add_succ_2 (a b : Nat) : Nat.succ a + Nat.succ b = Nat.succ (Nat.succ (a + b)) := by
  sorry

theorem mul_assoc_my_2 : ∀ a b c : Nat, (a * b) * c = a * (b * c) := by
  intro a b c
  simp [Nat.mul_comm]
  simp [Nat.mul_comm, Nat.mul_left_comm]

theorem my_and_comm_2 : ∀ {p q : Prop}, And p q → And q p := by
  simp
  intro p q hp hq
  exact ⟨hq, hp⟩

theorem my_add_comm_3 (n m : Nat) : n + m = m + n := by
  rw [Nat.add_comm]

theorem succ_add_succ_3 (a b : Nat) : Nat.succ a + Nat.succ b = Nat.succ (Nat.succ (a + b)) := by
  sorry

theorem mul_assoc_my_3 : ∀ a b c : Nat, (a * b) * c = a * (b * c) := by
  intro a b c
  simp [Nat.mul_comm]
  simp [Nat.mul_comm, Nat.mul_left_comm]

theorem my_and_comm_3 : ∀ {p q : Prop}, And p q → And q p := by
  simp
  intro p q hp hq
  exact ⟨hq, hp⟩

theorem my_add_comm_4 (n m : Nat) : n + m = m + n := by
  rw [Nat.add_comm]

theorem succ_add_succ_4 (a b : Nat) : Nat.succ a + Nat.succ b = Nat.succ (Nat.succ (a + b)) := by
  sorry

theorem mul_assoc_my_4 : ∀ a b c : Nat, (a * b) * c = a * (b * c) := by
  intro a b c
  simp [Nat.mul_comm]
  simp [Nat.mul_comm, Nat.mul_left_comm]

theorem my_and_comm_4 : ∀ {p q : Prop}, And p q → And q p := by
  simp
  intro p q hp hq
  exact ⟨hq, hp⟩