1 \ 5h1 class="section"
\ 6Induction and Recursion
\ 5/h1
\ 6
2 include "basics/types.ma".
4 (* Most of the types we have seen so far are enumerated types, composed by a
5 finite set of alternatives, and records, composed by tuples of heteregoneous
6 elements. A more interesting case of type definition is when some of the rules
7 defining its elements are recursive, i.e. they allow the formation of more
8 elements of the type in terms of the already defined ones. The most typical case
9 is provided by the natural numbers, that can be defined as the smallest set
10 generated by a constant 0 and a successor function from natural numbers to natural
13 inductive nat : Type[0] ≝
17 (* The two terms O and S are called constructors: they define the signature of the
18 type, whose objects are the elements freely generated by means of them. So,
19 examples of natural numbers are O, S O, S (S O), S (S (S O)) and so on.
21 The language of Matita allows the definition of well founded recursive functions
22 over inductive types; in order to guarantee termination of recursion you are only
23 allowed to make recursive calls on structurally smaller arguments than the ones
24 you received in input. Most mathematical functions can be naturally defined in this
25 way. For instance, the sum of two natural numbers can be defined as follows *)
30 | S a ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (add a m)
34 \ 5h2 class="section"
\ 6Elimination
\ 5/h2
\ 6
35 It is worth to observe that the previous algorithm works by recursion over the
36 first argument. This means that, for instance, (add O x) will reduce to x, as
37 expected, but (add x O) is stuck.
38 How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do
39 it is called induction. The induction principle states that, given a property P(n)
40 over natural numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m),
41 than we can conclude P(n) for any n.
43 The elim tactic, allow you to apply induction in a very simple way. If your goal is
44 P(n), the invocation of
46 will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m).
48 Let us apply it to our case *)
50 lemma add_0: ∀a.
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 a
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 a.
53 (* If you stop the computation here, you will see on the right the two subgoals
55 - ∀x. add x 0 = x → add (S x) O = S x
56 After normalization, both goals are trivial.
61 (* In a similar way, it is convenient to state a lemma about the behaviour of
62 add when the second argument is not zero. *)
64 lemma add_S : ∀a,b.
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 a (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 b)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 a b).
66 (* In the same way as before, we proceed by induction over a. *)
68 #a #b elim a normalize //
71 (* We are now in the position to prove the commutativity of the sum *)
73 theorem add_comm : ∀a,b.
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 a b
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 b a.
76 (* We have two sub goals:
78 G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x).
79 G1 is just our lemma add_O. For G2, we start introducing x and the induction
80 hypothesis IH; then, the goal is proved by rewriting using add_S and IH.
81 For Matita, the task is trivial and we can simply close the goal with // *)
87 inductive bool : Type[0] ≝
91 definition nat_of_bool ≝ λb. match b with
92 [ tt ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
93 | ff ⇒
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6
96 (* coercion nat_of_bool. ?? *)
98 (* Let us now define the following function: *)
100 definition twice ≝ λn.
\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 n n.
103 \ 5h2 class="section"
\ 6Existential
\ 5/h2
\ 6
104 We are interested to prove that for any natural number n there exists a natural
105 number m that is the integer half of n. This will give us the opportunity to
106 introduce new connectives and quantifiers and, later on, to make some interesting
107 consideration on proofs and computations. *)
109 theorem ex_half: ∀n.
\ 5a title="exists" href="cic:/fakeuri.def(1)"
\ 6∃
\ 5/a
\ 6m. n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 m
\ 5a title="logical or" href="cic:/fakeuri.def(1)"
\ 6∨
\ 5/a
\ 6 n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 m).
112 (* We proceed by induction on n, that breaks down to the following goals:
113 G1: ∃m.O = add O O ∨ O = S (add m m)
114 G2: ∀x.(∃m. x = add m m ∨ x = S (add m m))→ ∃m. S x = add m m ∨ S x = S (add m m)
115 The only way we have to prove an existential goal is by exhibiting the witness,
116 that in the case of first goal is O. We do it by apply the term called ex_intro
117 instantiated by the witness. Then, it is clear that we must follow the left branch
118 of the disjunction. One way to do it is by applying the term or_introl, that is
119 the first constructor of the disjunction. However, remembering the names of
120 constructors can be annyoing: we can invoke the application of the n-th
121 constructor of an inductive type (inferred by the current goal) by typing %n. At
122 this point we are left with the subgoal O = add O O, that is closed by
123 computation. It is worth to observe that invoking automation at depth /3/ would
124 also automatically close G1.
126 [@(
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6 …
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6) %1 //
129 \ 5h2 class="section"
\ 6Destructuration
\ 5/h2
\ 6
130 The case of G2 is more complex. We should start introducing x and the
132 IH: ∃m. x = add m m ∨ x = S (add m m)
133 At this point we should assume the existence of m enjoying the inductive
134 hypothesis. To eliminate the existential from the context we can just use the
135 case tactic. This situation where we introduce something into the context and
136 immediately eliminate it by case analysis is so frequent that Matita provides a
137 convenient shorthand: you can just type a single "*".
138 The star symbol should be reminiscent of an explosion: the idea is that you have
139 a structured hypothesis, and you ask to explode it into its constituents. In the
140 case of the existential, it allows to pass from a goal of the shape
142 to a goal of the shape
146 (* At this point we are left with a new goal with the following shape
147 G3: ∀m. x = add m m ∨ x = S (add m m) → ....
148 We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and
149 then reason by cases on this hypothesis. It is the same situation as before:
150 we explode the disjunctive hypothesis into its possible consituents. In the case
151 of a disjunction, the * tactic allows to pass from a goal of the form
153 to two subgoals of the form
157 (* In the first subgoal, we are under the assumption that x = add m m. The half
158 of (S x) is hence m, and we have to prove the right branch of the disjunction.
159 In the second subgoal, we are under the assumption that x = S (add m m). The halh
160 of (S x) is hence (S m), and have to follow the left branch of the disjunction.
162 [@(
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6 … m) /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"
\ 6or_intror
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/ | @(
\ 5a href="cic:/matita/basics/logic/ex.con(0,1,2)"
\ 6ex_intro
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 m)) normalize /
\ 5span class="autotactic"
\ 62
\ 5span class="autotrace"
\ 6 trace
\ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"
\ 6or_introl
\ 5/a
\ 6\ 5/span
\ 6\ 5/span
\ 6/
167 \ 5h2 class="section"
\ 6Computing vs. Proving
\ 5/h2
\ 6
168 Instead of proving the existence of a number corresponding to the half of n,
169 we could be interested in computing it. The best way to do it is to define this
170 division operation together with the remainder, that in our case is just a
171 boolean value: tt if the input term is even, and ff if the input term is odd.
172 Since we must return a pair, we could use a suitably defined record type, or
173 simply a product type nat × bool, defined in the basic library. The product type
174 is just a sort of general purpose record, with standard fields fst and snd, called
176 A pair of values n and m is written (pair … m n) or \langle n,m \rangle - visually
179 We first write down the function, and then discuss it.*)
183 [ O ⇒
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6\ 5span class="error" title="Parse error: [sym,] expected after [term level 19] (in [term])"
\ 6\ 5/span
\ 6,
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"
\ 6ff
\ 5/a
\ 6〉
184 | S a ⇒
\ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6
186 match (
\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"
\ 6snd
\ 5/a
\ 6\ 5span class="error" title="Parse error: SYMBOL ':' or RPAREN expected after [term] (in [term])"
\ 6\ 5/span
\ 6 … p) with
187 [ tt ⇒
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (
\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"
\ 6fst
\ 5/a
\ 6 … p),
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"
\ 6ff
\ 5/a
\ 6〉
188 | ff ⇒
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"
\ 6fst
\ 5/a
\ 6 … p,
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"
\ 6tt
\ 5/a
\ 6〉
192 (* The function is computed by recursion over the input n. If n is 0, then the
193 quotient is 0 and the remainder is tt. If n = S a, we start computing the half
194 of a, say 〈q,b〉. Then we have two cases according to the possible values of b:
195 if b is tt, then we must return 〈q,ff〉, while if b = ff then we must return
198 It is important to point out the deep, substantial analogy between the algorithm
199 for computing div2 and the the proof of ex_half. In particular ex_half returns a
200 proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the
201 witness n and a boolean indicating which one between the two conditions A(n) and
202 B(n) is met. This is precisely the quotient-remainder pair returned by div2.
203 In both cases we proceed by recurrence (respectively, induction or recursion) over
204 the input argument n. In case n = 0, we conclude the proof in ex_half by providing
205 the witness O and a proof of A(O); this corresponds to returning the pair 〈O,ff〉 in
206 div2. Similarly, in the inductive case n = S a, we must exploit the inductive
207 hypothesis for a (i.e. the result of the recursive call), distinguishing two subcases
208 according to the the two possibilites A(a) or B(a) (i.e. the two possibile values of
209 the remainder for a). The reader is strongly invited to check all remaining details.
211 Let us now prove that our div2 function has the expected behaviour.
214 lemma surjective_pairing: ∀A,B.∀p:A
\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6B. p
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"
\ 6fst
\ 5/a
\ 6 … p,
\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"
\ 6\snd
\ 5/a
\ 6\ 5span class="error" title="Parse error: [sym〉] or [sym,] expected after [term level 19] (in [term])"
\ 6\ 5/span
\ 6 … p〉.
217 lemma div2SO: ∀n,q.
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6q,
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"
\ 6ff
\ 5/a
\ 6〉 →
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6q,
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"
\ 6tt
\ 5/a
\ 6〉.
218 #n #q #H normalize >H normalize // qed.
220 lemma div2S1: ∀n,q.
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6q,
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"
\ 6tt
\ 5/a
\ 6〉 →
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 n)
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6\ 5span class="error" title="Parse error: [term] expected after [sym=] (in [term])"
\ 6\ 5/span
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 q,
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"
\ 6ff
\ 5/a
\ 6〉.
221 #n #q #H normalize >H normalize // qed.
223 lemma div2_ok: ∀n,q,r.
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6q,r〉 → n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 q) (
\ 5a href="cic:/matita/tutorial/chapter2/nat_of_bool.def(1)"
\ 6nat_of_bool
\ 5/a
\ 6 r).
225 [#q #r normalize #H destruct //
227 cut (
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 a
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"
\ 6fst
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 a),
\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"
\ 6snd
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 a)〉) [//]
228 cases (
\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"
\ 6snd
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 a))
229 [#H >(
\ 5a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"
\ 6div2S1
\ 5/a
\ 6 … H) #H1 destruct @
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6 \ 5span style="text-decoration: underline;"
\ 6>
\ 5/span
\ 6\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"
\ 6add_S
\ 5/a
\ 6 whd in ⊢ (???%); <
\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"
\ 6add_S
\ 5/a
\ 6 @(Hind … H)
230 |#H >(
\ 5a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"
\ 6div2SO
\ 5/a
\ 6 … H) #H1 destruct >
\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"
\ 6add_S
\ 5/a
\ 6 @
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6 @(Hind … H)
235 \ 5h2 class="section"
\ 6Mixing proofs and computations
\ 5/h2
\ 6
236 There is still another possibility, however, namely to mix the program and its
237 specification into a single entity. The idea is to refine the output type of the
238 div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a
239 specific pair satisfying the specification of the function. In other words, we need
240 the possibility to define, for a type A and a property P over A, the subset type
241 {a:A|P(a)} of all elements a of type A that satisfy the property P. Subset types
242 are just a particular case of the so called dependent types, that is types that
243 can depend over arguments (such as arrays of a specified length, taken as a
244 parameter).These kind of types are quite unusual in traditional programming
245 languages, and their study is one of the new frontiers of the current research on
248 There is nothing special in a subset type {a:A|P(a)}: it is just a record composed
249 by an element of a of type A and a proof of P(a). The crucial point is to have a
250 language reach enough to comprise proofs among its expressions.
253 record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝
257 definition qr_spec ≝ λn.λp.∀q,r. p
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6q,r〉 → n
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"
\ 6add
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 q) (
\ 5a href="cic:/matita/tutorial/chapter2/nat_of_bool.def(1)"
\ 6nat_of_bool
\ 5/a
\ 6 r).
259 (* We can now construct a function from n to {p|qr_spec n p} by composing the objects
262 definition div2P: ∀n.
\ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"
\ 6Sub
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6\ 5span style="text-decoration: underline;"
\ 6\ 5a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6\ 5/span
\ 6) (
\ 5a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"
\ 6qr_spec
\ 5/a
\ 6 n) ≝ λn.
263 \ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"
\ 6mk_Sub
\ 5/a
\ 6 ?? (
\ 5a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"
\ 6div2
\ 5/a
\ 6 n) (
\ 5a href="cic:/matita/tutorial/chapter2/div2_ok.def(4)"
\ 6div2_ok
\ 5/a
\ 6 n).
265 (* But we can also try do directly build such an object *)
267 definition div2Pagain : ∀n.
\ 5a href="cic:/matita/tutorial/chapter2/Sub.ind(1,0,2)"
\ 6Sub
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/nat.ind(1,0,0)"
\ 6nat
\ 5/a
\ 6\ 5a title="Product" href="cic:/fakeuri.def(1)"
\ 6×
\ 5/a
\ 6\ 5span style="text-decoration: underline;"
\ 6\ 5/span
\ 6\ 5a href="cic:/matita/tutorial/chapter2/bool.ind(1,0,0)"
\ 6bool
\ 5/a
\ 6) (
\ 5a href="cic:/matita/tutorial/chapter2/qr_spec.def(3)"
\ 6qr_spec
\ 5/a
\ 6 n).
269 [@(
\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"
\ 6mk_Sub
\ 5/a
\ 6 …
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6,
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"
\ 6ff
\ 5/a
\ 6〉) normalize #q #r #H destruct //
271 cut (p
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"
\ 6fst
\ 5/a
\ 6 … p,
\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"
\ 6snd
\ 5/a
\ 6 … p〉) [//]
272 cases (
\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"
\ 6snd
\ 5/a
\ 6 … p)
273 [#H @(
\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"
\ 6mk_Sub
\ 5/a
\ 6 …
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 (
\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"
\ 6fst
\ 5/a
\ 6 … p),
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"
\ 6ff
\ 5/a
\ 6〉) whd #q #r #H1 destruct @
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6 \ 5span style="text-decoration: underline;"
\ 6>
\ 5/span
\ 6\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"
\ 6add_S
\ 5/a
\ 6
274 whd in ⊢ (???%); <
\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"
\ 6add_S
\ 5/a
\ 6 @(qrspec … H)
275 |#H @(
\ 5a href="cic:/matita/tutorial/chapter2/Sub.con(0,1,2)"
\ 6mk_Sub
\ 5/a
\ 6 …
\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/basics/types/fst.fix(0,2,1)"
\ 6fst
\ 5/a
\ 6 … p,
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"
\ 6tt
\ 5/a
\ 6〉) whd #q #r #H1 destruct >
\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"
\ 6add_S
\ 5/a
\ 6 @
\ 5a href="cic:/matita/basics/logic/eq_f.def(3)"
\ 6eq_f
\ 5/a
\ 6 @(qrspec … H)
279 example quotient7:
\ 5a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"
\ 6witness
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter2/div2Pagain.def(4)"
\ 6div2Pagain
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6))))))))
\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6(
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6)),
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,1,0)"
\ 6tt
\ 5/a
\ 6〉.
282 example quotient8:
\ 5a href="cic:/matita/tutorial/chapter2/witness.fix(0,2,1)"
\ 6witness
\ 5/a
\ 6 … (
\ 5a href="cic:/matita/tutorial/chapter2/div2Pagain.def(4)"
\ 6div2Pagain
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6))))))
283 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"
\ 6=
\ 5/a
\ 6 \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"
\ 6〈
\ 5/a
\ 6\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/twice.def(2)"
\ 6twice
\ 5/a
\ 6 (
\ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"
\ 6S
\ 5/a
\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"
\ 6O
\ 5/a
\ 6))),
\ 5a href="cic:/matita/tutorial/chapter2/bool.con(0,2,0)"
\ 6ff
\ 5/a
\ 6〉.
285 \ 5pre
\ 6\ 5pre
\ 6 \ 5/pre
\ 6\ 5/pre
\ 6