+(*
+\ 5h1 class="section"\ 6Induction and Recursion\ 5/h1\ 6
+*)
include "basics/types.ma".
(* Most of the types we have seen so far are enumerated types, composed by a
generated by a constant 0 and a successor function from natural numbers to natural
numbers *)
-inductive nat : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="nat"\ 6inductive nat : Type[0] ≝
| O :nat
| S: nat →nat.
you received in input. Most mathematical functions can be naturally defined in this
way. For instance, the sum of two natural numbers can be defined as follows *)
-let rec add n m ≝
+\ 5img class="anchor" src="icons/tick.png" id="add"\ 6let rec add n m ≝
match n with
[ O ⇒ m
| S a ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"\ 6S\ 5/a\ 6 (add a m)
].
-(* It is worth to observe that the previous algorithm works by recursion over the
+(*
+\ 5h2 class="section"\ 6Elimination\ 5/h2\ 6
+It is worth to observe that the previous algorithm works by recursion over the
first argument. This means that, for instance, (add O x) will reduce to x, as
expected, but (add x O) is stuck.
How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do
Let us apply it to our case *)
-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.
+\ 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.
#a elim a
(* If you stop the computation here, you will see on the right the two subgoals
(* In a similar way, it is convenient to state a lemma about the behaviour of
add when the second argument is not zero. *)
-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).
+\ 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).
(* In the same way as before, we proceed by induction over a. *)
(* We are now in the position to prove the commutativity of the sum *)
-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.
+\ 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.
#a elim a normalize
(* We have two sub goals:
(* COERCIONS *)
-inductive bool : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="bool"\ 6inductive bool : Type[0] ≝
| tt : bool
| ff : bool.
-definition nat_of_bool ≝ λb. match b with
+\ 5img class="anchor" src="icons/tick.png" id="nat_of_bool"\ 6definition nat_of_bool ≝ λb. match b with
[ 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
| ff ⇒ \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6
].
(* Let us now define the following function: *)
-definition twice ≝ λn.\ 5a href="cic:/matita/tutorial/chapter2/add.fix(0,0,1)"\ 6add\ 5/a\ 6 n n.
+\ 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.
-(* We are interested to prove that for any natural number n there exists a natural
+(*
+\ 5h2 class="section"\ 6Existential\ 5/h2\ 6
+We are interested to prove that for any natural number n there exists a natural
number m that is the integer half of n. This will give us the opportunity to
introduce new connectives and quantifiers and, later on, to make some interesting
consideration on proofs and computations. *)
-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).
+\ 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).
#n elim n normalize
(* We proceed by induction on n, that breaks down to the following goals:
*)
[@(\ 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 //
-(* The case of G2 is more complex. We should start introducing x and the
+(*
+\ 5h2 class="section"\ 6Destructuration\ 5/h2\ 6
+The case of G2 is more complex. We should start introducing x and the
inductive hypothesis
IH: ∃m. x = add m m ∨ x = S (add m m)
At this point we should assume the existence of m enjoying the inductive
-hypothesis. To eliminate the existential from the context we can just use the case
-tactic. This situation where we introduce something into the context and immediately
-eliminate it by case analysis is so frequent that Matita provides a convenient
-shorthand: you can just type a single "*".
-The star symbol should be reminiscent of an explosion: the idea is that you have a
-structured hypothesis, and you ask to explode it into its constituents. In the case
-of the existential, it allows to pass from a goal of the shape
+hypothesis. To eliminate the existential from the context we can just use the
+case tactic. This situation where we introduce something into the context and
+immediately eliminate it by case analysis is so frequent that Matita provides a
+convenient shorthand: you can just type a single "*".
+The star symbol should be reminiscent of an explosion: the idea is that you have
+a structured hypothesis, and you ask to explode it into its constituents. In the
+case of the existential, it allows to pass from a goal of the shape
(∃x.P x) → Q
to a goal of the shape
∀x.P x → Q
|#x *
(* At this point we are left with a new goal with the following shape
G3: ∀m. x = add m m ∨ x = S (add m m) → ....
-We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and then
-reason by cases on this hypothesis. It is the same situation as before: we explode the
-disjunctive hypothesis into its possible consituents. In the case of a disjunction, the
-* tactic allows to pass from a goal of the form
+We should introduce m, the hypothesis H: x = add m m ∨ x = S (add m m), and
+then reason by cases on this hypothesis. It is the same situation as before:
+we explode the disjunctive hypothesis into its possible consituents. In the case
+of a disjunction, the * tactic allows to pass from a goal of the form
A∨B → Q
to two subgoals of the form
A → Q and B → Q
*)
#m * #eqx
-(* In the first subgoal, we are under the assumption that x = add m m. The half of (S x)
-is hence m, and we have to prove the right branch of the disjunction.
-In the second subgoal, we are under the assumption that x = S (add m m). The halh of (S x)
-is hence (S m), and have to follow the left branch of the disjunction.
+(* In the first subgoal, we are under the assumption that x = add m m. The half
+of (S x) is hence m, and we have to prove the right branch of the disjunction.
+In the second subgoal, we are under the assumption that x = S (add m m). The halh
+of (S x) is hence (S m), and have to follow the left branch of the disjunction.
*)
[@(\ 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/
]
qed.
-(* Instead of proving the existence of a number corresponding to the half of n, we could
-be interested in computing it. The best way to do it is to define this division operation
-together with the remainder, that in our case is just a boolean value: tt if the input term
-is even, and ff if the input term is odd. Since we must return a pair, we could use a
-suitably defined record type, or simply a product type nat × bool, defined in the basic library.
-The product type is just a sort of general purpose record, with standard fields fst and snd,
-called projections. A pair of values n and m is written (pair … m n) or \langle n,m \rangle -
-visually rendered as 〈n,m〉
+(*
+\ 5h2 class="section"\ 6Computing vs. Proving\ 5/h2\ 6
+Instead of proving the existence of a number corresponding to the half of n,
+we could be interested in computing it. The best way to do it is to define this
+division operation together with the remainder, that in our case is just a
+boolean value: tt if the input term is even, and ff if the input term is odd.
+Since we must return a pair, we could use a suitably defined record type, or
+simply a product type nat × bool, defined in the basic library. The product type
+is just a sort of general purpose record, with standard fields fst and snd, called
+projections.
+A pair of values n and m is written (pair … m n) or \langle n,m \rangle - visually
+rendered as 〈n,m〉
We first write down the function, and then discuss it.*)
-let rec div2 n ≝
+\ 5img class="anchor" src="icons/tick.png" id="div2"\ 6let rec div2 n ≝
match n with
-[ 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〉
+[ 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
| S a ⇒ \ 5span style="text-decoration: underline;"\ 6\ 5/span\ 6
let p ≝ (div2 a) in
- match (\ 5a href="cic:/matita/basics/types/snd.def(1)"\ 6snd\ 5/a\ 6 … p) with
- [ 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〉
- | 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〉
+ 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
+ [ 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
+ | 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
]
].
-(* The function is computed by recursion over the input n. If n is 0, then the quotient
-is 0 and the remainder is tt. If n = S a, we start computing the half of a, say 〈q,b〉.
-Then we have two cases according to the possible values of b: if b is tt, then we must return
- 〈q,ff〉, while if b = ff then we must return 〈S q,tt〉.
-
-It is important to point out the deep, substantial analogy between the algorithm for
-computing div2 and the the proof of ex_half. In particular ex_half returns a
-proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the witness
-n and a boolean indicating which one between the two conditions A(n) and B(n) is met.
-This is precisely the quotient-remainder pair returned by div2.
-In both cases we proceed by recurrence (respectively, induction or recursion) over the
-input argument n. In case n = 0, we conclude the proof in ex_half by providing the
-witness O and a proof of A(O); this corresponds to returning the pair 〈O,ff〉 in div2.
-Similarly, in the inductive case n = S a, we must exploit the inductive hypothesis
-for a (i.e. the result of the recursive call), distinguishing two subcases according
-to the the two possibilites A(a) or B(a) (i.e. the two possibile values of the remainder
-for a). The reader is strongly invited to check all remaining details.
+(* The function is computed by recursion over the input n. If n is 0, then the
+quotient is 0 and the remainder is tt. If n = S a, we start computing the half
+of a, say 〈q,b〉. Then we have two cases according to the possible values of b:
+if b is tt, then we must return 〈q,ff〉, while if b = ff then we must return
+〈S q,tt〉.
+
+It is important to point out the deep, substantial analogy between the algorithm
+for computing div2 and the the proof of ex_half. In particular ex_half returns a
+proof of the kind ∃n.A(n)∨B(n): the really informative content in it is the
+witness n and a boolean indicating which one between the two conditions A(n) and
+B(n) is met. This is precisely the quotient-remainder pair returned by div2.
+In both cases we proceed by recurrence (respectively, induction or recursion) over
+the input argument n. In case n = 0, we conclude the proof in ex_half by providing
+the witness O and a proof of A(O); this corresponds to returning the pair 〈O,ff〉 in
+div2. Similarly, in the inductive case n = S a, we must exploit the inductive
+hypothesis for a (i.e. the result of the recursive call), distinguishing two subcases
+according to the the two possibilites A(a) or B(a) (i.e. the two possibile values of
+the remainder for a). The reader is strongly invited to check all remaining details.
Let us now prove that our div2 function has the expected behaviour.
*)
-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〉.
+\ 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.
#A #B * // qed.
-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〉.
+\ 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.
#n #q #H normalize >H normalize // qed.
-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〉.
+\ 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.
#n #q #H normalize >H normalize // qed.
-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).
+\ 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).
#n elim n
[#q #r normalize #H destruct //
|#a #Hind #q #r
- 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)〉) [//]
- 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))
- [#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)
+ 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) [//]
+ 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))
+ [#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)
|#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)
]
qed.
-(* There is still another possibility, however, namely to mix the program and its
-specification into a single entity. The idea is to refine the output type of the div2
-function: it should not be just a generic pair 〈q,r〉 of natural numbers but a specific
-pair satisfying the specification of the function. In other words, we need the
-possibility to define, for a type A and a property P over A, the subset type
-{a:A|P(a)} of all elements a of type A that satisfy the property P. Subset types are
-just a particular case of the so called dependent types, that is types that can
-depend over arguments (such as arrays of a specified length, taken as a parameter).
-These kind of types are quite unusual in traditional programming languages, and their
-study is one of the new frontiers of the current research on type systems.
-
-There is nothing special in a subset type {a:A|P(a)}: it is just a record composed by
-an element of a of type A and a proof of P(a). The crucial point is to have a language
-reach enough to comprise proofs among its expressions.
+(*
+\ 5h2 class="section"\ 6Mixing proofs and computations\ 5/h2\ 6
+There is still another possibility, however, namely to mix the program and its
+specification into a single entity. The idea is to refine the output type of the
+div2 function: it should not be just a generic pair 〈q,r〉 of natural numbers but a
+specific pair satisfying the specification of the function. In other words, we need
+the possibility to define, for a type A and a property P over A, the subset type
+{a:A|P(a)} of all elements a of type A that satisfy the property P. Subset types
+are just a particular case of the so called dependent types, that is types that
+can depend over arguments (such as arrays of a specified length, taken as a
+parameter).These kind of types are quite unusual in traditional programming
+languages, and their study is one of the new frontiers of the current research on
+type systems.
+
+There is nothing special in a subset type {a:A|P(a)}: it is just a record composed
+by an element of a of type A and a proof of P(a). The crucial point is to have a
+language reach enough to comprise proofs among its expressions.
*)
-record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝
+\ 5img class="anchor" src="icons/tick.png" id="Sub"\ 6record Sub (A:Type[0]) (P:A → Prop) : Type[0] ≝
{witness: A;
proof: P witness}.
-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).
+\ 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).
(* We can now construct a function from n to {p|qr_spec n p} by composing the objects
we already have *)
-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.
+\ 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.
\ 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).
(* But we can also try do directly build such an object *)
-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).
+\ 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).
#n elim n
- [@(\ 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 //
+ [@(\ 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 //
|#a * #p #qrspec
- 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〉) [//]
- cases (\ 5a href="cic:/matita/basics/types/snd.def(1)"\ 6snd\ 5/a\ 6 … p)
- [#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)
- |#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)
+ 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) [//]
+ cases (\ 5a href="cic:/matita/basics/types/snd.fix(0,2,1)"\ 6snd\ 5/a\ 6 … p)
+ [#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
+ whd in ⊢ (???%); <\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 @(qrspec … H)
+ |#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)
]
qed.
-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〉.
+\ 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.
// qed.
-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))))))
- \ 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〉.
+\ 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))))))
+ \ 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.
// qed.
\ 5pre\ 6\ 5pre\ 6 \ 5/pre\ 6\ 5/pre\ 6
\ No newline at end of file
projects / helm.git / blobdiff