+(*
+\ 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 finite set of
-alternatives, and records, composed by tuples of heteregoneous elements.
-A more interesting case of type definition is when some of the rules defining its elements are
-recursive, i.e. they allow the formation of more elements of the type in terms of the already
-defined ones. The most typical case is provided by the natural numbers, that can be defined as
-the smallest set generated by a constant 0 and a successor function from natural numbers to
-natural numbers *)
+(* Most of the types we have seen so far are enumerated types, composed by a
+finite set of alternatives, and records, composed by tuples of heteregoneous
+elements. A more interesting case of type definition is when some of the rules
+defining its elements are recursive, i.e. they allow the formation of more
+elements of the type in terms of the already defined ones. The most typical case
+is provided by the natural numbers, that can be defined as the smallest set
+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.
-(* The two terms O and S are called constructors: they define the signature of the type, whose
-objects are the elements freely generated by means of them. So, examples of natural numbers are
-O, S O, S (S O), S (S (S O)) and so on.
+(* The two terms O and S are called constructors: they define the signature of the
+type, whose objects are the elements freely generated by means of them. So,
+examples of natural numbers are O, S O, S (S O), S (S (S O)) and so on.
-The language of Matita allows the definition of well founded recursive functions over inductive
-types; in order to guarantee termination of recursion you are only allowed to make recursive
-calls on structurally smaller arguments than the ones 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 *)
+The language of Matita allows the definition of well founded recursive functions
+over inductive types; in order to guarantee termination of recursion you are only
+allowed to make recursive calls on structurally smaller arguments than the ones
+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 first
-argument. This means that, for instance, (add O x) will reduce to x, as expected, but (add x O)
-is stack. How can we prove that, for a generic x, (add x O) = x? The mathematical tool to do it
-is called induction. The induction principle states that, given a property P(n) over natural
-numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m), than we can conclude
-P(n) for any n.
-
-The elim tactic, allow you to apply induction in a very simple way. If your goal is P(n), the
-invocation of
+(*
+\ 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
+it is called induction. The induction principle states that, given a property P(n)
+over natural numbers, if we prove P(0) and prove that, for any m, P(m) implies P(S m),
+than we can conclude P(n) for any n.
+
+The elim tactic, allow you to apply induction in a very simple way. If your goal is
+P(n), the invocation of
elim n
will break down your task to prove the two subgoals P(0) and ∀m.P(m) → P(S m).
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
normalize // qed.
-(* In a similar way, it is convenient to state a lemma about the behaviour of add when the
-second argument is not zero. *)
+(* 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:
G1: ∀b. b = add b O
G2: ∀x.(∀b. add x b = add b x) → ∀b. S (add x b) = add b (S x).
-G1 is just our lemma add_O. For G2, we start introducing x and the induction hypothesis IH;
-then, the goal is proved by rewriting using add_S and IH.
+G1 is just our lemma add_O. For G2, we start introducing x and the induction
+hypothesis IH; then, the goal is proved by rewriting using add_S and IH.
For Matita, the task is trivial and we can simply close the goal with // *)
// qed.
(* 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 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. *)
+(*
+\ 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:
G1: ∃m.O = add O O ∨ O = S (add m m)
G2: ∀x.(∃m. x = add m m ∨ x = S (add m m))→ ∃m. S x = add m m ∨ S x = S (add m m)
-The only way we have to prove an existential goal is by exhibiting the witness, that in the case
-of first goal is O. We do it by apply the term called ex_intro instantiated by the witness.
-Then, it is clear that we must follow the left branch of the disjunction. One way to do it is by
-applying the term or_introl, that is the first constructor of the disjunction. However,
-remembering the names of constructors can be annyoing: we can invoke the application of the n-th
-constructor of an inductive type (inferred by the current goal) by typing %n. At this point
-we are left with the subgoal O = add O O, that is closed by computation.
-It is worth to observe that invoking automation at depth /3/ would also automatically close G1.
+The only way we have to prove an existential goal is by exhibiting the witness,
+that in the case of first goal is O. We do it by apply the term called ex_intro
+instantiated by the witness. Then, it is clear that we must follow the left branch
+of the disjunction. One way to do it is by applying the term or_introl, that is
+the first constructor of the disjunction. However, remembering the names of
+constructors can be annyoing: we can invoke the application of the n-th
+constructor of an inductive type (inferred by the current goal) by typing %n. At
+this point we are left with the subgoal O = add O O, that is closed by
+computation. It is worth to observe that invoking automation at depth /3/ would
+also automatically close G1.
*)
[@(\ 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 inductive hypothesis
+(*
+\ 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
+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
(∃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) /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/
+ [@(\ 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