Added a Btauto plugin, that solves boolean tautologies.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14897 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 1182 insertions, 4 deletions

diff --git a/.gitignore b/.gitignore
index 32a40af67..0c8d63ae2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -137,6 +137,7 @@ plugins/xml/dumptree.ml
 plugins/xml/xmlentries.ml
 plugins/extraction/g_extraction.ml
 plugins/rtauto/g_rtauto.ml
+plugins/btauto/g_btauto.ml
 plugins/romega/g_romega.ml
 plugins/setoid_ring/newring.ml
 plugins/firstorder/g_ground.ml
diff --git a/Makefile.build b/Makefile.build
index 59ee457c9..c8b4fa5f1 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -447,7 +447,7 @@ noreal: logic arith bool zarith qarith lists sets fsets relations \
 ###########################################################################
 
 .PHONY: plugins omega micromega ring setoid_ring nsatz dp xml extraction
-.PHONY: field fourier funind cc subtac rtauto pluginsopt
+.PHONY: field fourier funind cc subtac rtauto btauto pluginsopt
 
 plugins: $(PLUGINSVO)
 omega: $(OMEGAVO) $(OMEGACMA) $(ROMEGAVO) $(ROMEGACMA)
@@ -464,6 +464,7 @@ funind: $(FUNINDCMA) $(FUNINDVO)
 cc: $(CCVO) $(CCCMA)
 subtac: $(SUBTACCMA)
 rtauto: $(RTAUTOVO) $(RTAUTOCMA)
+btauto: $(BTAUTOVO) $(BTAUTOCMA)
 
 pluginsopt: $(PLUGINSOPT)
 
diff --git a/Makefile.common b/Makefile.common
index b560bae5a..d4492736a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -82,7 +82,7 @@ SRCDIRS:=\
     omega	romega 		micromega 	quote		ring	dp \
     setoid_ring xml 		extraction 	fourier \
     cc 		funind 		firstorder 	field 		subtac \
-    rtauto 	nsatz           syntax          decl_mode)
+    rtauto 	nsatz           syntax          decl_mode	btauto)
 
 # Order is relevent here because kernel and checker contain files
 # with the same name
@@ -185,6 +185,7 @@ FUNINDCMA:=plugins/funind/recdef_plugin.cma
 FOCMA:=plugins/firstorder/ground_plugin.cma
 CCCMA:=plugins/cc/cc_plugin.cma
 SUBTACCMA:=plugins/subtac/subtac_plugin.cma
+BTAUTOCMA:=plugins/btauto/btauto_plugin.cma
 RTAUTOCMA:=plugins/rtauto/rtauto_plugin.cma
 NATSYNTAXCMA:=plugins/syntax/nat_syntax_plugin.cma
 OTHERSYNTAXCMA:=$(addprefix plugins/syntax/, \
@@ -198,7 +199,7 @@ DECLMODECMA:=plugins/decl_mode/decl_mode_plugin.cma
 PLUGINSCMA:=$(OMEGACMA) $(ROMEGACMA) $(MICROMEGACMA) $(DECLMODECMA) \
         $(QUOTECMA) $(RINGCMA) $(NEWRINGCMA) $(DPCMA) $(FIELDCMA) \
         $(FOURIERCMA) $(EXTRACTIONCMA) $(XMLCMA) \
-        $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) \
+        $(CCCMA)  $(FOCMA) $(SUBTACCMA) $(RTAUTOCMA) $(BTAUTOCMA) \
         $(FUNINDCMA) $(NSATZCMA) $(NATSYNTAXCMA) $(OTHERSYNTAXCMA)
 
 ifneq ($(HASNATDYNLINK),false)
@@ -315,6 +316,7 @@ NSATZVO:=$(call cat_vo_itarget, plugins/nsatz)
 FOURIERVO:=$(call cat_vo_itarget, plugins/fourier)
 FUNINDVO:=$(call cat_vo_itarget, plugins/funind)
 DPVO:=$(call cat_vo_itarget, plugins/dp)
+BTAUTOVO:=$(call cat_vo_itarget, plugins/btauto)
 RTAUTOVO:=$(call cat_vo_itarget, plugins/rtauto)
 EXTRACTIONVO:=$(call cat_vo_itarget, plugins/extraction)
 XMLVO:=
@@ -322,7 +324,7 @@ CCVO:=
 
 PLUGINSVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 	    $(XMLVO) $(FOURIERVO) $(CCVO) $(FUNINDVO) \
-	    $(RTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \
+	    $(RTAUTOVO) $(BTAUTOVO) $(NEWRINGVO) $(DPVO) $(QUOTEVO) \
             $(NSATZVO) $(EXTRACTIONVO)
 
 ALLVO:= $(THEORIESVO) $(PLUGINSVO)
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
new file mode 100644
index 000000000..f82db7c58
--- /dev/null
+++ b/plugins/btauto/Algebra.v
@@ -0,0 +1,534 @@
+Require Import Bool Arith DecidableClass.
+
+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.
+
+Hint Extern 5 => progress bool.
+
+Ltac define t x H :=
+set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x.
+
+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 [nat_compare ?x ?y] ] =>
+  destruct (nat_compare_spec x y); try (exfalso; omega)
+| [ X : context [nat_compare ?x ?y] |- _ ] =>
+  destruct (nat_compare_spec x y); try (exfalso; omega)
+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 -> nat -> 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 : nat -> poly -> Prop :=
+| valid_cst : forall k c, valid k (Cst c)
+| valid_poly : forall k p i q,
+  i < k -> ~ null q -> valid i p -> valid (S i) q -> valid k (Poly p i q).
+
+(** Linear polynomials are valid polynomials in which every variable appears at 
+  most once. *)
+
+Inductive linear : nat -> poly -> Prop :=
+| linear_cst : forall k c, linear k (Cst c)
+| linear_poly : forall k p i q, i < k -> ~ null q ->
+  linear i p -> linear i q -> linear k (Poly p i q).
+
+End Definitions.
+
+Section Computational.
+
+(** * The core reflexive part. *)
+
+Hint Constructors valid.
+
+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.
+
+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) &&
+    valid_dec i p && valid_dec (S 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; simpl in *; intuition; bool; try_decide; auto.
+  intros H; induction H; simpl 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 nat_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) 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 occurences 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.
+
+Lemma valid_le_compat : forall k l p, valid k p -> k <= l -> valid l p.
+Proof.
+intros k l p H Hl; induction H; constructor; eauto with arith.
+Qed.
+
+Lemma linear_le_compat : forall k l p, linear k p -> k <= l -> linear l p.
+Proof.
+intros k l p H; revert l; induction H; intuition.
+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.
+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 -> 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); [|now intuition].
+erewrite (IHHv2 var1 var2); [ring|now intuition].
+Qed.
+
+End Evaluation.
+
+Section Algebra.
+
+Require Import NPeano.
+
+(* 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 (nat_compare_spec n n0); 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 n var false && eval var p2) with (List.nth n var false && (v && eval var p2)) 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 n var false && eval var pl2)
+    with (List.nth n 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
+| [ |- max ?x ?y <= ?z ] =>
+  apply Nat.max_case_strong; intros; omega
+| [ |- ?z <= max ?x ?y ] =>
+  apply Nat.max_case_strong; intros; omega
+end.
+Hint Resolve Nat.le_max_r Nat.le_max_l.
+
+Hint Constructors valid linear.
+
+(* 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 (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 Nat.le_max_r].
+  now induction Hr; auto.
+  assert (Hle : max (S i) kr <= max k kr).
+    apply Nat.max_case_strong; intros; apply Nat.max_case_strong; intros; auto; omega.
+  apply (valid_le_compat (max (S i) kr)); [|assumption].
+  clear - IHHl1 IHHl2 Hl2 Hr H0; induction Hr.
+    constructor; auto.
+      now rewrite <- (Nat.max_id i); intuition.
+    destruct (nat_compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
+      now apply (valid_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
+      now apply (valid_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
+      now apply (valid_le_compat (max (S i0) (S i0))); [now auto|]; rewrite Nat.max_id; auto.
+      now apply (valid_le_compat (max (S i) i0)); intuition.
+      now apply (valid_le_compat (max i (S 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|omega].
+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 (max (S 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 (S 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.
+  now cutrewrite <- (max (S i) i0 = i0); intuition.
+  now cutrewrite <- (max (S i) (S i0) = S i0); intuition.
+Qed.
+
+Lemma poly_mul_valid_compat : forall kl kr pl pr, valid kl pl -> valid kr pr ->
+  valid (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 (max (max i kr) (max (S i) (max (S i) kr)))).
+    case_decide.
+      now apply (valid_le_compat (max i kr)); auto.
+      apply poly_add_valid_compat; auto.
+      now apply poly_mul_mon_valid_compat; intuition.
+    repeat apply Nat.max_case_strong; omega.
+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 (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 Nat.max_case_strong; omega].
+  now induction Hr; constructor; auto.
+  apply (linear_le_compat (max kr (S i))); [|repeat apply Nat.max_case_strong; omega].
+  induction Hr; simpl.
+    constructor; auto.
+    replace i with (max i i) by (apply Nat.max_id); apply IHHl1; now constructor.
+    destruct (nat_compare_spec i i0); subst; try case_decide; repeat (constructor; intuition).
+      now apply (linear_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
+      now apply (linear_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
+      now apply (linear_le_compat (max i0 i0)); [now auto|]; rewrite Nat.max_id; auto.
+      now apply (linear_le_compat (max i0 (S i))); intuition.
+      apply (linear_le_compat (max i (S i0))); intuition.
+Qed.
+
+End Algebra.
+
+Section Reduce.
+
+(* A stronger version of the next lemma *)
+
+Lemma reduce_aux_eval_compat : forall k p var, valid (S 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 p2)).
+  rewrite <- IHp2; auto; rewrite <- IHp1; [ring|].
+  apply (valid_le_compat k); now auto.
+  remember (List.nth k var false) as b; destruct b; ring_simplify; [|now auto].
+  case_decide; simpl.
+    rewrite <- (IHp2 n); [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.
+      now apply (valid_le_compat n); [auto|omega].
+    rewrite (IHp2 n); [|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 n); [auto|omega].
+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 ->
+  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 (exfalso; omega).
+    now apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|omega].
+    f_equal; apply IHp1; auto.
+    now eapply valid_le_compat; [eauto|omega].
+Qed.
+
+(* Reduce projects valid polynomials into linear ones *)
+
+Lemma linear_reduce_aux : forall i p, valid (S 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 <- (Nat.max_id i) at 1; apply poly_add_linear_compat.
+      apply IHp1; eapply valid_le_compat; eauto.
+      now intuition.
+  case_decide.
+    apply IHp1; eapply valid_le_compat; [eauto|omega].
+    constructor; try omega; auto.
+    erewrite (reduce_aux_le_compat n); [|assumption|omega].
+    now apply IHp1; eapply valid_le_compat; eauto.
+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|omega].
+    constructor; auto.
+    apply linear_reduce_aux; auto.
+Qed.
+
+End Reduce.
diff --git a/plugins/btauto/Btauto.v b/plugins/btauto/Btauto.v
new file mode 100644
index 000000000..d3331ccf8
--- /dev/null
+++ b/plugins/btauto/Btauto.v
@@ -0,0 +1,3 @@
+Require Import Algebra Reflect.
+
+Declare ML Module "btauto_plugin".
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
new file mode 100644
index 000000000..1327e5e2f
--- /dev/null
+++ b/plugins/btauto/Reflect.v
@@ -0,0 +1,360 @@
+Require Import Bool DecidableClass Algebra Ring NPeano.
+
+Section Bool.
+
+(* Boolean formulas and their evaluations *)
+
+Inductive formula :=
+| formula_var : nat -> 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).
+Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat.
+Local Hint Constructors valid.
+
+(* 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.
+  now exists (S n); constructor; intuition; inversion H.
+  now exists 0; auto.
+  now exists 0; auto.
+  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (max n1 n2); auto.
+  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (max (max n1 n2) (max n1 n2)); auto.
+  now destruct IHf as [n Hn]; exists (max 0 n); auto.
+  now destruct IHf1 as [n1 Hn1]; destruct IHf2 as [n2 Hn2]; exists (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.
+
+Fixpoint make_last {A} n (x def : A) :=
+match n with
+| 0 => cons x nil
+| S n => cons def (make_last n x def)
+end.
+
+(* 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 =>
+  match n with
+  | 0 => cons b l
+  | S n => cons a (list_replace l n b)
+  end
+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 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; intros i x def Hd; simpl.
+  destruct i; [exfalso; omega|now destruct i; auto].
+  destruct i; intuition.
+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; intros x def; simpl; 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; [destruct i; reflexivity|assumption].
+  destruct i; destruct j; simpl; solve [auto|congruence].
+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.
+  now destruct i; simpl in *; [reflexivity|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; omega.
+    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; omega.
+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 (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. *)
diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mllib
new file mode 100644
index 000000000..319a9c302
--- /dev/null
+++ b/plugins/btauto/btauto_plugin.mllib
@@ -0,0 +1,3 @@
+Refl_btauto
+G_btauto
+Btauto_plugin_mod
diff --git a/plugins/btauto/g_btauto.ml4 b/plugins/btauto/g_btauto.ml4
new file mode 100644
index 000000000..a7171b6bd
--- /dev/null
+++ b/plugins/btauto/g_btauto.ml4
@@ -0,0 +1,14 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma"  i*)
+
+TACTIC EXTEND btauto
+| [ "btauto" ] -> [ Refl_btauto.Btauto.tac ]
+END
+
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
new file mode 100644
index 000000000..1d01f3e54
--- /dev/null
+++ b/plugins/btauto/refl_btauto.ml
@@ -0,0 +1,253 @@
+let contrib_name = "btauto"
+
+let init_constant dir s =
+  let find_constant contrib dir s =
+    Libnames.constr_of_global (Coqlib.find_reference contrib dir s)
+  in
+  find_constant contrib_name dir s
+
+let get_constant dir s = lazy (Coqlib.gen_constant contrib_name dir s)
+
+let get_inductive dir s =
+  let glob_ref () = Coqlib.find_reference contrib_name ("Coq" :: dir) s in
+  Lazy.lazy_from_fun (fun () -> Libnames.destIndRef (glob_ref ()))
+
+let decomp_term (c : Term.constr) =
+  Term.kind_of_term (Term.strip_outer_cast c)
+
+let lapp c v  = Term.mkApp (Lazy.force c, v)
+
+let (===) = Term.eq_constr
+
+module CoqList = struct
+  let path = ["Init"; "Datatypes"]
+  let typ = get_constant path "list"
+  let _nil = get_constant path "nil"
+  let _cons = get_constant path "cons"
+
+  let cons ty h t = lapp _cons [|ty; h ; t|]
+  let nil ty = lapp _nil [|ty|]
+  let rec of_list ty = function
+    | [] -> nil ty
+    | t::q -> cons ty t (of_list ty q)
+  let type_of_list ty = lapp typ [|ty|]
+
+end
+
+module CoqNat = struct
+  let path = ["Init"; "Datatypes"]
+  let typ = get_constant path "nat"
+  let _S = get_constant path "S"
+  let _O = get_constant path "O"
+
+  (* A coq nat from an int *)
+  let rec of_int n =
+    if n <= 0 then Lazy.force _O
+    else
+      let ans = of_int (pred n) in
+      lapp _S [|ans|]
+
+end
+
+module Env = struct
+
+  module ConstrHashed = struct
+    type t = Term.constr
+    let equal = Term.eq_constr
+    let hash = Term.hash_constr
+  end
+
+  module ConstrHashtbl = Hashtbl.Make (ConstrHashed)
+
+  type t = (int ConstrHashtbl.t * int ref)
+
+  let add (tbl, off) (t : Term.constr) =
+    try ConstrHashtbl.find tbl t 
+    with
+    | Not_found -> 
+      let i = !off in 
+      let () = ConstrHashtbl.add tbl t i in
+      let () = incr off in
+      i
+
+  let empty () = (ConstrHashtbl.create 16, ref 0)
+
+  let to_list (env, _) =
+    (* we need to get an ordered list *)
+    let fold constr key accu = (key, constr) :: accu in
+    let l = ConstrHashtbl.fold fold env [] in
+    let sorted_l = List.sort (fun p1 p2 -> compare (fst p1) (fst p2)) l in
+    List.map snd sorted_l
+
+end
+
+module Bool = struct
+
+  let typ = get_constant ["Init"; "Datatypes"] "bool"
+  let ind = get_inductive ["Init"; "Datatypes"] "bool"
+  let trueb = get_constant ["Init"; "Datatypes"] "true"
+  let falseb = get_constant ["Init"; "Datatypes"] "false"
+  let andb = get_constant ["Init"; "Datatypes"] "andb"
+  let orb = get_constant ["Init"; "Datatypes"] "orb"
+  let xorb = get_constant ["Init"; "Datatypes"] "xorb"
+  let negb = get_constant ["Init"; "Datatypes"] "negb"
+
+  type t =
+  | Var of int
+  | Const of bool
+  | Andb of t * t
+  | Orb of t * t
+  | Xorb of t * t
+  | Negb of t
+  | Ifb of t * t * t
+
+  let quote (env : Env.t) (c : Term.constr) : t =
+    let trueb = Lazy.force trueb in
+    let falseb = Lazy.force falseb in
+    let andb = Lazy.force andb in
+    let orb = Lazy.force orb in
+    let xorb = Lazy.force xorb in
+    let negb = Lazy.force negb in
+
+    let rec aux c = match decomp_term c with
+    | Term.App (head, args) ->
+      if head === andb && Array.length args = 2 then
+        Andb (aux args.(0), aux args.(1))
+      else if head === orb && Array.length args = 2 then
+        Orb (aux args.(0), aux args.(1))
+      else if head === xorb && Array.length args = 2 then
+        Xorb (aux args.(0), aux args.(1))
+      else if head === negb && Array.length args = 1 then
+        Negb (aux args.(0))
+      else Var (Env.add env c)
+    | Term.Case (info, r, arg, pats) ->
+      let is_bool =
+        let i = info.Term.ci_ind in
+        Names.eq_ind i (Lazy.force ind)
+      in
+      if is_bool then
+        Ifb ((aux arg), (aux pats.(0)), (aux pats.(1)))
+      else
+        Var (Env.add env c)
+    | _ ->
+      if c === falseb then Const false
+      else if c === trueb then Const true
+      else Var (Env.add env c)
+    in
+    aux c
+
+end
+
+module Btauto = struct
+
+  open Pp
+
+  let eq = get_constant ["Init"; "Logic"]  "eq"
+
+  let f_var = get_constant ["btauto"; "Reflect"] "formula_var"
+  let f_btm = get_constant ["btauto"; "Reflect"] "formula_btm"
+  let f_top = get_constant ["btauto"; "Reflect"] "formula_top"
+  let f_cnj = get_constant ["btauto"; "Reflect"] "formula_cnj"
+  let f_dsj = get_constant ["btauto"; "Reflect"] "formula_dsj"
+  let f_neg = get_constant ["btauto"; "Reflect"] "formula_neg"
+  let f_xor = get_constant ["btauto"; "Reflect"] "formula_xor"
+  let f_ifb = get_constant ["btauto"; "Reflect"] "formula_ifb"
+
+  let eval = get_constant ["btauto"; "Reflect"] "formula_eval"
+  let witness = get_constant ["btauto"; "Reflect"] "boolean_witness"
+
+  let soundness = get_constant ["btauto"; "Reflect"] "reduce_poly_of_formula_sound_alt"
+
+  let rec convert = function
+  | Bool.Var n -> lapp f_var [|CoqNat.of_int n|]
+  | Bool.Const true -> Lazy.force f_top
+  | Bool.Const false -> Lazy.force f_btm
+  | Bool.Andb (b1, b2) -> lapp f_cnj [|convert b1; convert b2|]
+  | Bool.Orb (b1, b2) -> lapp f_dsj [|convert b1; convert b2|]
+  | Bool.Negb b -> lapp f_neg [|convert b|]
+  | Bool.Xorb (b1, b2) -> lapp f_xor [|convert b1; convert b2|]
+  | Bool.Ifb (b1, b2, b3) -> lapp f_ifb [|convert b1; convert b2; convert b3|]
+
+  let convert_env env : Term.constr = 
+    CoqList.of_list (Lazy.force Bool.typ) env
+
+  let reify env t = lapp eval [|convert_env env; convert t|]
+
+  let print_counterexample p env gl =
+    let var = lapp witness [|p|] in
+    (* Compute an assignment that dissatisfies the goal *)
+    let var = Tacmach.pf_reduction_of_red_expr gl Glob_term.CbvVm var in
+    let rec to_list l = match decomp_term l with
+    | Term.App (c, _)
+      when c === (Lazy.force CoqList._nil) -> []
+    | Term.App (c, [|_; h; t|])
+      when c === (Lazy.force CoqList._cons) ->
+      if h === (Lazy.force Bool.trueb) then (true :: to_list t)
+      else if h === (Lazy.force Bool.falseb) then (false :: to_list t)
+      else invalid_arg "to_list"
+    | _ -> invalid_arg "to_list"
+    in
+    let concat sep = function
+    | [] -> mt ()
+    | h :: t ->
+      let rec aux = function
+      | [] -> mt ()
+      | x :: t -> (sep ++ x ++ aux t)
+      in
+      h ++ aux t
+    in
+    let msg =
+      try
+        let var = to_list var in
+        let assign = List.combine env var in
+        let map_msg (key, v) =
+          let b = if v then str "true" else str "false" in
+          let term = Printer.pr_constr key in
+          term ++ spc () ++ str ":=" ++ spc () ++ b
+        in
+        let assign = List.map map_msg assign in
+        let l = str "[" ++ (concat (str ";" ++ spc ()) assign) ++ str "]" in
+        str "Not a tautology:" ++ spc () ++ l
+      with _ -> (str "Not a tautology")
+    in
+    Tacticals.tclFAIL 0 msg gl
+
+  let try_unification env gl =
+    let eq = Lazy.force eq in
+    let concl = Tacmach.pf_concl gl in
+    let t = decomp_term concl in
+    match t with
+    | Term.App (c, [|typ; p; _|]) when c === eq ->
+      (* should be an equality [@eq poly ?p (Cst false)] *)
+      let tac = Tacticals.tclORELSE0 Tactics.reflexivity (print_counterexample p env) in
+      tac gl
+    | _ ->
+      let msg = str "Btauto: Internal error" in
+      Tacticals.tclFAIL 0 msg gl
+
+  let tac gl =
+    let eq = Lazy.force eq in
+    let bool = Lazy.force Bool.typ in
+    let concl = Tacmach.pf_concl gl in
+    let t = decomp_term concl in
+    match t with
+    | Term.App (c, [|typ; tl; tr|])
+        when typ === bool && c === eq ->
+      let env = Env.empty () in
+      let fl = Bool.quote env tl in
+      let fr = Bool.quote env tr in
+      let env = Env.to_list env in
+      let fl = reify env fl in
+      let fr = reify env fr in
+      let changed_gl = Term.mkApp (c, [|typ; fl; fr|]) in
+      Tacticals.tclTHENLIST [
+        Tactics.change_in_concl None changed_gl;
+        Tactics.apply (Lazy.force soundness);
+        Tactics.normalise_vm_in_concl;
+        try_unification env
+      ] gl
+    | _ ->
+      let msg = str "Cannot recognize a boolean equality" in
+      Tacticals.tclFAIL 0 msg gl
+
+end
diff --git a/plugins/btauto/vo.itarget b/plugins/btauto/vo.itarget
new file mode 100644
index 000000000..1f72d3ef2
--- /dev/null
+++ b/plugins/btauto/vo.itarget
@@ -0,0 +1,3 @@
+Algebra.vo
+Reflect.vo
+Btauto.vo
diff --git a/plugins/pluginsbyte.itarget b/plugins/pluginsbyte.itarget
index 04cbdccb0..e6b044906 100644
--- a/plugins/pluginsbyte.itarget
+++ b/plugins/pluginsbyte.itarget
@@ -1,3 +1,4 @@
+btauto/btauto_plugin.cma
 field/field_plugin.cma
 setoid_ring/newring_plugin.cma
 extraction/extraction_plugin.cma
diff --git a/plugins/pluginsdyn.itarget b/plugins/pluginsdyn.itarget
index bbadfe696..61d295237 100644
--- a/plugins/pluginsdyn.itarget
+++ b/plugins/pluginsdyn.itarget
@@ -1,3 +1,4 @@
+btauto/btauto_plugin.cmxs
 field/field_plugin.cmxs
 setoid_ring/newring_plugin.cmxs
 extraction/extraction_plugin.cmxs
diff --git a/plugins/pluginsopt.itarget b/plugins/pluginsopt.itarget
index 74b3f5275..25ee7b8b8 100644
--- a/plugins/pluginsopt.itarget
+++ b/plugins/pluginsopt.itarget
@@ -1,3 +1,4 @@
+btauto/btauto_plugin.cmxa
 field/field_plugin.cmxa
 setoid_ring/newring_plugin.cmxa
 extraction/extraction_plugin.cmxa
diff --git a/plugins/pluginsvo.itarget b/plugins/pluginsvo.itarget
index db56534c9..2091adf29 100644
--- a/plugins/pluginsvo.itarget
+++ b/plugins/pluginsvo.itarget
@@ -1,3 +1,4 @@
+btauto/vo.otarget
 dp/vo.otarget
 field/vo.otarget
 fourier/vo.otarget