[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, 525 deletions

diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
deleted file mode 100644
index 896ee303cc..0000000000
--- a/plugins/nsatz/Nsatz.v
+++ /dev/null
@@ -1,525 +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)         *)
-(************************************************************************)
-
-(*
- Tactic nsatz: proofs of polynomials equalities in an integral domain 
-(commutative ring without zero divisor).
- 
-Examples: see test-suite/success/Nsatz.v
-
-Reification is done using type classes, defined in Ncring_tac.v
-
-*)
-
-Require Import List.
-Require Import Setoid.
-Require Import BinPos.
-Require Import BinList.
-Require Import Znumtheory.
-Require Export Morphisms Setoid Bool.
-Require Export Algebra_syntax.
-Require Export Ncring.
-Require Export Ncring_initial.
-Require Export Ncring_tac.
-Require Export Integral_domain.
-Require Import DiscrR.
-Require Import ZArith.
-Require Import Lia.
-
-Declare ML Module "nsatz_plugin".
-
-Section nsatz1.
-
-Context {R:Type}`{Rid:Integral_domain R}.
-
-Lemma psos_r1b: forall x y:R, x - y == 0 -> x == y.
-intros x y H; setoid_replace x with ((x - y) + y); simpl;
- [setoid_rewrite H | idtac]; simpl. cring. cring.
-Qed.
-
-Lemma psos_r1: forall x y, x == y -> x - y == 0.
-intros x y H; simpl; setoid_rewrite H; simpl; cring.
-Qed.
-
-Lemma nsatzR_diff: forall x y:R, not (x == y) -> not (x - y == 0).
-intros.
-intro; apply H.
-simpl; setoid_replace x with ((x - y) + y). simpl.
-setoid_rewrite H0.
-simpl; cring.
-simpl. simpl; cring.
-Qed.
-
-(* adpatation du code de Benjamin aux setoides *)
-Export Ring_polynom.
-Export InitialRing.
-
-Definition PolZ := Pol Z.
-Definition PEZ := PExpr Z.
-
-Definition P0Z : PolZ := P0 (C:=Z) 0%Z.
-
-Definition PolZadd : PolZ -> PolZ -> PolZ :=
-  @Padd  Z 0%Z Z.add Zeq_bool.
-
-Definition PolZmul : PolZ -> PolZ -> PolZ :=
-  @Pmul  Z 0%Z 1%Z Z.add Z.mul Zeq_bool.
-
-Definition PolZeq := @Peq Z Zeq_bool.
-
-Definition norm :=
-  @norm_aux Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp Zeq_bool.
-
-Fixpoint mult_l (la : list PEZ) (lp: list PolZ) : PolZ :=
- match la, lp with
- | a::la, p::lp => PolZadd (PolZmul (norm a) p) (mult_l la lp)
- | _, _ => P0Z
- end.
-
-Fixpoint compute_list (lla: list (list PEZ)) (lp:list PolZ) :=
- match lla with
- | List.nil => lp
- | la::lla => compute_list lla ((mult_l la lp)::lp)
- end.
-
-Definition check (lpe:list PEZ) (qe:PEZ) (certif: list (list PEZ) * list PEZ) :=
- let (lla, lq) := certif in
- let lp := List.map norm lpe in
- PolZeq (norm qe) (mult_l lq (compute_list lla lp)).
-
-
-(* Correction *)
-Definition PhiR : list R -> PolZ -> R :=
-  (Pphi ring0 add mul 
-    (InitialRing.gen_phiZ ring0 ring1 add mul opp)).
-
-Definition PEevalR : list R -> PEZ -> R :=
-   PEeval ring0 ring1 add mul sub opp
-    (gen_phiZ ring0 ring1 add mul opp)
-         N.to_nat pow.
-
-Lemma P0Z_correct : forall l, PhiR l P0Z = 0.
-Proof. trivial. Qed.
-
-Lemma Rext: ring_eq_ext add mul opp _==_.
-Proof.
-constructor; solve_proper.
-Qed.
-
-Lemma Rset : Setoid_Theory R _==_.
-apply ring_setoid.
-Qed.
-
-Definition Rtheory:ring_theory ring0 ring1 add mul sub opp _==_.
-apply mk_rt.
-apply ring_add_0_l.
-apply ring_add_comm.   
-apply ring_add_assoc.  
-apply ring_mul_1_l.    
-apply cring_mul_comm.
-apply ring_mul_assoc.
-apply ring_distr_l.    
-apply ring_sub_def.  
-apply ring_opp_def.
-Defined.
-
-Lemma PolZadd_correct : forall P' P l,
-  PhiR l (PolZadd P P') == ((PhiR l P) + (PhiR l P')).
-Proof.
-unfold PolZadd, PhiR. intros. simpl.
- refine (Padd_ok Rset Rext (Rth_ARth Rset Rext Rtheory)
-           (gen_phiZ_morph Rset Rext Rtheory) _ _ _).
-Qed.
-
-Lemma PolZmul_correct : forall P P' l,
-  PhiR l (PolZmul P P') == ((PhiR l P) * (PhiR l P')).
-Proof.
-unfold PolZmul, PhiR. intros. 
- refine (Pmul_ok Rset Rext (Rth_ARth Rset Rext Rtheory)
-           (gen_phiZ_morph Rset Rext Rtheory) _ _ _).
-Qed.
-
-Lemma R_power_theory
-     : Ring_theory.power_theory ring1 mul _==_ N.to_nat pow.
-apply Ring_theory.mkpow_th. unfold pow. intros. rewrite Nnat.N2Nat.id.
-reflexivity. Qed.
-
-Lemma norm_correct :
-  forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe).
-Proof.
- intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext Rtheory)
-           (gen_phiZ_morph Rset Rext Rtheory) R_power_theory).
-Qed.
-
-Lemma PolZeq_correct : forall P P' l,
-  PolZeq P P' = true ->
-  PhiR l P == PhiR l P'.
-Proof.
- intros;apply
-   (Peq_ok Rset Rext (gen_phiZ_morph Rset Rext Rtheory));trivial.
-Qed.
-
-Fixpoint Cond0 (A:Type) (Interp:A->R) (l:list A) : Prop :=
-  match l with
-  | List.nil => True
-  | a::l => Interp a == 0 /\ Cond0 A Interp l
-  end.
-
-Lemma mult_l_correct : forall l la lp,
-  Cond0 PolZ (PhiR l) lp ->
-  PhiR l (mult_l la lp) == 0.
-Proof.
- induction la;simpl;intros. cring.
- destruct lp;trivial. simpl. cring.
- simpl in H;destruct H.
- rewrite  PolZadd_correct.
- simpl. rewrite PolZmul_correct. simpl. rewrite  H.
- rewrite IHla. cring. trivial.
-Qed.
-
-Lemma compute_list_correct : forall l lla lp,
-  Cond0 PolZ (PhiR l) lp ->
-  Cond0 PolZ (PhiR l) (compute_list lla lp).
-Proof.
- induction lla;simpl;intros;trivial.
- apply IHlla;simpl;split;trivial.
- apply mult_l_correct;trivial.
-Qed.
-
-Lemma check_correct :
-  forall l lpe qe certif,
-    check lpe qe certif = true ->
-    Cond0 PEZ (PEevalR l) lpe ->
-    PEevalR l qe == 0.
-Proof.
- unfold check;intros l lpe qe (lla, lq) H2 H1.
- apply PolZeq_correct with (l:=l) in H2.
- rewrite norm_correct, H2.
- apply mult_l_correct.
- apply compute_list_correct.
- clear H2 lq lla qe;induction lpe;simpl;trivial.
- simpl in H1;destruct H1.
- rewrite <- norm_correct;auto.
-Qed.
-
-(* fin *)
-
-Definition R2:= 1 + 1.
-
-Fixpoint IPR p {struct p}: R :=
-  match p with
-    xH => ring1
-  | xO xH => 1+1
-  | xO p1 => R2*(IPR p1)
-  | xI xH => 1+(1+1)
-  | xI p1 => 1+(R2*(IPR p1))
-  end.
-
-Definition IZR1 z :=
-  match z with Z0 => 0
-             | Zpos p => IPR p
-             | Zneg p => -(IPR p)
-  end.
-
-Fixpoint interpret3 t fv {struct t}: R :=
-  match t with
-  | (PEadd t1 t2) =>
-       let v1  := interpret3 t1 fv in
-       let v2  := interpret3 t2 fv in (v1 + v2)
-  | (PEmul t1 t2) =>
-       let v1  := interpret3 t1 fv in
-       let v2  := interpret3 t2 fv in (v1 * v2)
-  | (PEsub t1 t2) =>
-       let v1  := interpret3 t1 fv in
-       let v2  := interpret3 t2 fv in (v1 - v2)
-  | (PEopp t1) =>
-       let v1  := interpret3 t1 fv in (-v1)
-  | (PEpow t1 t2) =>
-       let v1  := interpret3 t1 fv in pow v1 (N.to_nat t2)
-  | (PEc t1) => (IZR1 t1)
-  | PEO => 0
-  | PEI => 1
-  | (PEX _ n) => List.nth (pred (Pos.to_nat n)) fv 0
-  end.
-
-
-End nsatz1.
-
-Ltac equality_to_goal H x y:=
-  (* eliminate trivial  hypotheses, but it takes time!:
-  let h := fresh "nH" in
-    (assert (h:equality x y);
-    [solve [cring] | clear H; clear h])
-  || *) try (generalize (@psos_r1 _ _ _ _ _ _ _ _ _ _ _ x y H); clear H)
-.
-
-Ltac equalities_to_goal :=
-  lazymatch goal with
-  |  H: (_ ?x ?y) |- _ => equality_to_goal H x y
-  |  H: (_ _ ?x ?y) |- _ => equality_to_goal H x y
-  |  H: (_ _ _ ?x ?y) |- _ => equality_to_goal H x y
-  |  H: (_ _ _ _ ?x ?y) |- _ => equality_to_goal H x y
-(* extension possible :-) *)
-  |  H: (?x == ?y) |- _ => equality_to_goal H x y
-   end.
-
-(* lp est incluse dans fv. La met en tete. *)
-
-Ltac parametres_en_tete fv lp :=
-    match fv with
-     | (@nil _)          => lp
-     | (@cons _ ?x ?fv1) =>
-       let res := AddFvTail x lp in
-         parametres_en_tete fv1 res
-    end.
-
-Ltac append1 a l :=
- match l with
- | (@nil _)     => constr:(cons a l)
- | (cons ?x ?l) => let l' := append1 a l in constr:(cons x l')
- end.
-
-Ltac rev l :=
-  match l with
-   |(@nil _)      => l
-   | (cons ?x ?l) => let l' := rev l in append1 x l'
-  end.
-
-Ltac nsatz_call_n info nparam p rr lp kont := 
-(*  idtac "Trying power: " rr;*)
-  let ll := constr:(PEc info :: PEc nparam :: PEpow p rr :: lp) in
-(*  idtac "calcul...";*)
-  nsatz_compute ll; 
-(*  idtac "done";*)
-  match goal with
-  | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ =>
-    intros _;
-    let lci := fresh "lci" in
-    set (lci:=lci0);
-    let lq := fresh "lq" in
-    set (lq:=lq0);
-    kont c rr lq lci
-  end.
-
-Ltac nsatz_call radicalmax info nparam p lp kont :=
-  let rec try_n n :=
-    lazymatch n with
-    | 0%N => fail
-    | _ =>
-        (let r := eval compute in (N.sub radicalmax (N.pred n)) in
-         nsatz_call_n info nparam p r lp kont) ||
-         let n' := eval compute in (N.pred n) in try_n n'
-    end in
-  try_n radicalmax.
-
-
-Ltac lterm_goal g :=
-  match g with
-    ?b1 == ?b2 => constr:(b1::b2::nil)
-  | ?b1 == ?b2 -> ?g => let l := lterm_goal g in constr:(b1::b2::l)     
-  end.
-
-Ltac reify_goal l le lb:=
-  match le with
-     nil => idtac
-   | ?e::?le1 => 
-        match lb with
-         ?b::?lb1 => (* idtac "b="; idtac b;*)
-           let x := fresh "B" in
-           set (x:= b) at 1;
-           change x with (interpret3 e l); 
-           clear x;
-           reify_goal l le1 lb1
-        end
-  end.
-
-Ltac get_lpol g :=
-  match g with
-  (interpret3 ?p _) == _ => constr:(p::nil)
-  | (interpret3 ?p _) == _ -> ?g =>
-       let l := get_lpol g in constr:(p::l)     
-  end.
-
-Ltac nsatz_generic radicalmax info lparam lvar :=
- let nparam := eval compute in (Z.of_nat (List.length lparam)) in
- match goal with
-  |- ?g => let lb := lterm_goal g in 
-     match (match lvar with
-              |(@nil _) =>
-                 match lparam with
-                   |(@nil _) =>
-                     let r := eval red in (list_reifyl (lterm:=lb)) in r
-                   |_ =>
-                     match eval red in (list_reifyl (lterm:=lb)) with
-                       |(?fv, ?le) =>
-                         let fv := parametres_en_tete fv lparam in
-                           (* we reify a second time, with the good order
-                              for variables *)
-                         let r := eval red in 
-                                  (list_reifyl (lterm:=lb) (lvar:=fv)) in r
-                     end
-                  end
-              |_ => 
-                let fv := parametres_en_tete lvar lparam in
-                let r := eval red in (list_reifyl (lterm:=lb) (lvar:=fv)) in r
-            end) with
-          |(?fv, ?le) => 
-            reify_goal fv le lb ;
-            match goal with 
-                   |- ?g => 
-                       let lp := get_lpol g in 
-                       let lpol := eval compute in (List.rev lp) in
-                       intros;
-
-  let SplitPolyList kont :=
-    match lpol with
-    | ?p2::?lp2 => kont p2 lp2
-    | _ => idtac "polynomial not in the ideal"
-    end in 
-
-  SplitPolyList ltac:(fun p lp =>
-    let p21 := fresh "p21" in
-    let lp21 := fresh "lp21" in
-    set (p21:=p) ;
-    set (lp21:=lp);
-(*    idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *)
-    nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => 
-      let q := fresh "q" in
-      set (q := PEmul c (PEpow p21 r)); 
-      let Hg := fresh "Hg" in 
-      assert (Hg:check lp21 q (lci,lq) = true); 
-      [ (vm_compute;reflexivity) || idtac "invalid nsatz certificate"
-      | let Hg2 := fresh "Hg" in 
-            assert (Hg2: (interpret3 q fv) == 0);
-        [ (*simpl*) idtac; 
-          generalize (@check_correct _ _ _ _ _ _ _ _ _ _ _ fv lp21 q (lci,lq) Hg);
-          let cc := fresh "H" in
-             (*simpl*) idtac; intro cc; apply cc; clear cc;
-          (*simpl*) idtac;
-          repeat (split;[assumption|idtac]); exact I
-        | (*simpl in Hg2;*) (*simpl*) idtac; 
-          apply Rintegral_domain_pow with (interpret3 c fv) (N.to_nat r);
-          (*simpl*) idtac;
-            try apply integral_domain_one_zero;
-            try apply integral_domain_minus_one_zero;
-            try trivial;
-            try exact integral_domain_one_zero;
-            try exact integral_domain_minus_one_zero
-          || (solve [simpl; unfold R2, equality, eq_notation, addition, add_notation,
-                     one, one_notation, multiplication, mul_notation, zero, zero_notation;
-                     discrR || lia ])
-          || ((*simpl*) idtac) || idtac "could not prove discrimination result"
-        ]
-      ]
-) 
-)
-end end end .
-
-Ltac nsatz_default:=
-  intros;
-  try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _);
-  match goal with |- (@equality ?r _ _ _) =>
-    repeat equalities_to_goal;
-    nsatz_generic 6%N 1%Z (@nil r) (@nil r)
-  end.
-
-Tactic Notation "nsatz" := nsatz_default.
-
-Tactic Notation "nsatz" "with"
- "radicalmax" ":=" constr(radicalmax) 
- "strategy" ":=" constr(info) 
- "parameters" ":=" constr(lparam)
- "variables" ":=" constr(lvar):=
-  intros;
-  try apply (@psos_r1b _ _ _ _ _ _ _ _ _ _ _);
-  match goal with |- (@equality ?r _ _ _) =>
-    repeat equalities_to_goal;
-    nsatz_generic radicalmax info lparam lvar
-  end.
-
-(* Real numbers *)
-Require Import Reals.
-Require Import RealField.
-
-Lemma Rsth : Setoid_Theory R (@eq R).
-constructor;red;intros;subst;trivial.
-Qed.
-
-Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
-Defined.
-
-Instance Rri : (Ring (Ro:=Rops)).
-constructor;
-try (try apply Rsth;
-   try (unfold respectful, Proper; unfold equality; unfold eq_notation in *;
-  intros; try rewrite H; try rewrite H0; reflexivity)).
- exact Rplus_0_l. exact Rplus_comm. symmetry. apply Rplus_assoc.
- exact Rmult_1_l.  exact Rmult_1_r. symmetry. apply Rmult_assoc.
- exact Rmult_plus_distr_r. intros; apply Rmult_plus_distr_l. 
-exact Rplus_opp_r.
-Defined.
-
-Class can_compute_Z (z : Z) := dummy_can_compute_Z : True.
-Hint Extern 0 (can_compute_Z ?v) =>
-  match isZcst v with true => exact I end : typeclass_instances.
-Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z).
-Defined.
-
-Lemma R_one_zero: 1%R <> 0%R.
-discrR.
-Qed.
-
-Instance Rcri: (Cring (Rr:=Rri)).
-red. exact Rmult_comm. Defined.
-
-Instance Rdi : (Integral_domain (Rcr:=Rcri)). 
-constructor. 
-exact Rmult_integral. exact R_one_zero. Defined.
-
-(* Rational numbers *)
-Require Import QArith.
-
-Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
-Defined.
-
-Instance Qri : (Ring (Ro:=Qops)).
-constructor.
-try apply Q_Setoid. 
-apply Qplus_comp. 
-apply Qmult_comp. 
-apply Qminus_comp. 
-apply Qopp_comp.
- exact Qplus_0_l. exact Qplus_comm. apply Qplus_assoc.
- exact Qmult_1_l.  exact Qmult_1_r. apply Qmult_assoc.
- apply Qmult_plus_distr_l.  intros. apply Qmult_plus_distr_r. 
-reflexivity. exact Qplus_opp_r.
-Defined.
-
-Lemma Q_one_zero: not (Qeq 1%Q 0%Q).
-Proof. unfold Qeq. simpl. lia.  Qed.
-
-Instance Qcri: (Cring (Rr:=Qri)).
-red. exact Qmult_comm. Defined.
-
-Instance Qdi : (Integral_domain (Rcr:=Qcri)). 
-constructor. 
-exact Qmult_integral. exact Q_one_zero. Defined.
-
-(* Integers *)
-Lemma Z_one_zero: 1%Z <> 0%Z.
-Proof. lia. Qed.
-
-Instance Zcri: (Cring (Rr:=Zr)).
-red. exact Z.mul_comm. Defined.
-
-Instance Zdi : (Integral_domain (Rcr:=Zcri)). 
-constructor. 
-exact Zmult_integral. exact Z_one_zero. Defined.
-