[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

3 files changed, 0 insertions, 1005 deletions

diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
deleted file mode 100644
index 4a603f2c52..0000000000
--- a/plugins/btauto/Algebra.v
+++ /dev/null
@@ -1,591 +0,0 @@
-Require Import Bool PArith DecidableClass Ring Lia.
-
-Ltac bool :=
-repeat match goal with
-| [ H : ?P && ?Q = true |- _ ] =>
-  apply andb_true_iff in H; destruct H
-| |- ?P && ?Q = true =>
-  apply <- andb_true_iff; split
-end.
-
-Arguments decide P /H.
-
-Hint Extern 5 => progress bool : core.
-
-Ltac define t x H :=
-set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x.
-
-Lemma Decidable_sound : forall P (H : Decidable P),
-                          decide P = true -> P.
-Proof.
-intros P H Hp; apply -> Decidable_spec; assumption.
-Qed.
-
-Lemma Decidable_complete : forall P (H : Decidable P),
-  P -> decide P = true.
-Proof.
-intros P H Hp; apply <- Decidable_spec; assumption.
-Qed.
-
-Lemma Decidable_sound_alt : forall P (H : Decidable P),
-   ~ P -> decide P = false.
-Proof.
-intros P [wit spec] Hd; destruct wit; simpl; tauto. 
-Qed.
-
-Lemma Decidable_complete_alt : forall P (H : Decidable P),
-  decide P = false -> ~ P.
-Proof.
-  intros P [wit spec] Hd Hc; simpl in *; intuition congruence.
-Qed.
-
-Ltac try_rewrite :=
-repeat match goal with
-| [ H : ?P |- _ ] => rewrite H
-end.
-
-(* We opacify here decide for proofs, and will make it transparent for
-   reflexive tactics later on. *)
-
-Global Opaque decide.
-
-Ltac tac_decide :=
-match goal with
-| [ H : @decide ?P ?D = true |- _ ] => apply (@Decidable_sound P D) in H
-| [ H : @decide ?P ?D = false |- _ ] => apply (@Decidable_complete_alt P D) in H
-| [ |- @decide ?P ?D = true ] => apply (@Decidable_complete P D)
-| [ |- @decide ?P ?D = false ] => apply (@Decidable_sound_alt P D)
-| [ |- negb ?b = true ] => apply negb_true_iff
-| [ |- negb ?b = false ] => apply negb_false_iff
-| [ H : negb ?b = true |- _ ] => apply negb_true_iff in H
-| [ H : negb ?b = false |- _ ] => apply negb_false_iff in H
-end.
-
-Ltac try_decide := repeat tac_decide.
-
-Ltac make_decide P := match goal with
-| [ |- context [@decide P ?D] ] =>
-  let b := fresh "b" in
-  let H := fresh "H" in
-  define (@decide P D) b H; destruct b; try_decide
-| [ X : context [@decide P ?D] |- _ ] =>
-  let b := fresh "b" in
-  let H := fresh "H" in
-  define (@decide P D) b H; destruct b; try_decide
-end.
-
-Ltac case_decide := match goal with
-| [ |- context [@decide ?P ?D] ] =>
-  let b := fresh "b" in
-  let H := fresh "H" in
-  define (@decide P D) b H; destruct b; try_decide
-| [ X : context [@decide ?P ?D] |- _ ] =>
-  let b := fresh "b" in
-  let H := fresh "H" in
-  define (@decide P D) b H; destruct b; try_decide
-| [ |- context [Pos.compare ?x ?y] ] =>
-  destruct (Pos.compare_spec x y); try lia
-| [ X : context [Pos.compare ?x ?y] |- _ ] =>
-  destruct (Pos.compare_spec x y); try lia
-end.
-
-Section Definitions.
-
-(** * Global, inductive definitions. *)
-
-(** A Horner polynomial is either a constant, or a product P × (i + Q), where i 
-  is a variable. *)
-
-Inductive poly :=
-| Cst : bool -> poly
-| Poly : poly -> positive -> poly -> poly.
-
-(* TODO: We should use [positive] instead of [nat] to encode variables, for 
- efficiency purpose. *)
-
-Inductive null : poly -> Prop :=
-| null_intro : null (Cst false).
-
-(** Polynomials satisfy a uniqueness condition whenever they are valid. A 
-  polynomial [p] satisfies [valid n p] whenever it is well-formed and each of 
-  its variable indices is < [n]. *)
-
-Inductive valid : positive -> poly -> Prop :=
-| valid_cst : forall k c, valid k (Cst c)
-| valid_poly : forall k p i q,
-  Pos.lt i k -> ~ null q -> valid i p -> valid (Pos.succ i) q -> valid k (Poly p i q).
-
-(** Linear polynomials are valid polynomials in which every variable appears at 
-  most once. *)
-
-Inductive linear : positive -> poly -> Prop :=
-| linear_cst : forall k c, linear k (Cst c)
-| linear_poly : forall k p i q, Pos.lt i k -> ~ null q ->
-  linear i p -> linear i q -> linear k (Poly p i q).
-
-End Definitions.
-
-Section Computational.
-
-Program Instance Decidable_PosEq : forall (p q : positive), Decidable (p = q) :=
-  { Decidable_witness := Pos.eqb p q }.
-Next Obligation.
-apply Pos.eqb_eq.
-Qed.
-
-Program Instance Decidable_PosLt : forall p q, Decidable (Pos.lt p q) :=
-  { Decidable_witness := Pos.ltb p q }.
-Next Obligation.
-apply Pos.ltb_lt.
-Qed.
-
-Program Instance Decidable_PosLe : forall p q, Decidable (Pos.le p q) :=
-  { Decidable_witness := Pos.leb p q }.
-Next Obligation.
-apply Pos.leb_le.
-Qed.
-
-(** * The core reflexive part. *)
-
-Hint Constructors valid : core.
-
-Fixpoint beq_poly pl pr :=
-match pl with
-| Cst cl =>
-  match pr with
-  | Cst cr => decide (cl = cr)
-  | Poly _ _ _ => false
-  end
-| Poly pl il ql =>
-  match pr with
-  | Cst _ => false
-  | Poly pr ir qr =>
-    decide (il = ir) && beq_poly pl pr && beq_poly ql qr
-  end
-end.
-
-(* We could do that with [decide equality] but dependency in proofs is heavy *)
-Program Instance Decidable_eq_poly : forall (p q : poly), Decidable (eq p q) := {
-  Decidable_witness := beq_poly p q
-}.
-
-Next Obligation.
-split.
-revert q; induction p; intros [] ?; simpl in *; bool; try_decide;
-  f_equal; first [intuition congruence|auto].
-revert q; induction p; intros [] Heq; simpl in *; bool; try_decide; intuition;
-  try injection Heq; first[congruence|intuition].
-Qed.
-
-Program Instance Decidable_null : forall p, Decidable (null p) := {
-  Decidable_witness := match p with Cst false => true | _ => false end
-}.
-Next Obligation.
-split.
-  destruct p as [[]|]; first [discriminate|constructor].
-  inversion 1; trivial.
-Qed.
-
-Definition list_nth {A} p (l : list A) def :=
-  Pos.peano_rect (fun _ => list A -> A)
-    (fun l => match l with nil => def | cons t l => t end)
-    (fun _ F l => match l with nil => def | cons t l => F l end) p l.
-
-Fixpoint eval var (p : poly) :=
-match p with
-| Cst c => c
-| Poly p i q =>
-  let vi := list_nth i var false in
-  xorb (eval var p) (andb vi (eval var q))
-end.
-
-Fixpoint valid_dec k p :=
-match p with
-| Cst c => true
-| Poly p i q =>
-  negb (decide (null q)) && decide (i < k)%positive &&
-    valid_dec i p && valid_dec (Pos.succ i) q
-end.
-
-Program Instance Decidable_valid : forall n p, Decidable (valid n p) := {
-  Decidable_witness := valid_dec n p
-}.
-Next Obligation.
-split.
-  revert n; induction p; unfold valid_dec in *; intuition; bool; try_decide; auto.
-  intros H; induction H; unfold valid_dec in *; bool; try_decide; auto.
-Qed.
-
-(** Basic algebra *)
-
-(* Addition of polynomials *)
-
-Fixpoint poly_add pl {struct pl} :=
-match pl with
-| Cst cl =>
-  fix F pr := match pr with
-  | Cst cr => Cst (xorb cl cr)
-  | Poly pr ir qr => Poly (F pr) ir qr
-  end
-| Poly pl il ql =>
-  fix F pr {struct pr} := match pr with
-  | Cst cr => Poly (poly_add pl pr) il ql
-  | Poly pr ir qr =>
-    match Pos.compare il ir with
-    | Eq =>
-      let qs := poly_add ql qr in
-      (* Ensure validity *)
-      if decide (null qs) then poly_add pl pr
-      else Poly (poly_add pl pr) il qs
-    | Gt => Poly (poly_add pl (Poly pr ir qr)) il ql
-    | Lt => Poly (F pr) ir qr
-    end
-  end
-end.
-
-(* Multiply a polynomial by a constant *)
-
-Fixpoint poly_mul_cst v p :=
-match p with
-| Cst c => Cst (andb c v)
-| Poly p i q =>
-  let r := poly_mul_cst v q in
-  (* Ensure validity *)
-  if decide (null r) then poly_mul_cst v p
-  else Poly (poly_mul_cst v p) i r
-end.
-
-(* Multiply a polynomial by a monomial *)
-
-Fixpoint poly_mul_mon k p :=
-match p with
-| Cst c =>
-  if decide (null p) then p
-  else Poly (Cst false) k p
-| Poly p i q =>
-  if decide (i <= k)%positive then Poly (Cst false) k (Poly p i q)
-  else Poly (poly_mul_mon k p) i (poly_mul_mon k q)
-end.
-
-(* Multiplication of polynomials *)
-
-Fixpoint poly_mul pl {struct pl} :=
-match pl with
-| Cst cl => poly_mul_cst cl
-| Poly pl il ql =>
-  fun pr =>
-    (* Multiply by a factor *)
-    let qs := poly_mul ql pr in
-    (* Ensure validity *)
-    if decide (null qs) then poly_mul pl pr
-    else poly_add (poly_mul pl pr) (poly_mul_mon il qs)
-end.
-
-(** Quotienting a polynomial by the relation X_i^2 ~ X_i *)
-
-(* Remove the multiple occurrences of monomials x_k *)
-
-Fixpoint reduce_aux k p :=
-match p with
-| Cst c => Cst c
-| Poly p i q =>
-  if decide (i = k) then poly_add (reduce_aux k p) (reduce_aux k q)
-  else
-    let qs := reduce_aux i q in
-    (* Ensure validity *)
-    if decide (null qs) then (reduce_aux k p)
-    else Poly (reduce_aux k p) i qs
-end.
-
-(* Rewrite any x_k ^ {n + 1} to x_k *)
-
-Fixpoint reduce p :=
-match p with
-| Cst c => Cst c
-| Poly p i q =>
-  let qs := reduce_aux i q in
-  (* Ensure validity *)
-  if decide (null qs) then reduce p
-  else Poly (reduce p) i qs
-end.
-
-End Computational.
-
-Section Validity.
-
-(* Decision procedure of validity *)
-
-Hint Constructors valid linear : core.
-
-Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p.
-Proof.
-intros k l p H Hl; induction H; constructor; eauto.
-now eapply Pos.lt_le_trans; eassumption.
-Qed.
-
-Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p.
-Proof.
-intros k l p H; revert l; induction H; constructor; eauto; lia.
-Qed.
-
-Lemma linear_valid_incl : forall k p, linear k p -> valid k p.
-Proof.
-intros k p H; induction H; constructor; auto.
-eapply valid_le_compat; eauto; lia.
-Qed.
-
-End Validity.
-
-Section Evaluation.
-
-(* Useful simple properties *)
-
-Lemma eval_null_zero : forall p var, null p -> eval var p = false.
-Proof.
-intros p var []; reflexivity.
-Qed.
-
-Lemma eval_extensional_eq_compat : forall p var1 var2,
-  (forall x, list_nth x var1 false = list_nth x var2 false) -> eval var1 p = eval var2 p.
-Proof.
-intros p var1 var2 H; induction p; simpl; try_rewrite; auto.
-Qed.
-
-Lemma eval_suffix_compat : forall k p var1 var2,
-  (forall i, (i < k)%positive -> list_nth i var1 false = list_nth i var2 false) -> valid k p ->
-  eval var1 p = eval var2 p.
-Proof.
-intros k p var1 var2 Hvar Hv; revert var1 var2 Hvar.
-induction Hv; intros var1 var2 Hvar; simpl; [now auto|].
-rewrite Hvar; [|now auto]; erewrite (IHHv1 var1 var2).
-  + erewrite (IHHv2 var1 var2); [ring|].
-    intros; apply Hvar; lia.
-  + intros; apply Hvar; lia.
-Qed.
-
-End Evaluation.
-
-Section Algebra.
-
-(* Compatibility with evaluation *)
-
-Lemma poly_add_compat : forall pl pr var, eval var (poly_add pl pr) = xorb (eval var pl) (eval var pr).
-Proof.
-intros pl; induction pl; intros pr var; simpl.
-+ induction pr; simpl; auto; solve [try_rewrite; ring].
-+ induction pr; simpl; auto; try solve [try_rewrite; simpl; ring].
-  destruct (Pos.compare_spec p p0); repeat case_decide; simpl; first [try_rewrite; ring|idtac].
-    try_rewrite; ring_simplify; repeat rewrite xorb_assoc.
-    match goal with [ |- context [xorb (andb ?b1 ?b2) (andb ?b1 ?b3)] ] =>
-      replace (xorb (andb b1 b2) (andb b1 b3)) with (andb b1 (xorb b2 b3)) by ring
-    end.
-    rewrite <- IHpl2.
-    match goal with [ H : null ?p |- _ ] => rewrite (eval_null_zero _ _ H) end; ring.
-    simpl; rewrite IHpl1; simpl; ring.
-Qed.
-
-Lemma poly_mul_cst_compat : forall v p var,
-  eval var (poly_mul_cst v p) = andb v (eval var p).
-Proof.
-intros v p; induction p; intros var; simpl; [ring|].
-case_decide; simpl; try_rewrite; [ring_simplify|ring].
-replace (v && list_nth p2 var false && eval var p3) with (list_nth p2 var false && (v && eval var p3)) by ring.
-rewrite <- IHp2; inversion H; simpl; ring.
-Qed.
-
-Lemma poly_mul_mon_compat : forall i p var,
-  eval var (poly_mul_mon i p) = (list_nth i var false && eval var p).
-Proof.
-intros i p var; induction p; simpl; case_decide; simpl; try_rewrite; try ring.
-inversion H; ring.
-match goal with [ |- ?u = ?t ] => set (x := t); destruct x; reflexivity end.
-match goal with [ |- ?u = ?t ] => set (x := t); destruct x; reflexivity end.
-Qed.
-
-Lemma poly_mul_compat : forall pl pr var, eval var (poly_mul pl pr) = andb (eval var pl) (eval var pr).
-Proof.
-intros pl; induction pl; intros pr var; simpl.
-  apply poly_mul_cst_compat.
-  case_decide; simpl.
-    rewrite IHpl1; ring_simplify.
-    replace (eval var pr && list_nth p var false && eval var pl2)
-    with (list_nth p var false && (eval var pl2 && eval var pr)) by ring.
-    now rewrite <- IHpl2; inversion H; simpl; ring.
-    rewrite poly_add_compat, poly_mul_mon_compat, IHpl1, IHpl2; ring.
-Qed.
-
-Hint Extern 5 =>
-match goal with
-| [ |- (Pos.max ?x ?y <= ?z)%positive ] =>
-  apply Pos.max_case_strong; intros; lia
-| [ |- (?z <= Pos.max ?x ?y)%positive ] =>
-  apply Pos.max_case_strong; intros; lia
-| [ |- (Pos.max ?x ?y < ?z)%positive ] =>
-  apply Pos.max_case_strong; intros; lia
-| [ |- (?z < Pos.max ?x ?y)%positive ] =>
-  apply Pos.max_case_strong; intros; lia
-| _ => lia
-end : core.
-Hint Resolve Pos.le_max_r Pos.le_max_l : core.
-
-Hint Constructors valid linear : core.
-
-(* Compatibility of validity w.r.t algebraic operations *)
-
-Lemma poly_add_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr ->
-  valid (Pos.max kl kr) (poly_add pl pr).
-Proof.
-intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl.
-{ eapply valid_le_compat; [clear k|apply Pos.le_max_r].
-  now induction Hr; auto. }
-{  assert (Hle : (Pos.max (Pos.succ i) kr <= Pos.max k kr)%positive) by auto.
-  apply (valid_le_compat (Pos.max (Pos.succ i) kr)); [|assumption].
-  clear - IHHl1 IHHl2 Hl2 Hr H0; induction Hr.
-    constructor; auto.
-      now rewrite <- (Pos.max_id i); intuition.
-    destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
-      + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto.
-      + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia.
-      + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia.
-      + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition.
-      + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition.
-}
-Qed.
-
-Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_cst v p).
-Proof.
-intros k v p H; induction H; simpl; [now auto|].
-case_decide; [|now auto].
-eapply (valid_le_compat i); [now auto|lia].
-Qed.
-
-Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p.
-Proof.
-intros i p; induction p; simpl; case_decide; simpl; inversion 1; intuition.
-Qed.
-
-Lemma poly_mul_mon_valid_compat : forall k i p,
-  valid k p -> valid (Pos.max (Pos.succ i) k) (poly_mul_mon i p).
-Proof.
-intros k i p H; induction H; simpl poly_mul_mon; case_decide; intuition.
-+ apply (valid_le_compat (Pos.succ i)); auto; constructor; intuition.
-  - match goal with [ H : null ?p |- _ ] => solve[inversion H] end.
-+ apply (valid_le_compat k); auto; constructor; intuition.
-  - assert (X := poly_mul_mon_null_compat); intuition eauto.
-  - enough (Pos.max (Pos.succ i) i0 = i0) as <-; intuition.
-  - enough (Pos.max (Pos.succ i) (Pos.succ i0) = Pos.succ i0) as <-; intuition.
-Qed.
-
-Lemma poly_mul_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr ->
-  valid (Pos.max kl kr) (poly_mul pl pr).
-Proof.
-intros kl kr pl pr Hl Hr; revert kr pr Hr.
-induction Hl; intros kr pr Hr; simpl.
-+ apply poly_mul_cst_valid_compat; auto.
-  apply (valid_le_compat kr); now auto.
-+ apply (valid_le_compat (Pos.max (Pos.max i kr) (Pos.max (Pos.succ i) (Pos.max (Pos.succ i) kr)))).
-  - case_decide.
-    { apply (valid_le_compat (Pos.max i kr)); auto. }
-    { apply poly_add_valid_compat; auto.
-      now apply poly_mul_mon_valid_compat; intuition. }
-  - repeat apply Pos.max_case_strong; lia.
-Qed.
-
-(* Compatibility of linearity wrt to linear operations *)
-
-Lemma poly_add_linear_compat : forall kl kr pl pr, linear kl pl -> linear kr pr ->
-  linear (Pos.max kl kr) (poly_add pl pr).
-Proof.
-intros kl kr pl pr Hl; revert kr pr; induction Hl; intros kr pr Hr; simpl.
-+ apply (linear_le_compat kr); [|apply Pos.max_case_strong; lia].
-  now induction Hr; constructor; auto.
-+ apply (linear_le_compat (Pos.max kr (Pos.succ i))); [|now auto].
-  induction Hr; simpl.
-  - constructor; auto.
-    replace i with (Pos.max i i) by (apply Pos.max_id); intuition.
-  - destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
-    { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. }
-    { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. }
-    { apply (linear_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. }
-    { apply (linear_le_compat (Pos.max i0 (Pos.succ i))); intuition. }
-    { apply (linear_le_compat (Pos.max i (Pos.succ i0))); intuition. }
-Qed.
-
-End Algebra.
-
-Section Reduce.
-
-(* A stronger version of the next lemma *)
-
-Lemma reduce_aux_eval_compat : forall k p var, valid (Pos.succ k) p ->
-  (list_nth k var false && eval var (reduce_aux k p) = list_nth k var false && eval var p).
-Proof.
-intros k p var; revert k; induction p; intros k Hv; simpl; auto.
-inversion Hv; case_decide; subst.
-+ rewrite poly_add_compat; ring_simplify.
-  specialize (IHp1 k); specialize (IHp2 k).
-  destruct (list_nth k var false); ring_simplify; [|now auto].
-  rewrite <- (andb_true_l (eval var p1)), <- (andb_true_l (eval var p3)).
-  rewrite <- IHp2; auto; rewrite <- IHp1; [ring|].
-  apply (valid_le_compat k); [now auto|lia].
-+ remember (list_nth k var false) as b; destruct b; ring_simplify; [|now auto].
-  case_decide; simpl.
-  - rewrite <- (IHp2 p2); [inversion H|now auto]; simpl.
-    replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring); rewrite <- (IHp1 k).
-    { rewrite <- Heqb; ring. }
-    { apply (valid_le_compat p2); [auto|lia]. }
-  - rewrite (IHp2 p2); [|now auto].
-    replace (eval var p1) with (list_nth k var false && eval var p1) by (rewrite <- Heqb; ring).
-    rewrite <- (IHp1 k); [rewrite <- Heqb; ring|].
-    apply (valid_le_compat p2); [auto|lia].
-Qed.
-
-(* Reduction preserves evaluation by boolean assignations *)
-
-Lemma reduce_eval_compat : forall k p var, valid k p ->
-  eval var (reduce p) = eval var p.
-Proof.
-intros k p var H; induction H; simpl; auto.
-case_decide; try_rewrite; simpl.
-+ rewrite <- reduce_aux_eval_compat; auto; inversion H3; simpl; ring.
-+ repeat rewrite reduce_aux_eval_compat; try_rewrite; now auto.
-Qed.
-
-Lemma reduce_aux_le_compat : forall k l p, valid k p -> (k <= l)%positive ->
-  reduce_aux l p = reduce_aux k p.
-Proof.
-intros k l p; revert k l; induction p; intros k l H Hle; simpl; auto.
-inversion H; subst; repeat case_decide; subst; try lia.
-+ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|lia].
-+ f_equal; apply IHp1; auto.
-  now eapply valid_le_compat; [eauto|lia].
-Qed.
-
-(* Reduce projects valid polynomials into linear ones *)
-
-Lemma linear_reduce_aux : forall i p, valid (Pos.succ i) p -> linear i (reduce_aux i p).
-Proof.
-intros i p; revert i; induction p; intros i Hp; simpl.
-+ constructor.
-+ inversion Hp; subst; case_decide; subst.
-  - rewrite <- (Pos.max_id i) at 1; apply poly_add_linear_compat.
-    { apply IHp1; eapply valid_le_compat; [eassumption|lia]. }
-    { intuition. }
-  - case_decide.
-  { apply IHp1; eapply valid_le_compat; [eauto|lia]. }
-  { constructor; try lia; auto.
-    erewrite (reduce_aux_le_compat p2); [|assumption|lia].
-    apply IHp1; eapply valid_le_compat; [eauto|]; lia. }
-Qed.
-
-Lemma linear_reduce : forall k p, valid k p -> linear k (reduce p).
-Proof.
-intros k p H; induction H; simpl.
-+ now constructor.
-+ case_decide.
-  - eapply linear_le_compat; [eauto|lia].
-  - constructor; auto.
-    apply linear_reduce_aux; auto.
-Qed.
-
-End Reduce.
diff --git a/plugins/btauto/Btauto.v b/plugins/btauto/Btauto.v
deleted file mode 100644
index d3331ccf89..0000000000
--- a/plugins/btauto/Btauto.v
+++ /dev/null
@@ -1,3 +0,0 @@
-Require Import Algebra Reflect.
-
-Declare ML Module "btauto_plugin".
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.