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