diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/CanonicalStructures.tex | 383 | ||||
| -rw-r--r-- | doc/refman/Cases.tex | 843 | ||||
| -rw-r--r-- | doc/refman/Micromega.tex | 256 | ||||
| -rw-r--r-- | doc/refman/Omega.tex | 249 | ||||
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 4 | ||||
| -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/micromega.rst | 252 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 184 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 2 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 5 |
11 files changed, 1488 insertions, 1736 deletions
diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex deleted file mode 100644 index 8961b00964..0000000000 --- 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 376ef031db..0000000000 --- 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/Micromega.tex b/doc/refman/Micromega.tex deleted file mode 100644 index 2617142f5a..0000000000 --- a/doc/refman/Micromega.tex +++ /dev/null @@ -1,256 +0,0 @@ -\achapter{Micromega: tactics for solving arithmetic goals over ordered rings} -%HEVEA\cutname{micromega.html} -\aauthor{Frédéric Besson and Evgeny Makarov} -\newtheorem{theorem}{Theorem} - - -\asection{Short description of the tactics} -\tacindex{psatz} \tacindex{lra} \tacindex{lia} \tacindex{nia} \tacindex{nra} -\label{sec:psatz-hurry} -The {\tt Psatz} module ({\tt Require Import Psatz.}) gives access to -several tactics for solving arithmetic goals over {\tt Z}, {\tt Q}, and -{\tt R}:\footnote{Support for {\tt nat} and {\tt N} is obtained by - pre-processing the goal with the {\tt zify} tactic.}. -It also possible to get the tactics for integers by a {\tt Require Import Lia}, rationals {\tt Require Import Lqa} -and reals {\tt Require Import Lra}. -\begin{itemize} -\item {\tt lia} is a decision procedure for linear integer arithmetic (see Section~\ref{sec:lia}); -\item {\tt nia} is an incomplete proof procedure for integer non-linear arithmetic (see Section~\ref{sec:nia}); -\item {\tt lra} is a decision procedure for linear (real or rational) arithmetic (see Section~\ref{sec:lra}); -\item {\tt nra} is an incomplete proof procedure for non-linear (real or rational) arithmetic (see Section~\ref{sec:nra}); -\item {\tt psatz D n} where {\tt D} is {\tt Z} or {\tt Q} or {\tt R}, and - {\tt n} is an optional integer limiting the proof search depth is is an - incomplete proof procedure for non-linear arithmetic. It is based on - John Harrison's HOL Light driver to the external prover {\tt - csdp}\footnote{Sources and binaries can be found at - \url{https://projects.coin-or.org/Csdp}}. Note that the {\tt csdp} - driver is generating a \emph{proof cache} which makes it possible to - rerun scripts even without {\tt csdp} (see Section~\ref{sec:psatz}). -\end{itemize} - -The tactics solve propositional formulas parameterized by atomic arithmetic expressions -interpreted over a domain $D \in \{\mathbb{Z}, \mathbb{Q}, \mathbb{R} \}$. -The syntax of the formulas is the following: -\[ -\begin{array}{lcl} - F &::=& A \mid P \mid \mathit{True} \mid \mathit{False} \mid F_1 \land F_2 \mid F_1 \lor F_2 \mid F_1 \leftrightarrow F_2 \mid F_1 \to F_2 \mid \neg F\\ - A &::=& p_1 = p_2 \mid p_1 > p_2 \mid p_1 < p_2 \mid p_1 \ge p_2 \mid p_1 \le p_2 \\ - p &::=& c \mid x \mid {-}p \mid p_1 - p_2 \mid p_1 + p_2 \mid p_1 \times p_2 \mid p \verb!^! n -\end{array} -\] -where $c$ is a numeric constant, $x\in D$ is a numeric variable, the -operators $-$, $+$, $\times$ are respectively subtraction, addition, -product, $p \verb!^!n $ is exponentiation by a constant $n$, $P$ is an -arbitrary proposition. - % - For {\tt Q}, equality is not Leibniz equality {\tt =} but the equality of rationals {\tt ==}. - -For {\tt Z} (resp. {\tt Q} ), $c$ ranges over integer constants (resp. rational constants). -%% The following table details for each domain $D \in \{\mathbb{Z},\mathbb{Q},\mathbb{R}\}$ the range of constants $c$ and exponent $n$. -%% \[ -%% \begin{array}{|c|c|c|c|} -%% \hline -%% &\mathbb{Z} & \mathbb{Q} & \mathbb{R} \\ -%% \hline -%% c &\mathtt{Z} & \mathtt{Q} & (see below) \\ -%% \hline -%% n &\mathtt{Z} & \mathtt{Z} & \mathtt{nat}\\ -%% \hline -%% \end{array} -%% \] -For {\tt R}, the tactic recognizes as real constants the following expressions: -\begin{verbatim} -c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q - | Rdiv(c,c) | Rinv c -\end{verbatim} -where {\tt z} is a constant in {\tt Z} and {\tt q} is a constant in {\tt Q}. -This includes integer constants written using the decimal notation \emph{i.e.,} {\tt c\%R}. - -\asection{\emph{Positivstellensatz} refutations} -\label{sec:psatz-back} - -The name {\tt psatz} is an abbreviation for \emph{positivstellensatz} -- literally positivity theorem -- which -generalizes Hilbert's \emph{nullstellensatz}. -% -It relies on the notion of $\mathit{Cone}$. Given a (finite) set of -polynomials $S$, $\mathit{Cone}(S)$ is inductively defined as the -smallest set of polynomials closed under the following rules: -\[ -\begin{array}{l} -\dfrac{p \in S}{p \in \mathit{Cone}(S)} \quad -\dfrac{}{p^2 \in \mathit{Cone}(S)} \quad -\dfrac{p_1 \in \mathit{Cone}(S) \quad p_2 \in \mathit{Cone}(S) \quad -\Join \in \{+,*\}} {p_1 \Join p_2 \in \mathit{Cone}(S)}\\ -\end{array} -\] -The following theorem provides a proof principle for checking that a set -of polynomial inequalities does not have solutions.\footnote{Variants - deal with equalities and strict inequalities.} -\begin{theorem} - \label{thm:psatz} - Let $S$ be a set of polynomials.\\ - If ${-}1$ belongs to $\mathit{Cone}(S)$ then the conjunction - $\bigwedge_{p \in S} p\ge 0$ is unsatisfiable. -\end{theorem} -A proof based on this theorem is called a \emph{positivstellensatz} refutation. -% -The tactics work as follows. Formulas are normalized into conjunctive normal form $\bigwedge_i C_i$ where -$C_i$ has the general form $(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False})$ and $\Join \in \{>,\ge,=\}$ for $D\in -\{\mathbb{Q},\mathbb{R}\}$ and $\Join \in \{\ge, =\}$ for $\mathbb{Z}$. -% -For each conjunct $C_i$, the tactic calls a oracle which searches for $-1$ within the cone. -% -Upon success, the oracle returns a \emph{cone expression} that is normalized by the {\tt ring} tactic (see chapter~\ref{ring}) and checked to be -$-1$. - - -\asection{{\tt lra}: a decision procedure for linear real and rational arithmetic} -\label{sec:lra} -The {\tt lra} tactic is searching for \emph{linear} refutations using -Fourier elimination.\footnote{More efficient linear programming - techniques could equally be employed.} As a result, this tactic -explores a subset of the $\mathit{Cone}$ defined as -\[ -\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right| -~\alpha_p \mbox{ are positive constants} \right\}. -\] -The deductive power of {\tt lra} is the combined deductive power of {\tt ring\_simplify} and {\tt fourier}. -% -There is also an overlap with the {\tt field} tactic {\emph e.g.}, {\tt x = 10 * x / 10} is solved by {\tt lra}. - - -\asection{{\tt lia}: a tactic for linear integer arithmetic} -\tacindex{lia} -\label{sec:lia} - -The tactic {\tt lia} offers an alternative to the {\tt omega} and {\tt - romega} tactic (see Chapter~\ref{OmegaChapter}). -% -Roughly speaking, the deductive power of {\tt lia} is the combined deductive power of {\tt ring\_simplify} and {\tt omega}. -% -However, it solves linear goals that {\tt omega} and {\tt romega} do not solve, such as the -following so-called \emph{omega nightmare}~\cite{TheOmegaPaper}. -\begin{coq_example*} -Goal forall x y, - 27 <= 11 * x + 13 * y <= 45 -> - -10 <= 7 * x - 9 * y <= 4 -> False. -\end{coq_example*} -\begin{coq_eval} -intros x y; lia. -\end{coq_eval} -The estimation of the relative efficiency of {\tt lia} \emph{vs} {\tt omega} -and {\tt romega} is under evaluation. - -\paragraph{High level view of {\tt lia}.} -Over $\mathbb{R}$, \emph{positivstellensatz} refutations are a complete -proof principle.\footnote{In practice, the oracle might fail to produce - such a refutation.} -% -However, this is not the case over $\mathbb{Z}$. -% -Actually, \emph{positivstellensatz} refutations are not even sufficient -to decide linear \emph{integer} arithmetic. -% -The canonical example is {\tt 2 * x = 1 -> False} which is a theorem of $\mathbb{Z}$ but not a theorem of $\mathbb{R}$. -% -To remedy this weakness, the {\tt lia} tactic is using recursively a combination of: -% -\begin{itemize} -\item linear \emph{positivstellensatz} refutations; -\item cutting plane proofs; -\item case split. -\end{itemize} - -\paragraph{Cutting plane proofs} are a way to take into account the discreetness of $\mathbb{Z}$ by rounding up -(rational) constants up-to the closest integer. -% -\begin{theorem} - Let $p$ be an integer and $c$ a rational constant. - \[ - p \ge c \Rightarrow p \ge \lceil c \rceil - \] -\end{theorem} -For instance, from $2 x = 1$ we can deduce -\begin{itemize} -\item $x \ge 1/2$ which cut plane is $ x \ge \lceil 1/2 \rceil = 1$; -\item $ x \le 1/2$ which cut plane is $ x \le \lfloor 1/2 \rfloor = 0$. -\end{itemize} -By combining these two facts (in normal form) $x - 1 \ge 0$ and $-x \ge -0$, we conclude by exhibiting a \emph{positivstellensatz} refutation: $-1 -\equiv \mathbf{x-1} + \mathbf{-x} \in \mathit{Cone}(\{x-1,x\})$. - -Cutting plane proofs and linear \emph{positivstellensatz} refutations are a complete proof principle for integer linear arithmetic. - -\paragraph{Case split} enumerates over the possible values of an expression. -\begin{theorem} - Let $p$ be an integer and $c_1$ and $c_2$ integer constants. - \[ - c_1 \le p \le c_2 \Rightarrow \bigvee_{x \in [c_1,c_2]} p = x - \] -\end{theorem} -Our current oracle tries to find an expression $e$ with a small range $[c_1,c_2]$. -% -We generate $c_2 - c_1$ subgoals which contexts are enriched with an equation $e = i$ for $i \in [c_1,c_2]$ and -recursively search for a proof. - - -\asection{{\tt nra}: a proof procedure for non-linear arithmetic} -\tacindex{nra} -\label{sec:nra} -The {\tt nra} tactic is an {\emph experimental} proof procedure for non-linear arithmetic. -% -The tactic performs a limited amount of non-linear reasoning before running the -linear prover of {\tt lra}. -This pre-processing does the following: -\begin{itemize} -\item If the context contains an arithmetic expression of the form $e[x^2]$ where $x$ is a - monomial, the context is enriched with $x^2\ge 0$; -\item For all pairs of hypotheses $e_1\ge 0$, $e_2 \ge 0$, the context is enriched with $e_1 \times e_2 \ge 0$. -\end{itemize} -After this pre-processing, the linear prover of {\tt lra} searches for a proof -by abstracting monomials by variables. - -\asection{{\tt nia}: a proof procedure for non-linear integer arithmetic} -\tacindex{nia} -\label{sec:nia} -The {\tt nia} tactic is a proof procedure for non-linear integer arithmetic. -% -It performs a pre-processing similar to {\tt nra}. The obtained goal is solved using the linear integer prover {\tt lia}. - -\asection{{\tt psatz}: a proof procedure for non-linear arithmetic} -\label{sec:psatz} -The {\tt psatz} tactic explores the $\mathit{Cone}$ by increasing degrees -- hence the depth parameter $n$. -In theory, such a proof search is complete -- if the goal is provable the search eventually stops. -Unfortunately, the external oracle is using numeric (approximate) optimization techniques that might miss a -refutation. - -To illustrate the working of the tactic, consider we wish to prove the following Coq goal. -\begin{coq_eval} -Require Import ZArith Psatz. -Open Scope Z_scope. -\end{coq_eval} -\begin{coq_example*} -Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. -\end{coq_example*} -\begin{coq_eval} -intro x; psatz Z 2. -\end{coq_eval} -Such a goal is solved by {\tt intro x; psatz Z 2}. The oracle returns the -cone expression $2 \times (\mathbf{x-1}) + (\mathbf{x-1}) \times -(\mathbf{x-1}) + \mathbf{-x^2}$ (polynomial hypotheses are printed in -bold). By construction, this expression belongs to $\mathit{Cone}(\{-x^2, -x -1\})$. Moreover, by running {\tt ring} we obtain $-1$. By -Theorem~\ref{thm:psatz}, the goal is valid. -% - -%% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a -%% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. -%% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. -% - - - -%%% 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 82765da6ed..0000000000 --- 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 231742e569..86f123322c 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,12 +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{Micromega.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 0000000000..6843e9eaa1 --- /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 0000000000..64d4eddf04 --- /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/micromega.rst b/doc/sphinx/addendum/micromega.rst new file mode 100644 index 0000000000..e850587c8a --- /dev/null +++ b/doc/sphinx/addendum/micromega.rst @@ -0,0 +1,252 @@ +.. _ micromega: + +Micromega: tactics for solving arithmetic goals over ordered rings +================================================================== + +:Authors: Frédéric Besson and Evgeny Makarov + +Short description of the tactics +-------------------------------- + +The Psatz module (``Require Import Psatz.``) gives access to several +tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}`, and :math:`\mathbb{R}` [#]_. +It also possible to get the tactics for integers by a ``Require Import Lia``, +rationals ``Require Import Lqa`` and reals ``Require Import Lra``. + ++ ``lia`` is a decision procedure for linear integer arithmetic (see Section :ref:`lia <lia>`); ++ ``nia`` is an incomplete proof procedure for integer non-linear + arithmetic (see Section :ref:`nia <nia>`); ++ ``lra`` is a decision procedure for linear (real or rational) arithmetic + (see Section :ref:`lra <lra>`); ++ ``nra`` is an incomplete proof procedure for non-linear (real or + rational) arithmetic (see Section :ref:`nra <nra>`); ++ ``psatz D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and + ``n`` is an optional integer limiting the proof search depth + is an incomplete proof procedure for non-linear arithmetic. + It is based on John Harrison’s HOL Light + driver to the external prover `csdp` [#]_. Note that the `csdp` driver is + generating a *proof cache* which makes it possible to rerun scripts + even without `csdp` (see Section :ref:`psatz <psatz>`). + +The tactics solve propositional formulas parameterized by atomic +arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. +The syntax of the formulas is the following: + + .. productionlist:: `F` + F : A ∣ P ∣ True ∣ False ∣ F 1 ∧ F 2 ∣ F 1 ∨ F 2 ∣ F 1 ↔ F 2 ∣ F 1 → F 2 ∣ ¬ F + A : p 1 = p 2 ∣ p 1 > p 2 ∣ p 1 < p 2 ∣ p 1 ≥ p 2 ∣ p 1 ≤ p 2 + p : c ∣ x ∣ −p ∣ p 1 − p 2 ∣ p 1 + p 2 ∣ p 1 × p 2 ∣ p ^ n + +where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the +operators :math:`−, +, ×` are respectively subtraction, addition, and product; +:math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. +For :math:`\mathbb{Q}`, equality is not Leibniz equality = but the equality of +rationals ==. + +For :math:`\mathbb{Z}` (resp. :math:`\mathbb{Q}`), :math:`c` ranges over integer constants (resp. rational +constants). For :math:`\mathbb{R}`, the tactic recognizes as real constants the +following expressions: + +:: + + c ::= R0 | R1 | Rmul(c,c) | Rplus(c,c) | Rminus(c,c) | IZR z | IQR q | Rdiv(c,c) | Rinv c + +where :math:`z` is a constant in :math:`\mathbb{Z}` and :math:`q` is a constant in :math:`\mathbb{Q}`. +This includes integer constants written using the decimal notation, *i.e.*, c%R. + + +*Positivstellensatz* refutations +-------------------------------- + +The name `psatz` is an abbreviation for *positivstellensatz* – literally +"positivity theorem" – which generalizes Hilbert’s *nullstellensatz*. It +relies on the notion of Cone. Given a (finite) set of polynomials :math:`S`, +:math:`\mathit{Cone}(S)` is inductively defined as the smallest set of polynomials +closed under the following rules: + +:math:`\begin{array}{l} +\dfrac{p \in S}{p \in \mathit{Cone}(S)} \quad +\dfrac{}{p^2 \in \mathit{Cone}(S)} \quad +\dfrac{p_1 \in \mathit{Cone}(S) \quad p_2 \in \mathit{Cone}(S) \quad +\Join \in \{+,*\}} {p_1 \Join p_2 \in \mathit{Cone}(S)}\\ +\end{array}` + +The following theorem provides a proof principle for checking that a +set of polynomial inequalities does not have solutions [#]_. + +.. _psatz_thm: + +**Theorem (Psatz)**. Let :math:`S` be a set of polynomials. +If :math:`-1` belongs to :math:`\mathit{Cone}(S)`, then the conjunction +:math:`\bigwedge_{p \in S} p\ge 0` is unsatisfiable. +A proof based on this theorem is called a *positivstellensatz* +refutation. The tactics work as follows. Formulas are normalized into +conjunctive normal form :math:`\bigwedge_i C_i` where :math:`C_i` has the +general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False})` and +:math:`\Join \in \{>,\ge,=\}` for :math:`D\in \{\mathbb{Q},\mathbb{R}\}` and +:math:`\Join \in \{\ge, =\}` for :math:`\mathbb{Z}`. + +For each conjunct :math:`C_i`, the tactic calls a oracle which searches for +:math:`-1` within the cone. Upon success, the oracle returns a *cone +expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) +and checked to be :math:`-1`. + +.. _lra: + +`lra`: a decision procedure for linear real and rational arithmetic +------------------------------------------------------------------- + +The `lra` tactic is searching for *linear* refutations using Fourier +elimination [#]_. As a result, this tactic explores a subset of the *Cone* +defined as + + :math:`\mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}` + +The deductive power of `lra` is the combined deductive power of +`ring_simplify` and `fourier`. There is also an overlap with the field +tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. + + +.. _lia: + +`lia`: a tactic for linear integer arithmetic +--------------------------------------------- + +The tactic lia offers an alternative to the omega and romega tactic +(see :ref:`omega`). Roughly speaking, the deductive power of lia is +the combined deductive power of `ring_simplify` and `omega`. However, it +solves linear goals that `omega` and `romega` do not solve, such as the +following so-called *omega nightmare* :cite:`TheOmegaPaper`. + +.. coqtop:: in + + Goal forall x y, + 27 <= 11 * x + 13 * y <= 45 -> + -10 <= 7 * x - 9 * y <= 4 -> False. + +The estimation of the relative efficiency of `lia` *vs* `omega` and `romega` +is under evaluation. + +High level view of `lia` +~~~~~~~~~~~~~~~~~~~~~~~~ + +Over :math:`\mathbb{R}`, *positivstellensatz* refutations are a complete proof +principle [#]_. However, this is not the case over :math:`\mathbb{Z}`. Actually, +*positivstellensatz* refutations are not even sufficient to decide +linear *integer* arithmetic. The canonical example is :math:`2 * x = 1 -> \mathtt{False}` +which is a theorem of :math:`\mathbb{Z}` but not a theorem of :math:`{\mathbb{R}}`. To remedy this +weakness, the `lia` tactic is using recursively a combination of: + ++ linear *positivstellensatz* refutations; ++ cutting plane proofs; ++ case split. + +Cutting plane proofs +~~~~~~~~~~~~~~~~~~~~~~ + +are a way to take into account the discreteness of :math:`\mathbb{Z}` by rounding up +(rational) constants up-to the closest integer. + +.. _ceil_thm: + +**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then + + :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil` + +For instance, from 2 x = 1 we can deduce + ++ :math:`x \ge 1/2` whose cut plane is :math:`x \ge \lceil{1/2}\rceil = 1`; ++ :math:`x \le 1/2` whose cut plane is :math:`x \le \lfloor{1/2}\rfloor = 0`. + +By combining these two facts (in normal form) :math:`x − 1 \ge 0` and +:math:`-x \ge 0`, we conclude by exhibiting a *positivstellensatz* refutation: +:math:`−1 \equiv x−1 + −x \in \mathit{Cone}({x−1,x})`. + +Cutting plane proofs and linear *positivstellensatz* refutations are a +complete proof principle for integer linear arithmetic. + +Case split +~~~~~~~~~~~ + +enumerates over the possible values of an expression. + +.. _casesplit_thm: + +**Theorem**. Let :math:`p` be an integer and :math:`c_1` and :math:`c_2` +integer constants. Then: + + :math:`c_1 \le p \le c_2 \Rightarrow \bigvee_{x \in [c_1,c_2]} p = x` + +Our current oracle tries to find an expression :math:`e` with a small range +:math:`[c_1,c_2]`. We generate :math:`c_2 − c_1` subgoals which contexts are enriched +with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively search for +a proof. + +.. _nra: + +`nra`: a proof procedure for non-linear arithmetic +-------------------------------------------------- + +The `nra` tactic is an *experimental* proof procedure for non-linear +arithmetic. The tactic performs a limited amount of non-linear +reasoning before running the linear prover of `lra`. This pre-processing +does the following: + + ++ If the context contains an arithmetic expression of the form + :math:`e[x^2]` where :math:`x` is a monomial, the context is enriched with + :math:`x^2 \ge 0`; ++ For all pairs of hypotheses :math:`e_1 \ge 0`, :math:`e_2 \ge 0`, the context is + enriched with :math:`e_1 \times e_2 \ge 0`. + +After this pre-processing, the linear prover of `lra` searches for a +proof by abstracting monomials by variables. + +.. _nia: + +`nia`: a proof procedure for non-linear integer arithmetic +---------------------------------------------------------- + +The `nia` tactic is a proof procedure for non-linear integer arithmetic. +It performs a pre-processing similar to `nra`. The obtained goal is +solved using the linear integer prover `lia`. + +.. _psatz: + +`psatz`: a proof procedure for non-linear arithmetic +---------------------------------------------------- + +The `psatz` tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the +depth parameter :math:`n`. In theory, such a proof search is complete – if the +goal is provable the search eventually stops. Unfortunately, the +external oracle is using numeric (approximate) optimization techniques +that might miss a refutation. + +To illustrate the working of the tactic, consider we wish to prove the +following Coq goal: + +.. coqtop:: all + + Require Import ZArith Psatz. + Open Scope Z_scope. + Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False. + intro x. + psatz Z 2. + +As shown, such a goal is solved by ``intro x. psatz Z 2.``. The oracle returns the +cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) + -x^2` +(polynomial hypotheses are printed in bold). By construction, this expression +belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running `ring` we +obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. + +.. [#] Support for `nat` and :math:`\mathbb{N}` is obtained by pre-processing the goal with + the `zify` tactic. +.. [#] Sources and binaries can be found at https://projects.coin-or.org/Csdp +.. [#] Variants deal with equalities and strict inequalities. +.. [#] More efficient linear programming techniques could equally be employed. +.. [#] In practice, the oracle might fail to produce such a refutation. + +.. comment in original TeX: +.. %% \paragraph{The {\tt sos} tactic} -- where {\tt sos} stands for \emph{sum of squares} -- tries to prove that a +.. %% single polynomial $p$ is positive by expressing it as a sum of squares \emph{i.e.,} $\sum_{i\in S} p_i^2$. +.. %% This amounts to searching for $p$ in the cone without generators \emph{i.e.}, $Cone(\{\})$. diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst new file mode 100644 index 0000000000..20e40c5507 --- /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 4a9bd6c1a0..247f32103c 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 4566db4945..c5d4936b18 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -43,6 +43,11 @@ Table of contents .. toctree:: :caption: Addendum + addendum/extended-pattern-matching + addendum/canonical-structures + addendum/omega + addendum/micromega + .. toctree:: :caption: Reference |