[build] Consolidate stdlib's .v files under a single directory.

Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.

This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.

We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.

Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.

This could also imply a performance gain as we now effectively
traverse less directories when locating a library.

See also discussion in #10003

1 files changed, 0 insertions, 894 deletions

diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
deleted file mode 100644
index dc096554c8..0000000000
--- a/plugins/setoid_ring/InitialRing.v
+++ /dev/null
@@ -1,894 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-Require Import Zbool.
-Require Import BinInt.
-Require Import BinNat.
-Require Import Setoid.
-Require Import Ring_theory.
-Require Import Ring_polynom.
-Import List.
-
-Set Implicit Arguments.
-(* Set Universe Polymorphism. *)
-
-Import RingSyntax.
-
-(* An object to return when an expression is not recognized as a constant *)
-Definition NotConstant := false.
-
-(** Z is a ring and a setoid*)
-
-Lemma Zsth : Setoid_Theory Z (@eq Z).
-Proof (Eqsth Z).
-
-Lemma Zeqe : ring_eq_ext Z.add Z.mul Z.opp (@eq Z).
-Proof (Eq_ext Z.add Z.mul Z.opp).
-
-Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z).
-Proof.
- constructor. exact Z.add_0_l. exact Z.add_comm. exact Z.add_assoc.
- exact Z.mul_1_l. exact Z.mul_comm. exact Z.mul_assoc.
- exact Z.mul_add_distr_r. trivial. exact Z.sub_diag.
-Qed.
-
-(** Two generic morphisms from Z to (abrbitrary) rings, *)
-(**second one is more convenient for proofs but they are ext. equal*)
-Section ZMORPHISM.
- Variable R : Type.
- Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
- Variable req : R -> R -> Prop.
-  Notation "0" := rO.  Notation "1" := rI.
-  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
-  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
-  Notation "x == y" := (req x y).
-  Variable Rsth : Setoid_Theory R req.
-     Add Parametric Relation : R req
-       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
-       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
-       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
-      as R_setoid3.
-     Ltac rrefl := gen_reflexivity Rsth.
- Variable Reqe : ring_eq_ext radd rmul ropp req.
-   Add Morphism radd with signature (req ==> req ==> req) as radd_ext3.
-   Proof. exact (Radd_ext Reqe). Qed.
-   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext3.
-   Proof. exact (Rmul_ext Reqe). Qed.
-   Add Morphism ropp with signature (req ==> req) as ropp_ext3.
-   Proof. exact (Ropp_ext Reqe). Qed.
-
- Fixpoint gen_phiPOS1 (p:positive) : R :=
-  match p with
-  | xH => 1
-  | xO p => (1 + 1) * (gen_phiPOS1 p)
-  | xI p => 1 + ((1 + 1) * (gen_phiPOS1 p))
-  end.
-
- Fixpoint gen_phiPOS (p:positive) : R :=
-  match p with
-  | xH => 1
-  | xO xH => (1 + 1)
-  | xO p => (1 + 1) * (gen_phiPOS p)
-  | xI xH => 1 + (1 +1)
-  | xI p => 1 + ((1 + 1) * (gen_phiPOS p))
-  end.
-
- Definition gen_phiZ1 z :=
-  match z with
-  | Zpos p => gen_phiPOS1 p
-  | Z0 => 0
-  | Zneg p => -(gen_phiPOS1 p)
-  end.
-
- Definition gen_phiZ z :=
-  match z with
-  | Zpos p => gen_phiPOS p
-  | Z0 => 0
-  | Zneg p => -(gen_phiPOS p)
-  end.
- Notation "[ x ]" := (gen_phiZ x).
-
- Definition get_signZ z :=
-  match z with
-  | Zneg p => Some (Zpos p)
-  | _ => None
-  end.
-
- Lemma get_signZ_th : sign_theory Z.opp Zeq_bool get_signZ.
- Proof.
-  constructor.
-  destruct c;intros;try discriminate.
-  injection H as [= <-].
-  simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial.
- Qed.
-
-
- Section ALMOST_RING.
- Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
-   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext3.
-   Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite Rsth Reqe ARth.
-   Ltac add_push := gen_add_push radd Rsth Reqe ARth.
-
- Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
- Proof.
-  induction x;simpl.
-  rewrite IHx;destruct x;simpl;norm.
-  rewrite IHx;destruct x;simpl;norm.
-  rrefl.
- Qed.
-
- Lemma ARgen_phiPOS_Psucc : forall x,
-   gen_phiPOS1 (Pos.succ x) == 1 + (gen_phiPOS1 x).
- Proof.
-  induction x;simpl;norm.
-  rewrite IHx;norm.
-  add_push 1;rrefl.
- Qed.
-
- Lemma ARgen_phiPOS_add : forall x y,
-   gen_phiPOS1 (x + y) == (gen_phiPOS1 x) + (gen_phiPOS1 y).
- Proof.
-  induction x;destruct y;simpl;norm.
-  rewrite Pos.add_carry_spec.
-  rewrite ARgen_phiPOS_Psucc.
-  rewrite IHx;norm.
-  add_push (gen_phiPOS1 y);add_push 1;rrefl.
-  rewrite IHx;norm;add_push (gen_phiPOS1 y);rrefl.
-  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl.
-  rewrite IHx;norm;add_push(gen_phiPOS1 y); add_push 1;rrefl.
-  rewrite IHx;norm;add_push(gen_phiPOS1 y);rrefl.
-  add_push 1;rrefl.
-  rewrite ARgen_phiPOS_Psucc;norm;add_push 1;rrefl.
- Qed.
-
- Lemma ARgen_phiPOS_mult :
-   forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
- Proof.
-  induction x;intros;simpl;norm.
-  rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm.
-  rewrite IHx;rrefl.
- Qed.
-
- End ALMOST_RING.
-
- Variable Rth : ring_theory 0 1 radd rmul rsub ropp req.
- Let ARth := Rth_ARth Rsth Reqe Rth.
-   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext4.
-   Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite Rsth Reqe ARth.
-   Ltac add_push := gen_add_push radd Rsth Reqe ARth.
-
-(*morphisms are extensionally equal*)
- Lemma same_genZ : forall x, [x] == gen_phiZ1 x.
- Proof.
-  destruct x;simpl; try rewrite (same_gen ARth);rrefl.
- Qed.
-
- Lemma gen_Zeqb_ok : forall x y,
-   Zeq_bool x y = true -> [x] == [y].
- Proof.
-  intros x y H.
-  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
-  rewrite H1;rrefl.
- Qed.
-
- Lemma gen_phiZ1_pos_sub : forall x y,
- gen_phiZ1 (Z.pos_sub x y) == gen_phiPOS1 x + -gen_phiPOS1 y.
- Proof.
-  intros x y.
-  rewrite Z.pos_sub_spec.
-  case Pos.compare_spec; intros H; simpl.
-  rewrite H. rewrite (Ropp_def Rth);rrefl.
-  rewrite <- (Pos.sub_add y x H) at 2. rewrite Pos.add_comm.
-  rewrite (ARgen_phiPOS_add ARth);simpl;norm.
-  rewrite (Ropp_def Rth);norm.
-  rewrite <- (Pos.sub_add x y H) at 2.
-  rewrite (ARgen_phiPOS_add ARth);simpl;norm.
-  add_push (gen_phiPOS1 (x-y));rewrite (Ropp_def Rth); norm.
- Qed.
-
- Lemma gen_phiZ_add : forall x y, [x + y] == [x] + [y].
- Proof.
-  intros x y; repeat rewrite same_genZ; generalize x y;clear x y.
-  destruct x, y; simpl; norm.
-  apply (ARgen_phiPOS_add ARth).
-  apply gen_phiZ1_pos_sub.
-  rewrite gen_phiZ1_pos_sub. apply (Radd_comm Rth).
-  rewrite (ARgen_phiPOS_add ARth); norm.
- Qed.
-
- Lemma gen_phiZ_mul : forall x y, [x * y] == [x] * [y].
- Proof.
-  intros x y;repeat rewrite same_genZ.
-  destruct x;destruct y;simpl;norm;
-  rewrite  (ARgen_phiPOS_mult ARth);try (norm;fail).
-  rewrite (Ropp_opp Rsth Reqe Rth);rrefl.
- Qed.
-
- Lemma gen_phiZ_ext : forall x y : Z, x = y -> [x] == [y].
- Proof. intros;subst;rrefl. Qed.
-
-(*proof that [.] satisfies morphism specifications*)
- Lemma gen_phiZ_morph :
-  ring_morph 0 1 radd rmul rsub ropp req Z0 (Zpos xH)
-   Z.add Z.mul Z.sub Z.opp Zeq_bool gen_phiZ.
- Proof.
-  assert ( SRmorph : semi_morph 0 1 radd rmul req Z0 (Zpos xH)
-                  Z.add Z.mul Zeq_bool gen_phiZ).
-   apply mkRmorph;simpl;try rrefl.
-   apply gen_phiZ_add.  apply gen_phiZ_mul. apply gen_Zeqb_ok.
-  apply  (Smorph_morph Rsth Reqe Rth Zth SRmorph gen_phiZ_ext).
- Qed.
-
-End ZMORPHISM.
-
-(** N is a semi-ring and a setoid*)
-Lemma Nsth : Setoid_Theory N (@eq N).
-Proof (Eqsth N).
-
-Lemma Nseqe : sring_eq_ext N.add N.mul (@eq N).
-Proof (Eq_s_ext N.add N.mul).
-
-Lemma Nth : semi_ring_theory 0%N 1%N N.add N.mul (@eq N).
-Proof.
- constructor. exact N.add_0_l. exact N.add_comm. exact N.add_assoc.
- exact N.mul_1_l. exact N.mul_0_l. exact N.mul_comm. exact N.mul_assoc.
- exact N.mul_add_distr_r.
-Qed.
-
-Definition Nsub := SRsub N.add.
-Definition Nopp := (@SRopp N).
-
-Lemma Neqe : ring_eq_ext N.add N.mul Nopp (@eq N).
-Proof (SReqe_Reqe Nseqe).
-
-Lemma Nath :
- almost_ring_theory 0%N 1%N N.add N.mul Nsub Nopp (@eq N).
-Proof (SRth_ARth Nsth Nth).
-
-Lemma Neqb_ok : forall x y, N.eqb x y = true -> x = y.
-Proof. exact (fun x y => proj1 (N.eqb_eq x y)). Qed.
-
-(**Same as above : definition of two, extensionally equal, generic morphisms *)
-(**from N to any semi-ring*)
-Section NMORPHISM.
- Variable R : Type.
- Variable  (rO rI : R) (radd rmul: R->R->R).
- Variable req : R -> R -> Prop.
-  Notation "0" := rO.  Notation "1" := rI.
-  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
- Variable Rsth : Setoid_Theory R req.
-     Add Parametric Relation : R req
-       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
-       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
-       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
-       as R_setoid4.
-     Ltac rrefl := gen_reflexivity Rsth.
- Variable SReqe : sring_eq_ext radd rmul req.
- Variable SRth : semi_ring_theory 0 1 radd rmul req.
- Let ARth := SRth_ARth Rsth SRth.
- Let Reqe := SReqe_Reqe SReqe.
- Let ropp := (@SRopp R).
- Let rsub := (@SRsub R radd).
-  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
-  Notation "x == y" := (req x y).
-   Add Morphism radd with signature (req ==> req ==> req) as radd_ext4.
-   Proof. exact (Radd_ext Reqe). Qed.
-   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext4.
-   Proof. exact (Rmul_ext Reqe). Qed.
-   Ltac norm := gen_srewrite_sr Rsth Reqe ARth.
-
- Definition gen_phiN1 x :=
-  match x with
-  | N0 => 0
-  | Npos x => gen_phiPOS1 1 radd rmul x
-  end.
-
- Definition gen_phiN x :=
-  match x with
-  | N0 => 0
-  | Npos x => gen_phiPOS 1 radd rmul x
-  end.
- Notation "[ x ]" := (gen_phiN x).
-
- Lemma same_genN : forall x, [x] == gen_phiN1 x.
- Proof.
-  destruct x;simpl. reflexivity.
-  now rewrite (same_gen Rsth Reqe ARth).
- Qed.
-
- Lemma gen_phiN_add : forall x y, [x + y] == [x] + [y].
- Proof.
-  intros x y;repeat rewrite same_genN.
-  destruct x;destruct y;simpl;norm.
-  apply (ARgen_phiPOS_add Rsth Reqe ARth).
- Qed.
-
- Lemma gen_phiN_mult : forall x y, [x * y] == [x] * [y].
- Proof.
-  intros x y;repeat rewrite same_genN.
-  destruct x;destruct y;simpl;norm.
-  apply (ARgen_phiPOS_mult Rsth Reqe ARth).
- Qed.
-
- Lemma gen_phiN_sub : forall x y, [Nsub x y] == [x] - [y].
- Proof. exact gen_phiN_add. Qed.
-
-(*gen_phiN satisfies morphism specifications*)
- Lemma gen_phiN_morph : ring_morph 0 1 radd rmul rsub ropp req
-                           0%N 1%N N.add N.mul Nsub Nopp N.eqb gen_phiN.
- Proof.
-  constructor; simpl; try reflexivity.
-  apply gen_phiN_add. apply gen_phiN_sub. apply gen_phiN_mult.
-  intros x y EQ. apply N.eqb_eq in EQ. now subst.
- Qed.
-
-End NMORPHISM.
-
-(* Words on N : initial structure for almost-rings. *)
-Definition Nword := list N.
-Definition NwO : Nword := nil.
-Definition NwI : Nword := 1%N :: nil.
-
-Definition Nwcons n (w : Nword) : Nword :=
-  match w, n with
-  | nil, 0%N => nil
-  | _, _ => n :: w
-  end.
-
-Fixpoint Nwadd (w1 w2 : Nword) {struct w1} : Nword :=
-  match w1, w2 with
-  | n1::w1', n2:: w2' => (n1+n2)%N :: Nwadd w1' w2'
-  | nil, _ => w2
-  | _, nil => w1
-  end.
-
-Definition Nwopp (w:Nword) : Nword := Nwcons 0%N w.
-
-Definition Nwsub w1 w2 := Nwadd w1 (Nwopp w2).
-
-Fixpoint Nwscal (n : N) (w : Nword) {struct w} : Nword :=
-  match w with
-  | m :: w' => (n*m)%N :: Nwscal n w'
-  | nil => nil
-  end.
-
-Fixpoint Nwmul (w1 w2 : Nword) {struct w1} : Nword :=
-  match w1 with
-  | 0%N::w1' => Nwopp (Nwmul w1' w2)
-  | n1::w1' => Nwsub (Nwscal n1 w2) (Nwmul w1' w2)
-  | nil => nil
-  end.
-Fixpoint Nw_is0 (w : Nword) : bool :=
-  match w with
-  | nil => true
-  | 0%N :: w' => Nw_is0 w'
-  | _ => false
-  end.
-
-Fixpoint Nweq_bool (w1 w2 : Nword) {struct w1} : bool :=
-  match w1, w2 with
-  | n1::w1', n2::w2' =>
-     if N.eqb n1 n2 then Nweq_bool w1' w2' else false
-  | nil, _ => Nw_is0 w2
-  | _, nil => Nw_is0 w1
-  end.
-
-Section NWORDMORPHISM.
- Variable R : Type.
- Variable (rO rI : R) (radd rmul rsub: R->R->R) (ropp : R -> R).
- Variable req : R -> R -> Prop.
-  Notation "0" := rO.  Notation "1" := rI.
-  Notation "x + y" := (radd x y).  Notation "x * y " := (rmul x y).
-  Notation "x - y " := (rsub x y).  Notation "- x" := (ropp x).
-  Notation "x == y" := (req x y).
-  Variable Rsth : Setoid_Theory R req.
-     Add Parametric Relation : R req
-       reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
-       symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
-       transitivity proved by (@Equivalence_Transitive _ _ Rsth)
-      as R_setoid5.
-     Ltac rrefl := gen_reflexivity Rsth.
- Variable Reqe : ring_eq_ext radd rmul ropp req.
-   Add Morphism radd with signature (req ==> req ==> req) as radd_ext5.
-   Proof. exact (Radd_ext Reqe). Qed.
-   Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext5.
-   Proof. exact (Rmul_ext Reqe). Qed.
-   Add Morphism ropp with signature (req ==> req) as ropp_ext5.
-   Proof. exact (Ropp_ext Reqe). Qed.
-
- Variable ARth : almost_ring_theory 0 1 radd rmul rsub ropp req.
-   Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext7.
-   Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
-   Ltac norm := gen_srewrite Rsth Reqe ARth.
-   Ltac add_push := gen_add_push radd Rsth Reqe ARth.
-
- Fixpoint gen_phiNword (w : Nword) : R :=
-  match w with
-  | nil => 0
-  | n :: nil => gen_phiN rO rI radd rmul n
-  | N0 :: w' => - gen_phiNword w'
-  | n::w' => gen_phiN rO rI radd rmul n - gen_phiNword w'
-  end.
-
- Lemma gen_phiNword0_ok : forall w, Nw_is0 w = true -> gen_phiNword w == 0.
-Proof.
-induction w; simpl; intros; auto.
- reflexivity.
-
- destruct a.
-  destruct w.
-   reflexivity.
-
-   rewrite IHw; trivial.
-   apply (ARopp_zero Rsth Reqe ARth).
-
-   discriminate.
-Qed.
-
-  Lemma gen_phiNword_cons : forall w n,
-    gen_phiNword (n::w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
-induction w.
- destruct n; simpl; norm.
-
- intros.
- destruct n; norm.
-Qed.
-
-  Lemma gen_phiNword_Nwcons : forall w n,
-    gen_phiNword (Nwcons n w) == gen_phiN rO rI radd rmul n - gen_phiNword w.
-destruct w; intros.
- destruct n; norm.
-
- unfold Nwcons.
- rewrite gen_phiNword_cons.
- reflexivity.
-Qed.
-
- Lemma gen_phiNword_ok : forall w1 w2,
-   Nweq_bool w1 w2 = true -> gen_phiNword w1 == gen_phiNword w2.
-induction w1; intros.
- simpl.
- rewrite (gen_phiNword0_ok _ H).
- reflexivity.
-
- rewrite gen_phiNword_cons.
- destruct w2.
-  simpl in H.
-  destruct a; try  discriminate.
-  rewrite (gen_phiNword0_ok _ H).
-  norm.
-
-  simpl in H.
-  rewrite gen_phiNword_cons.
-  case_eq (N.eqb a n); intros H0.
-   rewrite H0 in H.
-   apply N.eqb_eq in H0. rewrite <- H0.
-   rewrite (IHw1 _ H).
-   reflexivity.
-
-   rewrite H0 in H;  discriminate H.
-Qed.
-
-
-Lemma Nwadd_ok : forall x y,
-   gen_phiNword (Nwadd x y) == gen_phiNword x + gen_phiNword y.
-induction x; intros.
- simpl.
- norm.
-
- destruct y.
-  simpl Nwadd; norm.
-
-  simpl Nwadd.
-  repeat rewrite gen_phiNword_cons.
-  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) by
-    (destruct Reqe; constructor; trivial).
-
-  rewrite IHx.
-  norm.
-  add_push (- gen_phiNword x); reflexivity.
-Qed.
-
-Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
-simpl.
-unfold Nwopp; simpl.
-intros.
-rewrite gen_phiNword_Nwcons; norm.
-Qed.
-
-Lemma Nwscal_ok : forall n x,
-  gen_phiNword (Nwscal n x) == gen_phiN rO rI radd rmul n * gen_phiNword x.
-induction x; intros.
- norm.
-
- simpl Nwscal.
- repeat rewrite gen_phiNword_cons.
- rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth))
-   by (destruct Reqe; constructor; trivial).
-
-  rewrite IHx.
-  norm.
-Qed.
-
-Lemma Nwmul_ok : forall x y,
-   gen_phiNword (Nwmul x y) == gen_phiNword x * gen_phiNword y.
-induction x; intros.
- norm.
-
- destruct a.
-  simpl Nwmul.
-  rewrite Nwopp_ok.
-  rewrite IHx.
-  rewrite gen_phiNword_cons.
-  norm.
-
-  simpl Nwmul.
-  unfold Nwsub.
-  rewrite Nwadd_ok.
-  rewrite Nwscal_ok.
-  rewrite Nwopp_ok.
-  rewrite IHx.
-  rewrite gen_phiNword_cons.
-  norm.
-Qed.
-
-(* Proof that [.] satisfies morphism specifications *)
- Lemma gen_phiNword_morph :
-  ring_morph 0 1 radd rmul rsub ropp req
-   NwO NwI Nwadd Nwmul Nwsub Nwopp Nweq_bool gen_phiNword.
-constructor.
- reflexivity.
-
- reflexivity.
-
- exact Nwadd_ok.
-
- intros.
- unfold Nwsub.
- rewrite Nwadd_ok.
- rewrite Nwopp_ok.
- norm.
-
- exact Nwmul_ok.
-
- exact Nwopp_ok.
-
- exact gen_phiNword_ok.
-Qed.
-
-End NWORDMORPHISM.
-
-Section GEN_DIV.
-
-  Variables  (R : Type) (rO : R) (rI : R) (radd : R -> R -> R)
-              (rmul : R -> R -> R) (rsub : R -> R -> R) (ropp : R -> R)
-              (req : R -> R -> Prop) (C : Type) (cO : C) (cI : C)
-              (cadd : C -> C -> C) (cmul : C -> C -> C) (csub : C -> C -> C)
-              (copp : C -> C) (ceqb : C -> C -> bool) (phi : C -> R).
- Variable Rsth : Setoid_Theory R req.
- Variable Reqe : ring_eq_ext radd rmul ropp req.
- Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
- Variable morph : ring_morph rO rI radd rmul rsub ropp req cO cI cadd cmul csub copp ceqb phi.
-
-  (* Useful tactics *)
-  Add Parametric Relation : R req
-    reflexivity  proved by (@Equivalence_Reflexive _ _ Rsth)
-    symmetry     proved by (@Equivalence_Symmetric _ _ Rsth)
-    transitivity proved by (@Equivalence_Transitive _ _ Rsth)
-   as R_set1.
- Ltac rrefl := gen_reflexivity Rsth.
-  Add Morphism radd with signature (req ==> req ==> req) as radd_ext.
-  Proof. exact (Radd_ext Reqe). Qed.
-  Add Morphism rmul with signature (req ==> req ==> req) as rmul_ext.
-  Proof. exact (Rmul_ext Reqe). Qed.
-  Add Morphism ropp with signature (req ==> req) as ropp_ext.
-  Proof. exact (Ropp_ext Reqe). Qed.
-  Add Morphism rsub with signature (req ==> req ==> req) as rsub_ext.
-  Proof. exact (ARsub_ext Rsth Reqe ARth). Qed.
- Ltac rsimpl := gen_srewrite Rsth Reqe ARth.
-
- Definition triv_div x y :=
-   if ceqb x y then (cI, cO)
-   else (cO, x).
-
- Ltac Esimpl :=repeat (progress (
-   match goal with
-   | |- context [phi cO] => rewrite (morph0 morph)
-   | |- context [phi cI] => rewrite (morph1 morph)
-   | |- context [phi (cadd ?x  ?y)] => rewrite ((morph_add morph) x y)
-   | |- context [phi (cmul ?x  ?y)] => rewrite ((morph_mul morph) x y)
-   | |- context [phi (csub ?x  ?y)] => rewrite ((morph_sub morph) x y)
-   | |- context [phi (copp ?x)] => rewrite ((morph_opp morph) x)
-   end)).
-
- Lemma triv_div_th : Ring_theory.div_theory  req cadd cmul phi triv_div.
- Proof.
-  constructor.
-  intros a b;unfold triv_div.
-  assert (X:= morph_eq morph a b);destruct (ceqb a b).
-  Esimpl.
-  rewrite X; trivial.
-  rsimpl.
-  Esimpl;  rsimpl.
-Qed.
-
- Variable zphi : Z -> R.
-
- Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem.
- Proof.
-  constructor.
-  intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst.
-  rewrite Z.mul_comm; rsimpl.
- Qed.
-
- Variable nphi : N -> R.
-
- Lemma Ntriv_div_th : div_theory req N.add N.mul nphi N.div_eucl.
-  constructor.
-  intros; generalize (N.div_eucl_spec a b); case N.div_eucl; intros; subst.
-  rewrite N.mul_comm; rsimpl.
- Qed.
-
-End GEN_DIV.
-
- (* syntaxification of constants in an abstract ring:
-    the inverse of gen_phiPOS *)
- Ltac inv_gen_phi_pos rI add mul t :=
-   let rec inv_cst t :=
-   match t with
-     rI => constr:(1%positive)
-   | (add rI rI) => constr:(2%positive)
-   | (add rI (add rI rI)) => constr:(3%positive)
-   | (mul (add rI rI) ?p) => (* 2p *)
-       match inv_cst p with
-         NotConstant => constr:(NotConstant)
-       | 1%positive => constr:(NotConstant) (* 2*1 is not convertible to 2 *)
-       | ?p => constr:(xO p)
-       end
-   | (add rI (mul (add rI rI) ?p)) => (* 1+2p *)
-       match inv_cst p with
-         NotConstant => constr:(NotConstant)
-       | 1%positive => constr:(NotConstant)
-       | ?p => constr:(xI p)
-       end
-   | _ => constr:(NotConstant)
-   end in
-   inv_cst t.
-
-(* The (partial) inverse of gen_phiNword *)
- Ltac inv_gen_phiNword rO rI add mul opp t :=
-   match t with
-     rO => constr:(NwO)
-   | _ =>
-     match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:(NotConstant)
-     | ?p => constr:(Npos p::nil)
-     end
-   end.
-
-
-(* The inverse of gen_phiN *)
- Ltac inv_gen_phiN rO rI add mul t :=
-   match t with
-     rO => constr:(0%N)
-   | _ =>
-     match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:(NotConstant)
-     | ?p => constr:(Npos p)
-     end
-   end.
-
-(* The inverse of gen_phiZ *)
- Ltac inv_gen_phiZ rO rI add mul opp t :=
-   match t with
-     rO => constr:(0%Z)
-   | (opp ?p) =>
-     match inv_gen_phi_pos rI add mul p with
-       NotConstant => constr:(NotConstant)
-     | ?p => constr:(Zneg p)
-     end
-   | _ =>
-     match inv_gen_phi_pos rI add mul t with
-       NotConstant => constr:(NotConstant)
-     | ?p => constr:(Zpos p)
-     end
-   end.
-
-(* A simple tactic recognizing only 0 and 1. The inv_gen_phiX above
-   are only optimisations that directly returns the reified constant
-   instead of resorting to the constant propagation of the simplification
-   algorithm. *)
-Ltac inv_gen_phi rO rI cO cI t :=
-  match t with
-  | rO => cO
-  | rI => cI
-  end.
-
-(* A simple tactic recognizing no constant *)
- Ltac inv_morph_nothing t := constr:(NotConstant).
-
-Ltac coerce_to_almost_ring set ext rspec :=
-  match type of rspec with
-  | ring_theory _ _ _ _ _ _ _ => constr:(Rth_ARth set ext rspec)
-  | semi_ring_theory _ _ _ _ _ => constr:(SRth_ARth set rspec)
-  | almost_ring_theory _ _ _ _ _ _ _ => rspec
-  | _ => fail 1 "not a valid ring theory"
-  end.
-
-Ltac coerce_to_ring_ext ext :=
-  match type of ext with
-  | ring_eq_ext _ _ _ _ => ext
-  | sring_eq_ext _ _ _ => constr:(SReqe_Reqe ext)
-  | _ => fail 1 "not a valid ring_eq_ext theory"
-  end.
-
-Ltac abstract_ring_morphism set ext rspec :=
-  match type of rspec with
-  | ring_theory _ _ _ _ _ _ _ => constr:(gen_phiZ_morph set ext rspec)
-  | semi_ring_theory _ _ _ _ _ => constr:(gen_phiN_morph set ext rspec)
-  | almost_ring_theory _ _ _ _ _ _ _ =>
-      constr:(gen_phiNword_morph set ext rspec)
-  | _ => fail 1 "bad ring structure"
-  end.
-
-Record hypo : Type := mkhypo {
-   hypo_type : Type;
-   hypo_proof : hypo_type
- }.
-
-Ltac gen_ring_pow set arth pspec :=
- match pspec with
- | None =>
-   match type of arth with
-   | @almost_ring_theory ?R ?rO ?rI ?radd ?rmul ?rsub ?ropp ?req =>
-     constr:(mkhypo (@pow_N_th R rI rmul req set))
-   | _ => fail 1 "gen_ring_pow"
-   end
- | Some ?t => constr:(t)
- end.
-
-Ltac gen_ring_sign morph sspec :=
-  match sspec with
-  | None =>
-    match type of morph with
-    | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
-               Z ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
-       constr:(@mkhypo (sign_theory copp ceqb get_signZ) get_signZ_th)
-    | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
-               ?C  ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceqb ?phi =>
-        constr:(mkhypo (@get_sign_None_th C copp ceqb))
-    | _ => fail 2 "ring anomaly : default_sign_spec"
-    end
- | Some ?t => constr:(t)
- end.
-
-Ltac default_div_spec set reqe arth morph :=
- match type of morph with
- | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
-               Z ?c0 ?c1 Z.add Z.mul ?csub ?copp ?ceq_b ?phi =>
-      constr:(mkhypo (Ztriv_div_th set phi))
- | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
-               N ?c0 ?c1 N.add N.mul ?csub ?copp ?ceq_b ?phi =>
-      constr:(mkhypo (Ntriv_div_th set phi))
- | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
-               ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
-      constr:(mkhypo (triv_div_th set reqe arth morph))
- | _ => fail 1 "ring anomaly : default_sign_spec"
- end.
-
-Ltac gen_ring_div set reqe arth morph dspec  :=
- match dspec with
- | None => default_div_spec set reqe arth morph
- | Some ?t => constr:(t)
- end.
-
-Ltac ring_elements set ext rspec pspec sspec dspec rk :=
-  let arth := coerce_to_almost_ring set ext rspec in
-  let ext_r := coerce_to_ring_ext ext in
-  let morph :=
-    match rk with
-    | Abstract => abstract_ring_morphism set ext rspec
-    | @Computational ?reqb_ok =>
-        match type of arth with
-        | almost_ring_theory ?rO ?rI ?add ?mul ?sub ?opp _ =>
-            constr:(IDmorph rO rI add mul sub opp set _ reqb_ok)
-        | _ => fail 2 "ring anomaly"
-        end
-    | @Morphism ?m =>
-       match type of m with
-       | ring_morph _ _ _ _ _ _ _  _ _ _ _ _ _  _ _ => m
-       | @semi_morph _ _ _ _ _ _  _ _ _ _ _  _ _   =>
-           constr:(SRmorph_Rmorph set m)
-       | _ => fail 2 "ring anomaly"
-       end
-    | _ => fail 1 "ill-formed ring kind"
-    end in
-  let p_spec := gen_ring_pow set arth pspec in
-  let s_spec := gen_ring_sign morph sspec in
-  let d_spec := gen_ring_div set ext_r arth morph dspec in
-  fun f => f arth ext_r morph p_spec s_spec d_spec.
-
-(* Given a ring structure and the kind of morphism,
-   returns 2 lemmas (one for ring, and one for ring_simplify). *)
-
- Ltac ring_lemmas set ext rspec pspec sspec dspec rk :=
-  let gen_lemma2 :=
-    match pspec with
-    | None => constr:(ring_rw_correct)
-    | Some _ => constr:(ring_rw_pow_correct)
-    end in
-  ring_elements set ext rspec pspec sspec dspec rk
-    ltac:(fun arth ext_r morph p_spec s_spec d_spec =>
-       lazymatch type of morph with
-       | @ring_morph ?R ?r0 ?rI ?radd ?rmul ?rsub ?ropp ?req
-               ?C ?c0 ?c1 ?cadd ?cmul ?csub ?copp ?ceq_b ?phi =>
-          let gen_lemma2_0 :=
-              constr:(gen_lemma2 R  r0 rI  radd rmul rsub ropp req set ext_r arth
-                                C  c0 c1 cadd cmul csub copp ceq_b phi morph) in
-          lazymatch p_spec with
-          | @mkhypo (power_theory _ _ _ ?Cp_phi ?rpow) ?pp_spec =>
-             let gen_lemma2_1 := constr:(gen_lemma2_0 _ Cp_phi rpow pp_spec) in
-             lazymatch d_spec with
-             | @mkhypo (div_theory _ _ _ _  ?cdiv) ?dd_spec =>
-                let gen_lemma2_2 := constr:(gen_lemma2_1 cdiv dd_spec) in
-                lazymatch s_spec with
-                | @mkhypo (sign_theory _ _ ?get_sign) ?ss_spec =>
-                  let lemma2 := constr:(gen_lemma2_2 get_sign ss_spec) in
-                  let lemma1 :=
-                    constr:(ring_correct set ext_r arth morph pp_spec dd_spec) in
-                  fun f => f arth ext_r morph lemma1 lemma2
-                | _ => fail "ring: bad sign specification"
-                end
-             | _ => fail "ring: bad coefficient division specification"
-             end
-          | _ => fail "ring: bad power specification"
-          end
-       | _ => fail "ring internal error: ring_lemmas, please report"
-       end).
-
-(* Tactic for constant *)
-Ltac isnatcst t :=
-  match t with
-    O => constr:(true)
-  | S ?p => isnatcst p
-  | _ => constr:(false)
-  end.
-
-Ltac isPcst t :=
-  match t with
-  | xI ?p => isPcst p
-  | xO ?p => isPcst p
-  | xH => constr:(true)
-  (* nat -> positive *)
-  | Pos.of_succ_nat ?n => isnatcst n
-  | _ => constr:(false)
-  end.
-
-Ltac isNcst t :=
-  match t with
-    N0 => constr:(true)
-  | Npos ?p => isPcst p
-  | _ => constr:(false)
-  end.
-
-Ltac isZcst t :=
-  match t with
-    Z0 => constr:(true)
-  | Zpos ?p => isPcst p
-  | Zneg ?p => isPcst p
-  (* injection nat -> Z *)
-  | Z.of_nat ?n => isnatcst n
-  (* injection N -> Z *)
-  | Z.of_N ?n => isNcst n
-  (* *)
-  | _ => constr:(false)
-  end.