2 suppose a : Nat
3 suppose b : Nat
4 suppose c : Nat
5 conclude eq(mult(mult(a, b), c), mult(a, mult(b, c)))
7axiom idempotence_of_one
8 suppose a : Nat
9 conclude eq(mult(1, a), a)
11axiom distributive_property_of_multiplication_over_addition
12 suppose a : Nat
13 suppose b : Nat
14 suppose c : Nat
15 conclude eq(mult(add(a, b), c), add(mult(a, c), mult(b, c)))
17axiom associativity_of_addition
18 suppose a : Nat
19 suppose b : Nat
20 suppose c : Nat
21 conclude eq(add(add(a, b), c), add(a, add(b, c)))
23axiom arithmetic1
24 conclude eq(add(1, 1), 2)
26# If a and b are propositions, and a and b are both true,
27# then a and b is true.
28theorem test1
29 suppose a : Prop
30 suppose b : Prop
31 suppose h1 : a
32 suppose h2 : b
33 conclude and(a, b)
34 proof
35 unpack-and
36 goal a
37 proof
38 exact h1
39 goal b
40 proof
41 exact h2
43# If a and b are propositions, and a and b are both true,
44# then a and b and a is true.
45theorem test2
46 suppose a : Prop
47 suppose b : Prop
48 suppose h1 : a
49 suppose h2 : b
50 conclude and(a, and(b, a))
51 proof
52 unpack-and
53 goal a
54 proof
55 exact h1
56 goal and(b, a)
57 proof
58 unpack-and
59 goal b
60 proof
61 exact h2
62 goal a
63 proof
64 exact h1
66# If a and (b or c) are true,
67# then (a and b) or (a and c) is true.
68theorem test3
69 suppose a : Prop
70 suppose b : Prop
71 suppose c : Prop
72 suppose h : and(a, or(b, c))
73 conclude or(and(a, b), and(a, c))
74 proof
75 we-have or_b_c : or(b, c)
76 proof
77 exact right(h)
78 cases or_b_c
79 case h_b : b
80 proof
81 assert-goal or(and(a, b), and(a, c))
82 focus-or left
83 assert-goal and(a, b)
84 unpack-and
85 goal a
86 proof
87 exact left(h)
88 goal b
89 proof
90 exact h_b
91 case h_c : c
92 proof
93 assert-goal or(and(a, b), and(a, c))
94 focus-or right
95 assert-goal and(a, c)
96 unpack-and
97 goal a
98 proof
99 exact left(h)
100 goal c
101 proof
102 exact h_c
104# If there exists a natural number n such that P n is true,
105# then there exists a natural number a such that P a is true.
106theorem existence
107 suppose P : func(Nat, Prop)
108 suppose n : Nat
109 suppose h : apply(P, n)
110 conclude exists(a : Nat, apply(P, a))
111 proof
112 witness n
113 assert-goal apply(P, n)
114 exact h
116# If n is an even natural number,
117# then n + 2 is also an even natural number.
118theorem abc
119 suppose n : Nat
120 suppose h : exists(m : Nat, eq(n, mult(m, 2)))
121 conclude exists(q : Nat, eq(add(n, 2), mult(q, 2)))
122 proof
123 deconstruct-exists h m h_m
124 assert h_m : eq(n, mult(m, 2))
125 define d_q : eq(q, add(m, 1))
126 witness q
127 assert-goal eq(add(n, 2), mult(q, 2))
128 calculate add(n, 2)
129 = add(mult(m, 2), 2) by-lhs h_m
130 = add(mult(m, 2), mult(1, 2)) by-rhs idempotence_of_one 2
131 = mult(add(m, 1), 2) by-rhs distributive_property_of_multiplication_over_addition m 1 2
132 = mult(q, 2) by-rhs d_q
134# If for every natural number n there exists a natural number m such that m = n + 1,
135# then for every natural number t there exists a natural number u such that u = t + 2.
136theorem forall2
137 suppose h : forall(n : Nat, exists(s : Nat, eq(s, add(n, 1))))
138 conclude forall(t : Nat, exists(u : Nat, eq(u, add(t, 2))))
139 proof
140 consider t
141 assert-goal exists(u : Nat, eq(u, add(t, 2)))
142 forall-apply h t h2
143 assert h2 : exists(s : Nat, eq(s, add(t, 1)))
144 deconstruct-exists h2 m h_m
145 assert h_m : eq(m, add(t, 1))
146 forall-apply h m h3
147 assert h3 : exists(s : Nat, eq(s, add(m, 1)))
148 deconstruct-exists h3 u h_u
149 assert h_u: eq(u, add(m, 1))
150 witness u
151 assert-goal eq(u, add(t, 2))
152 calculate u
153 = add(m, 1) by-lhs h_u
154 = add(add(t, 1), 1) by-lhs h_m
155 = add(t, add(1, 1)) by-lhs associativity_of_addition t 1 1
156 = add(t, 2) by-lhs arithmetic1
158# If m divides n and n divides p, then m divides p.
159theorem divides_transitive
160 suppose m : Nat
161 suppose n : Nat
162 suppose p : Nat
163 suppose h1 : exists(k1 : Nat, eq(n, mult(m, k1)))
164 suppose h2 : exists(k2 : Nat, eq(p, mult(n, k2)))
165 conclude exists(k3 : Nat, eq(p, mult(m, k3)))
166 proof
167 deconstruct-exists h1 k1 h_n
168 assert h_n : eq(n, mult(m, k1))
169 deconstruct-exists h2 k2 h_p
170 assert h_p : eq(p, mult(n, k2))
171 define d_k3 : eq(k3, mult(k1, k2))
172 witness k3
173 assert-goal eq(p, mult(m, k3))
174 calculate p
175 = mult(n, k2) by-lhs h_p
176 = mult(mult(m, k1), k2) by-lhs h_n
177 = mult(m, mult(k1, k2)) by-lhs associativity_of_multiplication m k1 k2
178 = mult(m, k3) by-rhs d_k3