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 ⇒ \ 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/nat.con(0,1,0)"\ 6O\ 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
+ [ O ⇒ \ 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/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 5/a\ 6〉
+ | S b ⇒ \ 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/nat.con(0,1,0)"\ 6O\ 5/a\ 6〉
]
-].
\ 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: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〉.
+#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/nat.con(0,1,0)"\ 6O\ 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/nat.con(0,2,0)"\ 6S\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter2/nat.con(0,1,0)"\ 6O\ 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/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/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/nat.con(0,1,0)"\ 6O\ 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〉 →
+ r \ 5a title="leibnitz's equality" 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 style="text-decoration: underline;"\ 6\ 5/span\ 6\ 5a title="logical and" 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/twice.def(2)"\ 6twice\ 5/a\ 6 q \ 5a title="logical or" href="cic:/fakeuri.def(1)"\ 6∨\ 5/a\ 6
+ r \ 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/nat.con(0,1,0)"\ 6O\ 5/a\ 6 \ 5a title="logical and" 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 q).
+#n elim n
+ [#q #r normalize #H destruct %1 /2/
+ |#a #Hind #q #r cases (Hind … (\ 5a href="cic:/matita/tutorial/chapter2/surjective_pairing.def(3)"\ 6surjective_pairing\ 5/a\ 6 …)) * #eqr #eqa
+ [>(\ 5a href="cic:/matita/tutorial/chapter2/div2SO.def(3)"\ 6div2SO\ 5/a\ 6 a (\ 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))) // #H %2 destruct <eqa /2/
+ |>(\ 5a href="cic:/matita/tutorial/chapter2/div2S1.def(3)"\ 6div2S1\ 5/a\ 6 a (\ 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))) // #H %1 destruct >\ 5a href="cic:/matita/tutorial/chapter2/add_S.def(2)"\ 6add_S\ 5/a\ 6 <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.
+
+*)
+
+
projects / helm.git / commitdiff