From db6262fd028086c6201fe4894243fcf691c65099 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 10:01:01 +0100 Subject: [Sphinx] Move chapter 17 to new infrastructure --- Makefile.doc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.doc') diff --git a/Makefile.doc b/Makefile.doc index df1e2d3c4..6f4bcfb67 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ + Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) -- cgit v1.2.3 From d2f43c7519f85d84ff8548aadfb8da46450b3acd Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 10:36:03 +0100 Subject: [Sphinx] Move chapter 19 to new infrastructure --- Makefile.doc | 2 +- doc/refman/CanonicalStructures.tex | 383 --------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/canonical-structures.rst | 383 +++++++++++++++++++++++++++ 4 files changed, 384 insertions(+), 385 deletions(-) delete mode 100644 doc/refman/CanonicalStructures.tex create mode 100644 doc/sphinx/addendum/canonical-structures.rst (limited to 'Makefile.doc') diff --git a/Makefile.doc b/Makefile.doc index df1e2d3c4..8830c69ea 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,7 +60,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ + Cases.v.tex Coercion.v.tex Extraction.v.tex \ Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) diff --git a/doc/refman/CanonicalStructures.tex b/doc/refman/CanonicalStructures.tex deleted file mode 100644 index 8961b0096..000000000 --- a/doc/refman/CanonicalStructures.tex +++ /dev/null @@ -1,383 +0,0 @@ -\achapter{Canonical Structures} -%HEVEA\cutname{canonical-structures.html} -\aauthor{Assia Mahboubi and Enrico Tassi} - -\label{CS-full} -\index{Canonical Structures!presentation} - -\noindent This chapter explains the basics of Canonical Structure and how they can be used -to overload notations and build a hierarchy of algebraic structures. -The examples are taken from~\cite{CSwcu}. We invite the interested reader -to refer to this paper for all the details that are omitted here for brevity. -The interested reader shall also find in~\cite{CSlessadhoc} a detailed -description of another, complementary, use of Canonical Structures: -advanced proof search. This latter papers also presents many techniques one -can employ to tune the inference of Canonical Structures. - -\section{Notation overloading} - -We build an infix notation $==$ for a comparison predicate. Such notation -will be overloaded, and its meaning will depend on the types of the terms -that are compared. - -\begin{coq_eval} -Require Import Arith. -\end{coq_eval} - -\begin{coq_example} -Module EQ. - Record class (T : Type) := Class { cmp : T -> T -> Prop }. - Structure type := Pack { obj : Type; class_of : class obj }. - Definition op (e : type) : obj e -> obj e -> Prop := - let 'Pack _ (Class _ the_cmp) := e in the_cmp. - Check op. - Arguments op {e} x y : simpl never. - Arguments Class {T} cmp. - Module theory. - Notation "x == y" := (op x y) (at level 70). - End theory. -End EQ. -\end{coq_example} - -We use Coq modules as name spaces. This allows us to follow the same pattern -and naming convention for the rest of the chapter. The base name space -contains the definitions of the algebraic structure. To keep the example -small, the algebraic structure \texttt{EQ.type} we are defining is very simplistic, -and characterizes terms on which a binary relation is defined, without -requiring such relation to validate any property. -The inner \texttt{theory} module contains the overloaded notation \texttt{==} and -will eventually contain lemmas holding on all the instances of the -algebraic structure (in this case there are no lemmas). - -Note that in practice the user may want to declare \texttt{EQ.obj} as a coercion, -but we will not do that here. - -The following line tests that, when we assume a type \texttt{e} that is in the -\texttt{EQ} class, then we can relates two of its objects with \texttt{==}. - -\begin{coq_example} -Import EQ.theory. -Check forall (e : EQ.type) (a b : EQ.obj e), a == b. -\end{coq_example} - -Still, no concrete type is in the \texttt{EQ} class. We amend that by equipping \texttt{nat} -with a comparison relation. - -\begin{coq_example} -Fail Check 3 == 3. -Definition nat_eq (x y : nat) := nat_compare x y = Eq. -Definition nat_EQcl : EQ.class nat := EQ.Class nat_eq. -Canonical Structure nat_EQty : EQ.type := EQ.Pack nat nat_EQcl. -Check 3 == 3. -Eval compute in 3 == 4. -\end{coq_example} - -This last test shows that Coq is now not only able to typecheck \texttt{3==3}, but -also that the infix relation was bound to the \texttt{nat\_eq} relation. This -relation is selected whenever \texttt{==} is used on terms of type \texttt{nat}. This -can be read in the line declaring the canonical structure \texttt{nat\_EQty}, -where the first argument to \texttt{Pack} is the key and its second argument -a group of canonical values associated to the key. In this case we associate -to \texttt{nat} only one canonical value (since its class, \texttt{nat\_EQcl} has just one -member). The use of the projection \texttt{op} requires its argument to be in -the class \texttt{EQ}, and uses such a member (function) to actually compare -its arguments. - -Similarly, we could equip any other type with a comparison relation, and -use the \texttt{==} notation on terms of this type. - -\subsection{Derived Canonical Structures} - -We know how to use \texttt{==} on base types, like \texttt{nat}, \texttt{bool}, \texttt{Z}. -Here we show how to deal with type constructors, i.e. how to make the -following example work: - -\begin{coq_example} -Fail Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). -\end{coq_example} - -The error message is telling that Coq has no idea on how to compare -pairs of objects. The following construction is telling Coq exactly how to do -that. - -\begin{coq_example} -Definition pair_eq (e1 e2 : EQ.type) (x y : EQ.obj e1 * EQ.obj e2) := - fst x == fst y /\ snd x == snd y. -Definition pair_EQcl e1 e2 := EQ.Class (pair_eq e1 e2). -Canonical Structure pair_EQty (e1 e2 : EQ.type) : EQ.type := - EQ.Pack (EQ.obj e1 * EQ.obj e2) (pair_EQcl e1 e2). -Check forall (e : EQ.type) (a b : EQ.obj e), (a,b) == (a,b). -Check forall n m : nat, (3,4) == (n,m). -\end{coq_example} - -Thanks to the \texttt{pair\_EQty} declaration, Coq is able to build a comparison -relation for pairs whenever it is able to build a comparison relation -for each component of the pair. The declaration associates to the key -\texttt{*} (the type constructor of pairs) the canonical comparison relation -\texttt{pair\_eq} whenever the type constructor \texttt{*} is applied to two types -being themselves in the \texttt{EQ} class. - -\section{Hierarchy of structures} - -To get to an interesting example we need another base class to be available. -We choose the class of types that are equipped with an order relation, -to which we associate the infix \texttt{<=} notation. - -\begin{coq_example} -Module LE. - Record class T := Class { cmp : T -> T -> Prop }. - Structure type := Pack { obj : Type; class_of : class obj }. - Definition op (e : type) : obj e -> obj e -> Prop := - let 'Pack _ (Class _ f) := e in f. - Arguments op {_} x y : simpl never. - Arguments Class {T} cmp. - Module theory. - Notation "x <= y" := (op x y) (at level 70). - End theory. -End LE. -\end{coq_example} - -As before we register a canonical \texttt{LE} class for \texttt{nat}. - -\begin{coq_example} -Import LE.theory. -Definition nat_le x y := nat_compare x y <> Gt. -Definition nat_LEcl : LE.class nat := LE.Class nat_le. -Canonical Structure nat_LEty : LE.type := LE.Pack nat nat_LEcl. -\end{coq_example} - -And we enable Coq to relate pair of terms with \texttt{<=}. - -\begin{coq_example} -Definition pair_le e1 e2 (x y : LE.obj e1 * LE.obj e2) := - fst x <= fst y /\ snd x <= snd y. -Definition pair_LEcl e1 e2 := LE.Class (pair_le e1 e2). -Canonical Structure pair_LEty (e1 e2 : LE.type) : LE.type := - LE.Pack (LE.obj e1 * LE.obj e2) (pair_LEcl e1 e2). -Check (3,4,5) <= (3,4,5). -\end{coq_example} - -At the current stage we can use \texttt{==} and \texttt{<=} on concrete types, -like tuples of natural numbers, but we can't develop an algebraic -theory over the types that are equipped with both relations. - -\begin{coq_example} -Check 2 <= 3 /\ 2 == 2. -Fail Check forall (e : EQ.type) (x y : EQ.obj e), x <= y -> y <= x -> x == y. -Fail Check forall (e : LE.type) (x y : LE.obj e), x <= y -> y <= x -> x == y. -\end{coq_example} - -We need to define a new class that inherits from both \texttt{EQ} and \texttt{LE}. - -\begin{coq_example} -Module LEQ. - Record mixin (e : EQ.type) (le : EQ.obj e -> EQ.obj e -> Prop) := - Mixin { compat : forall x y : EQ.obj e, le x y /\ le y x <-> x == y }. - Record class T := Class { - EQ_class : EQ.class T; - LE_class : LE.class T; - extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; class_of : class obj }. - Arguments Mixin {e le} _. - Arguments Class {T} _ _ _. -\end{coq_example} - -The \texttt{mixin} component of the \texttt{LEQ} class contains all the extra content -we are adding to \texttt{EQ} and \texttt{LE}. In particular it contains the requirement -that the two relations we are combining are compatible. - -Unfortunately there is still an obstacle to developing the algebraic theory -of this new class. - -\begin{coq_example} - Module theory. - Fail Check forall (le : type) (n m : obj le), n <= m -> n <= m -> n == m. -\end{coq_example} - -The problem is that the two classes \texttt{LE} and \texttt{LEQ} are not yet related by -a subclass relation. In other words Coq does not see that an object -of the \texttt{LEQ} class is also an object of the \texttt{LE} class. - -The following two constructions tell Coq how to canonically build -the \texttt{LE.type} and \texttt{EQ.type} structure given an \texttt{LEQ.type} structure -on the same type. - -\begin{coq_example} - Definition to_EQ (e : type) : EQ.type := - EQ.Pack (obj e) (EQ_class _ (class_of e)). - Canonical Structure to_EQ. - Definition to_LE (e : type) : LE.type := - LE.Pack (obj e) (LE_class _ (class_of e)). - Canonical Structure to_LE. -\end{coq_example} -We can now formulate out first theorem on the objects of the \texttt{LEQ} structure. -\begin{coq_example} - Lemma lele_eq (e : type) (x y : obj e) : x <= y -> y <= x -> x == y. - now intros; apply (compat _ _ (extra _ (class_of e)) x y); split. Qed. - Arguments lele_eq {e} x y _ _. - End theory. -End LEQ. -Import LEQ.theory. -Check lele_eq. -\end{coq_example} - -Of course one would like to apply results proved in the algebraic -setting to any concrete instate of the algebraic structure. - -\begin{coq_example} -Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. - Fail apply (lele_eq n m). Abort. -Example test_algebraic2 (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : - n <= m -> m <= n -> n == m. - Fail apply (lele_eq n m). Abort. -\end{coq_example} - -Again one has to tell Coq that the type \texttt{nat} is in the \texttt{LEQ} class, and how -the type constructor \texttt{*} interacts with the \texttt{LEQ} class. In the following -proofs are omitted for brevity. - -\begin{coq_example} -Lemma nat_LEQ_compat (n m : nat) : n <= m /\ m <= n <-> n == m. -\end{coq_example} -\begin{coq_eval} - -split. - unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq. - case (nat_compare_spec n m); [ reflexivity | | now intros _ [H _]; case H ]. - now intro H; apply nat_compare_gt in H; rewrite -> H; intros [_ K]; case K. -unfold EQ.op; unfold LE.op; simpl; unfold nat_le; unfold nat_eq. -case (nat_compare_spec n m); [ | intros H1 H2; discriminate H2 .. ]. -intro H; rewrite H; intros _; split; [ intro H1; discriminate H1 | ]. -case (nat_compare_eq_iff m m); intros _ H1. -now rewrite H1; auto; intro H2; discriminate H2. -Qed. -\end{coq_eval} -\begin{coq_example} -Definition nat_LEQmx := LEQ.Mixin nat_LEQ_compat. -Lemma pair_LEQ_compat (l1 l2 : LEQ.type) (n m : LEQ.obj l1 * LEQ.obj l2) : -n <= m /\ m <= n <-> n == m. -\end{coq_example} -\begin{coq_eval} - -case n; case m; unfold EQ.op; unfold LE.op; simpl. -intros n1 n2 m1 m2; split; [ intros [[Le1 Le2] [Ge1 Ge2]] | intros [H1 H2] ]. - now split; apply lele_eq. -case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l1)) m1 n1). -case (LEQ.compat _ _ (LEQ.extra _ (LEQ.class_of l2)) m2 n2). -intros _ H3 _ H4; apply H3 in H2; apply H4 in H1; clear H3 H4. -now case H1; case H2; split; split. -Qed. -\end{coq_eval} -\begin{coq_example} -Definition pair_LEQmx l1 l2 := LEQ.Mixin (pair_LEQ_compat l1 l2). -\end{coq_example} - -The following script registers an \texttt{LEQ} class for \texttt{nat} and for the -type constructor \texttt{*}. It also tests that they work as expected. - -Unfortunately, these declarations are very verbose. In the following -subsection we show how to make these declaration more compact. - -\begin{coq_example} -Module Add_instance_attempt. - Canonical Structure nat_LEQty : LEQ.type := - LEQ._Pack nat (LEQ.Class nat_EQcl nat_LEcl nat_LEQmx). - Canonical Structure pair_LEQty (l1 l2 : LEQ.type) : LEQ.type := - LEQ._Pack (LEQ.obj l1 * LEQ.obj l2) - (LEQ.Class - (EQ.class_of (pair_EQty (to_EQ l1) (to_EQ l2))) - (LE.class_of (pair_LEty (to_LE l1) (to_LE l2))) - (pair_LEQmx l1 l2)). - Example test_algebraic (n m : nat) : n <= m -> m <= n -> n == m. - now apply (lele_eq n m). Qed. - Example test_algebraic2 (n m : nat * nat) : n <= m -> m <= n -> n == m. - now apply (lele_eq n m). Qed. -End Add_instance_attempt. -\end{coq_example} - -Note that no direct proof of \texttt{n <= m -> m <= n -> n == m} is provided by the -user for \texttt{n} and \texttt{m} of type \texttt{nat * nat}. What the user provides is a proof of -this statement for \texttt{n} and \texttt{m} of type \texttt{nat} and a proof that the pair -constructor preserves this property. The combination of these two facts is a -simple form of proof search that Coq performs automatically while inferring -canonical structures. - -\subsection{Compact declaration of Canonical Structures} - -We need some infrastructure for that. - -\begin{coq_example*} -Require Import Strings.String. -\end{coq_example*} -\begin{coq_example} -Module infrastructure. - Inductive phantom {T : Type} (t : T) : Type := Phantom. - Definition unify {T1 T2} (t1 : T1) (t2 : T2) (s : option string) := - phantom t1 -> phantom t2. - Definition id {T} {t : T} (x : phantom t) := x. - Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p) - (at level 50, v ident, only parsing). - Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p) - (at level 50, v ident, only parsing). - Notation "'Error : t : s" := (unify _ t (Some s)) - (at level 50, format "''Error' : t : s"). - Open Scope string_scope. -End infrastructure. -\end{coq_example} - -To explain the notation \texttt{[find v | t1 \textasciitilde t2]} let us pick one -of its instances: \texttt{[find e | EQ.obj e \textasciitilde T | "is not an EQ.type" ]}. -It should be read as: ``find a class e such that its objects have type T -or fail with message "T is not an EQ.type"''. - -The other utilities are used to ask Coq to solve a specific unification -problem, that will in turn require the inference of some canonical -structures. They are explained in mode details in~\cite{CSwcu}. - -We now have all we need to create a compact ``packager'' to declare -instances of the \texttt{LEQ} class. - -\begin{coq_example} -Import infrastructure. -Definition packager T e0 le0 (m0 : LEQ.mixin e0 le0) := - [find e | EQ.obj e ~ T | "is not an EQ.type" ] - [find o | LE.obj o ~ T | "is not an LE.type" ] - [find ce | EQ.class_of e ~ ce ] - [find co | LE.class_of o ~ co ] - [find m | m ~ m0 | "is not the right mixin" ] - LEQ._Pack T (LEQ.Class ce co m). -Notation Pack T m := (packager T _ _ m _ id _ id _ id _ id _ id). -\end{coq_example} - -The object \texttt{Pack} takes a type \texttt{T} (the key) and a mixin \texttt{m}. It infers all -the other pieces of the class \texttt{LEQ} and declares them as canonical values -associated to the \texttt{T} key. All in all, the only new piece of information -we add in the \texttt{LEQ} class is the mixin, all the rest is already canonical -for \texttt{T} and hence can be inferred by Coq. - -\texttt{Pack} is a notation, hence it is not type checked at the time of its -declaration. It will be type checked when it is used, an in that case -\texttt{T} is going to be a concrete type. The odd arguments \texttt{\_} and \texttt{id} we -pass to the -packager represent respectively the classes to be inferred (like \texttt{e}, \texttt{o}, etc) and a token (\texttt{id}) to force their inference. Again, for all the details the -reader can refer to~\cite{CSwcu}. - -The declaration of canonical instances can now be way more compact: - -\begin{coq_example} -Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. -Canonical Structure pair_LEQty (l1 l2 : LEQ.type) := - Eval hnf in Pack (LEQ.obj l1 * LEQ.obj l2) (pair_LEQmx l1 l2). -\end{coq_example} - -Error messages are also quite intelligible (if one skips to the end of -the message). - -\begin{coq_example} -Fail Canonical Structure err := Eval hnf in Pack bool nat_LEQmx. -\end{coq_example} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 231742e56..dedead7f5 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -119,7 +119,6 @@ Options A and B of the licence are {\em not} elected.} \include{AddRefMan-pre}% \include{Cases.v}% \include{Coercion.v}% -\include{CanonicalStructures.v}% \include{Classes.v}% \include{Omega.v}% \include{Micromega.v} diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst new file mode 100644 index 000000000..8961b0096 --- /dev/null +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -0,0 +1,383 @@ +\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: -- cgit v1.2.3 From 179aa79f50f4be2c9db3f818413f147f3ad7e2c4 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 11:21:16 +0100 Subject: [Sphinx] Move chapter 21 to new infrastructure --- Makefile.doc | 2 +- doc/refman/Omega.tex | 249 ---------------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/omega.rst | 249 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 250 insertions(+), 251 deletions(-) delete mode 100644 doc/refman/Omega.tex create mode 100644 doc/sphinx/addendum/omega.rst (limited to 'Makefile.doc') diff --git a/Makefile.doc b/Makefile.doc index df1e2d3c4..b46d93373 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -61,7 +61,7 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ Cases.v.tex Coercion.v.tex CanonicalStructures.v.tex Extraction.v.tex \ - Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ + Program.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \ Setoid.v.tex Classes.v.tex Universes.v.tex \ Misc.v.tex) diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex deleted file mode 100644 index 82765da6e..000000000 --- a/doc/refman/Omega.tex +++ /dev/null @@ -1,249 +0,0 @@ -\achapter{Omega: a solver of quantifier-free problems in -Presburger Arithmetic} -%HEVEA\cutname{omega.html} -\aauthor{Pierre Crégut} -\label{OmegaChapter} - -\asection{Description of {\tt omega}} -\tacindex{omega} -\label{description} - -{\tt omega} solves a goal in Presburger arithmetic, i.e. a universally -quantified formula made of equations and inequations. Equations may -be specified either on the type \verb=nat= of natural numbers or on -the type \verb=Z= of binary-encoded integer numbers. Formulas on -\verb=nat= are automatically injected into \verb=Z=. The procedure -may use any hypothesis of the current proof session to solve the goal. - -Multiplication is handled by {\tt omega} but only goals where at -least one of the two multiplicands of products is a constant are -solvable. This is the restriction meant by ``Presburger arithmetic''. - -If the tactic cannot solve the goal, it fails with an error message. -In any case, the computation eventually stops. - -\asubsection{Arithmetical goals recognized by {\tt omega}} - -{\tt omega} applied only to quantifier-free formulas built from the -connectors - -\begin{quote} -\verb=/\, \/, ~, ->= -\end{quote} - -on atomic formulas. Atomic formulas are built from the predicates - -\begin{quote} -\verb!=, le, lt, gt, ge! -\end{quote} - - on \verb=nat= or from the predicates - -\begin{quote} -\verb!=, <, <=, >, >=! -\end{quote} - - on \verb=Z=. In expressions of type \verb=nat=, {\tt omega} recognizes - -\begin{quote} -\verb!plus, minus, mult, pred, S, O! -\end{quote} - -and in expressions of type \verb=Z=, {\tt omega} recognizes - -\begin{quote} -\verb!+, -, *, Z.succ!, and constants. -\end{quote} - -All expressions of type \verb=nat= or \verb=Z= not built on these -operators are considered abstractly as if they -were arbitrary variables of type \verb=nat= or \verb=Z=. - -\asubsection{Messages from {\tt omega}} -\label{errors} - -When {\tt omega} does not solve the goal, one of the following errors -is generated: - -\begin{ErrMsgs} - -\item \errindex{omega can't solve this system} - - This may happen if your goal is not quantifier-free (if it is - universally quantified, try {\tt intros} first; if it contains - existentials quantifiers too, {\tt omega} is not strong enough to solve your - goal). This may happen also if your goal contains arithmetical - operators unknown from {\tt omega}. Finally, your goal may be really - wrong! - -\item \errindex{omega: Not a quantifier-free goal} - - If your goal is universally quantified, you should first apply {\tt - intro} as many time as needed. - -\item \errindex{omega: Unrecognized predicate or connective: {\sl ident}} - -\item \errindex{omega: Unrecognized atomic proposition: {\sl prop}} - -\item \errindex{omega: Can't solve a goal with proposition variables} - -\item \errindex{omega: Unrecognized proposition} - -\item \errindex{omega: Can't solve a goal with non-linear products} - -\item \errindex{omega: Can't solve a goal with equality on {\sl type}} - -\end{ErrMsgs} - -%% This code is currently unplugged -%% -% \asubsection{Control over the output} -% There are some flags that can be set to get more information on the procedure - -% \begin{itemize} -% \item \verb=Time= to get the time used by the procedure -% \item \verb=System= to visualize the normalized systems. -% \item \verb=Action= to visualize the actions performed by the OMEGA -% procedure (see \ref{technical}). -% \end{itemize} - -% \comindex{Set omega Time} -% \comindex{UnSet omega Time} -% \comindex{Switch omega Time} -% \comindex{Set omega System} -% \comindex{UnSet omega System} -% \comindex{Switch omega System} -% \comindex{Set omega Action} -% \comindex{UnSet omega Action} -% \comindex{Switch omega Action} - -% Use {\tt Set omega {\rm\sl flag}} to set the flag -% {\rm\sl flag}. Use {\tt Unset omega {\rm\sl flag}} to unset it and -% {\tt Switch omega {\rm\sl flag}} to toggle it. - -\section{Using {\tt omega}} - -The {\tt omega} tactic does not belong to the core system. It should be -loaded by -\begin{coq_example*} -Require Import Omega. -Open Scope Z_scope. -\end{coq_example*} - -\example{} - -\begin{coq_example} -Goal forall m n:Z, 1 + 2 * m <> 2 * n. -intros; omega. -\end{coq_example} -\begin{coq_eval} -Abort. -\end{coq_eval} - -\example{} - -\begin{coq_example} -Goal forall z:Z, z > 0 -> 2 * z + 1 > z. -intro; omega. -\end{coq_example} - -% Other examples can be found in \verb+$COQLIB/theories/DEMOS/OMEGA+. - -\section{Options} - -\begin{quote} - \optindex{Stable Omega} - {\tt Unset Stable Omega} -\end{quote} -This deprecated option (on by default) is for compatibility with Coq -pre 8.5. It resets internal name counters to make executions of -{\tt omega} independent. - -\begin{quote} - \optindex{Omega UseLocalDefs} - {\tt Unset Omega UseLocalDefs} -\end{quote} -This option (on by default) allows {\tt omega} to use the bodies of -local variables. - -\begin{quote} - \optindex{Omega System} - {\tt Set Omega System} - \optindex{Omega Action} - {\tt Set Omega Action} -\end{quote} -These two options (off by default) activate the printing of debug -information. - -\asection{Technical data} -\label{technical} - -\asubsection{Overview of the tactic} -\begin{itemize} - -\item The goal is negated twice and the first negation is introduced as an - hypothesis. -\item Hypothesis are decomposed in simple equations or inequations. Multiple - goals may result from this phase. -\item Equations and inequations over \verb=nat= are translated over - \verb=Z=, multiple goals may result from the translation of - substraction. -\item Equations and inequations are normalized. -\item Goals are solved by the {\it OMEGA} decision procedure. -\item The script of the solution is replayed. - -\end{itemize} - -\asubsection{Overview of the {\it OMEGA} decision procedure} - -The {\it OMEGA} decision procedure involved in the {\tt omega} tactic uses -a small subset of the decision procedure presented in - -\begin{quote} - "The Omega Test: a fast and practical integer programming -algorithm for dependence analysis", William Pugh, Communication of the -ACM , 1992, p 102-114. -\end{quote} - -Here is an overview, look at the original paper for more information. - -\begin{itemize} - -\item Equations and inequations are normalized by division by the GCD of their - coefficients. -\item Equations are eliminated, using the Banerjee test to get a coefficient - equal to one. -\item Note that each inequation defines a half space in the space of real value - of the variables. - \item Inequations are solved by projecting on the hyperspace - defined by cancelling one of the variable. They are partitioned - according to the sign of the coefficient of the eliminated - variable. Pairs of inequations from different classes define a - new edge in the projection. - \item Redundant inequations are eliminated or merged in new - equations that can be eliminated by the Banerjee test. -\item The last two steps are iterated until a contradiction is reached - (success) or there is no more variable to eliminate (failure). - -\end{itemize} - -It may happen that there is a real solution and no integer one. The last -steps of the Omega procedure (dark shadow) are not implemented, so the -decision procedure is only partial. - -\asection{Bugs} - -\begin{itemize} -\item The simplification procedure is very dumb and this results in - many redundant cases to explore. - -\item Much too slow. - -\item Certainly other bugs! You can report them to \url{https://coq.inria.fr/bugs/}. - -\end{itemize} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 231742e56..afc1b9c57 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -121,7 +121,6 @@ Options A and B of the licence are {\em not} elected.} \include{Coercion.v}% \include{CanonicalStructures.v}% \include{Classes.v}% -\include{Omega.v}% \include{Micromega.v} \include{Extraction.v}% \include{Program.v}% diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst new file mode 100644 index 000000000..82765da6e --- /dev/null +++ b/doc/sphinx/addendum/omega.rst @@ -0,0 +1,249 @@ +\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: -- cgit v1.2.3