Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Legacy Ring and Legacy Field migrated to contribs

 One slight point to check someday : fourier used to
 launch a tactic called Ring.polynom in some cases.
 It it crucial ? If so, how to replace with the setoid_ring
 equivalent ?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit 2ed6aeb03fc0e25a47223189d8444cbb6b749f2d 1 parent afe903e
letouzey authored
Showing with 12 additions and 6,687 deletions.
  1. +3 −5 Makefile.build
  2. +7 −11 Makefile.common
  3. +0 −275 doc/refman/Polynom.tex
  4. +0 −1  doc/stdlib/index-list.html.template
  5. +0 −14 plugins/field/LegacyField.v
  6. +0 −36 plugins/field/LegacyField_Compl.v
  7. +0 −431 plugins/field/LegacyField_Tactic.v
  8. +0 −648 plugins/field/LegacyField_Theory.v
  9. +0 −192 plugins/field/field.ml4
  10. +0 −2  plugins/field/field_plugin.mllib
  11. +0 −4 plugins/field/vo.itarget
  12. +1 −2  plugins/fourier/Fourier.v
  13. +1 −1  plugins/fourier/fourierR.ml
  14. +0 −1  plugins/micromega/Psatz.v
  15. +0 −1  plugins/micromega/g_micromega.ml4
  16. +0 −2  plugins/pluginsbyte.itarget
  17. +0 −2  plugins/pluginsopt.itarget
  18. +0 −2  plugins/pluginsvo.itarget
  19. +0 −88 plugins/ring/LegacyArithRing.v
  20. +0 −43 plugins/ring/LegacyNArithRing.v
  21. +0 −35 plugins/ring/LegacyRing.v
  22. +0 −374 plugins/ring/LegacyRing_theory.v
  23. +0 −35 plugins/ring/LegacyZArithRing.v
  24. +0 −700 plugins/ring/Ring_abstract.v
  25. +0 −897 plugins/ring/Ring_normalize.v
  26. +0 −12 plugins/ring/Setoid_ring.v
  27. +0 −1,160 plugins/ring/Setoid_ring_normalize.v
  28. +0 −425 plugins/ring/Setoid_ring_theory.v
  29. +0 −134 plugins/ring/g_ring.ml4
  30. +0 −929 plugins/ring/ring.ml
  31. +0 −3  plugins/ring/ring_plugin.mllib
  32. +0 −10 plugins/ring/vo.itarget
  33. +0 −74 plugins/setoid_ring/Ring_equiv.v
  34. +0 −1  plugins/setoid_ring/vo.itarget
  35. +0 −76 test-suite/success/LegacyField.v
  36. +0 −22 theories/QArith/Qreals.v
  37. +0 −38 theories/Reals/LegacyRfield.v
  38. +0 −1  theories/Reals/vo.itarget
8 Makefile.build
View
@@ -433,18 +433,16 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
# 3) plugins
###########################################################################
-.PHONY: plugins omega micromega ring setoid_ring nsatz xml extraction
-.PHONY: field fourier funind cc rtauto btauto pluginsopt
+.PHONY: plugins omega micromega setoid_ring nsatz xml extraction
+.PHONY: fourier funind cc rtauto btauto pluginsopt
plugins: $(PLUGINSVO)
omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
micromega: $(MICROMEGAVO) $(MICROMEGACMA) $(CSDPCERT)
-ring: $(RINGVO) $(RINGCMA)
-setoid_ring: $(NEWRINGVO) $(NEWRINGCMA)
+setoid_ring: $(RINGVO) $(RINGCMA)
nsatz: $(NSATZVO) $(NSATZCMA)
xml: $(XMLVO) $(XMLCMA)
extraction: $(EXTRACTIONCMA)
-field: $(FIELDVO) $(FIELDCMA)
fourier: $(FOURIERVO) $(FOURIERCMA)
funind: $(FUNINDCMA) $(FUNINDVO)
cc: $(CCVO) $(CCCMA)
18 Makefile.common
View
@@ -74,9 +74,9 @@ SRCDIRS:=\
pretyping interp toplevel/utils toplevel parsing \
printing grammar intf ide/utils ide \
$(addprefix plugins/, \
- omega romega micromega quote ring \
+ omega romega micromega quote \
setoid_ring xml extraction fourier \
- cc funind firstorder field \
+ cc funind firstorder \
rtauto nsatz syntax decl_mode btauto)
# Order is relevent here because kernel and checker contain files
@@ -166,10 +166,8 @@ OMEGACMA:=plugins/omega/omega_plugin.cma
ROMEGACMA:=plugins/romega/romega_plugin.cma
MICROMEGACMA:=plugins/micromega/micromega_plugin.cma
QUOTECMA:=plugins/quote/quote_plugin.cma
-RINGCMA:=plugins/ring/ring_plugin.cma
-NEWRINGCMA:=plugins/setoid_ring/newring_plugin.cma
+RINGCMA:=plugins/setoid_ring/newring_plugin.cma
NSATZCMA:=plugins/nsatz/nsatz_plugin.cma
-FIELDCMA:=plugins/field/field_plugin.cma
XMLCMA:=plugins/xml/xml_plugin.cma
FOURIERCMA:=plugins/fourier/fourier_plugin.cma
EXTRACTIONCMA:=plugins/extraction/extraction_plugin.cma
@@ -188,7 +186,7 @@ OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
- $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(FIELDCMA) \
+ $(QUOTECMA) $(RINGCMA) \
$(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
$(CCCMA) $(FOCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
$(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
@@ -300,9 +298,7 @@ OMEGAVO:=$(call cat_vo_itarget, plugins/omega)
ROMEGAVO:=$(call cat_vo_itarget, plugins/romega)
MICROMEGAVO:=$(call cat_vo_itarget, plugins/micromega)
QUOTEVO:=$(call cat_vo_itarget, plugins/quote)
-RINGVO:=$(call cat_vo_itarget, plugins/ring)
-FIELDVO:=$(call cat_vo_itarget, plugins/field)
-NEWRINGVO:=$(call cat_vo_itarget, plugins/setoid_ring)
+RINGVO:=$(call cat_vo_itarget, plugins/setoid_ring)
NSATZVO:=$(call cat_vo_itarget, plugins/nsatz)
FOURIERVO:=$(call cat_vo_itarget, plugins/fourier)
FUNINDVO:=$(call cat_vo_itarget, plugins/funind)
@@ -312,9 +308,9 @@ EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
XMLVO:=
CCVO:=
-PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
+PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) \
$(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
- $(RTAUTOVO) $(BTAUTOVO) $(NEWRINGVO) $(QUOTEVO) \
+ $(RTAUTOVO) $(BTAUTOVO) $(RINGVO) $(QUOTEVO) \
$(NSATZVO) $(EXTRACTIONVO)
ALLVO:= $(THEORIESVO) $(PLUGINSVO)
275 doc/refman/Polynom.tex
View
@@ -637,281 +637,6 @@
on coefficients w.r.t. the field equality.
\end{description}
-\asection{Legacy implementation}
-
-\Warning This tactic is the {\tt ring} tactic of previous versions of
-\Coq{} and it should be considered as deprecated. It will probably be
-removed in future releases. It has been kept only for compatibility
-reasons and in order to help moving existing code to the newer
-implementation described above. For more details, please refer to the
-Coq Reference Manual, version 8.0.
-
-
-\subsection{\tt legacy ring \term$_1$ \dots\ \term$_n$
-\tacindex{legacy ring}
-\comindex{Add Legacy Ring}
-\comindex{Add Legacy Semi Ring}}
-
-This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
-associative commutative rewriting on every ring. The tactic must be
-loaded by \texttt{Require Import LegacyRing}. The ring must be declared in
-the \texttt{Add Ring} command. The ring of booleans (with \texttt{andb}
-as multiplication and \texttt{xorb} as addition)
-is predefined; if one wants to use the tactic on \texttt{nat} one must
-first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do
-\texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require
-Import LegacyNArithRing}.
-
-The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal
-conclusion. The tactic \texttt{ring} normalizes these terms
-w.r.t. associativity and commutativity and replace them by their
-normal form.
-
-\begin{Variants}
-\item \texttt{legacy ring} When the goal is an equality $t_1=t_2$, it
- acts like \texttt{ring\_simplify} $t_1$ $t_2$ and then
- solves the equality by reflexivity.
-
-\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
- S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
- proof that \texttt{forall (n:nat), S n = plus (S O) n}.
-
-\end{Variants}
-
-You can have a look at the files \texttt{LegacyRing.v},
-\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
-\texttt{Add Ring} command.
-
-\subsection{Add a ring structure}
-
-It can be done in the \Coq toplevel (No ML file to edit and to link
-with \Coq). First, \texttt{ring} can handle two kinds of structure:
-rings and semi-rings. Semi-rings are like rings without an opposite to
-addition. Their precise specification (in \gallina) can be found in
-the file
-
-\begin{quotation}
-\begin{verbatim}
-plugins/ring/Ring_theory.v
-\end{verbatim}
-\end{quotation}
-
-The typical example of ring is \texttt{Z}, the typical
-example of semi-ring is \texttt{nat}.
-
-The specification of a
-ring is divided in two parts: first the record of constants
-($\oplus$, $\otimes$, 1, 0, $\ominus$) and then the theorems
-(associativity, commutativity, etc.).
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Section Theory_of_semi_rings.
-
-Variable A : Type.
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-(* There is also a "weakly decidable" equality on A. That means
- that if (A_eq x y)=true then x=y but x=y can arise when
- (A_eq x y)=false. On an abstract ring the function [x,y:A]false
- is a good choice. The proof of A_eq_prop is in this case easy. *)
-Variable Aeq : A -> A -> bool.
-
-Record Semi_Ring_Theory : Prop :=
-{ SR_plus_sym : (n,m:A)[| n + m == m + n |];
- SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
-
- SR_mult_sym : (n,m:A)[| n*m == m*n |];
- SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
- SR_plus_zero_left :(n:A)[| 0 + n == n|];
- SR_mult_one_left : (n:A)[| 1*n == n |];
- SR_mult_zero_left : (n:A)[| 0*n == 0 |];
- SR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
- SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p;
- SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
-}.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Section Theory_of_rings.
-
-Variable A : Type.
-
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-Variable Aopp : A -> A.
-Variable Aeq : A -> A -> bool.
-
-
-Record Ring_Theory : Prop :=
-{ Th_plus_sym : (n,m:A)[| n + m == m + n |];
- Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
- Th_mult_sym : (n,m:A)[| n*m == m*n |];
- Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
- Th_plus_zero_left :(n:A)[| 0 + n == n|];
- Th_mult_one_left : (n:A)[| 1*n == n |];
- Th_opp_def : (n:A) [| n + (-n) == 0 |];
- Th_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
- Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
-}.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-To define a ring structure on A, you must provide an addition, a
-multiplication, an opposite function and two unities 0 and 1.
-
-You must then prove all theorems that make
-(A,Aplus,Amult,Aone,Azero,Aeq)
-a ring structure, and pack them with the \verb|Build_Ring_Theory|
-constructor.
-
-Finally to register a ring the syntax is:
-
-\comindex{Add Legacy Ring}
-\begin{quotation}
- \texttt{Add Legacy Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}
- \texttt{[} \textit{c1 \dots cn} \texttt{].}
-\end{quotation}
-
-\noindent where \textit{A} is a term of type \texttt{Set},
-\textit{Aplus} is a term of type \texttt{A->A->A},
-\textit{Amult} is a term of type \texttt{A->A->A},
-\textit{Aone} is a term of type \texttt{A},
-\textit{Azero} is a term of type \texttt{A},
-\textit{Ainv} is a term of type \texttt{A->A},
-\textit{Aeq} is a term of type \texttt{A->bool},
-\textit{T} is a term of type
-\texttt{(Ring\_Theory }\textit{A Aplus Amult Aone Azero Ainv
- Aeq}\texttt{)}.
-The arguments \textit{c1 \dots cn},
-are the names of constructors which define closed terms: a
-subterm will be considered as a constant if it is either one of the
-terms \textit{c1 \dots cn} or the application of one of these terms to
-closed terms. For \texttt{nat}, the given constructors are \texttt{S}
-and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
-\texttt{(S (S O))}, \ldots
-
-\begin{Variants}
-\item \texttt{Add Legacy Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T}
- \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Legacy Semi
- Ring}
-
- There are two differences with the \texttt{Add Ring} command: there
- is no inverse function and the term $T$ must be of type
- \texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero
- Aeq}\texttt{)}.
-
-\item \texttt{Add Legacy Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv
- Aeq T}\texttt{.}\comindex{Add Legacy Abstract Ring}
-
- This command should be used for when the operations of rings are not
- computable; for example the real numbers of
- \texttt{theories/REALS/}. Here $0+1$ is not beta-reduced to $1$ but
- you still may want to \textit{rewrite} it to $1$ using the ring
- axioms. The argument \texttt{Aeq} is not used; a good choice for
- that function is \verb+[x:A]false+.
-
-\item \texttt{Add Legacy Abstract Semi Ring} \textit{A Aplus Amult Aone Azero
- Aeq T}\texttt{.}\comindex{Add Legacy Abstract Semi Ring}
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{Not a valid (semi)ring theory}.
-
- That happens when the typing condition does not hold.
-\end{ErrMsgs}
-
-Currently, the hypothesis is made than no more than one ring structure
-may be declared for a given type in \texttt{Set} or \texttt{Type}.
-This allows automatic detection of the theory used to achieve the
-normalization. On popular demand, we can change that and allow several
-ring structures on the same set.
-
-The table of ring theories is compatible with the \Coq\
-sectioning mechanism. If you declare a ring inside a section, the
-declaration will be thrown away when closing the section.
-And when you load a compiled file, all the \texttt{Add Ring}
-commands of this file that are not inside a section will be loaded.
-
-The typical example of ring is \texttt{Z}, and the typical example of
-semi-ring is \texttt{nat}. Another ring structure is defined on the
-booleans.
-
-\Warning Only the ring of booleans is loaded by default with the
-\texttt{Ring} module. To load the ring structure for \texttt{nat},
-load the module \texttt{ArithRing}, and for \texttt{Z},
-load the module \texttt{ZArithRing}.
-
-\subsection{\tt legacy field
-\tacindex{legacy field}}
-
-This tactic written by David~Delahaye and Micaela~Mayero solves equalities
-using commutative field theory. Denominators have to be non equal to zero and,
-as this is not decidable in general, this tactic may generate side conditions
-requiring some expressions to be non equal to zero. This tactic must be loaded
-by {\tt Require Import LegacyField}. Field theories are declared (as for
-{\tt legacy ring}) with
-the {\tt Add Legacy Field} command.
-
-\subsection{\tt Add Legacy Field
-\comindex{Add Legacy Field}}
-
-This vernacular command adds a commutative field theory to the database for the
-tactic {\tt field}. You must provide this theory as follows:
-\begin{flushleft}
-{\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
-Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}
-\end{flushleft}
-where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is
-a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt
- A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it
- Azero}} is a term of type {\tt A}, {\tt {\it Aopp}} is a term of
-type {\tt A->A}, {\tt {\it Aeq}} is a term of type {\tt A->bool}, {\tt
- {\it Ainv}} is a term of type {\tt A->A}, {\tt {\it Rth}} is a term
-of type {\tt (Ring\_Theory {\it A Aplus Amult Aone Azero Ainv Aeq})},
-and {\tt {\it Tinvl}} is a term of type {\tt forall n:{\it A},
- {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}.
-To build a ring theory, refer to Chapter~\ref{ring} for more details.
-
-This command adds also an entry in the ring theory table if this theory is not
-already declared. So, it is useless to keep, for a given type, the {\tt Add
-Ring} command if you declare a theory with {\tt Add Field}, except if you plan
-to use specific features of {\tt ring} (see Chapter~\ref{ring}). However, the
-module {\tt ring} is not loaded by {\tt Add Field} and you have to make a {\tt
-Require Import Ring} if you want to call the {\tt ring} tactic.
-
-\begin{Variants}
-
-\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
-{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Field }with minus:={\it Aminus}}
-
-Adds also the term {\it Aminus} which must be a constant expressed by
-means of {\it Aopp}.
-
-\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
-{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Legacy Field }with div:={\it Adiv}}
-
-Adds also the term {\it Adiv} which must be a constant expressed by
-means of {\it Ainv}.
-
-\end{Variants}
-
-\SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt
-legacy field}.
-
\asection{History of \texttt{ring}}
First Samuel Boutin designed the tactic \texttt{ACDSimpl}.
1  doc/stdlib/index-list.html.template
View
@@ -576,7 +576,6 @@ through the <tt>Require Import</tt> command.</p>
theories/Reals/SeqSeries.v
theories/Reals/Sqrt_reg.v
theories/Reals/Rlogic.v
- theories/Reals/LegacyRfield.v
(theories/Reals/Reals.v)
</dd>
14 plugins/field/LegacyField.v
View
@@ -1,14 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-Require Export LegacyField_Compl.
-Require Export LegacyField_Theory.
-Require Export LegacyField_Tactic.
-Declare ML Module "field_plugin".
-
-(* Command declarations are moved to the ML side *)
36 plugins/field/LegacyField_Compl.v
View
@@ -1,36 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-Require Import List.
-
-Definition assoc_2nd :=
- (fix assoc_2nd_rec (A:Type) (B:Set)
- (eq_dec:forall e1 e2:B, {e1 = e2} + {e1 <> e2})
- (lst:list (prod A B)) {struct lst} :
- B -> A -> A :=
- fun (key:B) (default:A) =>
- match lst with
- | nil => default
- | (v,e) :: l =>
- match eq_dec e key with
- | left _ => v
- | right _ => assoc_2nd_rec A B eq_dec l key default
- end
- end).
-
-Definition mem :=
- (fix mem (A:Set) (eq_dec:forall e1 e2:A, {e1 = e2} + {e1 <> e2})
- (a:A) (l:list A) {struct l} : bool :=
- match l with
- | nil => false
- | a1 :: l1 =>
- match eq_dec a a1 with
- | left _ => true
- | right _ => mem A eq_dec a l1
- end
- end).
431 plugins/field/LegacyField_Tactic.v
View
@@ -1,431 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-Require Import List.
-Require Import LegacyRing.
-Require Export LegacyField_Compl.
-Require Export LegacyField_Theory.
-
-(**** Interpretation A --> ExprA ****)
-
-Ltac get_component a s := eval cbv beta iota delta [a] in (a s).
-
-Ltac body_of s := eval cbv beta iota delta [s] in s.
-
-Ltac mem_assoc var lvar :=
- match constr:lvar with
- | nil => constr:false
- | ?X1 :: ?X2 =>
- match constr:(X1 = var) with
- | (?X1 = ?X1) => constr:true
- | _ => mem_assoc var X2
- end
- end.
-
-Ltac number lvar :=
- let rec number_aux lvar cpt :=
- match constr:lvar with
- | (@nil ?X1) => constr:(@nil (prod X1 nat))
- | ?X2 :: ?X3 =>
- let l2 := number_aux X3 (S cpt) in
- constr:((X2,cpt) :: l2)
- end
- in number_aux lvar 0.
-
-Ltac build_varlist FT trm :=
- let rec seek_var lvar trm :=
- let AT := get_component A FT
- with AzeroT := get_component Azero FT
- with AoneT := get_component Aone FT
- with AplusT := get_component Aplus FT
- with AmultT := get_component Amult FT
- with AoppT := get_component Aopp FT
- with AinvT := get_component Ainv FT in
- match constr:trm with
- | AzeroT => lvar
- | AoneT => lvar
- | (AplusT ?X1 ?X2) =>
- let l1 := seek_var lvar X1 in
- seek_var l1 X2
- | (AmultT ?X1 ?X2) =>
- let l1 := seek_var lvar X1 in
- seek_var l1 X2
- | (AoppT ?X1) => seek_var lvar X1
- | (AinvT ?X1) => seek_var lvar X1
- | ?X1 =>
- let res := mem_assoc X1 lvar in
- match constr:res with
- | true => lvar
- | false => constr:(X1 :: lvar)
- end
- end in
- let AT := get_component A FT in
- let lvar := seek_var (@nil AT) trm in
- number lvar.
-
-Ltac assoc elt lst :=
- match constr:lst with
- | nil => fail
- | (?X1,?X2) :: ?X3 =>
- match constr:(elt = X1) with
- | (?X1 = ?X1) => constr:X2
- | _ => assoc elt X3
- end
- end.
-
-Ltac interp_A FT lvar trm :=
- let AT := get_component A FT
- with AzeroT := get_component Azero FT
- with AoneT := get_component Aone FT
- with AplusT := get_component Aplus FT
- with AmultT := get_component Amult FT
- with AoppT := get_component Aopp FT
- with AinvT := get_component Ainv FT in
- match constr:trm with
- | AzeroT => constr:EAzero
- | AoneT => constr:EAone
- | (AplusT ?X1 ?X2) =>
- let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
- constr:(EAplus e1 e2)
- | (AmultT ?X1 ?X2) =>
- let e1 := interp_A FT lvar X1 with e2 := interp_A FT lvar X2 in
- constr:(EAmult e1 e2)
- | (AoppT ?X1) =>
- let e := interp_A FT lvar X1 in
- constr:(EAopp e)
- | (AinvT ?X1) => let e := interp_A FT lvar X1 in
- constr:(EAinv e)
- | ?X1 => let idx := assoc X1 lvar in
- constr:(EAvar idx)
- end.
-
-(************************)
-(* Simplification *)
-(************************)
-
-(**** Generation of the multiplier ****)
-
-Ltac remove e l :=
- match constr:l with
- | nil => l
- | e :: ?X2 => constr:X2
- | ?X2 :: ?X3 => let nl := remove e X3 in constr:(X2 :: nl)
- end.
-
-Ltac union l1 l2 :=
- match constr:l1 with
- | nil => l2
- | ?X2 :: ?X3 =>
- let nl2 := remove X2 l2 in
- let nl := union X3 nl2 in
- constr:(X2 :: nl)
- end.
-
-Ltac raw_give_mult trm :=
- match constr:trm with
- | (EAinv ?X1) => constr:(X1 :: nil)
- | (EAopp ?X1) => raw_give_mult X1
- | (EAplus ?X1 ?X2) =>
- let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
- union l1 l2
- | (EAmult ?X1 ?X2) =>
- let l1 := raw_give_mult X1 with l2 := raw_give_mult X2 in
- eval compute in (app l1 l2)
- | _ => constr:(@nil ExprA)
- end.
-
-Ltac give_mult trm :=
- let ltrm := raw_give_mult trm in
- constr:(mult_of_list ltrm).
-
-(**** Associativity ****)
-
-Ltac apply_assoc FT lvar trm :=
- let t := eval compute in (assoc trm) in
- match constr:(t = trm) with
- | (?X1 = ?X1) => idtac
- | _ =>
- rewrite <- (assoc_correct FT trm); change (assoc trm) with t
- end.
-
-(**** Distribution *****)
-
-Ltac apply_distrib FT lvar trm :=
- let t := eval compute in (distrib trm) in
- match constr:(t = trm) with
- | (?X1 = ?X1) => idtac
- | _ =>
- rewrite <- (distrib_correct FT trm);
- change (distrib trm) with t
- end.
-
-(**** Multiplication by the inverse product ****)
-
-Ltac grep_mult := match goal with
- | id:(interp_ExprA _ _ _ <> _) |- _ => id
- end.
-
-Ltac weak_reduce :=
- match goal with
- | |- context [(interp_ExprA ?X1 ?X2 _)] =>
- cbv beta iota zeta
- delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list X1 X2 A Azero
- Aone Aplus Amult Aopp Ainv]
- end.
-
-Ltac multiply mul :=
- match goal with
- | |- (interp_ExprA ?FT ?X2 ?X3 = interp_ExprA ?FT ?X2 ?X4) =>
- let AzeroT := get_component Azero FT in
- cut (interp_ExprA FT X2 mul <> AzeroT);
- [ intro; (let id := grep_mult in apply (mult_eq FT X3 X4 mul X2 id))
- | weak_reduce;
- (let AoneT := get_component Aone ltac:(body_of FT)
- with AmultT := get_component Amult ltac:(body_of FT) in
- try
- match goal with
- | |- context [(AmultT _ AoneT)] => rewrite (AmultT_1r FT)
- end; clear FT X2) ]
- end.
-
-Ltac apply_multiply FT lvar trm :=
- let t := eval compute in (multiply trm) in
- match constr:(t = trm) with
- | (?X1 = ?X1) => idtac
- | _ =>
- rewrite <- (multiply_correct FT trm);
- change (multiply trm) with t
- end.
-
-(**** Permutations and simplification ****)
-
-Ltac apply_inverse mul FT lvar trm :=
- let t := eval compute in (inverse_simplif mul trm) in
- match constr:(t = trm) with
- | (?X1 = ?X1) => idtac
- | _ =>
- rewrite <- (inverse_correct FT trm mul);
- [ change (inverse_simplif mul trm) with t | assumption ]
- end.
-(**** Inverse test ****)
-
-Ltac strong_fail tac := first [ tac | fail 2 ].
-
-Ltac inverse_test_aux FT trm :=
- let AplusT := get_component Aplus FT
- with AmultT := get_component Amult FT
- with AoppT := get_component Aopp FT
- with AinvT := get_component Ainv FT in
- match constr:trm with
- | (AinvT _) => fail 1
- | (AoppT ?X1) =>
- strong_fail ltac:(inverse_test_aux FT X1; idtac)
- | (AplusT ?X1 ?X2) =>
- strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
- | (AmultT ?X1 ?X2) =>
- strong_fail ltac:(inverse_test_aux FT X1; inverse_test_aux FT X2)
- | _ => idtac
- end.
-
-Ltac inverse_test FT :=
- let AplusT := get_component Aplus FT in
- match goal with
- | |- (?X1 = ?X2) => inverse_test_aux FT (AplusT X1 X2)
- end.
-
-(**** Field itself ****)
-
-Ltac apply_simplif sfun :=
- match goal with
- | |- (interp_ExprA ?X1 ?X2 ?X3 = interp_ExprA _ _ _) =>
- sfun X1 X2 X3
- end;
- match goal with
- | |- (interp_ExprA _ _ _ = interp_ExprA ?X1 ?X2 ?X3) =>
- sfun X1 X2 X3
- end.
-
-Ltac unfolds FT :=
- match get_component Aminus FT with
- | Some ?X1 => unfold X1
- | _ => idtac
- end;
- match get_component Adiv FT with
- | Some ?X1 => unfold X1
- | _ => idtac
- end.
-
-Ltac reduce FT :=
- let AzeroT := get_component Azero FT
- with AoneT := get_component Aone FT
- with AplusT := get_component Aplus FT
- with AmultT := get_component Amult FT
- with AoppT := get_component Aopp FT
- with AinvT := get_component Ainv FT in
- (cbv beta iota zeta delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] ||
- compute).
-
-Ltac field_gen_aux FT :=
- let AplusT := get_component Aplus FT in
- match goal with
- | |- (?X1 = ?X2) =>
- let lvar := build_varlist FT (AplusT X1 X2) in
- let trm1 := interp_A FT lvar X1 with trm2 := interp_A FT lvar X2 in
- let mul := give_mult (EAplus trm1 trm2) in
- cut
- (let ft := FT in
- let vm := lvar in interp_ExprA ft vm trm1 = interp_ExprA ft vm trm2);
- [ compute; auto
- | intros ft vm; apply_simplif apply_distrib;
- apply_simplif apply_assoc; multiply mul;
- [ apply_simplif apply_multiply;
- apply_simplif ltac:(apply_inverse mul);
- (let id := grep_mult in
- clear id; weak_reduce; clear ft vm; first
- [ inverse_test FT; legacy ring | field_gen_aux FT ])
- | idtac ] ]
- end.
-
-Ltac field_gen FT :=
- unfolds FT; (inverse_test FT; legacy ring) || field_gen_aux FT.
-
-(*****************************)
-(* Term Simplification *)
-(*****************************)
-
-(**** Minus and division expansions ****)
-
-Ltac init_exp FT trm :=
- let e :=
- (match get_component Aminus FT with
- | Some ?X1 => eval cbv beta delta [X1] in trm
- | _ => trm
- end) in
- match get_component Adiv FT with
- | Some ?X1 => eval cbv beta delta [X1] in e
- | _ => e
- end.
-
-(**** Inverses simplification ****)
-
-Ltac simpl_inv trm :=
- match constr:trm with
- | (EAplus ?X1 ?X2) =>
- let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
- constr:(EAplus e1 e2)
- | (EAmult ?X1 ?X2) =>
- let e1 := simpl_inv X1 with e2 := simpl_inv X2 in
- constr:(EAmult e1 e2)
- | (EAopp ?X1) => let e := simpl_inv X1 in
- constr:(EAopp e)
- | (EAinv ?X1) => SimplInvAux X1
- | ?X1 => constr:X1
- end
- with SimplInvAux trm :=
- match constr:trm with
- | (EAinv ?X1) => simpl_inv X1
- | (EAmult ?X1 ?X2) =>
- let e1 := simpl_inv (EAinv X1) with e2 := simpl_inv (EAinv X2) in
- constr:(EAmult e1 e2)
- | ?X1 => let e := simpl_inv X1 in
- constr:(EAinv e)
- end.
-
-(**** Monom simplification ****)
-
-Ltac map_tactic fcn lst :=
- match constr:lst with
- | nil => lst
- | ?X2 :: ?X3 =>
- let r := fcn X2 with t := map_tactic fcn X3 in
- constr:(r :: t)
- end.
-
-Ltac build_monom_aux lst trm :=
- match constr:lst with
- | nil => eval compute in (assoc trm)
- | ?X1 :: ?X2 => build_monom_aux X2 (EAmult trm X1)
- end.
-
-Ltac build_monom lnum lden :=
- let ildn := map_tactic ltac:(fun e => constr:(EAinv e)) lden in
- let ltot := eval compute in (app lnum ildn) in
- let trm := build_monom_aux ltot EAone in
- match constr:trm with
- | (EAmult _ ?X1) => constr:X1
- | ?X1 => constr:X1
- end.
-
-Ltac simpl_monom_aux lnum lden trm :=
- match constr:trm with
- | (EAmult (EAinv ?X1) ?X2) =>
- let mma := mem_assoc X1 lnum in
- match constr:mma with
- | true =>
- let newlnum := remove X1 lnum in
- simpl_monom_aux newlnum lden X2
- | false => simpl_monom_aux lnum (X1 :: lden) X2
- end
- | (EAmult ?X1 ?X2) =>
- let mma := mem_assoc X1 lden in
- match constr:mma with
- | true =>
- let newlden := remove X1 lden in
- simpl_monom_aux lnum newlden X2
- | false => simpl_monom_aux (X1 :: lnum) lden X2
- end
- | (EAinv ?X1) =>
- let mma := mem_assoc X1 lnum in
- match constr:mma with
- | true =>
- let newlnum := remove X1 lnum in
- build_monom newlnum lden
- | false => build_monom lnum (X1 :: lden)
- end
- | ?X1 =>
- let mma := mem_assoc X1 lden in
- match constr:mma with
- | true =>
- let newlden := remove X1 lden in
- build_monom lnum newlden
- | false => build_monom (X1 :: lnum) lden
- end
- end.
-
-Ltac simpl_monom trm := simpl_monom_aux (@nil ExprA) (@nil ExprA) trm.
-
-Ltac simpl_all_monomials trm :=
- match constr:trm with
- | (EAplus ?X1 ?X2) =>
- let e1 := simpl_monom X1 with e2 := simpl_all_monomials X2 in
- constr:(EAplus e1 e2)
- | ?X1 => simpl_monom X1
- end.
-
-(**** Associativity and distribution ****)
-
-Ltac assoc_distrib trm := eval compute in (assoc (distrib trm)).
-
-(**** The tactic Field_Term ****)
-
-Ltac eval_weak_reduce trm :=
- eval
- cbv beta iota zeta
- delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero Aone Aplus
- Amult Aopp Ainv] in trm.
-
-Ltac field_term FT exp :=
- let newexp := init_exp FT exp in
- let lvar := build_varlist FT newexp in
- let trm := interp_A FT lvar newexp in
- let tma := eval compute in (assoc trm) in
- let tsmp :=
- simpl_all_monomials
- ltac:(assoc_distrib ltac:(simpl_all_monomials ltac:(simpl_inv tma))) in
- let trep := eval_weak_reduce (interp_ExprA FT lvar tsmp) in
- (replace exp with trep; [ legacy ring trep | field_gen FT ]).
648 plugins/field/LegacyField_Theory.v
View
@@ -1,648 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-Require Import List.
-Require Import Peano_dec.
-Require Import LegacyRing.
-Require Import LegacyField_Compl.
-
-Record Field_Theory : Type :=
- {A : Type;
- Aplus : A -> A -> A;
- Amult : A -> A -> A;
- Aone : A;
- Azero : A;
- Aopp : A -> A;
- Aeq : A -> A -> bool;
- Ainv : A -> A;
- Aminus : option (A -> A -> A);
- Adiv : option (A -> A -> A);
- RT : Ring_Theory Aplus Amult Aone Azero Aopp Aeq;
- Th_inv_def : forall n:A, n <> Azero -> Amult (Ainv n) n = Aone}.
-
-(* The reflexion structure *)
-Inductive ExprA : Set :=
- | EAzero : ExprA
- | EAone : ExprA
- | EAplus : ExprA -> ExprA -> ExprA
- | EAmult : ExprA -> ExprA -> ExprA
- | EAopp : ExprA -> ExprA
- | EAinv : ExprA -> ExprA
- | EAvar : nat -> ExprA.
-
-(**** Decidability of equality ****)
-
-Lemma eqExprA_O : forall e1 e2:ExprA, {e1 = e2} + {e1 <> e2}.
-Proof.
- double induction e1 e2; try intros;
- try (left; reflexivity) || (try (right; discriminate)).
- elim (H1 e0); intro y; elim (H2 e); intro y0;
- try
- (left; rewrite y; rewrite y0; auto) ||
- (right; red; intro; inversion H3; auto).
- elim (H1 e0); intro y; elim (H2 e); intro y0;
- try
- (left; rewrite y; rewrite y0; auto) ||
- (right; red; intro; inversion H3; auto).
- elim (H0 e); intro y.
- left; rewrite y; auto.
- right; red; intro; inversion H1; auto.
- elim (H0 e); intro y.
- left; rewrite y; auto.
- right; red; intro; inversion H1; auto.
- elim (eq_nat_dec n n0); intro y.
- left; rewrite y; auto.
- right; red; intro; inversion H; auto.
-Defined.
-
-Definition eq_nat_dec := Eval compute in eq_nat_dec.
-Definition eqExprA := Eval compute in eqExprA_O.
-
-(**** Generation of the multiplier ****)
-
-Fixpoint mult_of_list (e:list ExprA) : ExprA :=
- match e with
- | nil => EAone
- | e1 :: l1 => EAmult e1 (mult_of_list l1)
- end.
-
-Section Theory_of_fields.
-
-Variable T : Field_Theory.
-
-Let AT := A T.
-Let AplusT := Aplus T.
-Let AmultT := Amult T.
-Let AoneT := Aone T.
-Let AzeroT := Azero T.
-Let AoppT := Aopp T.
-Let AeqT := Aeq T.
-Let AinvT := Ainv T.
-Let RTT := RT T.
-Let Th_inv_defT := Th_inv_def T.
-
-Add Legacy Abstract Ring (A T) (Aplus T) (Amult T) (Aone T) (
- Azero T) (Aopp T) (Aeq T) (RT T).
-
-Add Legacy Abstract Ring AT AplusT AmultT AoneT AzeroT AoppT AeqT RTT.
-
-(***************************)
-(* Lemmas to be used *)
-(***************************)
-
-Lemma AplusT_comm : forall r1 r2:AT, AplusT r1 r2 = AplusT r2 r1.
-Proof.
- intros; legacy ring.
-Qed.
-
-Lemma AplusT_assoc :
- forall r1 r2 r3:AT, AplusT (AplusT r1 r2) r3 = AplusT r1 (AplusT r2 r3).
-Proof.
- intros; legacy ring.
-Qed.
-
-Lemma AmultT_comm : forall r1 r2:AT, AmultT r1 r2 = AmultT r2 r1.
-Proof.
- intros; legacy ring.
-Qed.
-
-Lemma AmultT_assoc :
- forall r1 r2 r3:AT, AmultT (AmultT r1 r2) r3 = AmultT r1 (AmultT r2 r3).
-Proof.
- intros; legacy ring.
-Qed.
-
-Lemma AplusT_Ol : forall r:AT, AplusT AzeroT r = r.
-Proof.
- intros; legacy ring.
-Qed.
-
-Lemma AmultT_1l : forall r:AT, AmultT AoneT r = r.
-Proof.
- intros; legacy ring.
-Qed.
-
-Lemma AplusT_AoppT_r : forall r:AT, AplusT r (AoppT r) = AzeroT.
-Proof.
- intros; legacy ring.
-Qed.
-
-Lemma AmultT_AplusT_distr :
- forall r1 r2 r3:AT,
- AmultT r1 (AplusT r2 r3) = AplusT (AmultT r1 r2) (AmultT r1 r3).
-Proof.
- intros; legacy ring.
-Qed.
-
-Lemma r_AplusT_plus : forall r r1 r2:AT, AplusT r r1 = AplusT r r2 -> r1 = r2.
-Proof.
- intros; transitivity (AplusT (AplusT (AoppT r) r) r1).
- legacy ring.
- transitivity (AplusT (AplusT (AoppT r) r) r2).
- repeat rewrite AplusT_assoc; rewrite <- H; reflexivity.
- legacy ring.
-Qed.
-
-Lemma r_AmultT_mult :
- forall r r1 r2:AT, AmultT r r1 = AmultT r r2 -> r <> AzeroT -> r1 = r2.
-Proof.
- intros; transitivity (AmultT (AmultT (AinvT r) r) r1).
- rewrite Th_inv_defT; [ symmetry ; apply AmultT_1l; auto | auto ].
- transitivity (AmultT (AmultT (AinvT r) r) r2).
- repeat rewrite AmultT_assoc; rewrite H; trivial.
- rewrite Th_inv_defT; [ apply AmultT_1l; auto | auto ].
-Qed.
-
-Lemma AmultT_Or : forall r:AT, AmultT r AzeroT = AzeroT.
-Proof.
- intro; legacy ring.
-Qed.
-
-Lemma AmultT_Ol : forall r:AT, AmultT AzeroT r = AzeroT.
-Proof.
- intro; legacy ring.
-Qed.
-
-Lemma AmultT_1r : forall r:AT, AmultT r AoneT = r.
-Proof.
- intro; legacy ring.
-Qed.
-
-Lemma AinvT_r : forall r:AT, r <> AzeroT -> AmultT r (AinvT r) = AoneT.
-Proof.
- intros; rewrite AmultT_comm; apply Th_inv_defT; auto.
-Qed.
-
-Lemma Rmult_neq_0_reg :
- forall r1 r2:AT, AmultT r1 r2 <> AzeroT -> r1 <> AzeroT /\ r2 <> AzeroT.
-Proof.
- intros r1 r2 H; split; red; intro; apply H; rewrite H0; legacy ring.
-Qed.
-
-(************************)
-(* Interpretation *)
-(************************)
-
-(**** ExprA --> A ****)
-
-Fixpoint interp_ExprA (lvar:list (AT * nat)) (e:ExprA) {struct e} :
- AT :=
- match e with
- | EAzero => AzeroT
- | EAone => AoneT
- | EAplus e1 e2 => AplusT (interp_ExprA lvar e1) (interp_ExprA lvar e2)
- | EAmult e1 e2 => AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2)
- | EAopp e => Aopp T (interp_ExprA lvar e)
- | EAinv e => Ainv T (interp_ExprA lvar e)
- | EAvar n => assoc_2nd AT nat eq_nat_dec lvar n AzeroT
- end.
-
-(************************)
-(* Simplification *)
-(************************)
-
-(**** Associativity ****)
-
-Definition merge_mult :=
- (fix merge_mult (e1:ExprA) : ExprA -> ExprA :=
- fun e2:ExprA =>
- match e1 with
- | EAmult t1 t2 =>
- match t2 with
- | EAmult t2 t3 => EAmult t1 (EAmult t2 (merge_mult t3 e2))
- | _ => EAmult t1 (EAmult t2 e2)
- end
- | _ => EAmult e1 e2
- end).
-
-Fixpoint assoc_mult (e:ExprA) : ExprA :=
- match e with
- | EAmult e1 e3 =>
- match e1 with
- | EAmult e1 e2 =>
- merge_mult (merge_mult (assoc_mult e1) (assoc_mult e2))
- (assoc_mult e3)
- | _ => EAmult e1 (assoc_mult e3)
- end
- | _ => e
- end.
-
-Definition merge_plus :=
- (fix merge_plus (e1:ExprA) : ExprA -> ExprA :=
- fun e2:ExprA =>
- match e1 with
- | EAplus t1 t2 =>
- match t2 with
- | EAplus t2 t3 => EAplus t1 (EAplus t2 (merge_plus t3 e2))
- | _ => EAplus t1 (EAplus t2 e2)
- end
- | _ => EAplus e1 e2
- end).
-
-Fixpoint assoc (e:ExprA) : ExprA :=
- match e with
- | EAplus e1 e3 =>
- match e1 with
- | EAplus e1 e2 =>
- merge_plus (merge_plus (assoc e1) (assoc e2)) (assoc e3)
- | _ => EAplus (assoc_mult e1) (assoc e3)
- end
- | _ => assoc_mult e
- end.
-
-Lemma merge_mult_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (merge_mult (EAmult e1 e2) e3) =
- interp_ExprA lvar (EAmult e1 (merge_mult e2 e3)).
-Proof.
-intros e1 e2; generalize e1; generalize e2; clear e1 e2.
-simple induction e2; auto; intros.
-unfold merge_mult at 1; fold merge_mult;
- unfold interp_ExprA at 2; fold interp_ExprA;
- rewrite (H0 e e3 lvar); unfold interp_ExprA at 1;
- fold interp_ExprA; unfold interp_ExprA at 5;
- fold interp_ExprA; auto.
-Qed.
-
-Lemma merge_mult_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (merge_mult e1 e2) = interp_ExprA lvar (EAmult e1 e2).
-Proof.
-simple induction e1; auto; intros.
-elim e0; try (intros; simpl; legacy ring).
-unfold interp_ExprA in H2; fold interp_ExprA in H2;
- cut
- (AmultT (interp_ExprA lvar e2)
- (AmultT (interp_ExprA lvar e4)
- (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e3))) =
- AmultT
- (AmultT (AmultT (interp_ExprA lvar e) (interp_ExprA lvar e4))
- (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
-intro H3; rewrite H3; rewrite <- H2; rewrite merge_mult_correct1;
- simpl; legacy ring.
-legacy ring.
-Qed.
-
-Lemma assoc_mult_correct1 :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
- AmultT (interp_ExprA lvar (assoc_mult e1))
- (interp_ExprA lvar (assoc_mult e2)) =
- interp_ExprA lvar (assoc_mult (EAmult e1 e2)).
-Proof.
-simple induction e1; auto; intros.
-rewrite <- (H e0 lvar); simpl; rewrite merge_mult_correct;
- simpl; rewrite merge_mult_correct; simpl;
- auto.
-Qed.
-
-Lemma assoc_mult_correct :
- forall (e:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (assoc_mult e) = interp_ExprA lvar e.
-Proof.
-simple induction e; auto; intros.
-elim e0; intros.
-intros; simpl; legacy ring.
-simpl; rewrite (AmultT_1l (interp_ExprA lvar (assoc_mult e1)));
- rewrite (AmultT_1l (interp_ExprA lvar e1)); apply H0.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite merge_mult_correct; simpl;
- rewrite merge_mult_correct; simpl; rewrite AmultT_assoc;
- rewrite assoc_mult_correct1; rewrite H2; simpl;
- rewrite <- assoc_mult_correct1 in H1; unfold interp_ExprA at 3 in H1;
- fold interp_ExprA in H1; rewrite (H0 lvar) in H1;
- rewrite (AmultT_comm (interp_ExprA lvar e3) (interp_ExprA lvar e1));
- rewrite <- AmultT_assoc; rewrite H1; rewrite AmultT_assoc;
- legacy ring.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-Qed.
-
-Lemma merge_plus_correct1 :
- forall (e1 e2 e3:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (merge_plus (EAplus e1 e2) e3) =
- interp_ExprA lvar (EAplus e1 (merge_plus e2 e3)).
-Proof.
-intros e1 e2; generalize e1; generalize e2; clear e1 e2.
-simple induction e2; auto; intros.
-unfold merge_plus at 1; fold merge_plus;
- unfold interp_ExprA at 2; fold interp_ExprA;
- rewrite (H0 e e3 lvar); unfold interp_ExprA at 1;
- fold interp_ExprA; unfold interp_ExprA at 5;
- fold interp_ExprA; auto.
-Qed.
-
-Lemma merge_plus_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (merge_plus e1 e2) = interp_ExprA lvar (EAplus e1 e2).
-Proof.
-simple induction e1; auto; intros.
-elim e0; try intros; try (simpl; legacy ring).
-unfold interp_ExprA in H2; fold interp_ExprA in H2;
- cut
- (AplusT (interp_ExprA lvar e2)
- (AplusT (interp_ExprA lvar e4)
- (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e3))) =
- AplusT
- (AplusT (AplusT (interp_ExprA lvar e) (interp_ExprA lvar e4))
- (interp_ExprA lvar e2)) (interp_ExprA lvar e3)).
-intro H3; rewrite H3; rewrite <- H2; rewrite merge_plus_correct1;
- simpl; legacy ring.
-legacy ring.
-Qed.
-
-Lemma assoc_plus_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
- AplusT (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)) =
- interp_ExprA lvar (assoc (EAplus e1 e2)).
-Proof.
-simple induction e1; auto; intros.
-rewrite <- (H e0 lvar); simpl; rewrite merge_plus_correct;
- simpl; rewrite merge_plus_correct; simpl;
- auto.
-Qed.
-
-Lemma assoc_correct :
- forall (e:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (assoc e) = interp_ExprA lvar e.
-Proof.
-simple induction e; auto; intros.
-elim e0; intros.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite merge_plus_correct; simpl;
- rewrite merge_plus_correct; simpl; rewrite AplusT_assoc;
- rewrite assoc_plus_correct; rewrite H2; simpl;
- apply
- (r_AplusT_plus (interp_ExprA lvar (assoc e1))
- (AplusT (interp_ExprA lvar (assoc e2))
- (AplusT (interp_ExprA lvar e3) (interp_ExprA lvar e1)))
- (AplusT (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e3))
- (interp_ExprA lvar e1))); rewrite <- AplusT_assoc;
- rewrite
- (AplusT_comm (interp_ExprA lvar (assoc e1)) (interp_ExprA lvar (assoc e2)))
- ; rewrite assoc_plus_correct; rewrite H1; simpl;
- rewrite (H0 lvar);
- rewrite <-
- (AplusT_assoc (AplusT (interp_ExprA lvar e2) (interp_ExprA lvar e1))
- (interp_ExprA lvar e3) (interp_ExprA lvar e1))
- ;
- rewrite
- (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e1)
- (interp_ExprA lvar e3));
- rewrite (AplusT_comm (interp_ExprA lvar e1) (interp_ExprA lvar e3));
- rewrite <-
- (AplusT_assoc (interp_ExprA lvar e2) (interp_ExprA lvar e3)
- (interp_ExprA lvar e1)); apply AplusT_comm.
-unfold assoc; fold assoc; unfold interp_ExprA;
- fold interp_ExprA; rewrite assoc_mult_correct;
- rewrite (H0 lvar); simpl; auto.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-simpl; rewrite (H0 lvar); auto.
-unfold assoc; fold assoc; unfold interp_ExprA;
- fold interp_ExprA; rewrite assoc_mult_correct;
- simpl; auto.
-Qed.
-
-(**** Distribution *****)
-
-Fixpoint distrib_EAopp (e:ExprA) : ExprA :=
- match e with
- | EAplus e1 e2 => EAplus (distrib_EAopp e1) (distrib_EAopp e2)
- | EAmult e1 e2 => EAmult (distrib_EAopp e1) (distrib_EAopp e2)
- | EAopp e => EAmult (EAopp EAone) (distrib_EAopp e)
- | e => e
- end.
-
-Definition distrib_mult_right :=
- (fix distrib_mult_right (e1:ExprA) : ExprA -> ExprA :=
- fun e2:ExprA =>
- match e1 with
- | EAplus t1 t2 =>
- EAplus (distrib_mult_right t1 e2) (distrib_mult_right t2 e2)
- | _ => EAmult e1 e2
- end).
-
-Fixpoint distrib_mult_left (e1 e2:ExprA) {struct e1} : ExprA :=
- match e1 with
- | EAplus t1 t2 =>
- EAplus (distrib_mult_left t1 e2) (distrib_mult_left t2 e2)
- | _ => distrib_mult_right e2 e1
- end.
-
-Fixpoint distrib_main (e:ExprA) : ExprA :=
- match e with
- | EAmult e1 e2 => distrib_mult_left (distrib_main e1) (distrib_main e2)
- | EAplus e1 e2 => EAplus (distrib_main e1) (distrib_main e2)
- | EAopp e => EAopp (distrib_main e)
- | _ => e
- end.
-
-Definition distrib (e:ExprA) : ExprA := distrib_main (distrib_EAopp e).
-
-Lemma distrib_mult_right_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (distrib_mult_right e1 e2) =
- AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
-Proof.
-simple induction e1; try intros; simpl; auto.
-rewrite AmultT_comm; rewrite AmultT_AplusT_distr; rewrite (H e2 lvar);
- rewrite (H0 e2 lvar); legacy ring.
-Qed.
-
-Lemma distrib_mult_left_correct :
- forall (e1 e2:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (distrib_mult_left e1 e2) =
- AmultT (interp_ExprA lvar e1) (interp_ExprA lvar e2).
-Proof.
-simple induction e1; try intros; simpl.
-rewrite AmultT_Ol; rewrite distrib_mult_right_correct; simpl;
- apply AmultT_Or.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-rewrite AmultT_comm;
- rewrite
- (AmultT_AplusT_distr (interp_ExprA lvar e2) (interp_ExprA lvar e)
- (interp_ExprA lvar e0));
- rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e));
- rewrite (AmultT_comm (interp_ExprA lvar e2) (interp_ExprA lvar e0));
- rewrite (H e2 lvar); rewrite (H0 e2 lvar); auto.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-rewrite distrib_mult_right_correct; simpl; apply AmultT_comm.
-Qed.
-
-Lemma distrib_correct :
- forall (e:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (distrib e) = interp_ExprA lvar e.
-Proof.
-simple induction e; intros; auto.
-simpl; rewrite <- (H lvar); rewrite <- (H0 lvar);
- unfold distrib; simpl; auto.
-simpl; rewrite <- (H lvar); rewrite <- (H0 lvar);
- unfold distrib; simpl; apply distrib_mult_left_correct.
-simpl; fold AoppT; rewrite <- (H lvar);
- unfold distrib; simpl; rewrite distrib_mult_right_correct;
- simpl; fold AoppT; legacy ring.
-Qed.
-
-(**** Multiplication by the inverse product ****)
-
-Lemma mult_eq :
- forall (e1 e2 a:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar a <> AzeroT ->
- interp_ExprA lvar (EAmult a e1) = interp_ExprA lvar (EAmult a e2) ->
- interp_ExprA lvar e1 = interp_ExprA lvar e2.
-Proof.
- simpl; intros;
- apply
- (r_AmultT_mult (interp_ExprA lvar a) (interp_ExprA lvar e1)
- (interp_ExprA lvar e2)); assumption.
-Qed.
-
-Fixpoint multiply_aux (a e:ExprA) {struct e} : ExprA :=
- match e with
- | EAplus e1 e2 => EAplus (EAmult a e1) (multiply_aux a e2)
- | _ => EAmult a e
- end.
-
-Definition multiply (e:ExprA) : ExprA :=
- match e with
- | EAmult a e1 => multiply_aux a e1
- | _ => e
- end.
-
-Lemma multiply_aux_correct :
- forall (a e:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (multiply_aux a e) =
- AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
-Proof.
-simple induction e; simpl; intros; try rewrite merge_mult_correct;
- auto.
- simpl; rewrite (H0 lvar); legacy ring.
-Qed.
-
-Lemma multiply_correct :
- forall (e:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar (multiply e) = interp_ExprA lvar e.
-Proof.
- simple induction e; simpl; auto.
- intros; apply multiply_aux_correct.
-Qed.
-
-(**** Permutations and simplification ****)
-
-Fixpoint monom_remove (a m:ExprA) {struct m} : ExprA :=
- match m with
- | EAmult m0 m1 =>
- match eqExprA m0 (EAinv a) with
- | left _ => m1
- | right _ => EAmult m0 (monom_remove a m1)
- end
- | _ =>
- match eqExprA m (EAinv a) with
- | left _ => EAone
- | right _ => EAmult a m
- end
- end.
-
-Definition monom_simplif_rem :=
- (fix monom_simplif_rem (a:ExprA) : ExprA -> ExprA :=
- fun m:ExprA =>
- match a with
- | EAmult a0 a1 => monom_simplif_rem a1 (monom_remove a0 m)
- | _ => monom_remove a m
- end).
-
-Definition monom_simplif (a m:ExprA) : ExprA :=
- match m with
- | EAmult a' m' =>
- match eqExprA a a' with
- | left _ => monom_simplif_rem a m'
- | right _ => m
- end
- | _ => m
- end.
-
-Fixpoint inverse_simplif (a e:ExprA) {struct e} : ExprA :=
- match e with
- | EAplus e1 e2 => EAplus (monom_simplif a e1) (inverse_simplif a e2)
- | _ => monom_simplif a e
- end.
-
-Lemma monom_remove_correct :
- forall (e a:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar a <> AzeroT ->
- interp_ExprA lvar (monom_remove a e) =
- AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
-Proof.
-simple induction e; intros.
-simpl; case (eqExprA EAzero (EAinv a)); intros;
- [ inversion e0 | simpl; trivial ].
-simpl; case (eqExprA EAone (EAinv a)); intros;
- [ inversion e0 | simpl; trivial ].
-simpl; case (eqExprA (EAplus e0 e1) (EAinv a)); intros;
- [ inversion e2 | simpl; trivial ].
-simpl; case (eqExprA e0 (EAinv a)); intros.
-rewrite e2; simpl; fold AinvT.
-rewrite <-
- (AmultT_assoc (interp_ExprA lvar a) (AinvT (interp_ExprA lvar a))
- (interp_ExprA lvar e1)); rewrite AinvT_r; [ legacy ring | assumption ].
-simpl; rewrite H0; auto; legacy ring.
-simpl; fold AoppT; case (eqExprA (EAopp e0) (EAinv a));
- intros; [ inversion e1 | simpl; trivial ].
-unfold monom_remove; case (eqExprA (EAinv e0) (EAinv a)); intros.
-case (eqExprA e0 a); intros.
-rewrite e2; simpl; fold AinvT; rewrite AinvT_r; auto.
-inversion e1; simpl; exfalso; auto.
-simpl; trivial.
-unfold monom_remove; case (eqExprA (EAvar n) (EAinv a)); intros;
- [ inversion e0 | simpl; trivial ].
-Qed.
-
-Lemma monom_simplif_rem_correct :
- forall (a e:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar a <> AzeroT ->
- interp_ExprA lvar (monom_simplif_rem a e) =
- AmultT (interp_ExprA lvar a) (interp_ExprA lvar e).
-Proof.
-simple induction a; simpl; intros; try rewrite monom_remove_correct;
- auto.
-elim (Rmult_neq_0_reg (interp_ExprA lvar e) (interp_ExprA lvar e0) H1);
- intros.
-rewrite (H0 (monom_remove e e1) lvar H3); rewrite monom_remove_correct; auto.
-legacy ring.
-Qed.
-
-Lemma monom_simplif_correct :
- forall (e a:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar a <> AzeroT ->
- interp_ExprA lvar (monom_simplif a e) = interp_ExprA lvar e.
-Proof.
-simple induction e; intros; auto.
-simpl; case (eqExprA a e0); intros.
-rewrite <- e2; apply monom_simplif_rem_correct; auto.
-simpl; trivial.
-Qed.
-
-Lemma inverse_correct :
- forall (e a:ExprA) (lvar:list (AT * nat)),
- interp_ExprA lvar a <> AzeroT ->
- interp_ExprA lvar (inverse_simplif a e) = interp_ExprA lvar e.
-Proof.
-simple induction e; intros; auto.
-simpl; rewrite (H0 a lvar H1); rewrite monom_simplif_correct; auto.
-unfold inverse_simplif; rewrite monom_simplif_correct; auto.
-Qed.
-
-End Theory_of_fields.
-
-(* Compatibility *)
-Notation AplusT_sym := AplusT_comm (only parsing).
-Notation AmultT_sym := AmultT_comm (only parsing).
192 plugins/field/field.ml4
View
@@ -1,192 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(*i camlp4deps: "grammar/grammar.cma" i*)
-
-open Names
-open Pp
-open Proof_type
-open Tacinterp
-open Tacmach
-open Term
-open Typing
-open Errors
-open Util
-open Vernacinterp
-open Vernacexpr
-open Tacexpr
-open Mod_subst
-open Coqlib
-
-(* Interpretation of constr's *)
-let constr_of c = Constrintern.interp_constr Evd.empty (Global.env()) c
-
-(* Construction of constants *)
-let constant dir s = gen_constant "Field" ("field"::dir) s
-let init_constant s = gen_constant_in_modules "Field" init_modules s
-
-(* To deal with the optional arguments *)
-let constr_of_opt a opt =
- let ac = constr_of a in
- let ac3 = mkArrow ac (mkArrow ac ac) in
- match opt with
- | None -> mkApp (init_constant "None",[|ac3|])
- | Some f -> mkApp (init_constant "Some",[|ac3;constr_of f|])
-
-module Cmap = Map.Make(struct type t = constr let compare = constr_ord end)
-
-(* Table of theories *)
-let th_tab = ref (Cmap.empty : constr Cmap.t)
-
-let lookup env typ =
- try Cmap.find typ !th_tab
- with Not_found ->
- errorlabstrm "field"
- (str "No field is declared for type" ++ spc() ++
- Printer.pr_lconstr_env env typ)
-
-let _ =
- let init () = th_tab := Cmap.empty in
- let freeze () = !th_tab in
- let unfreeze fs = th_tab := fs in
- Summary.declare_summary "field"
- { Summary.freeze_function = freeze;
- Summary.unfreeze_function = unfreeze;
- Summary.init_function = init }
-
-let load_addfield _ = ()
-let cache_addfield (_,(typ,th)) = th_tab := Cmap.add typ th !th_tab
-let subst_addfield (subst,(typ,th as obj)) =
- let typ' = subst_mps subst typ in
- let th' = subst_mps subst th in
- if typ' == typ && th' == th then obj else
- (typ',th')
-
-(* Declaration of the Add Field library object *)
-let in_addfield : types * constr -> Libobject.obj =
- Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with
- Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
- Libobject.cache_function = cache_addfield;
- Libobject.subst_function = subst_addfield;
- Libobject.classify_function = (fun a -> Libobject.Substitute a)}
-
-(* Adds a theory to the table *)
-let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
- ainv_l =
- begin
- (try
- Ring.add_theory true true false a None None None aplus amult aone azero
- (Some aopp) aeq rth Quote.ConstrSet.empty
- with | UserError("Add Semi Ring",_) -> ());
- let th = mkApp ((constant ["LegacyField_Theory"] "Build_Field_Theory"),
- [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
- begin
- let _ = type_of (Global.env ()) Evd.empty th in ();
- Lib.add_anonymous_leaf (in_addfield (a,th))
- end
- end
-
-(* Vernac command declaration *)
-open Extend
-open Pcoq
-open Genarg
-
-VERNAC ARGUMENT EXTEND divarg
-| [ "div" ":=" constr(adiv) ] -> [ adiv ]
-END
-
-VERNAC ARGUMENT EXTEND minusarg
-| [ "minus" ":=" constr(aminus) ] -> [ aminus ]
-END
-
-(*
-(* The v7->v8 translator needs printers, then temporary use ARGUMENT EXTEND...*)
-VERNAC ARGUMENT EXTEND minus_div_arg
-| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
-| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
-| [ ] -> [ None, None ]
-END
-*)
-
-(* For the translator, otherwise the code above is OK *)
-open Ppconstr
-let pp_minus_div_arg _prc _prlc _prt (omin,odiv) =
- if omin=None && odiv=None then mt() else
- spc() ++ str "with" ++
- pr_opt (fun c -> str "minus := " ++ _prc c) omin ++
- pr_opt (fun c -> str "div := " ++ _prc c) odiv
-(*
-let () =
- Pptactic.declare_extra_genarg_pprule true
- (rawwit_minus_div_arg,pp_minus_div_arg)
- (globwit_minus_div_arg,pp_minus_div_arg)
- (wit_minus_div_arg,pp_minus_div_arg)
-*)
-ARGUMENT EXTEND minus_div_arg
- TYPED AS constr_opt * constr_opt
- PRINTED BY pp_minus_div_arg
-| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
-| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
-| [ ] -> [ None, None ]
-END
-
-VERNAC COMMAND EXTEND Field
- [ "Add" "Legacy" "Field"
- constr(a) constr(aplus) constr(amult) constr(aone)
- constr(azero) constr(aopp) constr(aeq)
- constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]
- -> [ let (aminus_o, adiv_o) = md in
- add_field
- (constr_of a) (constr_of aplus) (constr_of amult)
- (constr_of aone) (constr_of azero) (constr_of aopp)
- (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
- (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l) ]
-END
-
-(* Guesses the type and calls field_gen with the right theory *)
-let field g =
- Coqlib.check_required_library ["Coq";"field";"LegacyField"];
- let typ =
- try match Hipattern.match_with_equation (pf_concl g) with
- | _,_,Hipattern.PolymorphicLeibnizEq (t,_,_) -> t
- | _ -> raise Exit
- with Hipattern.NoEquationFound | Exit ->
- error "The statement is not built from Leibniz' equality" in
- let th = VConstr ([],lookup (pf_env g) typ) in
- (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
- <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
-
-(* Verifies that all the terms have the same type and gives the right theory *)
-let guess_theory env evc = function
- | c::tl ->
- let t = type_of env evc c in
- if List.exists (fun c1 ->
- not (Reductionops.is_conv env evc t (type_of env evc c1))) tl then
- errorlabstrm "Field:" (str" All the terms must have the same type")
- else
- lookup env t
- | [] -> anomaly "Field: must have a non-empty constr list here"
-
-(* Guesses the type and calls Field_Term with the right theory *)
-let field_term l g =
- Coqlib.check_required_library ["Coq";"field";"LegacyField"];
- let env = (pf_env g)
- and evc = (project g) in
- let th = valueIn (VConstr ([],guess_theory env evc l))
- and nl = List.map (fun x -> valueIn (VConstr ([],x))) (Quote.sort_subterm g l) in
- (List.fold_right
- (fun c a ->
- let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
- Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g
-
-(* Declaration of Field *)
-
-TACTIC EXTEND legacy_field
-| [ "legacy" "field" ] -> [ field ]
-| [ "legacy" "field" ne_constr_list(l) ] -> [ field_term l ]
-END
2  plugins/field/field_plugin.mllib
View
@@ -1,2 +0,0 @@
-Field
-Field_plugin_mod
4 plugins/field/vo.itarget
View
@@ -1,4 +0,0 @@
-LegacyField_Compl.vo
-LegacyField_Tactic.vo
-LegacyField_Theory.vo
-LegacyField.vo
3  plugins/fourier/Fourier.v
View
@@ -8,8 +8,7 @@
(* "Fourier's method to solve linear inequations/equations systems.".*)
-Require Export LegacyRing.
-Require Export LegacyField.
+Require Export Field.
Require Export DiscrR.
Require Export Fourier_util.
Declare ML Module "fourier_plugin".
2  plugins/fourier/fourierR.ml
View
@@ -605,7 +605,7 @@ let rec fourier gl=
(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
[tclORELSE
- (Ring.polynom [])
+ (* TODO : Ring.polynom []*) tclIDTAC
tclIDTAC;
(tclTHEN (apply (get coq_sym_eqT))
(apply (get coq_Rinv_1)))]
1  plugins/micromega/Psatz.v
View
@@ -16,7 +16,6 @@ Require Import ZMicromega.
Require Import QMicromega.
Require Import RMicromega.
Require Import QArith.
-Require Export Ring_normalize.
Require Import ZArith.
Require Import Rdefinitions.
Require Export RingMicromega.
1  plugins/micromega/g_micromega.ml4
View
@@ -17,7 +17,6 @@
(*i camlp4deps: "grammar/grammar.cma" i*)
open Quote
-open Ring
open Mutils
open Glob_term
open Errors
2  plugins/pluginsbyte.itarget
View
@@ -1,5 +1,4 @@
btauto/btauto_plugin.cma
-field/field_plugin.cma
setoid_ring/newring_plugin.cma
extraction/extraction_plugin.cma
decl_mode/decl_mode_plugin.cma
@@ -10,7 +9,6 @@ romega/romega_plugin.cma
omega/omega_plugin.cma
micromega/micromega_plugin.cma
xml/xml_plugin.cma
-ring/ring_plugin.cma
cc/cc_plugin.cma
nsatz/nsatz_plugin.cma
funind/recdef_plugin.cma
2  plugins/pluginsopt.itarget
View
@@ -1,5 +1,4 @@
btauto/btauto_plugin.cmxa
-field/field_plugin.cmxa
setoid_ring/newring_plugin.cmxa
extraction/extraction_plugin.cmxa
decl_mode/decl_mode_plugin.cmxa
@@ -10,7 +9,6 @@ romega/romega_plugin.cmxa
omega/omega_plugin.cmxa
micromega/micromega_plugin.cmxa
xml/xml_plugin.cmxa
-ring/ring_plugin.cmxa
cc/cc_plugin.cmxa
nsatz/nsatz_plugin.cmxa
funind/recdef_plugin.cmxa
2  plugins/pluginsvo.itarget
View
@@ -1,12 +1,10 @@
btauto/vo.otarget
-field/vo.otarget
fourier/vo.otarget
funind/vo.otarget
nsatz/vo.otarget
micromega/vo.otarget
omega/vo.otarget
quote/vo.otarget
-ring/vo.otarget
romega/vo.otarget
rtauto/vo.otarget
setoid_ring/vo.otarget
88 plugins/ring/LegacyArithRing.v
View
@@ -1,88 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Instantiation of the Ring tactic for the naturals of Arith $*)
-
-Require Import Bool.
-Require Export LegacyRing.
-Require Export Arith.
-Require Import Eqdep_dec.
-
-Local Open Scope nat_scope.
-
-Fixpoint nateq (n m:nat) {struct m} : bool :=
- match n, m with
- | O, O => true
- | S n', S m' => nateq n' m'
- | _, _ => false
- end.
-
-Lemma nateq_prop : forall n m:nat, Is_true (nateq n m) -> n = m.
-Proof.
- simple induction n; simple induction m; intros; try contradiction.
- trivial.
- unfold Is_true in H1.
- rewrite (H n1 H1).
- trivial.
-Qed.
-
-Hint Resolve nateq_prop: arithring.
-
-Definition NatTheory : Semi_Ring_Theory plus mult 1 0 nateq.
- split; intros; auto with arith arithring.
-(* apply (fun n m p:nat => plus_reg_l m p n) with (n := n).
- trivial.*)
-Defined.
-
-
-Add Legacy Semi Ring nat plus mult 1 0 nateq NatTheory [ 0 S ].
-
-Goal forall n:nat, S n = 1 + n.
-intro; reflexivity.
-Save S_to_plus_one.
-
-(* Replace all occurrences of (S exp) by (plus (S O) exp), except when
- exp is already O and only for those occurrences than can be reached by going
- down plus and mult operations *)
-Ltac rewrite_S_to_plus_term t :=
- match constr:t with
- | 1 => constr:1
- | (S ?X1) =>
- let t1 := rewrite_S_to_plus_term X1 in
- constr:(1 + t1)
- | (?X1 + ?X2) =>
- let t1 := rewrite_S_to_plus_term X1
- with t2 := rewrite_S_to_plus_term X2 in
- constr:(t1 + t2)
- | (?X1 * ?X2) =>
- let t1 := rewrite_S_to_plus_term X1
- with t2 := rewrite_S_to_plus_term X2 in
- constr:(t1 * t2)
- | _ => constr:t
- end.
-
-(* Apply S_to_plus on both sides of an equality *)
-Ltac rewrite_S_to_plus :=
- match goal with
- | |- (?X1 = ?X2) =>
- try
- let t1 :=
- (**) (**)
- rewrite_S_to_plus_term X1
- with t2 := rewrite_S_to_plus_term X2 in
- change (t1 = t2)
- | |- (?X1 = ?X2) =>
- try
- let t1 :=
- (**) (**)
- rewrite_S_to_plus_term X1
- with t2 := rewrite_S_to_plus_term X2 in
- change (t1 = t2)
- end.
-
-Ltac ring_nat := rewrite_S_to_plus; ring.
43 plugins/ring/LegacyNArithRing.v
View
@@ -1,43 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Instantiation of the Ring tactic for the binary natural numbers *)
-
-Require Import Bool.
-Require Export LegacyRing.
-Require Export ZArith_base.
-Require Import NArith.
-Require Import Eqdep_dec.
-
-Definition Neq (n m:N) :=
- match (n ?= m)%N with
- | Datatypes.Eq => true
- | _ => false
- end.
-
-Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m.
- intros n m H; unfold Neq in H.
- apply N.compare_eq.
- destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ].
-Qed.
-
-Definition NTheory : Semi_Ring_Theory N.add N.mul 1%N 0%N Neq.
- split.
- apply N.add_comm.
- apply N.add_assoc.
- apply N.mul_comm.
- apply N.mul_assoc.
- apply N.add_0_l.
- apply N.mul_1_l.
- apply N.mul_0_l.
- apply N.mul_add_distr_r.
- apply Neq_prop.
-Qed.
-
-Add Legacy Semi Ring
- N N.add N.mul 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
35 plugins/ring/LegacyRing.v
View
@@ -1,35 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-Require Export Bool.
-Require Export LegacyRing_theory.
-Require Export Quote.
-Require Export Ring_normalize.
-Require Export Ring_abstract.
-Declare ML Module "ring_plugin".
-
-(* As an example, we provide an instantation for bool. *)
-(* Other instatiations are given in ArithRing and ZArithRing in the
- same directory *)
-
-Definition BoolTheory :
- Ring_Theory xorb andb true false (fun b:bool => b) eqb.
-split; simpl.
-destruct n; destruct m; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct n; destruct m; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct n; reflexivity.
-destruct n; reflexivity.
-destruct n; reflexivity.
-destruct n; destruct m; destruct p; reflexivity.
-destruct x; destruct y; reflexivity || simpl; tauto.
-Defined.
-
-Add Legacy Ring bool xorb andb true false (fun b:bool => b) eqb BoolTheory
- [ true false ].
374 plugins/ring/LegacyRing_theory.v
View
@@ -1,374 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-Require Export Bool.
-
-Set Implicit Arguments.
-
-Section Theory_of_semi_rings.
-
-Variable A : Type.
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-(* There is also a "weakly decidable" equality on A. That means
- that if (A_eq x y)=true then x=y but x=y can arise when
- (A_eq x y)=false. On an abstract ring the function [x,y:A]false
- is a good choice. The proof of A_eq_prop is in this case easy. *)
-Variable Aeq : A -> A -> bool.
-
-Infix "+" := Aplus (at level 50, left associativity).
-Infix "*" := Amult (at level 40, left associativity).
-Notation "0" := Azero.
-Notation "1" := Aone.
-
-Record Semi_Ring_Theory : Prop :=
- {SR_plus_comm : forall n m:A, n + m = m + n;
- SR_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
- SR_mult_comm : forall n m:A, n * m = m * n;
- SR_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
- SR_plus_zero_left : forall n:A, 0 + n = n;
- SR_mult_one_left : forall n:A, 1 * n = n;
- SR_mult_zero_left : forall n:A, 0 * n = 0;
- SR_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
-(* SR_plus_reg_left : forall n m p:A, n + m = n + p -> m = p;*)
- SR_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
-
-Variable T : Semi_Ring_Theory.
-
-Let plus_comm := SR_plus_comm T.
-Let plus_assoc := SR_plus_assoc T.
-Let mult_comm := SR_mult_comm T.
-Let mult_assoc := SR_mult_assoc T.
-Let plus_zero_left := SR_plus_zero_left T.
-Let mult_one_left := SR_mult_one_left T.
-Let mult_zero_left := SR_mult_zero_left T.
-Let distr_left := SR_distr_left T.
-(*Let plus_reg_left := SR_plus_reg_left T.*)
-
-Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
- mult_one_left mult_zero_left distr_left (*plus_reg_left*).
-
-(* Lemmas whose form is x=y are also provided in form y=x because Auto does
- not symmetry *)
-Lemma SR_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p).
-symmetry ; eauto. Qed.
-
-Lemma SR_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p).
-symmetry ; eauto. Qed.
-
-Lemma SR_plus_zero_left2 : forall n:A, n = 0 + n.
-symmetry ; eauto. Qed.
-
-Lemma SR_mult_one_left2 : forall n:A, n = 1 * n.
-symmetry ; eauto. Qed.
-
-Lemma SR_mult_zero_left2 : forall n:A, 0 = 0 * n.
-symmetry ; eauto. Qed.
-
-Lemma SR_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p.
-symmetry ; eauto. Qed.
-
-Lemma SR_plus_permute : forall n m p:A, n + (m + p) = m + (n + p).
-intros.
-rewrite plus_assoc.
-elim (plus_comm m n).
-rewrite <- plus_assoc.
-reflexivity.
-Qed.
-
-Lemma SR_mult_permute : forall n m p:A, n * (m * p) = m * (n * p).
-intros.
-rewrite mult_assoc.
-elim (mult_comm m n).
-rewrite <- mult_assoc.
-reflexivity.
-Qed.
-
-Hint Resolve SR_plus_permute SR_mult_permute.
-
-Lemma SR_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
-intros.
-repeat rewrite (mult_comm n).
-eauto.
-Qed.
-
-Lemma SR_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p).
-symmetry ; apply SR_distr_right. Qed.
-
-Lemma SR_mult_zero_right : forall n:A, n * 0 = 0.
-intro; rewrite mult_comm; eauto.
-Qed.
-
-Lemma SR_mult_zero_right2 : forall n:A, 0 = n * 0.
-intro; rewrite mult_comm; eauto.
-Qed.
-
-Lemma SR_plus_zero_right : forall n:A, n + 0 = n.
-intro; rewrite plus_comm; eauto.
-Qed.
-Lemma SR_plus_zero_right2 : forall n:A, n = n + 0.
-intro; rewrite plus_comm; eauto.
-Qed.
-
-Lemma SR_mult_one_right : forall n:A, n * 1 = n.
-intro; elim mult_comm; auto.
-Qed.
-
-Lemma SR_mult_one_right2 : forall n:A, n = n * 1.
-intro; elim mult_comm; auto.
-Qed.
-(*
-Lemma SR_plus_reg_right : forall n m p:A, m + n = p + n -> m = p.
-intros n m p; rewrite (plus_comm m n); rewrite (plus_comm p n); eauto.
-Qed.
-*)
-End Theory_of_semi_rings.
-
-Section Theory_of_rings.
-
-Variable A : Type.
-
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-Variable Aopp : A -> A.
-Variable Aeq : A -> A -> bool.
-
-Infix "+" := Aplus (at level 50, left associativity).
-Infix "*" := Amult (at level 40, left associativity).
-Notation "0" := Azero.
-Notation "1" := Aone.
-Notation "- x" := (Aopp x).
-
-Record Ring_Theory : Prop :=
- {Th_plus_comm : forall n m:A, n + m = m + n;
- Th_plus_assoc : forall n m p:A, n + (m + p) = n + m + p;
- Th_mult_comm : forall n m:A, n * m = m * n;
- Th_mult_assoc : forall n m p:A, n * (m * p) = n * m * p;
- Th_plus_zero_left : forall n:A, 0 + n = n;
- Th_mult_one_left : forall n:A, 1 * n = n;
- Th_opp_def : forall n:A, n + - n = 0;
- Th_distr_left : forall n m p:A, (n + m) * p = n * p + m * p;
- Th_eq_prop : forall x y:A, Is_true (Aeq x y) -> x = y}.
-
-Variable T : Ring_Theory.
-
-Let plus_comm := Th_plus_comm T.
-Let plus_assoc := Th_plus_assoc T.
-Let mult_comm := Th_mult_comm T.
-Let mult_assoc := Th_mult_assoc T.
-Let plus_zero_left := Th_plus_zero_left T.
-Let mult_one_left := Th_mult_one_left T.
-Let opp_def := Th_opp_def T.
-Let distr_left := Th_distr_left T.
-
-Hint Resolve plus_comm plus_assoc mult_comm mult_assoc plus_zero_left
- mult_one_left opp_def distr_left.
-
-(* Lemmas whose form is x=y are also provided in form y=x because Auto does
- not symmetry *)
-Lemma Th_mult_assoc2 : forall n m p:A, n * m * p = n * (m * p).
-symmetry ; eauto. Qed.
-
-Lemma Th_plus_assoc2 : forall n m p:A, n + m + p = n + (m + p).
-symmetry ; eauto. Qed.
-
-Lemma Th_plus_zero_left2 : forall n:A, n = 0 + n.
-symmetry ; eauto. Qed.
-
-Lemma Th_mult_one_left2 : forall n:A, n = 1 * n.
-symmetry ; eauto. Qed.
-
-Lemma Th_distr_left2 : forall n m p:A, n * p + m * p = (n + m) * p.
-symmetry ; eauto. Qed.
-
-Lemma Th_opp_def2 : forall n:A, 0 = n + - n.
-symmetry ; eauto. Qed.
-
-Lemma Th_plus_permute : forall n m p:A, n + (m + p) = m + (n + p).
-intros.
-rewrite plus_assoc.
-elim (plus_comm m n).
-rewrite <- plus_assoc.
-reflexivity.
-Qed.
-
-Lemma Th_mult_permute : forall n m p:A, n * (m * p) = m * (n * p).
-intros.
-rewrite mult_assoc.
-elim (mult_comm m n).
-rewrite <- mult_assoc.
-reflexivity.
-Qed.
-
-Hint Resolve Th_plus_permute Th_mult_permute.
-
-Lemma aux1 : forall a:A, a + a = a -> a = 0.
-intros.
-generalize (opp_def a).
-pattern a at 1.
-rewrite <- H.
-rewrite <- plus_assoc.
-rewrite opp_def.
-elim plus_comm.
-rewrite plus_zero_left.
-trivial.
-Qed.
-
-Lemma Th_mult_zero_left : forall n:A, 0 * n = 0.
-intros.
-apply aux1.
-rewrite <- distr_left.
-rewrite plus_zero_left.
-reflexivity.
-Qed.
-Hint Resolve Th_mult_zero_left.
-
-Lemma Th_mult_zero_left2 : forall n:A, 0 = 0 * n.
-symmetry ; eauto. Qed.
-
-Lemma aux2 : forall x y z:A, x + y = 0 -> x + z = 0 -> y = z.
-intros.
-rewrite <- (plus_zero_left y).
-elim H0.
-elim plus_assoc.
-elim (plus_comm y z).
-rewrite plus_assoc.
-rewrite H.
-rewrite plus_zero_left.
-reflexivity.
-Qed.
-
-Lemma Th_opp_mult_left : forall x y:A, - (x * y) = - x * y.
-intros.
-apply (aux2 (x:=(x * y)));
- [ apply opp_def | rewrite <- distr_left; rewrite opp_def; auto ].
-Qed.
-Hint Resolve Th_opp_mult_left.
-
-Lemma Th_opp_mult_left2 : forall x y:A, - x * y = - (x * y).
-symmetry ; eauto. Qed.
-
-Lemma Th_mult_zero_right : forall n:A, n * 0 = 0.
-intro; elim mult_comm; eauto.
-Qed.
-
-Lemma Th_mult_zero_right2 : forall n:A, 0 = n * 0.
-intro; elim mult_comm; eauto.
-Qed.
-
-Lemma Th_plus_zero_right : forall n:A, n + 0 = n.
-intro; rewrite plus_comm; eauto.
-Qed.
-
-Lemma Th_plus_zero_right2 : forall n:A, n = n + 0.
-intro; rewrite plus_comm; eauto.
-Qed.
-
-Lemma Th_mult_one_right : forall n:A, n * 1 = n.
-intro; elim mult_comm; eauto.
-Qed.
-
-Lemma Th_mult_one_right2 : forall n:A, n = n * 1.
-intro; elim mult_comm; eauto.
-Qed.
-
-Lemma Th_opp_mult_right : forall x y:A, - (x * y) = x * - y.
-intros; do 2 rewrite (mult_comm x); auto.
-Qed.
-
-Lemma Th_opp_mult_right2 : forall x y:A, x * - y = - (x * y).
-intros; do 2 rewrite (mult_comm x); auto.
-Qed.
-
-Lemma Th_plus_opp_opp : forall x y:A, - x + - y = - (x + y).
-intros.
-apply (aux2 (x:=(x + y)));
- [ elim plus_assoc; rewrite (Th_plus_permute y (- x)); rewrite plus_assoc;
- rewrite opp_def; rewrite plus_zero_left; auto
- | auto ].
-Qed.
-
-Lemma Th_plus_permute_opp : forall n m p:A, - m + (n + p) = n + (- m + p).
-eauto. Qed.
-
-Lemma Th_opp_opp : forall n:A, - - n = n.
-intro; apply (aux2 (x:=(- n))); [ auto | elim plus_comm; auto ].
-Qed.
-Hint Resolve Th_opp_opp.
-
-Lemma Th_opp_opp2 : forall n:A, n = - - n.
-symmetry ; eauto. Qed.
-
-Lemma Th_mult_opp_opp : forall x y:A, - x * - y = x * y.
-intros; rewrite <- Th_opp_mult_left; rewrite <- Th_opp_mult_right; auto.
-Qed.
-
-Lemma Th_mult_opp_opp2 : forall x y:A, x * y = - x * - y.
-symmetry ; apply Th_mult_opp_opp. Qed.
-
-Lemma Th_opp_zero : - 0 = 0.
-rewrite <- (plus_zero_left (- 0)).
-auto. Qed.
-(*
-Lemma Th_plus_reg_left : forall n m p:A, n + m = n + p -> m = p.
-intros; generalize (f_equal (fun z => - n + z) H).
-repeat rewrite plus_assoc.
-rewrite (plus_comm (- n) n).
-rewrite opp_def.
-repeat rewrite Th_plus_zero_left; eauto.
-Qed.
-
-Lemma Th_plus_reg_right : forall n m p:A, m + n = p + n -> m = p.
-intros.
-eapply Th_plus_reg_left with n.
-rewrite (plus_comm n m).
-rewrite (plus_comm n p).
-auto.
-Qed.
-*)
-Lemma Th_distr_right : forall n m p:A, n * (m + p) = n * m + n * p.
-intros.
-repeat rewrite (mult_comm n).
-eauto.
-Qed.
-
-Lemma Th_distr_right2 : forall n m p:A, n * m + n * p = n * (m + p).
-symmetry ; apply Th_distr_right.
-Qed.
-
-End Theory_of_rings.
-
-Hint Resolve Th_mult_zero_left (*Th_plus_reg_left*): core.
-
-Unset Implicit Arguments.
-
-Definition Semi_Ring_Theory_of :
- forall (A:Type) (Aplus Amult:A -> A -> A) (Aone Azero:A)
- (Aopp:A -> A) (Aeq:A -> A -> bool),
- Ring_Theory Aplus Amult Aone Azero Aopp Aeq ->
- Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
-intros until 1; case H.
-split; intros; simpl; eauto.
-Defined.
-
-(* Every ring can be viewed as a semi-ring : this property will be used
- in Abstract_polynom. *)
-Coercion Semi_Ring_Theory_of : Ring_Theory >-> Semi_Ring_Theory.
-
-
-Section product_ring.
-
-End product_ring.
-
-Section power_ring.
-
-End power_ring.
35 plugins/ring/LegacyZArithRing.v
View
@@ -1,35 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(* Instantiation of the Ring tactic for the binary integers of ZArith *)
-
-Require Export LegacyArithRing.
-Require Export ZArith_base.
-Require Import Eqdep_dec.
-Require Import LegacyRing.
-
-Definition Zeq (x y:Z) :=
- match (x ?= y)%Z with
- | Datatypes.Eq => true
- | _ => false
- end.
-
-Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y.
- intros x y H; unfold Zeq in H.
- apply Z.compare_eq.
- destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ].
-Qed.
-
-Definition ZTheory : Ring_Theory Z.add Z.mul 1%Z 0%Z Z.opp Zeq.
- split; intros; eauto with zarith.
- apply Zeq_prop; assumption.
-Qed.
-
-(* NatConstants and NatTheory are defined in Ring_theory.v *)
-Add Legacy Ring Z Z.add Z.mul 1%Z 0%Z Z.opp Zeq ZTheory
- [ Zpos Zneg 0%Z xO xI 1%positive ].
700 plugins/ring/Ring_abstract.v
View
@@ -1,700 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-Require Import LegacyRing_theory.
-Require Import Quote.
-Require Import Ring_normalize.
-
-Section abstract_semi_rings.
-
-Inductive aspolynomial : Type :=
- | ASPvar : index -> aspolynomial
- | ASP0 : aspolynomial
- | ASP1 : aspolynomial
- | ASPplus : aspolynomial -> aspolynomial -> aspolynomial
- | ASPmult : aspolynomial -> aspolynomial -> aspolynomial.
-
-Inductive abstract_sum : Type :=
- | Nil_acs : abstract_sum
- | Cons_acs : varlist -> abstract_sum -> abstract_sum.
-
-Fixpoint abstract_sum_merge (s1:abstract_sum) :
- abstract_sum -> abstract_sum :=
- match s1 with
- | Cons_acs l1 t1 =>
- (fix asm_aux (s2:abstract_sum) : abstract_sum :=
- match s2 with
- | Cons_acs l2 t2 =>
- if varlist_lt l1 l2
- then Cons_acs l1 (abstract_sum_merge t1 s2)
- else Cons_acs l2 (asm_aux t2)
- | Nil_acs => s1
- end)
- | Nil_acs => fun s2 => s2
- end.
-
-Fixpoint abstract_varlist_insert (l1:varlist) (s2:abstract_sum) {struct s2} :
- abstract_sum :=
- match s2 with
- | Cons_acs l2 t2 =>
- if varlist_lt l1 l2
- then Cons_acs l1 s2
- else Cons_acs l2 (abstract_varlist_insert l1 t2)
- | Nil_acs => Cons_acs l1 Nil_acs
- end.
-
-Fixpoint abstract_sum_scalar (l1:varlist) (s2:abstract_sum) {struct s2} :
- abstract_sum :=
- match s2 with
- | Cons_acs l2 t2 =>
- abstract_varlist_insert (varlist_merge l1 l2)
- (abstract_sum_scalar l1 t2)
- | Nil_acs => Nil_acs
- end.
-
-Fixpoint abstract_sum_prod (s1 s2:abstract_sum) {struct s1} : abstract_sum :=
- match s1 with
- | Cons_acs l1 t1 =>
- abstract_sum_merge (abstract_sum_scalar l1 s2)
- (abstract_sum_prod t1 s2)
- | Nil_acs => Nil_acs
- end.
-
-Fixpoint aspolynomial_normalize (p:aspolynomial) : abstract_sum :=
- match p with
- | ASPvar i => Cons_acs (Cons_var i Nil_var) Nil_acs
- | ASP1 => Cons_acs Nil_var Nil_acs
- | ASP0 => Nil_acs
- | ASPplus l r =>
- abstract_sum_merge (aspolynomial_normalize l)
- (aspolynomial_normalize r)
- | ASPmult l r =>
- abstract_sum_prod (aspolynomial_normalize l) (aspolynomial_normalize r)
- end.
-
-
-
-Variable A : Type.
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-Variable Aeq : A -> A -> bool.
-Variable vm : varmap A.
-Variable T : Semi_Ring_Theory Aplus Amult Aone Azero Aeq.
-
-Fixpoint interp_asp (p:aspolynomial) : A :=
- match p with
- | ASPvar i => interp_var Azero vm i
- | ASP0 => Azero
- | ASP1 => Aone
- | ASPplus l r => Aplus (interp_asp l) (interp_asp r)
- | ASPmult l r => Amult (interp_asp l) (interp_asp r)
- end.
-
-(* Local *) Definition iacs_aux :=
- (fix iacs_aux (a:A) (s:abstract_sum) {struct s} : A :=
- match s with
- | Nil_acs => a
- | Cons_acs l t =>
- Aplus a (iacs_aux (interp_vl Amult Aone Azero vm l) t)
- end).
-
-Definition interp_acs (s:abstract_sum) : A :=
- match s with
- | Cons_acs l t => iacs_aux (interp_vl Amult Aone Azero vm l) t
- | Nil_acs => Azero
- end.
-
-Hint Resolve (SR_plus_comm T).
-Hint Resolve (SR_plus_assoc T).
-Hint Resolve (SR_plus_assoc2 T).
-Hint Resolve (SR_mult_comm T).
-Hint Resolve (SR_mult_assoc T).
-Hint Resolve (SR_mult_assoc2 T).
-Hint Resolve (SR_plus_zero_left T).
-Hint Resolve (SR_plus_zero_left2 T).
-Hint Resolve (SR_mult_one_left T).
-Hint Resolve (SR_mult_one_left2 T).
-Hint Resolve (SR_mult_zero_left T).
-Hint Resolve (SR_mult_zero_left2 T).
-Hint Resolve (SR_distr_left T).
-Hint Resolve (SR_distr_left2 T).
-(*Hint Resolve (SR_plus_reg_left T).*)
-Hint Resolve (SR_plus_permute T).
-Hint Resolve (SR_mult_permute T).
-Hint Resolve (SR_distr_right T).
-Hint Resolve (SR_distr_right2 T).
-Hint Resolve (SR_mult_zero_right T).
-Hint Resolve (SR_mult_zero_right2 T).
-Hint Resolve (SR_plus_zero_right T).
-Hint Resolve (SR_plus_zero_right2 T).
-Hint Resolve (SR_mult_one_right T).
-Hint Resolve (SR_mult_one_right2 T).
-(*Hint Resolve (SR_plus_reg_right T).*)
-Hint Resolve eq_refl eq_sym eq_trans.
-Hint Immediate T.
-
-Remark iacs_aux_ok :
- forall (x:A) (s:abstract_sum), iacs_aux x s = Aplus x (interp_acs s).
-Proof.
- simple induction s; simpl; intros.
- trivial.
- reflexivity.
-Qed.
-
-Hint Extern 10 (_ = _ :>A) => rewrite iacs_aux_ok: core.
-
-Lemma abstract_varlist_insert_ok :
- forall (l:varlist) (s:abstract_sum),
- interp_acs (abstract_varlist_insert l s) =
- Aplus (interp_vl Amult Aone Azero vm l) (interp_acs s).
-
- simple induction s.
- trivial.
-
- simpl; intros.
- elim (varlist_lt l v); simpl.
- eauto.
- rewrite iacs_aux_ok.
- rewrite H; auto.
-
-Qed.
-
-Lemma abstract_sum_merge_ok :
- forall x y:abstract_sum,
- interp_acs (abstract_sum_merge x y) = Aplus (interp_acs x) (interp_acs y).
-
-Proof.
- simple induction x.
- trivial.
- simple induction y; intros.
-
- auto.
-
- simpl; elim (varlist_lt v v0); simpl.
- repeat rewrite iacs_aux_ok.
- rewrite H; simpl; auto.
-
- simpl in H0.
- repeat rewrite iacs_aux_ok.
- rewrite H0. simpl; auto.
-Qed.
-
-Lemma abstract_sum_scalar_ok :
- forall (l:varlist) (s:abstract_sum),
- interp_acs (abstract_sum_scalar l s) =
- Amult (interp_vl Amult Aone Azero vm l) (interp_acs s).
-Proof.
- simple induction s.
- simpl; eauto.
-
- simpl; intros.
- rewrite iacs_aux_ok.
- rewrite abstract_varlist_insert_ok.
- rewrite H.
- rewrite (varlist_merge_ok A Aplus Amult Aone Azero Aeq vm T).
- auto.
-Qed.
-
-Lemma abstract_sum_prod_ok :
- forall x y:abstract_sum,
- interp_acs (abstract_sum_prod x y) = Amult (interp_acs x) (interp_acs y).
-
-Proof.
- simple induction x.
- intros; simpl; eauto.
-
- destruct y as [| v0 a0]; intros.
-
- simpl; rewrite H; eauto.
-
- unfold abstract_sum_prod; fold abstract_sum_prod.
- rewrite abstract_sum_merge_ok.
- rewrite abstract_sum_scalar_ok.
- rewrite H; simpl; auto.
-Qed.
-
-Theorem aspolynomial_normalize_ok :
- forall x:aspolynomial, interp_asp x = interp_acs (aspolynomial_normalize x).
-Proof.
- simple induction x; simpl; intros; trivial.
- rewrite abstract_sum_merge_ok.
- rewrite H; rewrite H0; eauto.
- rewrite abstract_sum_prod_ok.
- rewrite H; rewrite H0; eauto.
-Qed.
-
-End abstract_semi_rings.
-
-Section abstract_rings.
-
-(* In abstract polynomials there is no constants other
- than 0 and 1. An abstract ring is a ring whose operations plus,
- and mult are not functions but constructors. In other words,
- when c1 and c2 are closed, (plus c1 c2) doesn't reduce to a closed
- term. "closed" mean here "without plus and mult". *)
-
-(* this section is not parametrized by a (semi-)ring.
- Nevertheless, they are two different types for semi-rings and rings
- and there will be 2 correction theorems *)
-
-Inductive apolynomial : Type :=
- | APvar : index -> apolynomial
- | AP0 : apolynomial
- | AP1 : apolynomial
- | APplus : apolynomial -> apolynomial -> apolynomial
- | APmult : apolynomial -> apolynomial -> apolynomial
- | APopp : apolynomial -> apolynomial.
-
-(* A canonical "abstract" sum is a list of varlist with the sign "+" or "-".
- Invariant : the list is sorted and there is no varlist is present
- with both signs. +x +x +x -x is forbidden => the canonical form is +x+x *)
-
-Inductive signed_sum : Type :=
- | Nil_varlist : signed_sum
- | Plus_varlist : varlist -> signed_sum -> signed_sum
- | Minus_varlist : varlist -> signed_sum -> signed_sum.
-
-Fixpoint signed_sum_merge (s1:signed_sum) : signed_sum -> signed_sum :=
- match s1 with
- | Plus_varlist l1 t1 =>
- (fix ssm_aux (s2:signed_sum) : signed_sum :=
- match s2 with
- | Plus_varlist l2 t2 =>
- if varlist_lt l1 l2
- then Plus_varlist l1 (signed_sum_merge t1 s2)
- else Plus_varlist l2 (ssm_aux t2)
- | Minus_varlist l2 t2 =>
- if varlist_eq l1 l2
- then signed_sum_merge t1 t2
- else
- if varlist_lt l1 l2
- then Plus_varlist l1 (signed_sum_merge t1 s2)
- else Minus_varlist l2 (ssm_aux t2)
- | Nil_varlist => s1
- end)
- | Minus_varlist l1 t1 =>
- (fix ssm_aux2 (s2:signed_sum) : signed_sum :=
- match s2 with
- | Plus_varlist l2 t2 =>
- if varlist_eq l1 l2
- then signed_sum_merge t1 t2
- else
- if varlist_lt l1 l2
- then Minus_varlist l1 (signed_sum_merge t1 s2)
- else Plus_varlist l2 (ssm_aux2 t2)
- | Minus_varlist l2 t2 =>
- if varlist_lt l1 l2
- then Minus_varlist l1 (signed_sum_merge t1 s2)
- else Minus_varlist l2 (ssm_aux2 t2)
- | Nil_varlist => s1
- end)
- | Nil_varlist => fun s2 => s2
- end.
-
-Fixpoint plus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} :
- signed_sum :=
- match s2 with
- | Plus_varlist l2 t2 =>
- if varlist_lt l1 l2
- then Plus_varlist l1 s2
- else Plus_varlist l2 (plus_varlist_insert l1 t2)
- | Minus_varlist l2 t2 =>
- if varlist_eq l1 l2
- then t2
- else
- if varlist_lt l1 l2
- then Plus_varlist l1 s2
- else Minus_varlist l2 (plus_varlist_insert l1 t2)
- | Nil_varlist => Plus_varlist l1 Nil_varlist
- end.
-
-Fixpoint minus_varlist_insert (l1:varlist) (s2:signed_sum) {struct s2} :
- signed_sum :=
- match s2 with
- | Plus_varlist l2 t2 =>
- if varlist_eq l1 l2
- then t2
- else
- if varlist_lt l1 l2
- then Minus_varlist l1 s2
- else Plus_varlist l2 (minus_varlis