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