diff options
| -rw-r--r-- | Makefile.doc | 4 | ||||
| -rw-r--r-- | doc/refman/CanonicalStructures.tex | 383 | ||||
| -rw-r--r-- | doc/refman/Cases.tex | 843 | ||||
| -rw-r--r-- | doc/refman/Omega.tex | 249 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/canonical-structures.rst | 435 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 611 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 184 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 2 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 3 |
10 files changed, 1236 insertions, 1481 deletions
diff --git a/Makefile.doc b/Makefile.doc index 940a3ebd7..4a247f1d9 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,8 +60,8 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ - Program.v.tex Omega.v.tex Polynom.v.tex Nsatz.v.tex \ + Coercion.v.tex Extraction.v.tex \ + Program.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex deleted file mode 100644 index 8961b0096..000000000 --- a/doc/refman/CanonicalStructures.tex +++ /dev/null @@ -1,383 +0,0 @@ -\achapter{Canonical Structures} -%HEVEA\cutname{canonical-structures.html} -\aauthor{Assia Mahboubi and Enrico Tassi} - -\label{CS-full} -\index{Canonical Structures!presentation} - -\noindent This chapter explains the basics of Canonical Structure and how they can be used -to overload notations and build a hierarchy of algebraic structures. -The examples are taken from~\cite{CSwcu}. We invite the interested reader -to refer to this paper for all the details that are omitted here for brevity. -The interested reader shall also find in~\cite{CSlessadhoc} a detailed -description of another, complementary, use of Canonical Structures: -advanced proof search. This latter papers also presents many techniques one -can employ to tune the inference of Canonical Structures. - -\section{Notation overloading} - -We build an infix notation $==$ for a comparison predicate. Such notation -will be overloaded, and its meaning will depend on the types of the terms -that are compared. - -\begin{coq_eval} -Require Import Arith. -\end{coq_eval} - -\begin{coq_example} -Module EQ. - Record class (T : Type) := Class { cmp : T -> T -> Prop }. - Structure type := Pack { obj : Type; class_of : class obj }. - Definition op (e : type) : obj e -> obj e -> Prop := - let 'Pack _ (Class _ the_cmp) := e in the_cmp. - Check op. - Arguments op {e} x y : simpl never. - Arguments Class {T} cmp. - Module theory. - Notation "x == y" := (op x y) (at level 70). - End theory. -End EQ. -\end{coq_example} - -We use Coq modules as name spaces. This allows us to follow the same pattern -and naming convention for the rest of the chapter. The base name space -contains the definitions of the algebraic structure. To keep the example -small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic, -and characterizes terms on which a binary relation is defined, without -requiring such relation to validate any property. -The inner \texttt{theory} module contains the overloaded notation \texttt{==} and -will eventually contain lemmas holding on all the instances of the -algebraic structure (in this case there are no lemmas). - -Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion, -but we will not do that here. - -The following line tests that, when we assume a type \texttt{e} that is in the -\texttt{EQ} class, then we can relates two of its objects with \texttt{==}. - -\begin{coq_example} -Import EQ.theory. -Check forall (e : EQ.type) (a b : EQ.obj e), a == b. -\end{coq_example} - -Still, no concrete type is in the \texttt{EQ} class. We amend that by equipping \texttt{nat} -with a comparison relation. - -\begin{coq_example} -Fail Check 3 == 3. -Definition nat_eq (x y : nat) := nat_compare x y = Eq. -Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq. -Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl. -Check 3 == 3. -Eval compute in 3 == 4. -\end{coq_example} - -This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but -also that the infix relation was bound to the \texttt{nat\_eq} relation. This -relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}. This -can be read in the line declaring the canonical structure \texttt{nat\_EQty}, -where the first argument to \texttt{Pack} is the key and its second argument -a group of canonical values associated to the key. In this case we associate -to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one -member). The use of the projection \texttt{op} requires its argument to be in -the class \texttt{EQ}, and uses such a member (function) to actually compare -its arguments. - -Similarly, we could equip any other type with a comparison relation, and -use the \texttt{==} notation on terms of this type. - -\subsection{Derived Canonical Structures} - -We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}. -Here we show how to deal with type constructors, i.e. how to make the -following example work: - -\begin{coq_example} -Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). -\end{coq_example} - -The error message is telling that Coq has no idea on how to compare -pairs of objects. The following construction is telling Coq exactly how to do -that. - -\begin{coq_example} -Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := - fst x == fst y /\ snd x == snd y. -Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2). -Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type := - EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2). -Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). -Check forall n m : nat, (3,4) == (n,m). -\end{coq_example} - -Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison -relation for pairs whenever it is able to build a comparison relation -for each component of the pair. The declaration associates to the key -\texttt{*} (the type constructor of pairs) the canonical comparison relation -\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types -being themselves in the \texttt{EQ} class. - -\section{Hierarchy of structures} - -To get to an interesting example we need another base class to be available. -We choose the class of types that are equipped with an order relation, -to which we associate the infix \texttt{<=} notation. - -\begin{coq_example} -Module LE. - Record class T := Class { cmp : T -> T -> Prop }. - Structure type := Pack { obj : Type; class_of : class obj }. - Definition op (e : type) : obj e -> obj e -> Prop := - let 'Pack _ (Class _ f) := e in f. - Arguments op {_} x y : simpl never. - Arguments Class {T} cmp. - Module theory. - Notation "x <= y" := (op x y) (at level 70). - End theory. -End LE. -\end{coq_example} - -As before we register a canonical \texttt{LE} class for \texttt{nat}. - -\begin{coq_example} -Import LE.theory. -Definition nat_le x y := nat_compare x y <> Gt. -Definition nat_LEcl : LE.class nat := LE.Class nat_le. -Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl. -\end{coq_example} - -And we enable Coq to relate pair of terms with \texttt{<=}. - -\begin{coq_example} -Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) := - fst x <= fst y /\ snd x <= snd y. -Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2). -Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type := - LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2). -Check (3,4,5) <= (3,4,5). -\end{coq_example} - -At the current stage we can use \texttt{==} and \texttt{<=} on concrete types, -like tuples of natural numbers, but we can't develop an algebraic -theory over the types that are equipped with both relations. - -\begin{coq_example} -Check 2 <= 3 /\ 2 == 2. -Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y. -Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y. -\end{coq_example} - -We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}. - -\begin{coq_example} -Module LEQ. - Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) := - Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }. - Record class T := Class { - EQ_class : EQ.class T; - LE_class : LE.class T; - extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; class_of : class obj }. - Arguments Mixin {e le} _. - Arguments Class {T} _ _ _. -\end{coq_example} - -The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content -we are adding to \texttt{EQ} and \texttt{LE}. In particular it contains the requirement -that the two relations we are combining are compatible. - -Unfortunately there is still an obstacle to developing the algebraic theory -of this new class. - -\begin{coq_example} - Module theory. - Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m. -\end{coq_example} - -The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by -a subclass relation. In other words Coq does not see that an object -of the \texttt{LEQ} class is also an object of the \texttt{LE} class. - -The following two constructions tell Coq how to canonically build -the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure -on the same type. - -\begin{coq_example} - Definition to_EQ (e : type) : EQ.type := - EQ.Pack (obj e) (EQ_class _ (class_of e)). - Canonical Structure to_EQ. - Definition to_LE (e : type) : LE.type := - LE.Pack (obj e) (LE_class _ (class_of e)). - Canonical Structure to_LE. -\end{coq_example} -We can now formulate out first theorem on the objects of the \texttt{LEQ} structure. -\begin{coq_example} - Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y. - now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed. - Arguments lele_eq {e} x y _ _. - End theory. -End LEQ. -Import LEQ.theory. -Check lele_eq. -\end{coq_example} - -Of course one would like to apply results proved in the algebraic -setting to any concrete instate of the algebraic structure. - -\begin{coq_example} -Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. - Fail apply (lele_eq n m). Abort. -Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : - n <= m -> m <= n -> n == m. - Fail apply (lele_eq n m). Abort. -\end{coq_example} - -Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how -the type constructor \texttt{*} interacts with the \texttt{LEQ} class. In the following -proofs are omitted for brevity. - -\begin{coq_example} -Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m. -\end{coq_example} -\begin{coq_eval} - -split. - unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq. - case (nat_compare_spec n m); [ reflexivity | | now intros _ [H _]; case H ]. - now intro H; apply nat_compare_gt in H; rewrite -> H; intros [_ K]; case K. -unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq. -case (nat_compare_spec n m); [ | intros H1 H2; discriminate H2 .. ]. -intro H; rewrite H; intros _; split; [ intro H1; discriminate H1 | ]. -case (nat_compare_eq_iff m m); intros _ H1. -now rewrite H1; auto; intro H2; discriminate H2. -Qed. -\end{coq_eval} -\begin{coq_example} -Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat. -Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : -n <= m /\ m <= n <-> n == m. -\end{coq_example} -\begin{coq_eval} - -case n; case m; unfold EQ.op; unfold LE.op; simpl. -intros n1 n2 m1 m2; split; [ intros [[Le1 Le2] [Ge1 Ge2]] | intros [H1 H2] ]. - now split; apply lele_eq. -case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l1)) m1 n1). -case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l2)) m2 n2). -intros _ H3 _ H4; apply H3 in H2; apply H4 in H1; clear H3 H4. -now case H1; case H2; split; split. -Qed. -\end{coq_eval} -\begin{coq_example} -Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2). -\end{coq_example} - -The following script registers an \texttt{LEQ} class for \texttt{nat} and for the -type constructor \texttt{*}. It also tests that they work as expected. - -Unfortunately, these declarations are very verbose. In the following -subsection we show how to make these declaration more compact. - -\begin{coq_example} -Module Add_instance_attempt. - Canonical Structure nat_LEQty : LEQ.type := - LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx). - Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type := - LEQ._Pack (LEQ.obj l1 * LEQ.obj l2) - (LEQ.Class - (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2))) - (LE.class_of (pair_LEty (to_LE l1) (to_LE l2))) - (pair_LEQmx l1 l2)). - Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. - now apply (lele_eq n m). Qed. - Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m. - now apply (lele_eq n m). Qed. -End Add_instance_attempt. -\end{coq_example} - -Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the -user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}. What the user provides is a proof of -this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair -constructor preserves this property. The combination of these two facts is a -simple form of proof search that Coq performs automatically while inferring -canonical structures. - -\subsection{Compact declaration of Canonical Structures} - -We need some infrastructure for that. - -\begin{coq_example*} -Require Import Strings.String. -\end{coq_example*} -\begin{coq_example} -Module infrastructure. - Inductive phantom {T : Type} (t : T) : Type := Phantom. - Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := - phantom t1 -> phantom t2. - Definition id {T} {t : T} (x : phantom t) := x. - Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) - (at level 50, v ident, only parsing). - Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) - (at level 50, v ident, only parsing). - Notation "'Error : t : s" := (unify _ t (Some s)) - (at level 50, format "''Error' : t : s"). - Open Scope string_scope. -End infrastructure. -\end{coq_example} - -To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one -of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}. -It should be read as: ``find a class e such that its objects have type T -or fail with message "T is not an EQ.type"''. - -The other utilities are used to ask Coq to solve a specific unification -problem, that will in turn require the inference of some canonical -structures. They are explained in mode details in~\cite{CSwcu}. - -We now have all we need to create a compact ``packager'' to declare -instances of the \texttt{LEQ} class. - -\begin{coq_example} -Import infrastructure. -Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) := - [find e | EQ.obj e ~ T | "is not an EQ.type" ] - [find o | LE.obj o ~ T | "is not an LE.type" ] - [find ce | EQ.class_of e ~ ce ] - [find co | LE.class_of o ~ co ] - [find m | m ~ m0 | "is not the right mixin" ] - LEQ._Pack T (LEQ.Class ce co m). -Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id). -\end{coq_example} - -The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}. It infers all -the other pieces of the class \texttt{LEQ} and declares them as canonical values -associated to the \texttt{T} key. All in all, the only new piece of information -we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical -for \texttt{T} and hence can be inferred by Coq. - -\texttt{Pack} is a notation, hence it is not type checked at the time of its -declaration. It will be type checked when it is used, an in that case -\texttt{T} is going to be a concrete type. The odd arguments \texttt{\_} and \texttt{id} we -pass to the -packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference. Again, for all the details the -reader can refer to~\cite{CSwcu}. - -The declaration of canonical instances can now be way more compact: - -\begin{coq_example} -Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. -Canonical Structure pair_LEQty (l1 l2 : LEQ.type) := - Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2). -\end{coq_example} - -Error messages are also quite intelligible (if one skips to the end of -the message). - -\begin{coq_example} -Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx. -\end{coq_example} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex deleted file mode 100644 index 376ef031d..000000000 --- a/doc/refman/Cases.tex +++ /dev/null @@ -1,843 +0,0 @@ -\achapter{Extended pattern-matching} -%HEVEA\cutname{cases.html} -%BEGIN LATEX -\defaultheaders -%END LATEX -\aauthor{Cristina Cornes and Hugo Herbelin} - -\label{Mult-match-full} -\ttindex{Cases} -\index{ML-like patterns} - -This section describes the full form of pattern-matching in {\Coq} terms. - -\asection{Patterns}\label{implementation} The full syntax of {\tt -match} is presented in Figures~\ref{term-syntax} -and~\ref{term-syntax-aux}. Identifiers in patterns are either -constructor names or variables. Any identifier that is not the -constructor of an inductive or co-inductive type is considered to be a -variable. A variable name cannot occur more than once in a given -pattern. It is recommended to start variable names by a lowercase -letter. - -If a pattern has the form $(c~\vec{x})$ where $c$ is a constructor -symbol and $\vec{x}$ is a linear vector of (distinct) variables, it is -called {\em simple}: it is the kind of pattern recognized by the basic -version of {\tt match}. On the opposite, if it is a variable $x$ or -has the form $(c~\vec{p})$ with $p$ not only made of variables, the -pattern is called {\em nested}. - -A variable pattern matches any value, and the identifier is bound to -that value. The pattern ``\texttt{\_}'' (called ``don't care'' or -``wildcard'' symbol) also matches any value, but does not bind -anything. It may occur an arbitrary number of times in a -pattern. Alias patterns written \texttt{(}{\sl pattern} \texttt{as} -{\sl identifier}\texttt{)} are also accepted. This pattern matches the -same values as {\sl pattern} does and {\sl identifier} is bound to the -matched value. -A pattern of the form {\pattern}{\tt |}{\pattern} is called -disjunctive. A list of patterns separated with commas is also -considered as a pattern and is called {\em multiple pattern}. However -multiple patterns can only occur at the root of pattern-matching -equations. Disjunctions of {\em multiple pattern} are allowed though. - -Since extended {\tt match} expressions are compiled into the primitive -ones, the expressiveness of the theory remains the same. Once the -stage of parsing has finished only simple patterns remain. Re-nesting -of pattern is performed at printing time. An easy way to see the -result of the expansion is to toggle off the nesting performed at -printing (use here {\tt Set Printing Matching}), then by printing the term -with \texttt{Print} if the term is a constant, or using the command -\texttt{Check}. - -The extended \texttt{match} still accepts an optional {\em elimination -predicate} given after the keyword \texttt{return}. Given a pattern -matching expression, if all the right-hand-sides of \texttt{=>} ({\em -rhs} in short) have the same type, then this type can be sometimes -synthesized, and so we can omit the \texttt{return} part. Otherwise -the predicate after \texttt{return} has to be provided, like for the basic -\texttt{match}. - -Let us illustrate through examples the different aspects of extended -pattern matching. Consider for example the function that computes the -maximum of two natural numbers. We can write it in primitive syntax -by: - -\begin{coq_example} -Fixpoint max (n m:nat) {struct m} : nat := - match n with - | O => m - | S n' => match m with - | O => S n' - | S m' => S (max n' m') - end - end. -\end{coq_example} - -\paragraph{Multiple patterns} - -Using multiple patterns in the definition of {\tt max} lets us write: - -\begin{coq_eval} -Reset max. -\end{coq_eval} -\begin{coq_example} -Fixpoint max (n m:nat) {struct m} : nat := - match n, m with - | O, _ => m - | S n', O => S n' - | S n', S m' => S (max n' m') - end. -\end{coq_example} - -which will be compiled into the previous form. - -The pattern-matching compilation strategy examines patterns from left -to right. A \texttt{match} expression is generated {\bf only} when -there is at least one constructor in the column of patterns. E.g. the -following example does not build a \texttt{match} expression. - -\begin{coq_example} -Check (fun x:nat => match x return nat with - | y => y - end). -\end{coq_example} - -\paragraph{Aliasing subpatterns} - -We can also use ``\texttt{as} {\ident}'' to associate a name to a -sub-pattern: - -\begin{coq_eval} -Reset max. -\end{coq_eval} -\begin{coq_example} -Fixpoint max (n m:nat) {struct n} : nat := - match n, m with - | O, _ => m - | S n' as p, O => p - | S n', S m' => S (max n' m') - end. -\end{coq_example} - -\paragraph{Nested patterns} - -Here is now an example of nested patterns: - -\begin{coq_example} -Fixpoint even (n:nat) : bool := - match n with - | O => true - | S O => false - | S (S n') => even n' - end. -\end{coq_example} - -This is compiled into: - -\begin{coq_example} -Unset Printing Matching. -Print even. -\end{coq_example} -\begin{coq_eval} -Set Printing Matching. -\end{coq_eval} - -In the previous examples patterns do not conflict with, but -sometimes it is comfortable to write patterns that admit a non -trivial superposition. Consider -the boolean function \texttt{lef} that given two natural numbers -yields \texttt{true} if the first one is less or equal than the second -one and \texttt{false} otherwise. We can write it as follows: - -\begin{coq_example} -Fixpoint lef (n m:nat) {struct m} : bool := - match n, m with - | O, x => true - | x, O => false - | S n, S m => lef n m - end. -\end{coq_example} - -Note that the first and the second multiple pattern superpose because -the couple of values \texttt{O O} matches both. Thus, what is the result -of the function on those values? To eliminate ambiguity we use the -{\em textual priority rule}: we consider patterns ordered from top to -bottom, then a value is matched by the pattern at the $ith$ row if and -only if it is not matched by some pattern of a previous row. Thus in the -example, -\texttt{O O} is matched by the first pattern, and so \texttt{(lef O O)} -yields \texttt{true}. - -Another way to write this function is: - -\begin{coq_eval} -Reset lef. -\end{coq_eval} -\begin{coq_example} -Fixpoint lef (n m:nat) {struct m} : bool := - match n, m with - | O, x => true - | S n, S m => lef n m - | _, _ => false - end. -\end{coq_example} - -Here the last pattern superposes with the first two. Because -of the priority rule, the last pattern -will be used only for values that do not match neither the first nor -the second one. - -Terms with useless patterns are not accepted by the -system. Here is an example: -% Test failure: "This clause is redundant." -\begin{coq_eval} -Set Printing Depth 50. -\end{coq_eval} -\begin{coq_example} -Fail Check (fun x:nat => - match x with - | O => true - | S _ => false - | x => true - end). -\end{coq_example} - -\paragraph{Disjunctive patterns} - -Multiple patterns that share the same right-hand-side can be -factorized using the notation \nelist{\multpattern}{\tt |}. For instance, -{\tt max} can be rewritten as follows: - -\begin{coq_eval} -Reset max. -\end{coq_eval} -\begin{coq_example} -Fixpoint max (n m:nat) {struct m} : nat := - match n, m with - | S n', S m' => S (max n' m') - | 0, p | p, 0 => p - end. -\end{coq_example} - -Similarly, factorization of (non necessary multiple) patterns -that share the same variables is possible by using the notation -\nelist{\pattern}{\tt |}. Here is an example: - -\begin{coq_example} -Definition filter_2_4 (n:nat) : nat := - match n with - | 2 as m | 4 as m => m - | _ => 0 - end. -\end{coq_example} - -Here is another example using disjunctive subpatterns. - -\begin{coq_example} -Definition filter_some_square_corners (p:nat*nat) : nat*nat := - match p with - | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n) - | _ => (0,0) - end. -\end{coq_example} - -\asection{About patterns of parametric types} -\paragraph{Parameters in patterns} -When matching objects of a parametric type, parameters do not bind in patterns. -They must be substituted by ``\_''. -Consider for example the type of polymorphic lists: - -\begin{coq_example} -Inductive List (A:Set) : Set := - | nil : List A - | cons : A -> List A -> List A. -\end{coq_example} - -We can check the function {\em tail}: - -\begin{coq_example} -Check - (fun l:List nat => - match l with - | nil _ => nil nat - | cons _ _ l' => l' - end). -\end{coq_example} - - -When we use parameters in patterns there is an error message: -% Test failure: "The parameters do not bind in patterns." -\begin{coq_eval} -Set Printing Depth 50. -\end{coq_eval} -\begin{coq_example} -Fail Check - (fun l:List nat => - match l with - | nil A => nil nat - | cons A _ l' => l' - end). -\end{coq_example} - -The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns} -(off by default) removes parameters from constructors in patterns: -\begin{coq_example} - Set Asymmetric Patterns. - Check (fun l:List nat => - match l with - | nil => nil - | cons _ l' => l' - end) - Unset Asymmetric Patterns. -\end{coq_example} - -\paragraph{Implicit arguments in patterns} -By default, implicit arguments are omitted in patterns. So we write: - -\begin{coq_example} -Arguments nil [A]. -Arguments cons [A] _ _. -Check - (fun l:List nat => - match l with - | nil => nil - | cons _ l' => l' - end). -\end{coq_example} - -But the possibility to use all the arguments is given by ``{\tt @}'' implicit -explicitations (as for terms~\ref{Implicits-explicitation}). - -\begin{coq_example} -Check - (fun l:List nat => - match l with - | @nil _ => @nil nat - | @cons _ _ l' => l' - end). -\end{coq_example} - -\asection{Matching objects of dependent types} -The previous examples illustrate pattern matching on objects of -non-dependent types, but we can also -use the expansion strategy to destructure objects of dependent type. -Consider the type \texttt{listn} of lists of a certain length: -\label{listn} - -\begin{coq_example} -Inductive listn : nat -> Set := - | niln : listn 0 - | consn : forall n:nat, nat -> listn n -> listn (S n). -\end{coq_example} - -\asubsection{Understanding dependencies in patterns} -We can define the function \texttt{length} over \texttt{listn} by: - -\begin{coq_example} -Definition length (n:nat) (l:listn n) := n. -\end{coq_example} - -Just for illustrating pattern matching, -we can define it by case analysis: - -\begin{coq_eval} -Reset length. -\end{coq_eval} -\begin{coq_example} -Definition length (n:nat) (l:listn n) := - match l with - | niln => 0 - | consn n _ _ => S n - end. -\end{coq_example} - -We can understand the meaning of this definition using the -same notions of usual pattern matching. - -% -% Constraining of dependencies is not longer valid in V7 -% -\iffalse -Now suppose we split the second pattern of \texttt{length} into two -cases so to give an -alternative definition using nested patterns: -\begin{coq_example} -Definition length1 (n:nat) (l:listn n) := - match l with - | niln => 0 - | consn n _ niln => S n - | consn n _ (consn _ _ _) => S n - end. -\end{coq_example} - -It is obvious that \texttt{length1} is another version of -\texttt{length}. We can also give the following definition: -\begin{coq_example} -Definition length2 (n:nat) (l:listn n) := - match l with - | niln => 0 - | consn n _ niln => 1 - | consn n _ (consn m _ _) => S (S m) - end. -\end{coq_example} - -If we forget that \texttt{listn} is a dependent type and we read these -definitions using the usual semantics of pattern matching, we can conclude -that \texttt{length1} -and \texttt{length2} are different functions. -In fact, they are equivalent -because the pattern \texttt{niln} implies that \texttt{n} can only match -the value $0$ and analogously the pattern \texttt{consn} determines that \texttt{n} can -only match values of the form $(S~v)$ where $v$ is the value matched by -\texttt{m}. - -The converse is also true. If -we destructure the length value with the pattern \texttt{O} then the list -value should be $niln$. -Thus, the following term \texttt{length3} corresponds to the function -\texttt{length} but this time defined by case analysis on the dependencies instead of on the list: - -\begin{coq_example} -Definition length3 (n:nat) (l:listn n) := - match l with - | niln => 0 - | consn O _ _ => 1 - | consn (S n) _ _ => S (S n) - end. -\end{coq_example} - -When we have nested patterns of dependent types, the semantics of -pattern matching becomes a little more difficult because -the set of values that are matched by a sub-pattern may be conditioned by the -values matched by another sub-pattern. Dependent nested patterns are -somehow constrained patterns. -In the examples, the expansion of -\texttt{length1} and \texttt{length2} yields exactly the same term - but the -expansion of \texttt{length3} is completely different. \texttt{length1} and -\texttt{length2} are expanded into two nested case analysis on -\texttt{listn} while \texttt{length3} is expanded into a case analysis on -\texttt{listn} containing a case analysis on natural numbers inside. - - -In practice the user can think about the patterns as independent and -it is the expansion algorithm that cares to relate them. \\ -\fi -% -% -% - -\asubsection{When the elimination predicate must be provided} -\paragraph{Dependent pattern matching} -The examples given so far do not need an explicit elimination predicate - because all the rhs have the same type and the -strategy succeeds to synthesize it. -Unfortunately when dealing with dependent patterns it often happens -that we need to write cases where the type of the rhs are -different instances of the elimination predicate. -The function \texttt{concat} for \texttt{listn} -is an example where the branches have different type -and we need to provide the elimination predicate: - -\begin{coq_example} -Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : - listn (n + m) := - match l in listn n return listn (n + m) with - | niln => l' - | consn n' a y => consn (n' + m) a (concat n' y m l') - end. -\end{coq_example} -The elimination predicate is {\tt fun (n:nat) (l:listn n) => listn~(n+m)}. -In general if $m$ has type {\tt (}$I$ $q_1$ {\ldots} $q_r$ $t_1$ {\ldots} $t_s${\tt )} where -$q_1$, {\ldots}, $q_r$ are parameters, the elimination predicate should be of -the form~: -{\tt fun} $y_1$ {\ldots} $y_s$ $x${\tt :}($I$~$q_1$ {\ldots} $q_r$ $y_1$ {\ldots} - $y_s${\tt ) =>} $Q$. - -In the concrete syntax, it should be written~: -\[ \kw{match}~m~\kw{as}~x~\kw{in}~(I~\_~\mbox{\ldots}~\_~y_1~\mbox{\ldots}~y_s)~\kw{return}~Q~\kw{with}~\mbox{\ldots}~\kw{end}\] - -The variables which appear in the \kw{in} and \kw{as} clause are new -and bounded in the property $Q$ in the \kw{return} clause. The -parameters of the inductive definitions should not be mentioned and -are replaced by \kw{\_}. - -\paragraph{Multiple dependent pattern matching} -Recall that a list of patterns is also a pattern. So, when we destructure several -terms at the same time and the branches have different types we need to provide the -elimination predicate for this multiple pattern. It is done using the same -scheme, each term may be associated to an \kw{as} and \kw{in} clause in order to -introduce a dependent product. - -For example, an equivalent definition for \texttt{concat} (even though the -matching on the second term is trivial) would have been: - -\begin{coq_eval} -Reset concat. -\end{coq_eval} -\begin{coq_example} -Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : - listn (n + m) := - match l in listn n, l' return listn (n + m) with - | niln, x => x - | consn n' a y, x => consn (n' + m) a (concat n' y m x) - end. -\end{coq_example} - -Even without real matching over the second term, this construction can be used to -keep types linked. If {\tt a} and {\tt b} are two {\tt listn} of the same length, -by writing -\begin{coq_eval} - Unset Printing Matching. -\end{coq_eval} -\begin{coq_example} -Check (fun n (a b: listn n) => match a,b with - |niln,b0 => tt - |consn n' a y, bS => tt -end). -\end{coq_example} -\begin{coq_eval} - Set Printing Matching. -\end{coq_eval} - -I have a copy of {\tt b} in type {\tt listn 0} resp {\tt listn (S n')}. - -% Notice that this time, the predicate \texttt{[n,\_:nat](listn (plus n -% m))} is binary because we -% destructure both \texttt{l} and \texttt{l'} whose types have arity one. -% In general, if we destructure the terms $e_1\ldots e_n$ -% the predicate will be of arity $m$ where $m$ is the sum of the -% number of dependencies of the type of $e_1, e_2,\ldots e_n$ -% (the $\lambda$-abstractions -% should correspond from left to right to each dependent argument of the -% type of $e_1\ldots e_n$). -% When the arity of the predicate (i.e. number of abstractions) is not -% correct Coq raises an error message. For example: - -% % Test failure -% \begin{coq_eval} -% Reset concat. -% Set Printing Depth 50. -% (********** The following is not correct and should produce ***********) -% (** Error: the term l' has type listn m while it is expected to have **) -% (** type listn (?31 + ?32) **) -% \end{coq_eval} -% \begin{coq_example} -% Fixpoint concat -% (n:nat) (l:listn n) (m:nat) -% (l':listn m) {struct l} : listn (n + m) := -% match l, l' with -% | niln, x => x -% | consn n' a y, x => consn (n' + m) a (concat n' y m x) -% end. -% \end{coq_example} - -\paragraph{Patterns in {\tt in}} -\label{match-in-patterns} - -If the type of the matched term is more precise than an inductive applied to -variables, arguments of the inductive in the {\tt in} branch can be more -complicated patterns than a variable. - -Moreover, constructors whose type do not follow the same pattern will -become impossible branches. In an impossible branch, you can answer -anything but {\tt False\_rect unit} has the advantage to be subterm of -anything. % ??? - -To be concrete: the {\tt tail} function can be written: -\begin{coq_example} -Definition tail n (v: listn (S n)) := - match v in listn (S m) return listn m with - | niln => False_rect unit - | consn n' a y => y - end. -\end{coq_example} -and {\tt tail n v} will be subterm of {\tt v}. - -\asection{Using pattern matching to write proofs} -In all the previous examples the elimination predicate does not depend -on the object(s) matched. But it may depend and the typical case -is when we write a proof by induction or a function that yields an -object of dependent type. An example of proof using \texttt{match} in -given in Section~\ref{refine-example}. - -For example, we can write -the function \texttt{buildlist} that given a natural number -$n$ builds a list of length $n$ containing zeros as follows: - -\begin{coq_example} -Fixpoint buildlist (n:nat) : listn n := - match n return listn n with - | O => niln - | S n => consn n 0 (buildlist n) - end. -\end{coq_example} - -We can also use multiple patterns. -Consider the following definition of the predicate less-equal -\texttt{Le}: - -\begin{coq_example} -Inductive LE : nat -> nat -> Prop := - | LEO : forall n:nat, LE 0 n - | LES : forall n m:nat, LE n m -> LE (S n) (S m). -\end{coq_example} - -We can use multiple patterns to write the proof of the lemma - \texttt{forall (n m:nat), (LE n m)}\verb=\/=\texttt{(LE m n)}: - -\begin{coq_example} -Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n := - match n, m return LE n m \/ LE m n with - | O, x => or_introl (LE x 0) (LEO x) - | x, O => or_intror (LE x 0) (LEO x) - | S n as n', S m as m' => - match dec n m with - | or_introl h => or_introl (LE m' n') (LES n m h) - | or_intror h => or_intror (LE n' m') (LES m n h) - end - end. -\end{coq_example} -In the example of \texttt{dec}, -the first \texttt{match} is dependent while -the second is not. - -% In general, consider the terms $e_1\ldots e_n$, -% where the type of $e_i$ is an instance of a family type -% $\lb (\vec{d_i}:\vec{D_i}) \mto T_i$ ($1\leq i -% \leq n$). Then, in expression \texttt{match} $e_1,\ldots, -% e_n$ \texttt{of} \ldots \texttt{end}, the -% elimination predicate ${\cal P}$ should be of the form: -% $[\vec{d_1}:\vec{D_1}][x_1:T_1]\ldots [\vec{d_n}:\vec{D_n}][x_n:T_n]Q.$ - -The user can also use \texttt{match} in combination with the tactic -\texttt{refine} (see Section~\ref{refine}) to build incomplete proofs -beginning with a \texttt{match} construction. - -\asection{Pattern-matching on inductive objects involving local -definitions} - -If local definitions occur in the type of a constructor, then there are two ways -to match on this constructor. Either the local definitions are skipped and -matching is done only on the true arguments of the constructors, or the bindings -for local definitions can also be caught in the matching. - -Example. - -\begin{coq_eval} -Reset Initial. -Require Import Arith. -\end{coq_eval} - -\begin{coq_example*} -Inductive list : nat -> Set := - | nil : list 0 - | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)). -\end{coq_example*} - -In the next example, the local definition is not caught. - -\begin{coq_example} -Fixpoint length n (l:list n) {struct l} : nat := - match l with - | nil => 0 - | cons n l0 => S (length (2 * n) l0) - end. -\end{coq_example} - -But in this example, it is. - -\begin{coq_example} -Fixpoint length' n (l:list n) {struct l} : nat := - match l with - | nil => 0 - | @cons _ m l0 => S (length' m l0) - end. -\end{coq_example} - -\Rem for a given matching clause, either none of the local definitions or all of -them can be caught. - -\Rem you can only catch {\tt let} bindings in mode where you bind all variables and so you -have to use @ syntax. - -\Rem this feature is incoherent with the fact that parameters cannot be caught and -consequently is somehow hidden. For example, there is no mention of it in error messages. - -\asection{Pattern-matching and coercions} - -If a mismatch occurs between the expected type of a pattern and its -actual type, a coercion made from constructors is sought. If such a -coercion can be found, it is automatically inserted around the -pattern. - -Example: - -\begin{coq_example} -Inductive I : Set := - | C1 : nat -> I - | C2 : I -> I. -Coercion C1 : nat >-> I. -Check (fun x => match x with - | C2 O => 0 - | _ => 0 - end). -\end{coq_example} - - -\asection{When does the expansion strategy fail ?}\label{limitations} -The strategy works very like in ML languages when treating -patterns of non-dependent type. -But there are new cases of failure that are due to the presence of -dependencies. - -The error messages of the current implementation may be sometimes -confusing. When the tactic fails because patterns are somehow -incorrect then error messages refer to the initial expression. But the -strategy may succeed to build an expression whose sub-expressions are -well typed when the whole expression is not. In this situation the -message makes reference to the expanded expression. We encourage -users, when they have patterns with the same outer constructor in -different equations, to name the variable patterns in the same -positions with the same name. -E.g. to write {\small\texttt{(cons n O x) => e1}} -and {\small\texttt{(cons n \_ x) => e2}} instead of -{\small\texttt{(cons n O x) => e1}} and -{\small\texttt{(cons n' \_ x') => e2}}. -This helps to maintain certain name correspondence between the -generated expression and the original. - -Here is a summary of the error messages corresponding to each situation: - -\begin{ErrMsgs} -\item \sverb{The constructor } {\sl - ident} \sverb{ expects } {\sl num} \sverb{ arguments} - - \sverb{The variable } {\sl ident} \sverb{ is bound several times - in pattern } {\sl term} - - \sverb{Found a constructor of inductive type } {\term} - \sverb{ while a constructor of } {\term} \sverb{ is expected} - - Patterns are incorrect (because constructors are not applied to - the correct number of the arguments, because they are not linear or - they are wrongly typed). - -\item \errindex{Non exhaustive pattern-matching} - -The pattern matching is not exhaustive. - -\item \sverb{The elimination predicate } {\sl term} \sverb{ should be - of arity } {\sl num} \sverb{ (for non dependent case) or } {\sl - num} \sverb{ (for dependent case)} - -The elimination predicate provided to \texttt{match} has not the - expected arity. - - -%\item the whole expression is wrongly typed - -% CADUC ? -% , or the synthesis of -% implicit arguments fails (for example to find the elimination -% predicate or to resolve implicit arguments in the rhs). - -% There are {\em nested patterns of dependent type}, the elimination -% predicate corresponds to non-dependent case and has the form -% $[x_1:T_1]...[x_n:T_n]T$ and {\bf some} $x_i$ occurs {\bf free} in -% $T$. Then, the strategy may fail to find out a correct elimination -% predicate during some step of compilation. In this situation we -% recommend the user to rewrite the nested dependent patterns into -% several \texttt{match} with {\em simple patterns}. - -\item {\tt Unable to infer a match predicate\\ - Either there is a type incompatibility or the problem involves\\ - dependencies} - - There is a type mismatch between the different branches. - The user should provide an elimination predicate. - -% Obsolete ? -% \item because of nested patterns, it may happen that even though all -% the rhs have the same type, the strategy needs dependent elimination -% and so an elimination predicate must be provided. The system warns -% about this situation, trying to compile anyway with the -% non-dependent strategy. The risen message is: - -% \begin{itemize} -% \item {\tt Warning: This pattern matching may need dependent -% elimination to be compiled. I will try, but if fails try again -% giving dependent elimination predicate.} -% \end{itemize} - - -%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% % LA PROPAGATION DES CONTRAINTES ARRIERE N'EST PAS FAITE DANS LA V7 -% TODO -% \item there are {\em nested patterns of dependent type} and the -% strategy builds a term that is well typed but recursive calls in fix -% point are reported as illegal: -% \begin{itemize} -% \item {\tt Error: Recursive call applied to an illegal term ...} -% \end{itemize} - -% This is because the strategy generates a term that is correct w.r.t. -% the initial term but which does not pass the guard condition. In -% this situation we recommend the user to transform the nested dependent -% patterns into {\em several \texttt{match} of simple patterns}. Let us -% explain this with an example. Consider the following definition of a -% function that yields the last element of a list and \texttt{O} if it is -% empty: - -% \begin{coq_example} -% Fixpoint last [n:nat; l:(listn n)] : nat := -% match l of -% (consn _ a niln) => a -% | (consn m _ x) => (last m x) | niln => O -% end. -% \end{coq_example} - -% It fails because of the priority between patterns, we know that this -% definition is equivalent to the following more explicit one (which -% fails too): - -% \begin{coq_example*} -% Fixpoint last [n:nat; l:(listn n)] : nat := -% match l of -% (consn _ a niln) => a -% | (consn n _ (consn m b x)) => (last n (consn m b x)) -% | niln => O -% end. -% \end{coq_example*} - -% Note that the recursive call {\tt (last n (consn m b x))} is not -% guarded. When treating with patterns of dependent types the strategy -% interprets the first definition of \texttt{last} as the second -% one\footnote{In languages of the ML family the first definition would -% be translated into a term where the variable \texttt{x} is shared in -% the expression. When patterns are of non-dependent types, Coq -% compiles as in ML languages using sharing. When patterns are of -% dependent types the compilation reconstructs the term as in the -% second definition of \texttt{last} so to ensure the result of -% expansion is well typed.}. Thus it generates a term where the -% recursive call is rejected by the guard condition. - -% You can get rid of this problem by writing the definition with -% \emph{simple patterns}: - -% \begin{coq_example} -% Fixpoint last [n:nat; l:(listn n)] : nat := -% <[_:nat]nat>match l of -% (consn m a x) => Cases x of niln => a | _ => (last m x) end -% | niln => O -% end. -% \end{coq_example} - -\end{ErrMsgs} - - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex deleted file mode 100644 index 82765da6e..000000000 --- a/doc/refman/Omega.tex +++ /dev/null @@ -1,249 +0,0 @@ -\achapter{Omega: a solver of quantifier-free problems in -Presburger Arithmetic} -%HEVEA\cutname{omega.html} -\aauthor{Pierre Crégut} -\label{OmegaChapter} - -\asection{Description of {\tt omega}} -\tacindex{omega} -\label{description} - -{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally -quantified formula made of equations and inequations. Equations may -be specified either on the type \verb=nat= of natural numbers or on -the type \verb=Z= of binary-encoded integer numbers. Formulas on -\verb=nat= are automatically injected into \verb=Z=. The procedure -may use any hypothesis of the current proof session to solve the goal. - -Multiplication is handled by {\tt omega} but only goals where at -least one of the two multiplicands of products is a constant are -solvable. This is the restriction meant by ``Presburger arithmetic''. - -If the tactic cannot solve the goal, it fails with an error message. -In any case, the computation eventually stops. - -\asubsection{Arithmetical goals recognized by {\tt omega}} - -{\tt omega} applied only to quantifier-free formulas built from the -connectors - -\begin{quote} -\verb=/\, \/, ~, ->= -\end{quote} - -on atomic formulas. Atomic formulas are built from the predicates - -\begin{quote} -\verb!=, le, lt, gt, ge! -\end{quote} - - on \verb=nat= or from the predicates - -\begin{quote} -\verb!=, <, <=, >, >=! -\end{quote} - - on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes - -\begin{quote} -\verb!plus, minus, mult, pred, S, O! -\end{quote} - -and in expressions of type \verb=Z=, {\tt omega} recognizes - -\begin{quote} -\verb!+, -, *, Z.succ!, and constants. -\end{quote} - -All expressions of type \verb=nat= or \verb=Z= not built on these -operators are considered abstractly as if they -were arbitrary variables of type \verb=nat= or \verb=Z=. - -\asubsection{Messages from {\tt omega}} -\label{errors} - -When {\tt omega} does not solve the goal, one of the following errors -is generated: - -\begin{ErrMsgs} - -\item \errindex{omega can't solve this system} - - This may happen if your goal is not quantifier-free (if it is - universally quantified, try {\tt intros} first; if it contains - existentials quantifiers too, {\tt omega} is not strong enough to solve your - goal). This may happen also if your goal contains arithmetical - operators unknown from {\tt omega}. Finally, your goal may be really - wrong! - -\item \errindex{omega: Not a quantifier-free goal} - - If your goal is universally quantified, you should first apply {\tt - intro} as many time as needed. - -\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}} - -\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}} - -\item \errindex{omega: Can't solve a goal with proposition variables} - -\item \errindex{omega: Unrecognized proposition} - -\item \errindex{omega: Can't solve a goal with non-linear products} - -\item \errindex{omega: Can't solve a goal with equality on {\sl type}} - -\end{ErrMsgs} - -%% This code is currently unplugged -%% -% \asubsection{Control over the output} -% There are some flags that can be set to get more information on the procedure - -% \begin{itemize} -% \item \verb=Time= to get the time used by the procedure -% \item \verb=System= to visualize the normalized systems. -% \item \verb=Action= to visualize the actions performed by the OMEGA -% procedure (see \ref{technical}). -% \end{itemize} - -% \comindex{Set omega Time} -% \comindex{UnSet omega Time} -% \comindex{Switch omega Time} -% \comindex{Set omega System} -% \comindex{UnSet omega System} -% \comindex{Switch omega System} -% \comindex{Set omega Action} -% \comindex{UnSet omega Action} -% \comindex{Switch omega Action} - -% Use {\tt Set omega {\rm\sl flag}} to set the flag -% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and -% {\tt Switch omega {\rm\sl flag}} to toggle it. - -\section{Using {\tt omega}} - -The {\tt omega} tactic does not belong to the core system. It should be -loaded by -\begin{coq_example*} -Require Import Omega. -Open Scope Z_scope. -\end{coq_example*} - -\example{} - -\begin{coq_example} -Goal forall m n:Z, 1 + 2 * m <> 2 * n. -intros; omega. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\example{} - -\begin{coq_example} -Goal forall z:Z, z > 0 -> 2 * z + 1 > z. -intro; omega. -\end{coq_example} - -% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. - -\section{Options} - -\begin{quote} - \optindex{Stable Omega} - {\tt Unset Stable Omega} -\end{quote} -This deprecated option (on by default) is for compatibility with Coq -pre 8.5. It resets internal name counters to make executions of -{\tt omega} independent. - -\begin{quote} - \optindex{Omega UseLocalDefs} - {\tt Unset Omega UseLocalDefs} -\end{quote} -This option (on by default) allows {\tt omega} to use the bodies of -local variables. - -\begin{quote} - \optindex{Omega System} - {\tt Set Omega System} - \optindex{Omega Action} - {\tt Set Omega Action} -\end{quote} -These two options (off by default) activate the printing of debug -information. - -\asection{Technical data} -\label{technical} - -\asubsection{Overview of the tactic} -\begin{itemize} - -\item The goal is negated twice and the first negation is introduced as an - hypothesis. -\item Hypothesis are decomposed in simple equations or inequations. Multiple - goals may result from this phase. -\item Equations and inequations over \verb=nat= are translated over - \verb=Z=, multiple goals may result from the translation of - substraction. -\item Equations and inequations are normalized. -\item Goals are solved by the {\it OMEGA} decision procedure. -\item The script of the solution is replayed. - -\end{itemize} - -\asubsection{Overview of the {\it OMEGA} decision procedure} - -The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses -a small subset of the decision procedure presented in - -\begin{quote} - "The Omega Test: a fast and practical integer programming -algorithm for dependence analysis", William Pugh, Communication of the -ACM , 1992, p 102-114. -\end{quote} - -Here is an overview, look at the original paper for more information. - -\begin{itemize} - -\item Equations and inequations are normalized by division by the GCD of their - coefficients. -\item Equations are eliminated, using the Banerjee test to get a coefficient - equal to one. -\item Note that each inequation defines a half space in the space of real value - of the variables. - \item Inequations are solved by projecting on the hyperspace - defined by cancelling one of the variable. They are partitioned - according to the sign of the coefficient of the eliminated - variable. Pairs of inequations from different classes define a - new edge in the projection. - \item Redundant inequations are eliminated or merged in new - equations that can be eliminated by the Banerjee test. -\item The last two steps are iterated until a contradiction is reached - (success) or there is no more variable to eliminate (failure). - -\end{itemize} - -It may happen that there is a real solution and no integer one. The last -steps of the Omega procedure (dark shadow) are not implemented, so the -decision procedure is only partial. - -\asection{Bugs} - -\begin{itemize} -\item The simplification procedure is very dumb and this results in - many redundant cases to explore. - -\item Much too slow. - -\item Certainly other bugs! You can report them to \url{https://coq.inria.fr/bugs/}. - -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 4b7f9d91b..86f123322 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,11 +117,8 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% -\include{Cases.v}% \include{Coercion.v}% -\include{CanonicalStructures.v}% \include{Classes.v}% -\include{Omega.v}% \include{Extraction.v}% \include{Program.v}% \include{Polynom.v}% = Ring diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst new file mode 100644 index 000000000..6843e9eaa --- /dev/null +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -0,0 +1,435 @@ +.. include:: ../replaces.rst +.. _canonicalstructures: + +Canonical Structures +====================== + +:Authors: Assia Mahboubi and Enrico Tassi + +This chapter explains the basics of Canonical Structure and how they can be used +to overload notations and build a hierarchy of algebraic structures. The +examples are taken from :cite:`CSwcu`. We invite the interested reader to refer +to this paper for all the details that are omitted here for brevity. The +interested reader shall also find in :cite:`CSlessadhoc` a detailed description +of another, complementary, use of Canonical Structures: advanced proof search. +This latter papers also presents many techniques one can employ to tune the +inference of Canonical Structures. + + +Notation overloading +------------------------- + +We build an infix notation == for a comparison predicate. Such +notation will be overloaded, and its meaning will depend on the types +of the terms that are compared. + +.. coqtop:: all + + Module EQ. + Record class (T : Type) := Class { cmp : T -> T -> Prop }. + Structure type := Pack { obj : Type; class_of : class obj }. + Definition op (e : type) : obj e -> obj e -> Prop := + let 'Pack _ (Class _ the_cmp) := e in the_cmp. + Check op. + Arguments op {e} x y : simpl never. + Arguments Class {T} cmp. + Module theory. + Notation "x == y" := (op x y) (at level 70). + End theory. + End EQ. + +We use Coq modules as name spaces. This allows us to follow the same +pattern and naming convention for the rest of the chapter. The base +name space contains the definitions of the algebraic structure. To +keep the example small, the algebraic structure ``EQ.type`` we are +defining is very simplistic, and characterizes terms on which a binary +relation is defined, without requiring such relation to validate any +property. The inner theory module contains the overloaded notation ``==`` +and will eventually contain lemmas holding on all the instances of the +algebraic structure (in this case there are no lemmas). + +Note that in practice the user may want to declare ``EQ.obj`` as a +coercion, but we will not do that here. + +The following line tests that, when we assume a type ``e`` that is in +theEQ class, then we can relates two of its objects with ``==``. + +.. coqtop:: all + + Import EQ.theory. + Check forall (e : EQ.type) (a b : EQ.obj e), a == b. + +Still, no concrete type is in the ``EQ`` class. + +.. coqtop:: all + + Fail Check 3 == 3. + +We amend that by equipping ``nat`` with a comparison relation. + +.. coqtop:: all + + Definition nat_eq (x y : nat) := Nat.compare x y = Eq. + Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq. + Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl. + Check 3 == 3. + Eval compute in 3 == 4. + +This last test shows that |Coq| is now not only able to typecheck ``3 == 3``, +but also that the infix relation was bound to the ``nat_eq`` relation. +This relation is selected whenever ``==`` is used on terms of type nat. +This can be read in the line declaring the canonical structure +``nat_EQty``, where the first argument to ``Pack`` is the key and its second +argument a group of canonical values associated to the key. In this +case we associate to nat only one canonical value (since its class, +``nat_EQcl`` has just one member). The use of the projection ``op`` requires +its argument to be in the class ``EQ``, and uses such a member (function) +to actually compare its arguments. + +Similarly, we could equip any other type with a comparison relation, +and use the ``==`` notation on terms of this type. + + +Derived Canonical Structures +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We know how to use ``== `` on base types, like ``nat``, ``bool``, ``Z``. Here we show +how to deal with type constructors, i.e. how to make the following +example work: + + +.. coqtop:: all + + Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). + +The error message is telling that |Coq| has no idea on how to compare +pairs of objects. The following construction is telling Coq exactly +how to do that. + +.. coqtop:: all + + Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := + fst x == fst y /\ snd x == snd y. + + Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2). + + Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type := + EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2). + + Check forall (e : EQ.type) (a b : EQ.obj e), (a, b) == (a, b). + + Check forall n m : nat, (3, 4) == (n, m). + +Thanks to the ``pair_EQty`` declaration, |Coq| is able to build a comparison +relation for pairs whenever it is able to build a comparison relation +for each component of the pair. The declaration associates to the key ``*`` +(the type constructor of pairs) the canonical comparison +relation ``pair_eq`` whenever the type constructor ``*`` is applied to two +types being themselves in the ``EQ`` class. + +Hierarchy of structures +---------------------------- + +To get to an interesting example we need another base class to be +available. We choose the class of types that are equipped with an +order relation, to which we associate the infix ``<=`` notation. + +.. coqtop:: all + + Module LE. + + Record class T := Class { cmp : T -> T -> Prop }. + + Structure type := Pack { obj : Type; class_of : class obj }. + + Definition op (e : type) : obj e -> obj e -> Prop := + let 'Pack _ (Class _ f) := e in f. + + Arguments op {_} x y : simpl never. + + Arguments Class {T} cmp. + + Module theory. + + Notation "x <= y" := (op x y) (at level 70). + + End theory. + + End LE. + +As before we register a canonical ``LE`` class for ``nat``. + +.. coqtop:: all + + Import LE.theory. + + Definition nat_le x y := Nat.compare x y <> Gt. + + Definition nat_LEcl : LE.class nat := LE.Class nat_le. + + Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl. + +And we enable |Coq| to relate pair of terms with ``<=``. + +.. coqtop:: all + + Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) := + fst x <= fst y /\ snd x <= snd y. + + Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2). + + Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type := + LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2). + + Check (3,4,5) <= (3,4,5). + +At the current stage we can use ``==`` and ``<=`` on concrete types, like +tuples of natural numbers, but we can’t develop an algebraic theory +over the types that are equipped with both relations. + +.. coqtop:: all + + Check 2 <= 3 /\ 2 == 2. + + Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y. + + Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y. + +We need to define a new class that inherits from both ``EQ`` and ``LE``. + + +.. coqtop:: all + + Module LEQ. + + Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) := + Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }. + + Record class T := Class { + EQ_class : EQ.class T; + LE_class : LE.class T; + extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. + + Structure type := _Pack { obj : Type; class_of : class obj }. + + Arguments Mixin {e le} _. + + Arguments Class {T} _ _ _. + +The mixin component of the ``LEQ`` class contains all the extra content we +are adding to ``EQ`` and ``LE``. In particular it contains the requirement +that the two relations we are combining are compatible. + +Unfortunately there is still an obstacle to developing the algebraic +theory of this new class. + +.. coqtop:: all + + Module theory. + + Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m. + + +The problem is that the two classes ``LE`` and ``LEQ`` are not yet related by +a subclass relation. In other words |Coq| does not see that an object of +the ``LEQ`` class is also an object of the ``LE`` class. + +The following two constructions tell |Coq| how to canonically build the +``LE.type`` and ``EQ.type`` structure given an ``LEQ.type`` structure on the same +type. + +.. coqtop:: all + + Definition to_EQ (e : type) : EQ.type := + EQ.Pack (obj e) (EQ_class _ (class_of e)). + + Canonical Structure to_EQ. + + Definition to_LE (e : type) : LE.type := + LE.Pack (obj e) (LE_class _ (class_of e)). + + Canonical Structure to_LE. + +We can now formulate out first theorem on the objects of the ``LEQ`` +structure. + +.. coqtop:: all + + Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y. + + now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. + + Qed. + + Arguments lele_eq {e} x y _ _. + + End theory. + + End LEQ. + + Import LEQ.theory. + + Check lele_eq. + +Of course one would like to apply results proved in the algebraic +setting to any concrete instate of the algebraic structure. + +.. coqtop:: all + + Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. + + Fail apply (lele_eq n m). + + Abort. + + Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : + n <= m -> m <= n -> n == m. + + Fail apply (lele_eq n m). + + Abort. + +Again one has to tell |Coq| that the type ``nat`` is in the ``LEQ`` class, and +how the type constructor ``*`` interacts with the ``LEQ`` class. In the +following proofs are omitted for brevity. + +.. coqtop:: all + + Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m. + + Admitted. + + Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat. + + Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : + n <= m /\ m <= n <-> n == m. + + Admitted. + + Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2). + +The following script registers an ``LEQ`` class for ``nat`` and for the type +constructor ``*``. It also tests that they work as expected. + +Unfortunately, these declarations are very verbose. In the following +subsection we show how to make these declaration more compact. + +.. coqtop:: all + + Module Add_instance_attempt. + + Canonical Structure nat_LEQty : LEQ.type := + LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx). + + Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type := + LEQ._Pack (LEQ.obj l1 * LEQ.obj l2) + (LEQ.Class + (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2))) + (LE.class_of (pair_LEty (to_LE l1) (to_LE l2))) + (pair_LEQmx l1 l2)). + + Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. + + now apply (lele_eq n m). + + Qed. + + Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m. + + now apply (lele_eq n m). Qed. + + End Add_instance_attempt. + +Note that no direct proof of ``n <= m -> m <= n -> n == m`` is provided by +the user for ``n`` and m of type ``nat * nat``. What the user provides is a +proof of this statement for ``n`` and ``m`` of type ``nat`` and a proof that the +pair constructor preserves this property. The combination of these two +facts is a simple form of proof search that |Coq| performs automatically +while inferring canonical structures. + +Compact declaration of Canonical Structures +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We need some infrastructure for that. + +.. coqtop:: all + + Require Import Strings.String. + + Module infrastructure. + + Inductive phantom {T : Type} (t : T) : Type := Phantom. + + Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := + phantom t1 -> phantom t2. + + Definition id {T} {t : T} (x : phantom t) := x. + + Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) + (at level 50, v ident, only parsing). + + Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) + (at level 50, v ident, only parsing). + + Notation "'Error : t : s" := (unify _ t (Some s)) + (at level 50, format "''Error' : t : s"). + + Open Scope string_scope. + + End infrastructure. + +To explain the notation ``[find v | t1 ~ t2]`` let us pick one of its +instances: ``[find e | EQ.obj e ~ T | "is not an EQ.type" ]``. It should be +read as: “find a class e such that its objects have type T or fail +with message "T is not an EQ.type"”. + +The other utilities are used to ask |Coq| to solve a specific unification +problem, that will in turn require the inference of some canonical structures. +They are explained in mode details in :cite:`CSwcu`. + +We now have all we need to create a compact “packager” to declare +instances of the ``LEQ`` class. + +.. coqtop:: all + + Import infrastructure. + + Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) := + [find e | EQ.obj e ~ T | "is not an EQ.type" ] + [find o | LE.obj o ~ T | "is not an LE.type" ] + [find ce | EQ.class_of e ~ ce ] + [find co | LE.class_of o ~ co ] + [find m | m ~ m0 | "is not the right mixin" ] + LEQ._Pack T (LEQ.Class ce co m). + + Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id). + +The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers all +the other pieces of the class ``LEQ`` and declares them as canonical +values associated to the ``T`` key. All in all, the only new piece of +information we add in the ``LEQ`` class is the mixin, all the rest is +already canonical for ``T`` and hence can be inferred by |Coq|. + +``Pack`` is a notation, hence it is not type checked at the time of its +declaration. It will be type checked when it is used, an in that case ``T`` is +going to be a concrete type. The odd arguments ``_`` and ``id`` we pass to the +packager represent respectively the classes to be inferred (like ``e``, ``o``, +etc) and a token (``id``) to force their inference. Again, for all the details +the reader can refer to :cite:`CSwcu`. + +The declaration of canonical instances can now be way more compact: + +.. coqtop:: all + + Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. + + Canonical Structure pair_LEQty (l1 l2 : LEQ.type) := + Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2). + +Error messages are also quite intelligible (if one skips to the end of +the message). + +.. coqtop:: all + + Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx. + diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst new file mode 100644 index 000000000..64d4eddf0 --- /dev/null +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -0,0 +1,611 @@ +.. include:: ../replaces.rst + +.. _extendedpatternmatching: + +Extended pattern-matching +========================= + +:Authors: Cristina Cornes and Hugo Herbelin + +.. TODO links to figures + +This section describes the full form of pattern-matching in |Coq| terms. + +.. |rhs| replace:: right hand side + +Patterns +-------- + +The full syntax of match is presented in Figures 1.1 and 1.2. +Identifiers in patterns are either constructor names or variables. Any +identifier that is not the constructor of an inductive or co-inductive +type is considered to be a variable. A variable name cannot occur more +than once in a given pattern. It is recommended to start variable +names by a lowercase letter. + +If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x +is a linear vector of (distinct) variables, it is called *simple*: it +is the kind of pattern recognized by the basic version of match. On +the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not +only made of variables, the pattern is called *nested*. + +A variable pattern matches any value, and the identifier is bound to +that value. The pattern “``_``” (called “don't care” or “wildcard” symbol) +also matches any value, but does not bind anything. It may occur an +arbitrary number of times in a pattern. Alias patterns written +:n:`(@pattern as @identifier)` are also accepted. This pattern matches the +same values as ``pattern`` does and ``identifier`` is bound to the matched +value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A +list of patterns separated with commas is also considered as a pattern +and is called *multiple pattern*. However multiple patterns can only +occur at the root of pattern-matching equations. Disjunctions of +*multiple pattern* are allowed though. + +Since extended ``match`` expressions are compiled into the primitive ones, +the expressiveness of the theory remains the same. Once the stage of +parsing has finished only simple patterns remain. Re-nesting of +pattern is performed at printing time. An easy way to see the result +of the expansion is to toggle off the nesting performed at printing +(use here :opt:`Set Printing Matching`), then by printing the term with :cmd:`Print` +if the term is a constant, or using the command :cmd:`Check`. + +The extended ``match`` still accepts an optional *elimination predicate* +given after the keyword ``return``. Given a pattern matching expression, +if all the right-hand-sides of ``=>`` have the same +type, then this type can be sometimes synthesized, and so we can omit +the return part. Otherwise the predicate after return has to be +provided, like for the basicmatch. + +Let us illustrate through examples the different aspects of extended +pattern matching. Consider for example the function that computes the +maximum of two natural numbers. We can write it in primitive syntax +by: + +.. coqtop:: in undo + + Fixpoint max (n m:nat) {struct m} : nat := + match n with + | O => m + | S n' => match m with + | O => S n' + | S m' => S (max n' m') + end + end. + +Multiple patterns +----------------- + +Using multiple patterns in the definition of max lets us write: + +.. coqtop:: in undo + + Fixpoint max (n m:nat) {struct m} : nat := + match n, m with + | O, _ => m + | S n', O => S n' + | S n', S m' => S (max n' m') + end. + +which will be compiled into the previous form. + +The pattern-matching compilation strategy examines patterns from left +to right. A match expression is generated **only** when there is at least +one constructor in the column of patterns. E.g. the following example +does not build a match expression. + +.. coqtop:: all + + Check (fun x:nat => match x return nat with + | y => y + end). + + +Aliasing subpatterns +-------------------- + +We can also use :n:`as @ident` to associate a name to a sub-pattern: + +.. coqtop:: in undo + + Fixpoint max (n m:nat) {struct n} : nat := + match n, m with + | O, _ => m + | S n' as p, O => p + | S n', S m' => S (max n' m') + end. + +Nested patterns +--------------- + +Here is now an example of nested patterns: + +.. coqtop:: in + + Fixpoint even (n:nat) : bool := + match n with + | O => true + | S O => false + | S (S n') => even n' + end. + +This is compiled into: + +.. coqtop:: all undo + + Unset Printing Matching. + Print even. + +In the previous examples patterns do not conflict with, but sometimes +it is comfortable to write patterns that admit a non trivial +superposition. Consider the boolean function :g:`lef` that given two +natural numbers yields :g:`true` if the first one is less or equal than the +second one and :g:`false` otherwise. We can write it as follows: + +.. coqtop:: in undo + + Fixpoint lef (n m:nat) {struct m} : bool := + match n, m with + | O, x => true + | x, O => false + | S n, S m => lef n m + end. + +Note that the first and the second multiple pattern superpose because +the couple of values ``O O`` matches both. Thus, what is the result of the +function on those values? To eliminate ambiguity we use the *textual +priority rule*: we consider patterns ordered from top to bottom, then +a value is matched by the pattern at the ith row if and only if it is +not matched by some pattern of a previous row. Thus in the example,O O +is matched by the first pattern, and so :g:`(lef O O)` yields true. + +Another way to write this function is: + +.. coqtop:: in + + Fixpoint lef (n m:nat) {struct m} : bool := + match n, m with + | O, x => true + | S n, S m => lef n m + | _, _ => false + end. + +Here the last pattern superposes with the first two. Because of the +priority rule, the last pattern will be used only for values that do +not match neither the first nor the second one. + +Terms with useless patterns are not accepted by the system. Here is an +example: + +.. coqtop:: all + + Fail Check (fun x:nat => + match x with + | O => true + | S _ => false + | x => true + end). + + +Disjunctive patterns +-------------------- + +Multiple patterns that share the same right-hand-side can be +factorized using the notation :n:`{+| @mult_pattern}`. For +instance, :g:`max` can be rewritten as follows: + +.. coqtop:: in undo + + Fixpoint max (n m:nat) {struct m} : nat := + match n, m with + | S n', S m' => S (max n' m') + | 0, p | p, 0 => p + end. + +Similarly, factorization of (non necessary multiple) patterns that +share the same variables is possible by using the notation :n:`{+| @pattern}`. +Here is an example: + +.. coqtop:: in + + Definition filter_2_4 (n:nat) : nat := + match n with + | 2 as m | 4 as m => m + | _ => 0 + end. + + +Here is another example using disjunctive subpatterns. + +.. coqtop:: in + + Definition filter_some_square_corners (p:nat*nat) : nat*nat := + match p with + | ((2 as m | 4 as m), (3 as n | 5 as n)) => (m,n) + | _ => (0,0) + end. + +About patterns of parametric types +---------------------------------- + +Parameters in patterns +~~~~~~~~~~~~~~~~~~~~~~ + +When matching objects of a parametric type, parameters do not bind in +patterns. They must be substituted by “``_``”. Consider for example the +type of polymorphic lists: + +.. coqtop:: in + + Inductive List (A:Set) : Set := + | nil : List A + | cons : A -> List A -> List A. + +We can check the function *tail*: + +.. coqtop:: all + + Check + (fun l:List nat => + match l with + | nil _ => nil nat + | cons _ _ l' => l' + end). + +When we use parameters in patterns there is an error message: + +.. coqtop:: all + + Fail Check + (fun l:List nat => + match l with + | nil A => nil nat + | cons A _ l' => l' + end). + +.. opt:: Asymmetric Patterns + +This option (off by default) removes parameters from constructors in patterns: + +.. coqtop:: all + + Set Asymmetric Patterns. + Check (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end) + Unset Asymmetric Patterns. + +Implicit arguments in patterns +------------------------------ + +By default, implicit arguments are omitted in patterns. So we write: + +.. coqtop:: all + + Arguments nil [A]. + Arguments cons [A] _ _. + Check + (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end). + +But the possibility to use all the arguments is given by “``@``” implicit +explicitations (as for terms 2.7.11). + +.. coqtop:: all + + Check + (fun l:List nat => + match l with + | @nil _ => @nil nat + | @cons _ _ l' => l' + end). + + +Matching objects of dependent types +----------------------------------- + +The previous examples illustrate pattern matching on objects of non- +dependent types, but we can also use the expansion strategy to +destructure objects of dependent type. Consider the type :g:`listn` of +lists of a certain length: + +.. coqtop:: in reset + + Inductive listn : nat -> Set := + | niln : listn 0 + | consn : forall n:nat, nat -> listn n -> listn (S n). + + +Understanding dependencies in patterns +-------------------------------------- + +We can define the function length over :g:`listn` by: + +.. coqtop:: in + + Definition length (n:nat) (l:listn n) := n. + +Just for illustrating pattern matching, we can define it by case +analysis: + +.. coqtop:: in + + Definition length (n:nat) (l:listn n) := + match l with + | niln => 0 + | consn n _ _ => S n + end. + +We can understand the meaning of this definition using the same +notions of usual pattern matching. + + +When the elimination predicate must be provided +----------------------------------------------- + +Dependent pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The examples given so far do not need an explicit elimination +predicate because all the |rhs| have the same type and the strategy +succeeds to synthesize it. Unfortunately when dealing with dependent +patterns it often happens that we need to write cases where the type +of the |rhs| are different instances of the elimination predicate. The +function concat for listn is an example where the branches have +different type and we need to provide the elimination predicate: + +.. coqtop:: in + + Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : + listn (n + m) := + match l in listn n return listn (n + m) with + | niln => l' + | consn n' a y => consn (n' + m) a (concat n' y m l') + end. + +The elimination predicate is :g:`fun (n:nat) (l:listn n) => listn (n+m)`. +In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr` +are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`. + +In the concrete syntax, it should be written : +``match m as x in (I _ … _ y1 … ys) return Q with … end`` +The variables which appear in the ``in`` and ``as`` clause are new and bounded +in the property :g:`Q` in the return clause. The parameters of the +inductive definitions should not be mentioned and are replaced by ``_``. + +Multiple dependent pattern matching +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Recall that a list of patterns is also a pattern. So, when we +destructure several terms at the same time and the branches have +different types we need to provide the elimination predicate for this +multiple pattern. It is done using the same scheme, each term may be +associated to an as and in clause in order to introduce a dependent +product. + +For example, an equivalent definition for :g:`concat` (even though the +matching on the second term is trivial) would have been: + +.. coqtop:: in + + Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : + listn (n + m) := + match l in listn n, l' return listn (n + m) with + | niln, x => x + | consn n' a y, x => consn (n' + m) a (concat n' y m x) + end. + +Even without real matching over the second term, this construction can +be used to keep types linked. If :g:`a` and :g:`b` are two :g:`listn` of the same +length, by writing + +.. coqtop:: in + + Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : + listn (n + m) := + match l in listn n, l' return listn (n + m) with + | niln, x => x + | consn n' a y, x => consn (n' + m) a (concat n' y m x) + end. + +I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`. + + +Patterns in ``in`` +~~~~~~~~~~~~~~~~~~ + +If the type of the matched term is more precise than an inductive +applied to variables, arguments of the inductive in the ``in`` branch can +be more complicated patterns than a variable. + +Moreover, constructors whose type do not follow the same pattern will +become impossible branches. In an impossible branch, you can answer +anything but False_rect unit has the advantage to be subterm of +anything. + +To be concrete: the tail function can be written: + +.. coqtop:: in + + Definition tail n (v: listn (S n)) := + match v in listn (S m) return listn m with + | niln => False_rect unit + | consn n' a y => y + end. + +and :g:`tail n v` will be subterm of :g:`v`. + +Using pattern matching to write proofs +-------------------------------------- + +In all the previous examples the elimination predicate does not depend +on the object(s) matched. But it may depend and the typical case is +when we write a proof by induction or a function that yields an object +of dependent type. An example of proof using match in given in Section +8.2.3. + +For example, we can write the function :g:`buildlist` that given a natural +number :g:`n` builds a list of length :g:`n` containing zeros as follows: + +.. coqtop:: in + + Fixpoint buildlist (n:nat) : listn n := + match n return listn n with + | O => niln + | S n => consn n 0 (buildlist n) + end. + +We can also use multiple patterns. Consider the following definition +of the predicate less-equal :g:`Le`: + +.. coqtop:: in + + Inductive LE : nat -> nat -> Prop := + | LEO : forall n:nat, LE 0 n + | LES : forall n m:nat, LE n m -> LE (S n) (S m). + +We can use multiple patterns to write the proof of the lemma +:g:`forall (n m:nat), (LE n m) \/ (LE m n)`: + +.. coqtop:: in + + Fixpoint dec (n m:nat) {struct n} : LE n m \/ LE m n := + match n, m return LE n m \/ LE m n with + | O, x => or_introl (LE x 0) (LEO x) + | x, O => or_intror (LE x 0) (LEO x) + | S n as n', S m as m' => + match dec n m with + | or_introl h => or_introl (LE m' n') (LES n m h) + | or_intror h => or_intror (LE n' m') (LES m n h) + end + end. + +In the example of :g:`dec`, the first match is dependent while the second +is not. + +The user can also use match in combination with the tactic :tacn:`refine` (see +Section 8.2.3) to build incomplete proofs beginning with a match +construction. + + +Pattern-matching on inductive objects involving local definitions +----------------------------------------------------------------- + +If local definitions occur in the type of a constructor, then there +are two ways to match on this constructor. Either the local +definitions are skipped and matching is done only on the true +arguments of the constructors, or the bindings for local definitions +can also be caught in the matching. + +.. example:: + + .. coqtop:: in + + Inductive list : nat -> Set := + | nil : list 0 + | cons : forall n:nat, let m := (2 * n) in list m -> list (S (S m)). + + In the next example, the local definition is not caught. + + .. coqtop:: in + + Fixpoint length n (l:list n) {struct l} : nat := + match l with + | nil => 0 + | cons n l0 => S (length (2 * n) l0) + end. + + But in this example, it is. + + .. coqtop:: in + + Fixpoint length' n (l:list n) {struct l} : nat := + match l with + | nil => 0 + | @cons _ m l0 => S (length' m l0) + end. + +.. note:: For a given matching clause, either none of the local + definitions or all of them can be caught. + +.. note:: You can only catch let bindings in mode where you bind all + variables and so you have to use ``@`` syntax. + +.. note:: this feature is incoherent with the fact that parameters + cannot be caught and consequently is somehow hidden. For example, + there is no mention of it in error messages. + +Pattern-matching and coercions +------------------------------ + +If a mismatch occurs between the expected type of a pattern and its +actual type, a coercion made from constructors is sought. If such a +coercion can be found, it is automatically inserted around the +pattern. + +.. example:: + + .. coqtop:: in + + Inductive I : Set := + | C1 : nat -> I + | C2 : I -> I. + + Coercion C1 : nat >-> I. + + .. coqtop:: all + + Check (fun x => match x with + | C2 O => 0 + | _ => 0 + end). + + +When does the expansion strategy fail? +-------------------------------------- + +The strategy works very like in ML languages when treating patterns of +non-dependent type. But there are new cases of failure that are due to +the presence of dependencies. + +The error messages of the current implementation may be sometimes +confusing. When the tactic fails because patterns are somehow +incorrect then error messages refer to the initial expression. But the +strategy may succeed to build an expression whose sub-expressions are +well typed when the whole expression is not. In this situation the +message makes reference to the expanded expression. We encourage +users, when they have patterns with the same outer constructor in +different equations, to name the variable patterns in the same +positions with the same name. E.g. to write ``(cons n O x) => e1`` and +``(cons n _ x) => e2`` instead of ``(cons n O x) => e1`` and +``(cons n' _ x') => e2``. This helps to maintain certain name correspondence between the +generated expression and the original. + +Here is a summary of the error messages corresponding to each +situation: + +.. exn:: The constructor @ident expects @num arguments + + The variable ident is bound several times in pattern termFound a constructor + of inductive type term while a constructor of term is expectedPatterns are + incorrect (because constructors are not applied to the correct number of the + arguments, because they are not linear or they are wrongly typed). + +.. exn:: Non exhaustive pattern-matching + + The pattern matching is not exhaustive. + +.. exn:: The elimination predicate term should be of arity @num (for non \ + dependent case) or @num (for dependent case) + + The elimination predicate provided to match has not the expected arity. + +.. exn:: Unable to infer a match predicate + Either there is a type incompatibility or the problem involves dependencies + + There is a type mismatch between the different branches. The user should + provide an elimination predicate. diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst new file mode 100644 index 000000000..20e40c550 --- /dev/null +++ b/doc/sphinx/addendum/omega.rst @@ -0,0 +1,184 @@ +.. _omega: + +Omega: a solver for quantifier-free problems in Presburger Arithmetic +===================================================================== + +:Author: Pierre Crégut + +Description of ``omega`` +------------------------ + +This tactic does not need any parameter: + +.. tacn:: omega + +``omega`` solves a goal in Presburger arithmetic, i.e. a universally +quantified formula made of equations and inequations. Equations may +be specified either on the type ``nat`` of natural numbers or on +the type ``Z`` of binary-encoded integer numbers. Formulas on +``nat`` are automatically injected into ``Z``. The procedure +may use any hypothesis of the current proof session to solve the goal. + +Multiplication is handled by ``omega`` but only goals where at +least one of the two multiplicands of products is a constant are +solvable. This is the restriction meant by "Presburger arithmetic". + +If the tactic cannot solve the goal, it fails with an error message. +In any case, the computation eventually stops. + +Arithmetical goals recognized by ``omega`` +------------------------------------------ + +``omega`` applied only to quantifier-free formulas built from the +connectors:: + + /\ \/ ~ -> + +on atomic formulas. Atomic formulas are built from the predicates:: + + = < <= > >= + +on ``nat`` or ``Z``. In expressions of type ``nat``, ``omega`` recognizes:: + + + - * S O pred + +and in expressions of type ``Z``, ``omega`` recognizes numeral constants and:: + + + - * Z.succ Z.pred + +All expressions of type ``nat`` or ``Z`` not built on these +operators are considered abstractly as if they +were arbitrary variables of type ``nat`` or ``Z``. + +Messages from ``omega`` +----------------------- + +When ``omega`` does not solve the goal, one of the following errors +is generated: + +.. exn:: omega can't solve this system + + This may happen if your goal is not quantifier-free (if it is + universally quantified, try ``intros`` first; if it contains + existentials quantifiers too, ``omega`` is not strong enough to solve your + goal). This may happen also if your goal contains arithmetical + operators unknown from ``omega``. Finally, your goal may be really + wrong! + +.. exn:: omega: Not a quantifier-free goal + + If your goal is universally quantified, you should first apply + ``intro`` as many time as needed. + +.. exn:: omega: Unrecognized predicate or connective: @ident + +.. exn:: omega: Unrecognized atomic proposition: ... + +.. exn:: omega: Can't solve a goal with proposition variables + +.. exn:: omega: Unrecognized proposition + +.. exn:: omega: Can't solve a goal with non-linear products + +.. exn:: omega: Can't solve a goal with equality on type ... + + +Using ``omega`` +--------------- + +The ``omega`` tactic does not belong to the core system. It should be +loaded by + +.. coqtop:: in + + Require Import Omega. + +.. example:: + + .. coqtop:: all + + Require Import Omega. + + Open Scope Z_scope. + + Goal forall m n:Z, 1 + 2 * m <> 2 * n. + intros; omega. + Abort. + + Goal forall z:Z, z > 0 -> 2 * z + 1 > z. + intro; omega. + Abort. + + +Options +------- + +.. opt:: Stable Omega + +This deprecated option (on by default) is for compatibility with Coq pre 8.5. It +resets internal name counters to make executions of ``omega`` independent. + +.. opt:: Omega UseLocalDefs + +This option (on by default) allows ``omega`` to use the bodies of local +variables. + +.. opt:: Omega System + +This option (off by default) activate the printing of debug information + +.. opt:: Omega Action + +This option (off by default) activate the printing of debug information + +Technical data +-------------- + +Overview of the tactic +~~~~~~~~~~~~~~~~~~~~~~ + + * The goal is negated twice and the first negation is introduced as an hypothesis. + * Hypothesis are decomposed in simple equations or inequations. Multiple + goals may result from this phase. + * Equations and inequations over ``nat`` are translated over + ``Z``, multiple goals may result from the translation of substraction. + * Equations and inequations are normalized. + * Goals are solved by the OMEGA decision procedure. + * The script of the solution is replayed. + +Overview of the OMEGA decision procedure +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +The OMEGA decision procedure involved in the ``omega`` tactic uses +a small subset of the decision procedure presented in :cite:`TheOmegaPaper` +Here is an overview, look at the original paper for more information. + + * Equations and inequations are normalized by division by the GCD of their + coefficients. + * Equations are eliminated, using the Banerjee test to get a coefficient + equal to one. + * Note that each inequation defines a half space in the space of real value + of the variables. + * Inequations are solved by projecting on the hyperspace + defined by cancelling one of the variable. They are partitioned + according to the sign of the coefficient of the eliminated + variable. Pairs of inequations from different classes define a + new edge in the projection. + * Redundant inequations are eliminated or merged in new + equations that can be eliminated by the Banerjee test. + * The last two steps are iterated until a contradiction is reached + (success) or there is no more variable to eliminate (failure). + +It may happen that there is a real solution and no integer one. The last +steps of the Omega procedure (dark shadow) are not implemented, so the +decision procedure is only partial. + +Bugs +---- + + * The simplification procedure is very dumb and this results in + many redundant cases to explore. + + * Much too slow. + + * Certainly other bugs! You can report them to https://coq.inria.fr/bugs/. diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 4a9bd6c1a..247f32103 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -1312,7 +1312,7 @@ Languages}, year = {1994} } -@article{ TheOmegaPaper, +@article{TheOmegaPaper, author = "W. Pugh", title = "The Omega test: a fast and practical integer programming algorithm for dependence analysis", journal = "Communication of the ACM", diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index ddcb4c4cb..c5d4936b1 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -43,6 +43,9 @@ Table of contents .. toctree:: :caption: Addendum + addendum/extended-pattern-matching + addendum/canonical-structures + addendum/omega addendum/micromega .. toctree:: |