From 97e098c550b57e889f2bcbc18ca8242e881fb9cc Mon Sep 17 00:00:00 2001
From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 12 Oct 2011 11:06:00 +0000
Subject: [PATCH] commit by user andrea

---
 weblib/tutorial/chapter2.ma | 78 ++++++++++++++++++++++++++++++++-----
 1 file changed, 68 insertions(+), 10 deletions(-)

diff --git a/weblib/tutorial/chapter2.ma b/weblib/tutorial/chapter2.ma
index 449838e3a..ec3724cd8 100644
--- a/weblib/tutorial/chapter2.ma
+++ b/weblib/tutorial/chapter2.ma
@@ -141,17 +141,75 @@ be interested in computing it. The best way to do it is to define this division
 together with the remainder, that is 0 if the input term is even, and 1 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 N × N, defined in the basic library. The product type is just a sort of
-general purpose record, with standard fields fst and snd, called projections. *)
+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 ≝ 
 match n with
-[ O ⇒ <O,O>
-| S a ⇒ <O,O>
-].
-
- let p \def(div2 a) in
-   match (snd p) with
-   [ O ⇒ <fst p,1>
-   | S b \Rightarrow <S(fst p),O>  
+[ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a,a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉
+| S a ⇒ span style="text-decoration: underline;"/span
+   let p ≝ (div2 a) in
+   match (a href="cic:/matita/basics/types/snd.def(1)"snd/a … p) with
+   [ O ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p, a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉
+   | S b ⇒ a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … p),a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉 
    ]
-]. 
\ No newline at end of file
+]. 
+
+(* The function is computed by recursion over the input n. If n is 0, then both quotient
+and remainder are 0. If n = S a, we start computing the half of a, say 〈q,r〉. Then we
+have two cases according to the possible values of b: if b is 0, then we must return
+ 〈q,1〉, while if b = 1 (no other case is possible), then we must return 〈S q,0〉.
+
+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,O〉 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:Aa title="Product" href="cic:/fakeuri.def(1)"×/aB. p a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/basics/types/fst.def(1)"fst/a … p,a title="pair pi2" href="cic:/fakeuri.def(1)"\snd/a … p〉.
+#A #B * // qed.
+
+lemma div2SO: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aspan style="text-decoration: underline;"/spanq, a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉.
+#n #q #H normalize >H normalize // qed.
+
+lemma div2S1: ∀n,q. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉 → a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a (a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a n) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aa href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a q,a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a〉.
+#n #q #H normalize >H normalize // qed.
+
+ lemma div2_ok: ∀n,q,r. a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="Pair construction" href="cic:/fakeuri.def(1)"〈/aq,r〉 →
+   r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a span style="text-decoration: underline;"/spana title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q a title="logical or" href="cic:/fakeuri.def(1)"∨/a 
+   r a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"O/a a title="logical and" href="cic:/fakeuri.def(1)"∧/a n a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/tutorial/chapter2/nat.con(0,2,0)"S/a (a href="cic:/matita/tutorial/chapter2/twice.def(2)"twice/a q).
+#n elim n
+  [#q #r normalize #H destruct %1 /2/
+  |#a #Hind #q #r cases (Hind … (a href="cic:/matita/tutorial/chapter2/surjective_pairing.def(3)"surjective_pairing/a …)) * #eqr #eqa
+    [>(a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"div2SO/a a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))) // #H %2 destruct <eqa /2/
+    |>(a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"div2S1/a a (a href="cic:/matita/basics/types/fst.def(1)"fst/a … (a href="cic:/matita/tutorial/chapter2/div2.fix(0,0,2)"div2/a a))) // #H %1 destruct >a href="cic:/matita/tutorial/chapter2/add_S.def(2)"add_S/a <eqa /2/
+    ]
+  ]
+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 type 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 lenght, 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. 
+
+*)
+
+
-- 
2.39.2