-include "basics/logic.ma".
+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.
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 your received in input.
+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 *)
].
(* It is worth to observe that the previous algorithm works by recursion over the first
-argument. This means that, for instance, (add 0 x) will reduce to x, as expected, but (add x 0)
-is stack. How can we prove that, for a generic x, (add x 0) = x? The mathematical tool do it is
+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 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 vcery simple way. If your goal is P(n), the
+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).
definition 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 m there
-exists a natural number m that is the integer half of m. This
-will give us the opportunity to introduce new connectives
-and quantifiers, and later on to make some interesting consideration
-on proofs and computations. *)
+(* We are interested to prove that for any natural number m there exists a natural number m that
+is the integer half of m. 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).
#n elim n normalize
*)
[@(\ 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/
]
-qed.
\ No newline at end of file
+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 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. *)
+
+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>
+ ]
+].
\ No newline at end of file
projects / helm.git / blobdiff