X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Ftutorial%2Fchapter5.ma;h=21a8abd2fcc515d169a2dca0335ab3136497da8f;hb=9c0398174ebfa6b483dbdd5c10e8b15e39067329;hp=9257767859935f9381519423008b66dea852066e;hpb=65c5a379db69f0df0c803f4b24bb3219c9da752a;p=helm.git diff --git a/matita/matita/lib/tutorial/chapter5.ma b/matita/matita/lib/tutorial/chapter5.ma index 925776785..21a8abd2f 100644 --- a/matita/matita/lib/tutorial/chapter5.ma +++ b/matita/matita/lib/tutorial/chapter5.ma @@ -2,7 +2,9 @@ More Data Types *) -include "basics/logic.ma". +include "tutorial/chapter4.ma". +include "arithmetics/nat.ma". + (******************************** Option Type *********************************) @@ -18,506 +20,405 @@ inductive option (A:Type[0]) : Type[0] ≝ None : option A | Some : A → option A. +let rec pred (n:nat) : option nat ≝ + match n with + [ O ⇒ None nat + | S a ⇒ Some nat a + ]. + (* The type option A is isomorphic to the disjoint sum between A and unit. The -two bijections are simply defined as -follows: -\begin{lstlisting}[language=grafite] -definition option_to_sum ≝ λA.λx:option A. +two bijections are simply defined as follows: *) + +definition option_to_sum : ∀A.option A → unit + A ≝ λA.λx:option A. match x with [ None ⇒ inl ?? it | Some a ⇒ inr ?? a ]. -\end{lstlisting} -\begin{lstlisting}[language=grafite] -definition sum_to_option ≝ λA.λx:unit+A. +definition sum_to_option :∀A. unit + A → option A ≝ λA.λx:unit+A. match x with [ inl a ⇒ None A | inr a ⇒ Some A a ]. -\end{lstlisting} -The fact that going from the option type to the sum and back again we get the -original element follows from a straightforward case analysis: -\begin{lstlisting}[language=grafite] + +(* The fact that going from the option type to the sum and back again we get the +original element follows from a straightforward case analysis: *) + lemma option_bij1: ∀A,x. sum_to_option A (option_to_sum A x) = x. -#A * // qed. -\end{lstlisting} -The other direction is just slightly more complex, since we need to exploit -the fact that the unit type contains a single element: we could use lemma ... or -proceed by cases on the unit element. -\begin{lstlisting}[language=grafite] +#A * [normalize // | #a normalize // ] qed. + +(* The other direction is just slightly more complex, since we need to exploit +the fact that the unit type contains a single element: we could use lemma +eq_unit or proceed by cases on the unit element. *) + lemma option_bij2: ∀A,x. option_to_sum A (sum_to_option A x) = x. -#A * // * // qed. -\end{lstlisting} -We shall see more examples of functions involving the otion type in the -next section. - -\subsection{Lists} -The option type, as well as the cartesian product or the sum are simple -examples of polymorphic types, that is types that depend in a uniform -and effective way on other types. This form of polymorphism (sometimes -called {\em parametric} polymporphism to distinguish it from the -{\em ad hoc} polymorphism -typical of object oriented languages) is a major feature of modern -functional programming languages: in many intersting cases, -it allows to write {\em generic} functions operating on inputs without -depending on their type. Typical examples can be found on lists. -For instance, appending two lists is an operation that is essentially -independent from the type $A$ of the elements in the list, and we would like -to write a {\em single} append function working parametrically on $A$. - -The first step is to define a type for lists polimorphic over the -type $A$ of its elements: -\begin{lstlisting}[language=grafite] +#A * #x [normalize cases x // | //] qed. + +(* We shall see more examples of functions involving the otion type in the +next section. *) + +(********************************** Lists *************************************) + +(* The option type, as well as the cartesian product or the sum are simple +examples of polymorphic types, that is types that depend in a uniform and +effective way on other types. This form of polymorphism (sometimes called +"parametric" polymporphism to distinguish it from the "ad hoc" polymorphism +typical of object oriented languages) is a major feature of modern functional +programming languages: in many intersting cases, it allows to write generic +functions operating on inputs without depending on their type. Typical examples +can be found on lists. +For instance, appending two lists is an operation that is essentially +independent from the type A of the elements in the list, and we would like to +write a single append function working parametrically on A. + +The first step is to define a type for lists polimorphic over the type A of its +elements: *) + inductive list (A:Type[0]) : Type[0] := | nil: list A | cons: A -> list A -> list A. -\end{lstlisting} -The deinition should be clear: a list is either empty (\verb+nil+) or -is is obtained by concatenating (\verb+cons+) an element of type $A$ -to a given list. In other word, the type of lists is the smallest inductive -type generated by the two constructors \verb+nil+ and \verb+cons+. - -The first element of a list is called its {\em head}. If the list -is empty the head is undefined: as discussed in the previous section, -we should either return a ``default'' -element, or decide to return an option type. -We have an additional complication in this -case, since the ``default'' element should have type $A$ (as the head), -and we know nothing about $A$ (it could even be an empty type!). We -have no way to guess a canonical element, and the only -possibility (along this approach) is to take it in input. These -are the two options: -\begin{lstlisting}[language=grafite] + +(* The definition should be clear: a list is either empty (nil) or it is +obtained by concatenating (cons) an element of type A to a given list. In other +words, the type of lists is the smallest inductive type generated by the two +constructors nil and cons. + +The first element of a list is called its "head". If the list is empty the head +is undefined: as discussed in the previous section, we should either return a +``default'' element, or decide to return an option type. +We have an additional complication in this case, since the ``default'' element +should have type A, and we know nothing about A (it could even be an empty +type!). We have no way to guess a canonical element, and the only possibility +(along this approach) is to take it in input. These are the two options: *) + definition hd ≝ λA.λl: list A.λd:A. match l with [ nil ⇒ d | cons a _ ⇒ a]. -definition option_hd ≝ - λA.λl:list A. match l with - [ nil ⇒ None ? - | cons a _ ⇒ Some ? a ]. -\end{lstlisting} -What remains of a list after removing its head is called the {\em tail} -of the list. Again, the tail of an empty list is undefined, but in -this case the result must be a list, and we have a canonical inhabitant -of lists, that is the empty list. So, it is natural to extend the -definition of tail saying that the tail of nil is nil (that is -very similar to say that the predecessor of $0$ is $0$): -\begin{lstlisting}[language=grafite] +definition option_hd ≝ λA.λl:list A. + match l with [ nil ⇒ None ? | cons a _ ⇒ Some ? a ]. + +(* What remains of a list after removing its head is called the "tail" of the +list. Again, the tail of an empty list is undefined, but in this case the result +must be a list, and we have a canonical inhabitant of lists, that is the empty +list. So, it is natural to extend the definition of tail saying that the tail of +nil is nil (that is very similar to say that the predecessor of 0 is 0): *) + definition tail ≝ λA.λl: list A. - match l with [ nil ⇒ [] | cons hd tl ⇒ tl]. -\end{lstlisting} + match l with [ nil ⇒ nil ? | cons hd tl ⇒ tl]. + +(* Using destruct, it is easy to prove that cons is injective in both +arguments. *) -Using destruct, it is easy to prove that \verb+cons+ is injective -in both arguments. -\begin{lstlisting}[language=grafite] -lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → a1 = a2. +lemma cons_injective_l : ∀A.∀a1,a2:A.∀l1,l2. + cons ?a1 l1 = cons ? a2 l2 → a1 = a2. #A #a1 #a2 #l1 #l2 #Heq destruct // qed. -lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2.a1::l1 = a2::l2 → l1 = l2. +lemma cons_injective_r : ∀A.∀a1,a2:A.∀l1,l2. + cons ? a1 l1 = cons ? a2 l2 → l1 = l2. #A #a1 #a2 #l1 #l2 #Heq destruct // qed. -\end{lstlisting} -The append function is defined by recursion over the first list: -\begin{lstlisting}[language=grafite] + +(* The append function is defined by recursion over the first list: *) let rec append A (l1: list A) l2 on l1 ≝ match l1 with [ nil ⇒ l2 - | cons hd tl ⇒ hd :: append A tl l2 ]. -\end{lstlisting} -We leave to the reader to prove that \verb+append+ is associative, and -that \verb+nil+ is a neutral element for it. + | cons hd tl ⇒ cons ? hd (append A tl l2) ]. + +(******************************* list notation ********************************) + +(* Before discussing more operations over lists, it is convenient to introduce a +bit of notation; in particular, we shall write a::l for (cons ? a l); +[a1;a2,…, an] for the list composed by the elements a1, a2,…, an and l1@l2 for +the concatenation of l1 and l2. + +This can be obtained by the following declarations: *) + +notation "hvbox(hd break :: tl)" + right associative with precedence 47 for @{'cons $hd $tl}. + +notation "[ list0 term 19 x sep ; ]" + non associative with precedence 90 + for ${fold right @'nil rec acc @{'cons $x $acc}}. -\input{list_notation.tex} +notation "hvbox(l1 break @ l2)" + right associative with precedence 47 for @{'append $l1 $l2}. -We conclude this section discussing another important operation -over lists, namely the reverse funtion, retrurning -a list with the same elements of the original list but in reverse order. +interpretation "nil" 'nil = (nil ?). +interpretation "cons" 'cons hd tl = (cons ? hd tl). +interpretation "append" 'append l1 l2 = (append ? l1 l2). -One could define the revert operation as follows: -\begin{lstlisting}[language=grafite] -let rec rev S l1 on l1 ≝ +(* Note that [ ] is an alternative notation for the empty list, and [a] is a +list containing a singleton element a. +Let us check the notation: *) + +example append_ex1: [true;false]@[true] = [true;false;true]. +normalize // qed. + +(* As a simple exerices, now that we have a comfortable notation, let to prove +that append is associative, and that nil is a neutral element for it. *) + +lemma associative_append: ∀A.∀l1,l2,l3:list A. l1 @ (l2 @ l3) = (l1 @ l2) @ l3. +#A #l1 elim l1 [normalize //] +#a #tl #Hind #l2 #l3 normalize @eq_f @Hind qed. + +lemma append_nil: ∀A.∀l:list A. l@[ ] = l. +#A #l elim l // #a #tl #Hind normalize >Hind // qed. + +let rec length (A:Type[0]) (l:list A) on l ≝ + match l with + [ nil ⇒ O + | cons a tl ⇒ 1+(length A tl) + ]. + +interpretation "list length" 'card l = (length ? l). + +lemma length_tail: ∀A,l. length ? (tail A l) = pred (length ? l). +#A #l elim l // +qed. + +lemma length_append: ∀A.∀l1,l2:list A. + |l1@l2| = |l1|+|l2|. +#A #l1 elim l1 // normalize /2/ +qed. + +let rec nth (A:Type[0]) (l:list A) n on n ≝ + match n with + [ O ⇒ option_hd ? l + | S x ⇒ nth A (tail ? l) x + ]. + +lemma nth_length : ∀A,l,n. n < length A l → nth A l n ≠ None ?. +#A #l elim l + [#n normalize #H @False_ind /2 by absurd/ + |#a #tl #Hind #n normalize + #H lapply (le_S_S_to_le … H) -H cases n + [#_ normalize % #H1 destruct (H1) + |#m #H normalize @Hind @H + ] + ] +qed. + + +(*************************** More list operations *****************************) + +(* We conclude this section discussing another important operation over lists, +namely the reverse funtion, retrurning a list with the same elements of the +original list but in reverse order. + +One could define the revert operation as follows: *) + +let rec rev A (l1: list A) on l1 ≝ match l1 with - [ nil ⇒ nil + [ nil ⇒ nil ? | cons a tl ⇒ rev A tl @ [a] ]. -\end{lstlisting} -However, this implementation is sligtly inefficient, since it has a -quadratic complexity. -A better solution consists in exploiting an accumulator, passing through -the following auxilary function: -\begin{lstlisting}[language=grafite] -let rec rev_append S (l1,l2:list S) on l1 ≝ + +(* However, this implementation is sligtly inefficient, since it has a quadratic +complexity. A better solution consists in exploiting an accumulator, passing +through the following auxilary function: *) + +let rec rev_append A (l1,l2:list A) on l1 ≝ match l1 with [ nil ⇒ l2 - | cons a tl ⇒ rev_append S tl (a::l2) + | cons a tl ⇒ rev_append A tl (a::l2) ]. definition reverse ≝λS.λl.rev_append S l []. -\end{lstlisting} -{\bf Exercise} Prove the following results: -\begin{lstlisting}[language=grafite] -lemma reverse_cons : ∀S,a,l. reverse S (a::l) = (reverse S l)@[a]. +lemma reverse_single : ∀S,a. reverse S [a] = [a]. +// qed. + +example example_rev1: reverse ? [true;false] = [false;true]. +normalize // qed. + +(* Let us prove the following results, as a simple exercise. + +lemma reverse_cons : ∀A,a,l. reverse A (a::l) = (reverse A l)@[a]. + +If you try a brute force approach (e.g., induction on l); you will get in +trouble. The point is that reverse is defined as a particular case of +rev_append, and you should suitably generalize your result taking rev_append in +mind. +*) + +lemma rev_append_append: ∀A,l1,l2,l3. + rev_append A l1 (l2@l3) = rev_append A l1 l2 @l3. +#A #l1 elim l1 // +#hd #tl normalize #Hind #l2 #l3 @(Hind (hd::l2)) qed. + +(* Now we get reverse_cons as a trivial corollary, since + reverse A (a::l) = rev_append A (a::l) [ ] = rev_append l [a] = + rev_append l ([ ]@[a]) = (rev_append l [ ])@[a] = reverse A l @ [a] +*) + +lemma reverse_cons : ∀A,a,l. reverse A (a::l) = reverse A l@[a]. +#A #a #l normalize reverse_cons +>reverse_cons >Hind >associative_append // +qed. lemma reverse_reverse : ∀S,l. reverse S (reverse S l) = l. -\end{lstlisting} +#S #l elim l // #a #tl #Hind >reverse_cons >reverse_append +>reverse_single >Hind // qed. -\subsection{List iterators} -In general, an iterator for some data type is an object that enables to +(***************************** List iterators *********************************) + +(* In general, an iterator for some data type is an object that enables to traverse its structure performing a given computation. -There is a canonical set of iterators over lists deriving from -the programming experience. In this section we shall review a few of -them, proving some of their properties. - -A first, famous iterator is the map function, that -applies a function $f$ to each element of a list $[a_1,\dots , a_n]$, -building the list $[f\,a_1; \dots ; f\,a_n]$. -\begin{lstlisting}[language=grafite] +There is a canonical set of iterators over lists deriving from the programming +experience. In this section we shall review a few of them, proving some of their +properties. + +A first, famous iterator is the map function, that applies a function f to each +element of a list [a1,…, an], building the list [f a1; … ; f an]. *) + let rec map (A,B:Type[0]) (f: A → B) (l:list A) on l: list B ≝ match l with [ nil ⇒ nil ? | cons x tl ⇒ f x :: (map A B f tl)]. -\end{lstlisting} -The \verb+map+ function distributes over \verb+append+, as can be simply -proved by induction over the first list: -\begin{lstlisting}[language=grafite] + +(* The map function distributes over append, as can be simply proved by +induction over the first list: *) + lemma map_append : ∀A,B,f,l1,l2. (map A B f l1) @ (map A B f l2) = map A B f (l1@l2). #A #B #f #l1 elim l1 - [ #l2 @refl | #h #t #IH #l2 normalize // ] qed. -\end{lstlisting} -The most important itarator is traditionally called {\em fold}; we -shall only consider the so called fold-right variant, -that takes in input a function $f:A\to B \to B$, a list $[a_1; \dots; a_n]$ -of elements of type $A$, a base element $b:B$ and returns -the value $f\,a_1\,(f\,a_2\,(\dots (f\,a_n\,b) \dots))$. -\begin{lstlisting}[language=grafite] + [ #l2 @refl | #h #t #IH #l2 normalize >IH // ] qed. + +lemma length_map: ∀A,B,l.∀f:A→B. length ? (map ?? f l) = length ? l. +#A #B #l #f elim l // #a #tl #Hind normalize // +qed. + +(* The most important iterator is traditionally called "fold"; we shall only +consider the so called fold-right variant, that takes in input a function +f:A→B→B, a list [a1; …; an] of elements of type A, a base element b:B and +returns the value f a1 (f a2 (… (f an b) …)). *) + let rec foldr (A,B:Type[0]) (f:A → B → B) (b:B) (l:list A) on l :B ≝ match l with [ nil ⇒ b | cons a l ⇒ f a (foldr A B f b l)]. -\end{lstlisting} -Many other interesting functions can be defined in terms of \verb+foldr+. -A first interesting example is the filter function, taking in input -a boolean test \verb+p+ and a list $l$ and returning the sublist of all -elements of $l$ satisfying the test. -\begin{lstlisting}[language=grafite] + +(* Many other interesting functions can be defined in terms of foldr. A first +interesting example is the filter function, taking in input a boolean test p and +a list l and returning the sublist of all elements of l satisfying the test. *) + definition filter ≝ λT.λp:T → bool. foldr T (list T) (λx,l0.if p x then x::l0 else l0) (nil T). -\end{lstlisting} -As another example, we can generalize the map function to an operation -taking in input a binary function $f:A\to B \to C$, two lists -$[a_1;\dots ;a_n]$ and $[b_1;\dots ;b_m]$ and returning the list -$[f\,a_1\,b_1; \dots ;f\,a_n\,b_1;\dots ;f\,a_1\,b_m; f\,a_n\,b_m]$ -\begin{lstlisting}[language=grafite] + +(* As another example, we can generalize the map function to an operation taking +in input a binary function f:A → B → C, two lists [a1;… ;an] and [b1;… ;bm] and +returning the list [f a1 b1; ˙… ;f an b1;… ;f a1 b_m; … f an bm]. *) + definition compose ≝ λA,B,C.λf:A→B→C.λl1,l2. foldr ?? (λi,acc.(map ?? (f i) l2)@acc) [ ] l1. -\end{lstlisting} -The folded function $\lambda$\verb+i,acc.(map ?? (f i) l2)@acc+ -takes in input an element $i$ and an accumulator, -and add to the accumulator the values obtained by mapping the -partial instantiation $f\,i$ on the elements of $l_2$. This function -is iterated over -all elements of the first list $l_1$, starting with an empty accumulator. - -\subsection{Naive Set Theory} -Given a ``universe'' $U$ (an arbitrary type $U:Type$), a naive but -practical way to deal with ``sets'' in $U$ is simply to identify -them with their characteristic property, that is to as functions -of type $U\to \mbox{Prop}$. - -For instance, the empty set is defined by the False predicate; -a singleton set $\{x\}$ is defined by the property that its elements are -equal to $x$. - -\begin{lstlisting}[language=grafite] -definition empty_set ≝ λU:Type[0].λu:U.False. -definition singleton ≝ λU.λx,u:U.x=u. -\end{lstlisting} - -The membership relation is trivial: an element $x$ is in the set -(defined by the property) $P$ if and only if it enjoyes the property: - -\begin{lstlisting}[language=grafite] -definition member ≝ λU:Type[0].λu:U.P→Prop:U.P u. -\end{lstlisting} -The operations of union, intersection, complementation and substraction -are defined in a straightforward way, in terms of logical operations: - -\begin{lstlisting}[language=grafite] -definition union ≝ λU:Type[0].λP,Q:U → Prop.λa.P a ∨ Q a. - -definition intersection ≝ λU:Type[0].λP,Q:U → Prop.λa..P a ∧ Q a. - -definition complement ≝ λU:Type[0].λA:U → Prop.λw.¬ A w. - -definition substraction ≝ λU:Type[0].λA,B:U → Prop.λw.A w ∧ ¬ B w. -\end{lstlisting} -More interesting are the notions of subset and equality. Given -two sets $P$ and $Q$, $P$ is a subset of $Q$ when any element $u$ in -$P$ is also in $Q$, that is when $P\,u$ implies $Q\,u$. -\begin{lstlisting}[language=grafite] -definition subset: ∀A:Type[0].∀P,Q:A→Prop.Prop ≝ λA,P,Q.∀a:A.(P a → Q a). -\end{lstlisting} -Then, two sets $P$ and $Q$ are equal when $P \subseteq Q$ and -$Q \subseteq P$, or equivalently when for any element $u$, -$P\,u \iff Q\,u$. -\begin{lstlisting}[language=grafite] -definition eqP ≝ λA:Type.λP,Q:A → Prop.∀a:A.P a ↔ Q a. -\end{lstlisting} -We shall use the infix notation $\approx$ for the previous notion of -equality. -It is important to observe that the \verb+eqP+ is -different from Leibniz equality of section \ref{}. As we already -observed, Leibniz equality is a pretty syntactical (or intensional) -notion, that is a notion concerning the {\em connotation} of an object -and not its {\em denotation} (the shape assumed by the object, and -not the information it is supposed to convey). Intensionality stands -in contrast with {\em extensionality}, referring to principles that -judge objects to be equal if they enjoy {\em a given subset} of external, -observable properties (e.g. the property of having the same -elements). For instance given two sets $A$ and $B$ we can prove that -$A\cup B \approx B\cup A$, since they have the same elements, but -there is no way to prove $A\cup B = B\cup A$. - -The main practical consequence is that, while we can always exploit -a Leibniz equality between two terms $t_1$ and $t_2$ for rewriting -one into the other (in fact, this is the {\em essence} of Leibniz -equality), we cannot do the same for an extensional equality (we -could only rewrite inside propositions ``compatible'' with our -external observation of the objects). - -\subsection{Sets with decidable equality} -We say that a property $P:A\to Prop$ over a datatype $A$ -is {\em decidable} when we have an -effective way to assess the validity of $P\,a$ for any -$a:A$. As a consequence -of G\"odel incompleteness theorem, not every predicate -is decidable: for instance, extensional equality on sets is not decidable, -in general. - -Decidability can be expressed in several possible ways. A convenient -one is to state it in terms of the computability of the characterisitc -function of the predicate $P$, that is in terms of the existence of a -function $Pb: A \to \mbox{bool}$ such that - \[P\,a \iff Pb\,a = \mbox{true}\] -Decidability is an important issue, and since equality is an essential -predicate, it is always interesting to try to understand when a given -notion of equality is decidable or not. - -In particular, Leibniz equality on inductively generated datastructures -is often decidable, since we can simply write a decision algorithm by -structural induction on the terms. For instance we can define -characteristic functions for booleans and natural numbers in the following -way: -\begin{lstlisting}[language=grafite] -definition beqb ≝ λb1,b2. - match b1 with [ true ⇒ b2 | false ⇒ notb b2]. - -let rec neqb n m ≝ -match n with - [ O ⇒ match m with [ O ⇒ true | S q ⇒ false] - | S p ⇒ match m with [ O ⇒ false | S q ⇒ neqb p q] - ]. -\end{lstlisting} -It is so important to know if Leibniz equality for a given type is decidable -that turns out to be convenient to pack this information into a single -algebraic datastructure, called \verb+DeqSet+: -\begin{lstlisting}[language=grafite] -record DeqSet : Type[1] ≝ - { carr :> Type[0]; - eqb: carr → carr → bool; - eqb_true: ∀x,y. (eqb x y = true) ↔ (x = y)}. - -notation "a == b" non associative with precedence 45 for @{ 'eqb $a $b }. -interpretation "eqb" 'eqb a b = (eqb ? a b). -\end{lstlisting} -A \verb+DeqSet+ is simply a record composed by a carrier type \verb+carr+, -a boolean function \verb+eqb: carr+$\to$\verb+carr+$\to$\verb+carr+ representing -the decision algorithm, and a {\em proof} \verb+eqb_true+ that the decision algorithm -is correct. The \verb+:>+ symbol declares \verb+carr+ as a {\em coercion} from a DeqSet to its -carrier type. We use the infix notation ``=='' for the decidable -equality \verb+eqb+ of the carrier. - -Suppose we proved the following facts (do it as an exercise) -\begin{lstlisting}[language=grafite] -lemma beqb_true_to_eq: ∀b1,b2. beqb b1 b2 = true ↔ b1 = b2. -lemma neqb_true_to_eq: ∀n,m:nat. eqb n m = true → n = m. -\end{lstlisting} -Then, we can build the following records: -\begin{lstlisting}[language=grafite] -definition DeqBool ≝ mk_DeqSet bool beqb beqb_true_to_eq. -definition DeqNat ≝ mk_DeqSet nat eqb eqbnat_true. -\end{lstlisting} -Note that, since we declare a coercion from the \verb+DeqSet+ to its -carrier, the expression \verb+0:DeqNat+ is well typed, and it is understood -by the system as \verb+0:carr DeqNat+ (that is, coercions are automatically -insterted by the system, if required). - -%It is convenient to have a simple way to {\em reflect} \cite{ssreflect} -%a proof of -%$(eqb\;x\;y = true)$ into a proof of $(x = y)$; we use the two operators -%$\mathit{\\P}$ and $\mathit{\\b}$ to this aim. - -\subsection{Unification hints} -Suppose now to write an expression of the following kind: -\[b == \mbox{false}\] -that, after removing the notation, is equivalent to -\[eqb\;?\;b\;\mbox{false}\] -The system knows that $\mbox{false}$ is a boolean, so in order to -accept the expression, he should {\em figure out} some \verb+DeqSet+ -having \verb+bool+ -as carrier. This is not a trivial operation: Matita should either try -to synthetize it (that is a complex operation known as {\em narrowing}) -or look into its database of results for a possible solution. - -In this situations, we may suggest the intended solution to Matita using -the mechanism of unification hints \cite{hints}. The concrete syntax -of unification hints is a bit involved: we strongly recommend the user -to include the file \verb+hints_declaration.ma+ that allows you -to write thing in a more convenient and readable way. -\begin{lstlisting}[language=grafite] -include ``hints_declaration.ma''. -\end{lstlisting} -For instance, the following declaration tells Matita that a solution -of the equation \verb+bool = carr X+ is $X = DeqBool$. -\begin{lstlisting}[language=grafite] -unification hint 0 ≔ ; - X ≟ DeqBool -(* ---------------------------------------- *) ⊢ - bool ≡ carr X. -\end{lstlisting} -Using the previous notation (we suggest the reader to cut and paste it -from previous hints) the hint is expressed as an inference rule. -The conclusion of the rule is the unification problem that we intend to solve, -containing one or more variables $X_1,\dots X_b$. The premises of -the rule are the solutions we are suggesting to Matita. In general, -unification hints should only be used when there exists just one -``intended'' (canonical) solution for the given equation. -When you declare a unification hint, Matita verifies it correctness by -instantiating the unification problem with the hinted solution, -and checking the convertibility between the two sides of the equation. -\begin{lstlisting}[language=grafite] -example exhint: ∀b:bool. (b == false) = true → b = false. -#b #H @(\P H). -qed. -\end{lstlisting} -In a similar way, - -\begin{lstlisting}[language=grafite] -unification hint 0 ≔ b1,b2:bool; - X ≟ mk_DeqSet bool beqb beqb_true -(* ---------------------------------------- *) ⊢ - beqb b1 b2 ≡ eqb X b1 b2. -\end{lstlisting} - - -\subsection{Prop vs. bool} -It is probably time to make a discussion about \verb+Prop+ and \verb+bool+, and -their different roles in a the Calculus of Inductive Constructions. - -Inhabitants of the sort \verb+Prop+ are logical propositions. In turn, logical -propositions \verb+P:Prop+ can be inhabitated by their proofs $H:P$. Since, in -general, the validity of a property $P$is not decidable, the role of the -proof is to provide a witness of the correctness of $P$ that the system can -automatically check. - -On the other hand, bool is just an inductive datatype with two constructors true -and false: these are terms, not types, and cannot be inhabited. -Logical connectives on bool are computable functions, defined by their -truth tables, using case analysis. - - Prop and bool are, in a sense, complementary: the former is more suited for -abstract logical reasoning, -while the latter allows, in some situations, for brute-force evaluation. -Suppose for instance that we wish to prove that the $2 \le 3!$. Starting -from the definition of the factorial function and properties of the less -or equal relation, the previous proof could take several steps. Suppose -however we proved the decidability of $\le$, that is the existence of -a boolean function $\mbox{leb}$ reflecting $\le$ in the sense that -\[n \le m \iff \mbox{leb}\,n,m = \mbox{true}\] -Then, we could reduce the verification of $2 \le 3!$ to that of -of $\mbox{leb}\,2,3! = \mbox{true}$ that just requires a mere computation! - -\subsection{Finite Sets} -A finite set is a record consisting of a DeqSet $A$, -a list of elements of type A enumerating all the elements of the set, -and the proofs that the enumeration does not contain repetitions -and is complete (\verb+memb+ is the membership operation on -lists, defined in the obvious way, and the question mark is an {\em -implicit parameter} automatically filled in by the system). -\begin{lstlisting}[language=grafite] -record FinSet : ≝ -{ FinSetcarr:> DeqSet; - enum: list FinSetcarr; - enum_unique: uniqueb FinSetcarr enum = true; - enum_complete : ∀x:FinSetcarr. memb ? x enum = true}. -\end{lstlisting} -The library provides many operations for building new \verb+FinSet+s by -composing -existing ones: for example, -if \verb+A+ and \verb+B+ have type \verb+FinSet+, then -also \verb+option A+, \verb+A+$\times$\verb+B+, -\verb+A+$\oplus$\verb+B+ are finite sets. In all these cases, unification -hints are used to suggest the {\em intended} finite set structure -associated with them, that makes their use quite transparent to the user. - -A particularly intersting case is that of the arrow type \verb+A+$\to$\verb+B+. -We may define the graph of \verb+f:A+$\to$\verb+B+, as the -set (sigma type) of all pairs $\langle a,b \rangle$ such that -$f (a) = b$. -\begin{lstlisting}[language=grafite] -definition graph_of ≝ λA,B.λf:A→B. Σp:A×B.f (\fst p) = \snd p. -\end{lstlisting} -In case the equality is decidable, we may effectively -enumerate all elements of the graph by simply filtering from -pairs in \verb+A+$\times$\verb+B+ those satisfying the -test $\lambda$\verb+p.f (\fst p) == \snd p)+: - -\begin{lstlisting}[language=grafite] -definition graph_enum ≝ λA,B:FinSet.λf:A→B. - filter ? (λp.f (\fst p) == \snd p) (enum (FinProd A B)). -\end{lstlisting} -The proofs that this enumeration does not contain repetitions and -is complete are straightforward. - -\subsection{Vectors} -A vector of length $n$ of elements of type $A$ -is simply defined in Matita as a record composed -by a list of elements of type $A$, plus a proof that the -list has the expected length. Vectors are a paradigmatic example -of {\em dependent} type, that is of a type whose definition depends on -a term. -\begin{lstlisting}[language=grafite] -record Vector (A:Type) (n:nat): Type ≝ + +(* The folded function + λi,acc.(map ?? (f i) l2)@acc +takes in input an element i and an accumulator, and add to the accumulator the +values obtained by mapping the partial instantiation (f i) on the elements of +l2. This function is iterated over all elements of the first list l1, starting +with an empty accumulator. *) + +(************************************ Vectors *********************************) + +(* A vector of length n of elements of type A is simply defined in Matita as a +record composed by a list of elements of type A, plus a proof that the list has +the expected length. Vectors are a paradigmatic example of dependent type, that +is of a type whose definition depends on a term. *) + +record Vector (A:Type[0]) (n:nat): Type[0] ≝ { vec :> list A; len: length ? vec = n }. -\end{lstlisting} -Given a list $l$ we may trivially turn it into a vector of length $|l|$; -we just need to prove that $|l|=|l|$ that follows from the reflexivity -of equality. -\begin{lstlisting}[language=grafite] + +(* Given a list l we may trivially turn it into a vector of length |l|; we just +need to prove that |l|=|l| that follows from the reflexivity of equality. *) + lemma Vector_of_list ≝ λA,l.mk_Vector A (|l|) l (refl ??). -\end{lstlisting} - -Most functions operating on lists can be naturally extended to -vectors: interesting cases are \verb+vec_append+, concatenating vectors, -and \verb+vec_map+, mapping a function $f$ on all elements of the input -vector and returning a vector of the same dimension of the input one. - -Since a vector is automatically coerced, if needed, to the list of -its elements, we may simply use typical functions over lists (such as -\verb+nth+) to extract/filter specific components. - -The function \verb+change_vec A n v a i+ replaces the content of -the vector $v$ at position $i$ with the value $a$. - -The most frequent operation on vectors for the purposes or our work -is their comparison. In this case, we have essentially two possible -approaches: we may proceed component-wise, using the following lemma -\begin{lstlisting}[language=grafite] -lemma eq_vec: ∀A,n.∀v1,v2:Vector A n.∀d. - (∀i. i < n → nth i A v1 d = nth i A v2 d) → v1 = v2. -\end{lstlisting} -or alternatively we may manipulate vectors exploiting the commutation -or idempotency of \verb+change_vec+ and its interplay with -other operations. + +(* Then we can prove that any vector of zero lenght has no elements: *) + +lemma vector_nil: ∀A.∀v:Vector A 0. + v = Vector_of_list A [ ]. +#A * * // #a #tl normalize #H destruct +qed. + +(* It is convenient to re-define on vectors the hd, tail and cons operations +on lists *) + +definition vec_tail ≝ λA.λn.λv:Vector A n. + mk_Vector A (pred n) (tail A v) ?. +>length_tail >(len A n v) // +qed. + +definition vec_cons ≝ λA.λa.λn.λv:Vector A n. + mk_Vector A (S n) (cons A a v) ?. +normalize >(len A n v) // +qed. + +definition vec_hd ≝ λA.λn.λv:Vector A (S n). hd A v ?. +elim v * [normalize #H destruct | #a #H #eq @a] +qed. + +(* Any vector of lenght (S n) can be expanded as a concatenation of a head and a +tail vector of length n *) + +lemma vec_expand: ∀A,n,v. + v = vec_cons A (vec_hd A n v) n (vec_tail A (S n) v). +#A #n * #l cases l [normalize in ⊢ (%→?); #H destruct |//] +qed. + +(* Most functions operating on lists can be naturally extended to vectors: +interesting cases are vec_append, concatenating vectors, and vec_map, mapping a +function f on all elements of the input vector and returning a vector of the +same dimension of the input one. *) + +definition vec_append ≝ λA.λn1,n2.λv1:Vector A n1.λv2: Vector A n2. +mk_Vector A (n1+n2) (v1@v2) ?. +>length_append >(len … v1) >(len … v2) // qed. + +definition vec_map ≝ λA,B.λf:A→B.λn.λv:Vector A n. +mk_Vector B n (map ?? f v) + (trans_eq … (length_map …) (len A n v)). + +(* Since a vector is automatically coerced, if needed, to the list of its +elements, we may simply use typical functions over lists (such as nth) to +extract/filter specific components. + +The following function (change_vec A n v a i) replaces the content of the vector +v at position i with the value a. *) + +let rec change_vec (A:Type[0]) (n:nat) on n ≝ +match n return λn0.∀v:Vector A n0.A→nat→Vector A n0 with +[ O ⇒ λv,a,i.v +| S m ⇒ λv,a,i. + match i with + [ O ⇒ vec_cons A a m (vec_tail … v) + | S j ⇒ vec_cons A (vec_hd A m v) m (change_vec A m (vec_tail … v) a j) + ] +]. + +(* A frequent operation between vectors is their comparison. The following +lemma allow us to reduce the comparisons of vectors of a same lenght to the +comparison of their components. *) + +lemma eq_vec: ∀A,n.∀v1,v2:Vector A n. + (∀i. i < n → nth A v1 i = nth A v2 i) → v1 = v2. +#A #n elim n -n + [#v1 #v2 #_ >(vector_nil A v1) >(vector_nil A v2) // + |#n #Hind #v1 #v2 #H >(vec_expand … v1) >(vec_expand … v2) + >(Hind (vec_tail … v1) (vec_tail … v2)) + [cut (vec_hd A n v1 = vec_hd A n v2) // lapply (H 0 (lt_O_S ?)) -H + >(vec_expand … v1) in ⊢ (%→?); >(vec_expand … v2) in ⊢ (%→?); + change with (Some ?? = Some ?? → ?) #H destruct (H) @e0 + |#i #ltin @(H (S i)) @le_S_S // + ] + ] +qed. +