-\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 ≝