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

diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
deleted file mode 100644
index 867fe69550..0000000000
--- a/plugins/btauto/Reflect.v
+++ /dev/null
@@ -1,411 +0,0 @@
-Require Import Bool DecidableClass Algebra Ring PArith Lia.
-
-Section Bool.
-
-(* Boolean formulas and their evaluations *)
-
-Inductive formula :=
-| formula_var : positive -> formula
-| formula_btm : formula
-| formula_top : formula
-| formula_cnj : formula -> formula -> formula
-| formula_dsj : formula -> formula -> formula
-| formula_neg : formula -> formula
-| formula_xor : formula -> formula -> formula
-| formula_ifb : formula -> formula -> formula -> formula.
-
-Fixpoint formula_eval var f := match f with
-| formula_var x => list_nth x var false 
-| formula_btm => false
-| formula_top => true
-| formula_cnj fl fr => (formula_eval var fl) && (formula_eval var fr)
-| formula_dsj fl fr => (formula_eval var fl) || (formula_eval var fr)
-| formula_neg f => negb (formula_eval var f)
-| formula_xor fl fr => xorb (formula_eval var fl) (formula_eval var fr)
-| formula_ifb fc fl fr =>
-  if formula_eval var fc then formula_eval var fl else formula_eval var fr
-end.
-
-End Bool.
-
-(* Translation of formulas into polynomials *)
-
-Section Translation.
-
-(* This is straightforward. *)
-
-Fixpoint poly_of_formula f := match f with
-| formula_var x => Poly (Cst false) x (Cst true) 
-| formula_btm => Cst false
-| formula_top => Cst true
-| formula_cnj fl fr =>
-  let pl := poly_of_formula fl in
-  let pr := poly_of_formula fr in
-  poly_mul pl pr
-| formula_dsj fl fr =>
-  let pl := poly_of_formula fl in
-  let pr := poly_of_formula fr in
-  poly_add (poly_add pl pr) (poly_mul pl pr)
-| formula_neg f => poly_add (Cst true) (poly_of_formula f)
-| formula_xor fl fr => poly_add (poly_of_formula fl) (poly_of_formula fr)
-| formula_ifb fc fl fr =>
-  let pc := poly_of_formula fc in
-  let pl := poly_of_formula fl in
-  let pr := poly_of_formula fr in
-  poly_add pr (poly_add (poly_mul pc pl) (poly_mul pc pr))
-end.
-
-Opaque poly_add.
-
-(* Compatibility of translation wrt evaluation *)
-
-Lemma poly_of_formula_eval_compat : forall var f,
-  eval var (poly_of_formula f) = formula_eval var f.
-Proof.
-intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto.
-  now simpl; match goal with [ |- ?t = ?u ] => destruct u; reflexivity end.
-  rewrite poly_mul_compat, IHf1, IHf2; ring.
-  repeat rewrite poly_add_compat.
-  rewrite poly_mul_compat; try_rewrite.
-  now match goal with [ |- ?t = ?x || ?y ] => destruct x; destruct y; reflexivity end.
-  rewrite poly_add_compat; try_rewrite.
-  now match goal with [ |- ?t = negb ?x ] => destruct x; reflexivity end.
-  rewrite poly_add_compat; congruence.
-  rewrite ?poly_add_compat, ?poly_mul_compat; try_rewrite.
-  match goal with
-    [ |- ?t = if ?b1 then ?b2 else ?b3 ] => destruct b1; destruct b2; destruct b3; reflexivity
-  end.
-Qed.
-
-Hint Extern 5 => change 0 with (min 0 0) : core.
-Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core.
-Local Hint Constructors valid : core.
-Hint Extern 5 => lia : core.
-
-(* Compatibility with validity *)
-
-Lemma poly_of_formula_valid_compat : forall f, exists n, valid n (poly_of_formula f).
-Proof.
-intros f; induction f; simpl.
-+ exists (Pos.succ p); constructor; intuition; inversion H.
-+ exists 1%positive; auto.
-+ exists 1%positive; auto.
-+ destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (Pos.max n1 n2); auto.
-+ destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (Pos.max (Pos.max n1 n2) (Pos.max n1 n2)); auto.
-+ destruct IHf as [n Hn]; exists (Pos.max 1 n); auto.
-+ destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (Pos.max n1 n2); auto.
-+ destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; destruct IHf3 as [n3 Hn3]; eexists; eauto.
-Qed.
-
-(* The soundness lemma ; alas not complete! *)
-
-Lemma poly_of_formula_sound : forall fl fr var,
-  poly_of_formula fl = poly_of_formula fr -> formula_eval var fl = formula_eval var fr.
-Proof.
-intros fl fr var Heq.
-repeat rewrite <- poly_of_formula_eval_compat.
-rewrite Heq; reflexivity.
-Qed.
-
-End Translation.
-
-Section Completeness.
-
-(* Lemma reduce_poly_of_formula_simpl : forall fl fr var,
-  simpl_eval (var_of_list var) (reduce (poly_of_formula fl)) = simpl_eval (var_of_list var) (reduce (poly_of_formula fr)) ->
-  formula_eval var fl = formula_eval var fr.
-Proof.
-intros fl fr var Hrw.
-do 2 rewrite <- poly_of_formula_eval_compat.
-destruct (poly_of_formula_valid_compat fl) as [nl Hl].
-destruct (poly_of_formula_valid_compat fr) as [nr Hr].
-rewrite <- (reduce_eval_compat nl (poly_of_formula fl)); [|assumption].
-rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); [|assumption].
-do 2 rewrite <- eval_simpl_eval_compat; assumption.
-Qed. *)
-
-(* Soundness of the method ; immediate *)
-
-Lemma reduce_poly_of_formula_sound : forall fl fr var,
-  reduce (poly_of_formula fl) = reduce (poly_of_formula fr) ->
-  formula_eval var fl = formula_eval var fr.
-Proof.
-intros fl fr var Heq.
-repeat rewrite <- poly_of_formula_eval_compat.
-destruct (poly_of_formula_valid_compat fl) as [nl Hl].
-destruct (poly_of_formula_valid_compat fr) as [nr Hr].
-rewrite <- (reduce_eval_compat nl (poly_of_formula fl)); auto.
-rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); auto.
-rewrite Heq; reflexivity.
-Qed.
-
-Definition make_last {A} n (x def : A) :=
-  Pos.peano_rect (fun _ => list A)
-    (cons x nil)
-    (fun _ F => cons def F) n.
-
-(* Replace the nth element of a list *)
-
-Fixpoint list_replace l n b :=
-match l with
-| nil => make_last n b false
-| cons a l =>
-  Pos.peano_rect _
-    (cons b l) (fun n _ => cons a (list_replace l n b)) n
-end.
-
-(** Extract a non-null witness from a polynomial *)
-
-Existing Instance Decidable_null.
-
-Fixpoint boolean_witness p :=
-match p with
-| Cst c => nil
-| Poly p i q =>
-  if decide (null p) then
-    let var := boolean_witness q in
-    list_replace var i true
-  else
-    let var := boolean_witness p in
-    list_replace var i false
-end.
-
-Lemma list_nth_base : forall A (def : A) l,
-  list_nth 1 l def = match l with nil => def | cons x _ => x end.
-Proof.
-intros A def l; unfold list_nth.
-rewrite Pos.peano_rect_base; reflexivity.
-Qed.
-
-Lemma list_nth_succ : forall A n (def : A) l,
-  list_nth (Pos.succ n) l def =
-    match l with nil => def | cons _ l => list_nth n l def end.
-Proof.
-intros A def l; unfold list_nth.
-rewrite Pos.peano_rect_succ; reflexivity.
-Qed.
-
-Lemma list_nth_nil : forall A n (def : A),
-  list_nth n nil def = def.
-Proof.
-intros A n def; induction n using Pos.peano_rect.
-+ rewrite list_nth_base; reflexivity.
-+ rewrite list_nth_succ; reflexivity.
-Qed.
-
-Lemma make_last_nth_1 : forall A n i x def, i <> n ->
-  list_nth i (@make_last A n x def) def = def.
-Proof.
-intros A n; induction n using Pos.peano_rect; intros i x def Hd;
-  unfold make_last; simpl.
-+ induction i using Pos.peano_case; [elim Hd; reflexivity|].
-  rewrite list_nth_succ, list_nth_nil; reflexivity.
-+ unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def).
-  induction i using Pos.peano_case.
-  - rewrite list_nth_base; reflexivity.
-  - rewrite list_nth_succ; apply IHn; lia.
-Qed.
-
-Lemma make_last_nth_2 : forall A n x def, list_nth n (@make_last A n x def) def = x.
-Proof.
-intros A n; induction n using Pos.peano_rect; intros x def; simpl.
-+ reflexivity.
-+ unfold make_last; rewrite Pos.peano_rect_succ; fold (make_last n x def).
-  rewrite list_nth_succ; auto.
-Qed.
-
-Lemma list_replace_nth_1 : forall var i j x, i <> j ->
-  list_nth i (list_replace var j x) false = list_nth i var false.
-Proof.
-intros var; induction var; intros i j x Hd; simpl.
-+ rewrite make_last_nth_1, list_nth_nil; auto.
-+ induction j using Pos.peano_rect.
-  - rewrite Pos.peano_rect_base.
-    induction i using Pos.peano_rect; [now elim Hd; auto|].
-    rewrite 2list_nth_succ; reflexivity.
-  - rewrite Pos.peano_rect_succ.
-    induction i using Pos.peano_rect.
-    { rewrite 2list_nth_base; reflexivity. }
-    { rewrite 2list_nth_succ; apply IHvar; lia. }
-Qed.
-
-Lemma list_replace_nth_2 : forall var i x, list_nth i (list_replace var i x) false = x.
-Proof.
-intros var; induction var; intros i x; simpl.
-+ now apply make_last_nth_2.
-+ induction i using Pos.peano_rect.
-  - rewrite Pos.peano_rect_base, list_nth_base; reflexivity.
-  - rewrite Pos.peano_rect_succ, list_nth_succ; auto.
-Qed.
-
-(* The witness is correct only if the polynomial is linear *)
-
-Lemma boolean_witness_nonzero : forall k p, linear k p -> ~ null p ->
-  eval (boolean_witness p) p = true.
-Proof.
-intros k p Hl Hp; induction Hl; simpl.
-  destruct c; [reflexivity|elim Hp; now constructor].
-  case_decide.
-    rewrite eval_null_zero; [|assumption]; rewrite list_replace_nth_2; simpl.
-    match goal with [ |- (if ?b then true else false) = true ] =>
-      assert (Hrw : b = true); [|rewrite Hrw; reflexivity]
-    end.
-    erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
-    now intros j Hd; apply list_replace_nth_1; lia.
-    rewrite list_replace_nth_2, xorb_false_r.
-    erewrite eval_suffix_compat; [now eauto| |now apply linear_valid_incl; eauto].
-    now intros j Hd; apply list_replace_nth_1; lia.
-Qed.
-
-(* This should be better when using the [vm_compute] tactic instead of plain reflexivity. *)
-
-Lemma reduce_poly_of_formula_sound_alt : forall var fl fr,
-  reduce (poly_add (poly_of_formula fl) (poly_of_formula fr)) = Cst false ->
-  formula_eval var fl = formula_eval var fr.
-Proof.
-intros var fl fr Heq.
-repeat rewrite <- poly_of_formula_eval_compat.
-destruct (poly_of_formula_valid_compat fl) as [nl Hl].
-destruct (poly_of_formula_valid_compat fr) as [nr Hr].
-rewrite <- (reduce_eval_compat nl (poly_of_formula fl)); auto.
-rewrite <- (reduce_eval_compat nr (poly_of_formula fr)); auto.
-rewrite <- xorb_false_l; change false with (eval var (Cst false)).
-rewrite <- poly_add_compat, <- Heq.
-repeat rewrite poly_add_compat.
-rewrite (reduce_eval_compat nl); [|assumption].
-rewrite (reduce_eval_compat (Pos.max nl nr)); [|apply poly_add_valid_compat; assumption].
-rewrite (reduce_eval_compat nr); [|assumption].
-rewrite poly_add_compat; ring.
-Qed.
-
-(* The completeness lemma *)
-
-(* Lemma reduce_poly_of_formula_complete : forall fl fr,
-  reduce (poly_of_formula fl) <> reduce (poly_of_formula fr) ->
-  {var | formula_eval var fl <> formula_eval var fr}.
-Proof.
-intros fl fr H.
-pose (p := poly_add (reduce (poly_of_formula fl)) (poly_opp (reduce (poly_of_formula fr)))).
-pose (var := boolean_witness p).
-exists var.
-  intros Hc; apply (f_equal Z_of_bool) in Hc.
-  assert (Hfl : linear 0 (reduce (poly_of_formula fl))).
-    now destruct (poly_of_formula_valid_compat fl) as [n Hn]; apply (linear_le_compat n); [|now auto]; apply linear_reduce; auto.
-  assert (Hfr : linear 0 (reduce (poly_of_formula fr))).
-    now destruct (poly_of_formula_valid_compat fr) as [n Hn]; apply (linear_le_compat n); [|now auto]; apply linear_reduce; auto.
-  repeat rewrite <- poly_of_formula_eval_compat in Hc.
-  define (decide (null p)) b Hb; destruct b; tac_decide.
-    now elim H; apply (null_sub_implies_eq 0 0); fold p; auto;
-    apply linear_valid_incl; auto.
-  elim (boolean_witness_nonzero 0 p); auto.
-    unfold p; rewrite <- (min_id 0); apply poly_add_linear_compat; try apply poly_opp_linear_compat; now auto.
-    unfold p at 2; rewrite poly_add_compat, poly_opp_compat.
-    destruct (poly_of_formula_valid_compat fl) as [nl Hnl].
-    destruct (poly_of_formula_valid_compat fr) as [nr Hnr].
-    repeat erewrite reduce_eval_compat; eauto.
-    fold var; rewrite Hc; ring.
-Defined. *)
-
-End Completeness.
-
-(* Reification tactics *)
-
-(* For reflexivity purposes, that would better be transparent *)
-
-Global Transparent decide poly_add.
-
-(* Ltac append_var x l k :=
-match l with
-| nil => constr: (k, cons x l)
-| cons x _ => constr: (k, l)
-| cons ?y ?l =>
-  let ans := append_var x l (S k) in
-  match ans with (?k, ?l) => constr: (k, cons y l) end
-end.
-
-Ltac build_formula t l :=
-match t with
-| true => constr: (formula_top, l)
-| false => constr: (formula_btm, l)
-| ?fl && ?fr =>
-  match build_formula fl l with (?tl, ?l) =>
-    match build_formula fr l with (?tr, ?l) =>
-      constr: (formula_cnj tl tr, l)
-    end
-  end
-| ?fl || ?fr =>
-  match build_formula fl l with (?tl, ?l) =>
-    match build_formula fr l with (?tr, ?l) =>
-      constr: (formula_dsj tl tr, l)
-    end
-  end
-| negb ?f =>
-  match build_formula f l with (?t, ?l) =>
-    constr: (formula_neg t, l)
-  end
-| _ =>
-  let ans := append_var t l 0 in
-  match ans with (?k, ?l) => constr: (formula_var k, l) end
-end.
-
-(* Extract a counterexample from a polynomial and display it *)
-
-Ltac counterexample p l :=
-  let var := constr: (boolean_witness p) in
-  let var := eval vm_compute in var in
-  let rec print l vl :=
-    match l with
-    | nil => idtac
-    | cons ?x ?l =>
-      match vl with
-      | nil =>
-        idtac x ":=" "false"; print l (@nil bool)
-      | cons ?v ?vl =>
-        idtac x ":=" v; print l vl
-      end
-    end
-  in
-  idtac "Counter-example:"; print l var.
-
-Ltac btauto_reify :=
-lazymatch goal with
-| [ |- @eq bool ?t ?u ] =>
-  lazymatch build_formula t (@nil bool) with
-  | (?fl, ?l) =>
-    lazymatch build_formula u l with
-    | (?fr, ?l) =>
-      change (formula_eval l fl = formula_eval l fr)
-    end
-  end
-| _ => fail "Cannot recognize a boolean equality"
-end.
-
-(* The long-awaited tactic *)
-
-Ltac btauto :=
-lazymatch goal with
-| [ |- @eq bool ?t ?u ] =>
-  lazymatch build_formula t (@nil bool) with
-  | (?fl, ?l) =>
-    lazymatch build_formula u l with
-    | (?fr, ?l) =>
-      change (formula_eval l fl = formula_eval l fr);
-      apply reduce_poly_of_formula_sound_alt;
-      vm_compute; (reflexivity || fail "Not a tautology")
-    end
-  end
-| _ => fail "Cannot recognize a boolean equality"
-end. *)
-
-Register formula_var as plugins.btauto.f_var.
-Register formula_btm as plugins.btauto.f_btm.
-Register formula_top as plugins.btauto.f_top.
-Register formula_cnj as plugins.btauto.f_cnj.
-Register formula_dsj as plugins.btauto.f_dsj.
-Register formula_neg as plugins.btauto.f_neg.
-Register formula_xor as plugins.btauto.f_xor.
-Register formula_ifb as plugins.btauto.f_ifb.
-
-Register formula_eval as plugins.btauto.eval.
-Register boolean_witness as plugins.btauto.witness.
-Register reduce_poly_of_formula_sound_alt as plugins.btauto.soundness.