More Data Types
*)
-include "basics/logic.ma".
+include "tutorial/chapter4.ma".
+include "arithmetics/nat.ma".
+
(******************************** Option Type *********************************)
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 <rev_append_append % qed.
+
+(* More generally, we can prove the following property of rev_append
+specyfing its general behaviour *)
+
+lemma rev_append_def : ∀S,l1,l2.
+ rev_append S l1 l2 = (reverse S l1) @ l2 .
+#S #l1 #l2 normalize <rev_append_append //
+qed.
lemma reverse_append: ∀S,l1,l2.
reverse S (l1 @ l2) = (reverse S l2)@(reverse S l1).
+#S #l1 elim l1 [normalize // | #a #tl #Hind #l2 >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.
+
projects / helm.git / blobdiff