diff options
Diffstat (limited to 'plugins/btauto')
| -rw-r--r-- | plugins/btauto/Algebra.v | 591 | ||||
| -rw-r--r-- | plugins/btauto/Btauto.v | 3 | ||||
| -rw-r--r-- | plugins/btauto/Reflect.v | 398 | ||||
| -rw-r--r-- | plugins/btauto/btauto_plugin.mllib | 3 | ||||
| -rw-r--r-- | plugins/btauto/g_btauto.ml4 | 16 | ||||
| -rw-r--r-- | plugins/btauto/refl_btauto.ml | 260 | ||||
| -rw-r--r-- | plugins/btauto/vo.itarget | 3 |
7 files changed, 1274 insertions, 0 deletions
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v new file mode 100644 index 00000000..bc5a3900 --- /dev/null +++ b/plugins/btauto/Algebra.v @@ -0,0 +1,591 @@ +Require Import Bool PArith DecidableClass Omega ROmega. + +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. + +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 (exfalso; zify; romega) +| [ X : context [Pos.compare ?x ?y] |- _ ] => + destruct (Pos.compare_spec x y); try (exfalso; zify; romega) +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. + +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 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)%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; zify; romega. +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; zify; romega. +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; zify; omega. + + intros; apply Hvar; zify; omega. +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; zify; romega +| [ |- (?z <= Pos.max ?x ?y)%positive ] => + apply Pos.max_case_strong; intros; zify; romega +| [ |- (Pos.max ?x ?y < ?z)%positive ] => + apply Pos.max_case_strong; intros; zify; romega +| [ |- (?z < Pos.max ?x ?y)%positive ] => + apply Pos.max_case_strong; intros; zify; romega +| _ => zify; omega +end. +Hint Resolve Pos.le_max_r Pos.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 (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; zify; romega. + + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega. + + 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|zify; romega]. +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. + - cutrewrite <- (Pos.max (Pos.succ i) i0 = i0); intuition. + - cutrewrite <- (Pos.max (Pos.succ i) (Pos.succ i0) = Pos.succ i0); 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; zify; 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 (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; zify; omega]. + 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|zify; omega]. ++ 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|zify; omega]. } + - 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|zify; 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)%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 (exfalso; zify; omega). ++ apply IHp1; [|now auto]; eapply valid_le_compat; [eauto|zify; omega]. ++ f_equal; apply IHp1; auto. + now eapply valid_le_compat; [eauto|zify; omega]. +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|zify; omega]. } + { intuition. } + - case_decide. + { apply IHp1; eapply valid_le_compat; [eauto|zify; omega]. } + { constructor; try (zify; omega); auto. + erewrite (reduce_aux_le_compat p2); [|assumption|zify; omega]. + apply IHp1; eapply valid_le_compat; [eauto|]; zify; omega. } +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|zify; 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 00000000..d3331ccf --- /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 00000000..3bd7cd62 --- /dev/null +++ b/plugins/btauto/Reflect.v @@ -0,0 +1,398 @@ +Require Import Bool DecidableClass Algebra Ring PArith ROmega Omega. + +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). +Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat. +Local Hint Constructors valid. +Hint Extern 5 => zify; omega. + +(* 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; zify; omega. +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; zify; omega. } +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; zify; 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; zify; 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 (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. *) diff --git a/plugins/btauto/btauto_plugin.mllib b/plugins/btauto/btauto_plugin.mllib new file mode 100644 index 00000000..319a9c30 --- /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 00000000..8e00b1c1 --- /dev/null +++ b/plugins/btauto/g_btauto.ml4 @@ -0,0 +1,16 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i camlp4deps: "grammar/grammar.cma" i*) + +DECLARE PLUGIN "btauto_plugin" + +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 00000000..57268a9c --- /dev/null +++ b/plugins/btauto/refl_btauto.ml @@ -0,0 +1,260 @@ + +let contrib_name = "btauto" + +let init_constant dir s = + let find_constant contrib dir s = + Universes.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 () -> Globnames.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 CoqPositive = struct + let path = ["Numbers"; "BinNums"] + let typ = get_constant path "positive" + let _xH = get_constant path "xH" + let _xO = get_constant path "xO" + let _xI = get_constant path "xI" + + (* A coq nat from an int *) + let rec of_int n = + if n <= 1 then Lazy.force _xH + else + let ans = of_int (n / 2) in + if n mod 2 = 0 then lapp _xO [|ans|] + else lapp _xI [|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 1) + + 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 -> Int.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 [|CoqPositive.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 (Genredexpr.CbvVm None) 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 e when Errors.noncritical e -> (str "Not a tautology") + in + Tacticals.tclFAIL 0 msg gl + + let try_unification env = + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let eq = Lazy.force eq 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.New.tclORELSE0 Tactics.reflexivity (Proofview.V82.tactic (print_counterexample p env)) in + tac + | _ -> + let msg = str "Btauto: Internal error" in + Tacticals.New.tclFAIL 0 msg + end + + let tac = + Proofview.Goal.nf_enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let eq = Lazy.force eq in + let bool = Lazy.force Bool.typ 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.New.tclTHENLIST [ + Tactics.change_concl changed_gl; + Tactics.apply (Lazy.force soundness); + Proofview.V82.tactic (Tactics.normalise_vm_in_concl); + try_unification env + ] + | _ -> + let msg = str "Cannot recognize a boolean equality" in + Tacticals.New.tclFAIL 0 msg + end + +end diff --git a/plugins/btauto/vo.itarget b/plugins/btauto/vo.itarget new file mode 100644 index 00000000..1f72d3ef --- /dev/null +++ b/plugins/btauto/vo.itarget @@ -0,0 +1,3 @@ +Algebra.vo +Reflect.vo +Btauto.vo |