weblib/tutorial/chapter2.ma

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