aboutsummaryrefslogtreecommitdiff
path: root/theories
diff options
context:
space:
mode:
authorFrédéric Besson2020-05-11 11:59:42 +0200
committerMaxime Dénès2020-06-14 11:26:41 +0200
commitf8e91cb0a227a2d0423412e7533163568e1e9fdf (patch)
tree3a16a91e7167cb942686ab6657b76e3b86c151df /theories
parent13e8d04b2f080fbc7ca169bc39e53c8dd091d279 (diff)
[micromega] native support for boolean operators
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
Diffstat (limited to 'theories')
-rw-r--r--theories/Bool/Bool.v2
-rw-r--r--theories/Init/Datatypes.v1
-rw-r--r--theories/ZArith/BinInt.v7
-rw-r--r--theories/micromega/Lia.v2
-rw-r--r--theories/micromega/QMicromega.v75
-rw-r--r--theories/micromega/RMicromega.v126
-rw-r--r--theories/micromega/Tauto.v2247
-rw-r--r--theories/micromega/ZMicromega.v78
-rw-r--r--theories/micromega/ZifyBool.v227
-rw-r--r--theories/micromega/ZifyClasses.v31
10 files changed, 1739 insertions, 1057 deletions
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index d70978fabe..9e10786fcd 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -130,6 +130,8 @@ Definition eqb (b1 b2:bool) : bool :=
| false, false => true
end.
+Register eqb as core.bool.eqb.
+
Lemma eqb_subst :
forall (P:bool -> Prop) (b1 b2:bool), eqb b1 b2 = true -> P b1 -> P b2.
Proof.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index cba90043d5..8ab12ae534 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -73,6 +73,7 @@ Infix "&&" := andb : bool_scope.
Register andb as core.bool.andb.
Register orb as core.bool.orb.
+Register implb as core.bool.implb.
Register xorb as core.bool.xorb.
Register negb as core.bool.negb.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 1729b9f85e..a566348dd5 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -47,6 +47,8 @@ Register mul as num.Z.mul.
Register pow as num.Z.pow.
Register of_nat as num.Z.of_nat.
+
+
(** When including property functors, only inline t eq zero one two *)
Set Inline Level 30.
@@ -81,6 +83,11 @@ Register le as num.Z.le.
Register lt as num.Z.lt.
Register ge as num.Z.ge.
Register gt as num.Z.gt.
+Register leb as num.Z.leb.
+Register ltb as num.Z.ltb.
+Register geb as num.Z.geb.
+Register gtb as num.Z.gtb.
+Register eqb as num.Z.eqb.
(** * Decidability of equality. *)
diff --git a/theories/micromega/Lia.v b/theories/micromega/Lia.v
index 3d955fec4f..b2c5884ed7 100644
--- a/theories/micromega/Lia.v
+++ b/theories/micromega/Lia.v
@@ -19,7 +19,6 @@ Require Import BinNums.
Require Coq.micromega.Tauto.
Declare ML Module "micromega_plugin".
-
Ltac zchecker :=
intros ?__wit ?__varmap ?__ff ;
exact (ZTautoChecker_sound __ff __wit
@@ -30,7 +29,6 @@ Ltac lia := Zify.zify; xlia zchecker.
Ltac nia := Zify.zify; xnlia zchecker.
-
(* Local Variables: *)
(* coding: utf-8 *)
(* End: *)
diff --git a/theories/micromega/QMicromega.v b/theories/micromega/QMicromega.v
index 1fbc5a648a..90ed0ab9d2 100644
--- a/theories/micromega/QMicromega.v
+++ b/theories/micromega/QMicromega.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -107,7 +107,7 @@ Proof.
apply QNpower.
Qed.
-Definition Qeval_op2 (o : Op2) : Q -> Q -> Prop :=
+Definition Qeval_pop2 (o : Op2) : Q -> Q -> Prop :=
match o with
| OpEq => Qeq
| OpNEq => fun x y => ~ x == y
@@ -117,13 +117,63 @@ match o with
| OpGt => fun x y => Qlt y x
end.
-Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) :=
- let (lhs,o,rhs) := ff in Qeval_op2 o (Qeval_expr e lhs) (Qeval_expr e rhs).
+
+Definition Qlt_bool (x y : Q) :=
+ (Qnum x * QDen y <? Qnum y * QDen x)%Z.
+
+Definition Qeval_bop2 (o : Op2) : Q -> Q -> bool :=
+ match o with
+ | OpEq => Qeq_bool
+ | OpNEq => fun x y => negb (Qeq_bool x y)
+ | OpLe => Qle_bool
+ | OpGe => fun x y => Qle_bool y x
+ | OpLt => Qlt_bool
+ | OpGt => fun x y => Qlt_bool y x
+ end.
+
+Lemma Qlt_bool_iff : forall q1 q2,
+ Qlt_bool q1 q2 = true <-> q1 < q2.
+Proof.
+ unfold Qlt_bool.
+ unfold Qlt. intros.
+ apply Z.ltb_lt.
+Qed.
+
+Lemma pop2_bop2 :
+ forall (op : Op2) (q1 q2 : Q), is_true (Qeval_bop2 op q1 q2) <-> Qeval_pop2 op q1 q2.
+Proof.
+ unfold is_true.
+ destruct op ; simpl; intros.
+ - apply Qeq_bool_iff.
+ - rewrite <- Qeq_bool_iff.
+ rewrite negb_true_iff.
+ destruct (Qeq_bool q1 q2) ; intuition congruence.
+ - apply Qle_bool_iff.
+ - apply Qle_bool_iff.
+ - apply Qlt_bool_iff.
+ - apply Qlt_bool_iff.
+Qed.
+
+Definition Qeval_op2 (k:Tauto.kind) : Op2 -> Q -> Q -> Tauto.rtyp k:=
+ if k as k0 return (Op2 -> Q -> Q -> Tauto.rtyp k0)
+ then Qeval_pop2 else Qeval_bop2.
+
+
+Lemma Qeval_op2_hold : forall k op q1 q2,
+ Tauto.hold k (Qeval_op2 k op q1 q2) <-> Qeval_pop2 op q1 q2.
+Proof.
+ destruct k.
+ simpl ; tauto.
+ simpl. apply pop2_bop2.
+Qed.
+
+Definition Qeval_formula (e:PolEnv Q) (k: Tauto.kind) (ff : Formula Q) :=
+ let (lhs,o,rhs) := ff in Qeval_op2 k o (Qeval_expr e lhs) (Qeval_expr e rhs).
Definition Qeval_formula' :=
eval_formula Qplus Qmult Qminus Qopp Qeq Qle Qlt (fun x => x) (fun x => x) (pow_N 1 Qmult).
-Lemma Qeval_formula_compat : forall env f, Qeval_formula env f <-> Qeval_formula' env f.
+ Lemma Qeval_formula_compat : forall env b f, Tauto.hold b (Qeval_formula env b f) <-> Qeval_formula' env f.
Proof.
intros.
unfold Qeval_formula.
@@ -131,6 +181,8 @@ Proof.
repeat rewrite Qeval_expr_compat.
unfold Qeval_formula'.
unfold Qeval_expr'.
+ simpl.
+ rewrite Qeval_op2_hold.
split ; destruct Fop ; simpl; auto.
Qed.
@@ -186,10 +238,10 @@ Definition qdeduce := nformula_plus_nformula 0 Qplus Qeq_bool.
Definition normQ := norm 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
Declare Equivalent Keys normQ RingMicromega.norm.
-Definition cnfQ (Annot TX AF: Type) (f: TFormula (Formula Q) Annot TX AF) :=
+Definition cnfQ (Annot:Type) (TX: Tauto.kind -> Type) (AF: Type) (k: Tauto.kind) (f: TFormula (Formula Q) Annot TX AF k) :=
rxcnf qunsat qdeduce (Qnormalise Annot) (Qnegate Annot) true f.
-Definition QTautoChecker (f : BFormula (Formula Q)) (w: list QWitness) : bool :=
+Definition QTautoChecker (f : BFormula (Formula Q) Tauto.isProp) (w: list QWitness) : bool :=
@tauto_checker (Formula Q) (NFormula Q) unit
qunsat qdeduce
(Qnormalise unit)
@@ -208,8 +260,11 @@ Proof.
destruct t.
apply (check_inconsistent_sound Qsor QSORaddon) ; auto.
- unfold qdeduce. intros. revert H. apply (nformula_plus_nformula_correct Qsor QSORaddon);auto.
- - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now eapply (cnf_normalise_correct Qsor QSORaddon);eauto.
- - intros. rewrite Qeval_formula_compat. unfold Qeval_formula'. now eapply (cnf_negate_correct Qsor QSORaddon);eauto.
+ - intros.
+ rewrite Qeval_formula_compat.
+ eapply (cnf_normalise_correct Qsor QSORaddon) ; eauto.
+ - intros. rewrite Tauto.hold_eNOT. rewrite Qeval_formula_compat.
+ now eapply (cnf_negate_correct Qsor QSORaddon);eauto.
- intros t w0.
unfold eval_tt.
intros.
diff --git a/theories/micromega/RMicromega.v b/theories/micromega/RMicromega.v
index fd8903eac9..09b44f145d 100644
--- a/theories/micromega/RMicromega.v
+++ b/theories/micromega/RMicromega.v
@@ -1,7 +1,7 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * Copyright INRIA, CNRS and contributors *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
+(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -15,14 +15,13 @@
(************************************************************************)
Require Import OrderedRing.
-Require Import RingMicromega.
+Require Import QMicromega RingMicromega.
Require Import Refl.
-Require Import Raxioms Rfunctions RIneq Rpow_def.
+Require Import Sumbool Raxioms Rfunctions RIneq Rpow_def.
Require Import QArith.
Require Import Qfield.
Require Import Qreals.
Require Import DeclConstant.
-Require Import Ztac.
Require Setoid.
(*Declare ML Module "micromega_plugin".*)
@@ -344,16 +343,17 @@ Proof.
apply Qeq_bool_eq in C2.
rewrite C2.
simpl.
- rewrite Qpower0.
+ assert (z <> 0%Z).
+ { intro ; subst. apply Z.lt_irrefl in C1. auto. }
+ rewrite Qpower0 by auto.
apply Q2R_0.
- intro ; subst ; slia C1 C1.
+ rewrite Q2RpowerRZ.
rewrite IHc.
reflexivity.
rewrite andb_false_iff in C.
destruct C.
simpl. apply Z.ltb_ge in H.
- right ; normZ. slia H H0.
+ right. Ztac.normZ. Ztac.slia H H0.
left ; apply Qeq_bool_neq; auto.
+ simpl.
rewrite <- IHc.
@@ -382,7 +382,7 @@ Definition INZ (n:N) : R :=
Definition Reval_expr := eval_pexpr Rplus Rmult Rminus Ropp R_of_Rcst N.to_nat pow.
-Definition Reval_op2 (o:Op2) : R -> R -> Prop :=
+Definition Reval_pop2 (o:Op2) : R -> R -> Prop :=
match o with
| OpEq => @eq R
| OpNEq => fun x y => ~ x = y
@@ -392,27 +392,91 @@ Definition Reval_op2 (o:Op2) : R -> R -> Prop :=
| OpGt => Rgt
end.
+Definition sumboolb {A B : Prop} (x : @sumbool A B) : bool :=
+ if x then true else false.
-Definition Reval_formula (e: PolEnv R) (ff : Formula Rcst) :=
- let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs).
+
+Definition Reval_bop2 (o : Op2) : R -> R -> bool :=
+ match o with
+ | OpEq => fun x y => sumboolb (Req_EM_T x y)
+ | OpNEq => fun x y => negb (sumboolb (Req_EM_T x y))
+ | OpLe => fun x y => (sumboolb (Rle_lt_dec x y))
+ | OpGe => fun x y => (sumboolb (Rge_gt_dec x y))
+ | OpLt => fun x y => (sumboolb (Rlt_le_dec x y))
+ | OpGt => fun x y => (sumboolb (Rgt_dec x y))
+ end.
+
+Lemma pop2_bop2 :
+ forall (op : Op2) (r1 r2 : R), is_true (Reval_bop2 op r1 r2) <-> Reval_pop2 op r1 r2.
+Proof.
+ unfold is_true.
+ destruct op ; simpl; intros;
+ match goal with
+ | |- context[sumboolb (?F ?X ?Y)] =>
+ destruct (F X Y) ; simpl; intuition try congruence
+ end.
+ - apply Rlt_not_le in r. tauto.
+ - apply Rgt_not_ge in r. tauto.
+ - apply Rlt_not_le in H. tauto.
+Qed.
+
+Definition Reval_op2 (k: Tauto.kind) : Op2 -> R -> R -> Tauto.rtyp k:=
+ if k as k0 return (Op2 -> R -> R -> Tauto.rtyp k0)
+ then Reval_pop2 else Reval_bop2.
+
+Lemma Reval_op2_hold : forall b op q1 q2,
+ Tauto.hold b (Reval_op2 b op q1 q2) <-> Reval_pop2 op q1 q2.
+Proof.
+ destruct b.
+ simpl ; tauto.
+ simpl. apply pop2_bop2.
+Qed.
+
+Definition Reval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Rcst) :=
+ let (lhs,o,rhs) := ff in Reval_op2 k o (Reval_expr e lhs) (Reval_expr e rhs).
Definition Reval_formula' :=
eval_sformula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt N.to_nat pow R_of_Rcst.
-Definition QReval_formula :=
- eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow .
+Lemma Reval_pop2_eval_op2 : forall o e1 e2,
+ Reval_pop2 o e1 e2 <->
+ eval_op2 eq Rle Rlt o e1 e2.
+Proof.
+ destruct o ; simpl ; try tauto.
+ split.
+ apply Rge_le.
+ apply Rle_ge.
+Qed.
-Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f.
+Lemma Reval_formula_compat : forall env b f, Tauto.hold b (Reval_formula env b f) <-> Reval_formula' env f.
Proof.
intros.
unfold Reval_formula.
destruct f.
unfold Reval_formula'.
- unfold Reval_expr.
- split ; destruct Fop ; simpl ; auto.
- apply Rge_le.
- apply Rle_ge.
+ simpl.
+ rewrite Reval_op2_hold.
+ apply Reval_pop2_eval_op2.
+Qed.
+
+Definition QReval_expr := eval_pexpr Rplus Rmult Rminus Ropp Q2R to_nat pow.
+
+Definition QReval_formula (e: PolEnv R) (k: Tauto.kind) (ff : Formula Q) :=
+ let (lhs,o,rhs) := ff in Reval_op2 k o (QReval_expr e lhs) (QReval_expr e rhs).
+
+
+Definition QReval_formula' :=
+ eval_formula Rplus Rmult Rminus Ropp (@eq R) Rle Rlt Q2R N.to_nat pow.
+
+Lemma QReval_formula_compat : forall env b f, Tauto.hold b (QReval_formula env b f) <-> QReval_formula' env f.
+Proof.
+ intros.
+ unfold QReval_formula.
+ destruct f.
+ unfold QReval_formula'.
+ rewrite Reval_op2_hold.
+ apply Reval_pop2_eval_op2.
Qed.
Definition Qeval_nformula :=
@@ -451,7 +515,7 @@ Definition runsat := check_inconsistent 0%Q Qeq_bool Qle_bool.
Definition rdeduce := nformula_plus_nformula 0%Q Qplus Qeq_bool.
-Definition RTautoChecker (f : BFormula (Formula Rcst)) (w: list RWitness) : bool :=
+Definition RTautoChecker (f : BFormula (Formula Rcst) Tauto.isProp) (w: list RWitness) : bool :=
@tauto_checker (Formula Q) (NFormula Q)
unit runsat rdeduce
(Rnormalise unit) (Rnegate unit)
@@ -463,18 +527,20 @@ Proof.
unfold RTautoChecker.
intros TC env.
apply tauto_checker_sound with (eval:=QReval_formula) (eval':= Qeval_nformula) (env := env) in TC.
- - change (eval_f (fun x : Prop => x) (QReval_formula env))
+ - change (eval_f e_rtyp (QReval_formula env))
with
(eval_bf (QReval_formula env)) in TC.
rewrite eval_bf_map in TC.
unfold eval_bf in TC.
rewrite eval_f_morph with (ev':= Reval_formula env) in TC ; auto.
- intro.
- unfold QReval_formula.
- rewrite <- eval_formulaSC with (phiS := R_of_Rcst).
- rewrite Reval_formula_compat.
- tauto.
- intro. rewrite Q_of_RcstR. reflexivity.
+ intros.
+ apply Tauto.hold_eiff.
+ rewrite QReval_formula_compat.
+ unfold QReval_formula'.
+ rewrite <- eval_formulaSC with (phiS := R_of_Rcst).
+ rewrite Reval_formula_compat.
+ tauto.
+ intro. rewrite Q_of_RcstR. reflexivity.
-
apply Reval_nformula_dec.
- destruct t.
@@ -482,8 +548,12 @@ Proof.
- unfold rdeduce.
intros. revert H.
eapply (nformula_plus_nformula_correct Rsor QSORaddon); eauto.
- - now apply (cnf_normalise_correct Rsor QSORaddon).
- - intros. now eapply (cnf_negate_correct Rsor QSORaddon); eauto.
+ -
+ intros.
+ rewrite QReval_formula_compat.
+ eapply (cnf_normalise_correct Rsor QSORaddon) ; eauto.
+ - intros. rewrite Tauto.hold_eNOT. rewrite QReval_formula_compat.
+ now eapply (cnf_negate_correct Rsor QSORaddon); eauto.
- intros t w0.
unfold eval_tt.
intros.
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index 6e89089355..dddced5739 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -17,49 +17,64 @@
Require Import List.
Require Import Refl.
Require Import Bool.
+Require Import Relation_Definitions Setoid.
Set Implicit Arguments.
+(** Formulae are either interpreted over Prop or bool. *)
+Inductive kind : Type :=
+|isProp
+|isBool.
+
+Register isProp as micromega.kind.isProp.
+Register isBool as micromega.kind.isBool.
+
Section S.
Context {TA : Type}. (* type of interpreted atoms *)
- Context {TX : Type}. (* type of uninterpreted terms (Prop) *)
+ Context {TX : kind -> Type}. (* type of uninterpreted terms (Prop) *)
Context {AA : Type}. (* type of annotations for atoms *)
Context {AF : Type}. (* type of formulae identifiers *)
- Inductive GFormula : Type :=
- | TT : GFormula
- | FF : GFormula
- | X : TX -> GFormula
- | A : TA -> AA -> GFormula
- | Cj : GFormula -> GFormula -> GFormula
- | D : GFormula -> GFormula -> GFormula
- | N : GFormula -> GFormula
- | I : GFormula -> option AF -> GFormula -> GFormula.
+ Inductive GFormula : kind -> Type :=
+ | TT : forall (k: kind), GFormula k
+ | FF : forall (k: kind), GFormula k
+ | X : forall (k: kind), TX k -> GFormula k
+ | A : forall (k: kind), TA -> AA -> GFormula k
+ | AND : forall (k: kind), GFormula k -> GFormula k -> GFormula k
+ | OR : forall (k: kind), GFormula k -> GFormula k -> GFormula k
+ | NOT : forall (k: kind), GFormula k -> GFormula k
+ | IMPL : forall (k: kind), GFormula k -> option AF -> GFormula k -> GFormula k
+ | IFF : forall (k: kind), GFormula k -> GFormula k -> GFormula k
+ | EQ : GFormula isBool -> GFormula isBool -> GFormula isProp.
Register TT as micromega.GFormula.TT.
Register FF as micromega.GFormula.FF.
Register X as micromega.GFormula.X.
Register A as micromega.GFormula.A.
- Register Cj as micromega.GFormula.Cj.
- Register D as micromega.GFormula.D.
- Register N as micromega.GFormula.N.
- Register I as micromega.GFormula.I.
+ Register AND as micromega.GFormula.AND.
+ Register OR as micromega.GFormula.OR.
+ Register NOT as micromega.GFormula.NOT.
+ Register IMPL as micromega.GFormula.IMPL.
+ Register IFF as micromega.GFormula.IFF.
+ Register EQ as micromega.GFormula.EQ.
Section MAPX.
- Variable F : TX -> TX.
+ Variable F : forall k, TX k -> TX k.
- Fixpoint mapX (f : GFormula) : GFormula :=
+ Fixpoint mapX (k:kind) (f : GFormula k) : GFormula k :=
match f with
- | TT => TT
- | FF => FF
- | X x => X (F x)
- | A a an => A a an
- | Cj f1 f2 => Cj (mapX f1) (mapX f2)
- | D f1 f2 => D (mapX f1) (mapX f2)
- | N f => N (mapX f)
- | I f1 o f2 => I (mapX f1) o (mapX f2)
+ | TT k => TT k
+ | FF k => FF k
+ | X x => X (F x)
+ | A k a an => A k a an
+ | AND f1 f2 => AND (mapX f1) (mapX f2)
+ | OR f1 f2 => OR (mapX f1) (mapX f2)
+ | NOT f => NOT (mapX f)
+ | IMPL f1 o f2 => IMPL (mapX f1) o (mapX f2)
+ | IFF f1 f2 => IFF (mapX f1) (mapX f2)
+ | EQ f1 f2 => EQ (mapX f1) (mapX f2)
end.
End MAPX.
@@ -68,16 +83,17 @@ Section S.
Variable ACC : Type.
Variable F : ACC -> AA -> ACC.
- Fixpoint foldA (f : GFormula) (acc : ACC) : ACC :=
+ Fixpoint foldA (k: kind) (f : GFormula k) (acc : ACC) : ACC :=
match f with
- | TT => acc
- | FF => acc
+ | TT _ => acc
+ | FF _ => acc
| X x => acc
- | A a an => F acc an
- | Cj f1 f2
- | D f1 f2
- | I f1 _ f2 => foldA f1 (foldA f2 acc)
- | N f => foldA f acc
+ | A _ a an => F acc an
+ | AND f1 f2
+ | OR f1 f2
+ | IFF f1 f2
+ | IMPL f1 _ f2 | EQ f1 f2 => foldA f1 (foldA f2 acc)
+ | NOT f => foldA f acc
end.
End FOLDANNOT.
@@ -89,84 +105,212 @@ Section S.
| Some id => id :: l
end.
- Fixpoint ids_of_formula f :=
+ Fixpoint ids_of_formula (k: kind) (f:GFormula k) :=
match f with
- | I f id f' => cons_id id (ids_of_formula f')
+ | IMPL f id f' => cons_id id (ids_of_formula f')
| _ => nil
end.
- Fixpoint collect_annot (f : GFormula) : list AA :=
+ Fixpoint collect_annot (k: kind) (f : GFormula k) : list AA :=
match f with
- | TT | FF | X _ => nil
- | A _ a => a ::nil
- | Cj f1 f2
- | D f1 f2
- | I f1 _ f2 => collect_annot f1 ++ collect_annot f2
- | N f => collect_annot f
+ | TT _ | FF _ | X _ => nil
+ | A _ _ a => a ::nil
+ | AND f1 f2
+ | OR f1 f2
+ | IFF f1 f2 | EQ f1 f2
+ | IMPL f1 _ f2 => collect_annot f1 ++ collect_annot f2
+ | NOT f => collect_annot f
end.
- Variable ex : TX -> Prop. (* [ex] will be the identity *)
+ Definition rtyp (k: kind) : Type := if k then Prop else bool.
- Section EVAL.
+ Variable ex : forall (k: kind), TX k -> rtyp k. (* [ex] will be the identity *)
- Variable ea : TA -> Prop.
+ Section EVAL.
- Fixpoint eval_f (f:GFormula) {struct f}: Prop :=
- match f with
- | TT => True
- | FF => False
- | A a _ => ea a
- | X p => ex p
- | Cj e1 e2 => (eval_f e1) /\ (eval_f e2)
- | D e1 e2 => (eval_f e1) \/ (eval_f e2)
- | N e => ~ (eval_f e)
- | I f1 _ f2 => (eval_f f1) -> (eval_f f2)
- end.
+ Variable ea : forall (k: kind), TA -> rtyp k.
+
+ Definition eTT (k: kind) : rtyp k :=
+ if k as k' return rtyp k' then True else true.
+
+ Definition eFF (k: kind) : rtyp k :=
+ if k as k' return rtyp k' then False else false.
+
+ Definition eAND (k: kind) : rtyp k -> rtyp k -> rtyp k :=
+ if k as k' return rtyp k' -> rtyp k' -> rtyp k'
+ then and else andb.
+
+ Definition eOR (k: kind) : rtyp k -> rtyp k -> rtyp k :=
+ if k as k' return rtyp k' -> rtyp k' -> rtyp k'
+ then or else orb.
+
+ Definition eIMPL (k: kind) : rtyp k -> rtyp k -> rtyp k :=
+ if k as k' return rtyp k' -> rtyp k' -> rtyp k'
+ then (fun x y => x -> y) else implb.
+
+ Definition eIFF (k: kind) : rtyp k -> rtyp k -> rtyp k :=
+ if k as k' return rtyp k' -> rtyp k' -> rtyp k'
+ then iff else eqb.
+
+ Definition eNOT (k: kind) : rtyp k -> rtyp k :=
+ if k as k' return rtyp k' -> rtyp k'
+ then not else negb.
+
+ Fixpoint eval_f (k: kind) (f:GFormula k) {struct f}: rtyp k :=
+ match f in GFormula k' return rtyp k' with
+ | TT tk => eTT tk
+ | FF tk => eFF tk
+ | A k a _ => ea k a
+ | X p => ex p
+ | @AND k e1 e2 => eAND k (eval_f e1) (eval_f e2)
+ | @OR k e1 e2 => eOR k (eval_f e1) (eval_f e2)
+ | @NOT k e => eNOT k (eval_f e)
+ | @IMPL k f1 _ f2 => eIMPL k (eval_f f1) (eval_f f2)
+ | @IFF k f1 f2 => eIFF k (eval_f f1) (eval_f f2)
+ | EQ f1 f2 => (eval_f f1) = (eval_f f2)
+ end.
+ Lemma eval_f_rew : forall k (f:GFormula k),
+ eval_f f =
+ match f in GFormula k' return rtyp k' with
+ | TT tk => eTT tk
+ | FF tk => eFF tk
+ | A k a _ => ea k a
+ | X p => ex p
+ | @AND k e1 e2 => eAND k (eval_f e1) (eval_f e2)
+ | @OR k e1 e2 => eOR k (eval_f e1) (eval_f e2)
+ | @NOT k e => eNOT k (eval_f e)
+ | @IMPL k f1 _ f2 => eIMPL k (eval_f f1) (eval_f f2)
+ | @IFF k f1 f2 => eIFF k (eval_f f1) (eval_f f2)
+ | EQ f1 f2 => (eval_f f1) = (eval_f f2)
+ end.
+ Proof.
+ destruct f ; reflexivity.
+ Qed.
End EVAL.
+ Definition hold (k: kind) : rtyp k -> Prop :=
+ if k as k0 return (rtyp k0 -> Prop) then fun x => x else is_true.
+ Definition eiff (k: kind) : rtyp k -> rtyp k -> Prop :=
+ if k as k' return rtyp k' -> rtyp k' -> Prop then iff else @eq bool.
+ Lemma eiff_refl : forall (k: kind) (x : rtyp k),
+ eiff k x x.
+ Proof.
+ destruct k ; simpl; tauto.
+ Qed.
- Lemma eval_f_morph :
- forall (ev ev' : TA -> Prop) (f : GFormula),
- (forall a, ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f).
+ Lemma eiff_sym : forall k (x y : rtyp k), eiff k x y -> eiff k y x.
+ Proof.
+ destruct k ; simpl; intros ; intuition.
+ Qed.
+
+ Lemma eiff_trans : forall k (x y z : rtyp k), eiff k x y -> eiff k y z -> eiff k x z.
+ Proof.
+ destruct k ; simpl; intros ; intuition congruence.
+ Qed.
+
+ Lemma hold_eiff : forall (k: kind) (x y : rtyp k),
+ (hold k x <-> hold k y) <-> eiff k x y.
+ Proof.
+ destruct k ; simpl.
+ - tauto.
+ - unfold is_true.
+ destruct x,y ; intuition congruence.
+ Qed.
+
+ Instance eiff_eq (k: kind) : Equivalence (eiff k).
+ Proof.
+ constructor.
+ - exact (eiff_refl k).
+ - exact (eiff_sym k).
+ - exact (eiff_trans k).
+ Qed.
+
+ Add Parametric Morphism (k: kind) : (@eAND k) with signature eiff k ==> eiff k ==> eiff k as eAnd_morph.
+ Proof.
+ intros.
+ destruct k ; simpl in *; intuition congruence.
+ Qed.
+
+ Add Parametric Morphism (k: kind) : (@eOR k) with signature eiff k ==> eiff k ==> eiff k as eOR_morph.
+ Proof.
+ intros.
+ destruct k ; simpl in *; intuition congruence.
+ Qed.
+
+ Add Parametric Morphism (k: kind) : (@eIMPL k) with signature eiff k ==> eiff k ==> eiff k as eIMPL_morph.
+ Proof.
+ intros.
+ destruct k ; simpl in *; intuition congruence.
+ Qed.
+
+ Add Parametric Morphism (k: kind) : (@eIFF k) with signature eiff k ==> eiff k ==> eiff k as eIFF_morph.
Proof.
- induction f ; simpl ; try tauto.
intros.
- apply H.
+ destruct k ; simpl in *; intuition congruence.
Qed.
+ Add Parametric Morphism (k: kind) : (@eNOT k) with signature eiff k ==> eiff k as eNOT_morph.
+ Proof.
+ intros.
+ destruct k ; simpl in *; intuition congruence.
+ Qed.
+
+ Lemma eval_f_morph :
+ forall (ev ev' : forall (k: kind), TA -> rtyp k),
+ (forall k a, eiff k (ev k a) (ev' k a)) ->
+ forall (k: kind)(f : GFormula k),
+ (eiff k (eval_f ev f) (eval_f ev' f)).
+ Proof.
+ induction f ; simpl.
+ - reflexivity.
+ - reflexivity.
+ - reflexivity.
+ - apply H.
+ - rewrite IHf1. rewrite IHf2. reflexivity.
+ - rewrite IHf1. rewrite IHf2. reflexivity.
+ - rewrite IHf. reflexivity.
+ - rewrite IHf1. rewrite IHf2. reflexivity.
+ - rewrite IHf1. rewrite IHf2. reflexivity.
+ - simpl in *. intuition congruence.
+ Qed.
End S.
(** Typical boolean formulae *)
-Definition BFormula (A : Type) := @GFormula A Prop unit unit.
+Definition eKind (k: kind) := if k then Prop else bool.
+Register eKind as micromega.eKind.
+
+Definition BFormula (A : Type) := @GFormula A eKind unit unit.
Register BFormula as micromega.BFormula.type.
Section MAPATOMS.
Context {TA TA':Type}.
- Context {TX : Type}.
+ Context {TX : kind -> Type}.
Context {AA : Type}.
Context {AF : Type}.
-Fixpoint map_bformula (fct : TA -> TA') (f : @GFormula TA TX AA AF ) : @GFormula TA' TX AA AF :=
- match f with
- | TT => TT
- | FF => FF
- | X p => X p
- | A a t => A (fct a) t
- | Cj f1 f2 => Cj (map_bformula fct f1) (map_bformula fct f2)
- | D f1 f2 => D (map_bformula fct f1) (map_bformula fct f2)
- | N f => N (map_bformula fct f)
- | I f1 a f2 => I (map_bformula fct f1) a (map_bformula fct f2)
- end.
+ Fixpoint map_bformula (k: kind)(fct : TA -> TA') (f : @GFormula TA TX AA AF k) : @GFormula TA' TX AA AF k:=
+ match f with
+ | TT k => TT k
+ | FF k => FF k
+ | X k p => X k p
+ | A k a t => A k (fct a) t
+ | AND f1 f2 => AND (map_bformula fct f1) (map_bformula fct f2)
+ | OR f1 f2 => OR (map_bformula fct f1) (map_bformula fct f2)
+ | NOT f => NOT (map_bformula fct f)
+ | IMPL f1 a f2 => IMPL (map_bformula fct f1) a (map_bformula fct f2)
+ | IFF f1 f2 => IFF (map_bformula fct f1) (map_bformula fct f2)
+ | EQ f1 f2 => EQ (map_bformula fct f1) (map_bformula fct f2)
+ end.
End MAPATOMS.
@@ -204,345 +348,458 @@ Section S.
(** Our cnf is optimised and detects contradictions on the fly. *)
Fixpoint add_term (t: Term' * Annot) (cl : clause) : option clause :=
- match cl with
- | nil =>
- match deduce (fst t) (fst t) with
- | None => Some (t ::nil)
- | Some u => if unsat u then None else Some (t::nil)
+ match cl with
+ | nil =>
+ match deduce (fst t) (fst t) with
+ | None => Some (t ::nil)
+ | Some u => if unsat u then None else Some (t::nil)
+ end
+ | t'::cl =>
+ match deduce (fst t) (fst t') with
+ | None =>
+ match add_term t cl with
+ | None => None
+ | Some cl' => Some (t' :: cl')
end
- | t'::cl =>
- match deduce (fst t) (fst t') with
- | None =>
+ | Some u =>
+ if unsat u then None else
match add_term t cl with
| None => None
| Some cl' => Some (t' :: cl')
end
- | Some u =>
- if unsat u then None else
- match add_term t cl with
- | None => None
- | Some cl' => Some (t' :: cl')
- end
+ end
+ end.
+
+ Fixpoint or_clause (cl1 cl2 : clause) : option clause :=
+ match cl1 with
+ | nil => Some cl2
+ | t::cl => match add_term t cl2 with
+ | None => None
+ | Some cl' => or_clause cl cl'
+ end
+ end.
+
+ Definition xor_clause_cnf (t:clause) (f:cnf) : cnf :=
+ List.fold_left (fun acc e =>
+ match or_clause t e with
+ | None => acc
+ | Some cl => cl :: acc
+ end) f nil .
+
+ Definition or_clause_cnf (t: clause) (f:cnf) : cnf :=
+ match t with
+ | nil => f
+ | _ => xor_clause_cnf t f
+ end.
+
+
+ Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf :=
+ match f with
+ | nil => cnf_tt
+ | e :: rst => (or_cnf rst f') +++ (or_clause_cnf e f')
+ end.
+
+
+ Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf :=
+ f1 +++ f2.
+
+ (** TX is Prop in Coq and EConstr.constr in Ocaml.
+ AF is unit in Coq and Names.Id.t in Ocaml
+ *)
+ Definition TFormula (TX: kind -> Type) (AF: Type) := @GFormula Term TX Annot AF.
+
+
+ Definition is_cnf_tt (c : cnf) : bool :=
+ match c with
+ | nil => true
+ | _ => false
+ end.
+
+ Definition is_cnf_ff (c : cnf) : bool :=
+ match c with
+ | nil::nil => true
+ | _ => false
+ end.
+
+ Definition and_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
+ if is_cnf_ff f1 || is_cnf_ff f2
+ then cnf_ff
+ else
+ if is_cnf_tt f2
+ then f1
+ else and_cnf f1 f2.
+
+
+ Definition or_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
+ if is_cnf_tt f1 || is_cnf_tt f2
+ then cnf_tt
+ else if is_cnf_ff f2
+ then f1 else or_cnf f1 f2.
+
+ Section REC.
+ Context {TX : kind -> Type}.
+ Context {AF : Type}.
+
+ Variable REC : forall (pol : bool) (k: kind) (f : TFormula TX AF k), cnf.
+
+ Definition mk_and (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):=
+ (if pol then and_cnf_opt else or_cnf_opt) (REC pol f1) (REC pol f2).
+
+ Definition mk_or (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):=
+ (if pol then or_cnf_opt else and_cnf_opt) (REC pol f1) (REC pol f2).
+
+ Definition mk_impl (k: kind) (pol:bool) (f1 f2 : TFormula TX AF k):=
+ (if pol then or_cnf_opt else and_cnf_opt) (REC (negb pol) f1) (REC pol f2).
+
+
+ Definition mk_iff (k: kind) (pol:bool) (f1 f2: TFormula TX AF k):=
+ or_cnf_opt (and_cnf_opt (REC (negb pol) f1) (REC false f2))
+ (and_cnf_opt (REC pol f1) (REC true f2)).
+
+
+ End REC.
+
+ Definition is_bool {TX : kind -> Type} {AF: Type} (k: kind) (f : TFormula TX AF k) :=
+ match f with
+ | TT _ => Some true
+ | FF _ => Some false
+ | _ => None
+ end.
+
+ Lemma is_bool_inv : forall {TX : kind -> Type} {AF: Type} (k: kind) (f : TFormula TX AF k) res,
+ is_bool f = Some res -> f = if res then TT _ else FF _.
+ Proof.
+ intros.
+ destruct f ; inversion H; reflexivity.
+ Qed.
+
+
+ Fixpoint xcnf {TX : kind -> Type} {AF: Type} (pol : bool) (k: kind) (f : TFormula TX AF k) {struct f}: cnf :=
+ match f with
+ | TT _ => if pol then cnf_tt else cnf_ff
+ | FF _ => if pol then cnf_ff else cnf_tt
+ | X _ p => if pol then cnf_ff else cnf_ff (* This is not complete - cannot negate any proposition *)
+ | A _ x t => if pol then normalise x t else negate x t
+ | NOT e => xcnf (negb pol) e
+ | AND e1 e2 => mk_and xcnf pol e1 e2
+ | OR e1 e2 => mk_or xcnf pol e1 e2
+ | IMPL e1 _ e2 => mk_impl xcnf pol e1 e2
+ | IFF e1 e2 => match is_bool e2 with
+ | Some isb => xcnf (if isb then pol else negb pol) e1
+ | None => mk_iff xcnf pol e1 e2
+ end
+ | EQ e1 e2 =>
+ match is_bool e2 with
+ | Some isb => xcnf (if isb then pol else negb pol) e1
+ | None => mk_iff xcnf pol e1 e2
+ end
+ end.
+
+ Section CNFAnnot.
+
+ (** Records annotations used to optimise the cnf.
+ Those need to be kept when pruning the formula.
+ For efficiency, this is a separate function.
+ *)
+
+ Fixpoint radd_term (t : Term' * Annot) (cl : clause) : clause + list Annot :=
+ match cl with
+ | nil => (* if t is unsat, the clause is empty BUT t is needed. *)
+ match deduce (fst t) (fst t) with
+ | Some u => if unsat u then inr ((snd t)::nil) else inl (t::nil)
+ | None => inl (t::nil)
+ end
+ | t'::cl => (* if t /\ t' is unsat, the clause is empty BUT t & t' are needed *)
+ match deduce (fst t) (fst t') with
+ | Some u => if unsat u then inr ((snd t)::(snd t')::nil)
+ else match radd_term t cl with
+ | inl cl' => inl (t'::cl')
+ | inr l => inr l
+ end
+ | None => match radd_term t cl with
+ | inl cl' => inl (t'::cl')
+ | inr l => inr l
+ end
end
end.
- Fixpoint or_clause (cl1 cl2 : clause) : option clause :=
+ Fixpoint ror_clause cl1 cl2 :=
match cl1 with
- | nil => Some cl2
- | t::cl => match add_term t cl2 with
- | None => None
- | Some cl' => or_clause cl cl'
+ | nil => inl cl2
+ | t::cl => match radd_term t cl2 with
+ | inl cl' => ror_clause cl cl'
+ | inr l => inr l
end
end.
- Definition xor_clause_cnf (t:clause) (f:cnf) : cnf :=
- List.fold_left (fun acc e =>
- match or_clause t e with
- | None => acc
- | Some cl => cl :: acc
- end) f nil .
+ Definition xror_clause_cnf t f :=
+ List.fold_left (fun '(acc,tg) e =>
+ match ror_clause t e with
+ | inl cl => (cl :: acc,tg)
+ | inr l => (acc,tg+++l)
+ end) f (nil,nil).
- Definition or_clause_cnf (t: clause) (f:cnf) : cnf :=
+ Definition ror_clause_cnf t f :=
match t with
- | nil => f
- | _ => xor_clause_cnf t f
+ | nil => (f,nil)
+ | _ => xror_clause_cnf t f
end.
- Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf :=
+ Fixpoint ror_cnf (f f':list clause) :=
match f with
- | nil => cnf_tt
- | e :: rst => (or_cnf rst f') +++ (or_clause_cnf e f')
+ | nil => (cnf_tt,nil)
+ | e :: rst =>
+ let (rst_f',t) := ror_cnf rst f' in
+ let (e_f', t') := ror_clause_cnf e f' in
+ (rst_f' +++ e_f', t +++ t')
end.
+ Definition annot_of_clause (l : clause) : list Annot :=
+ List.map snd l.
- Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf :=
- f1 +++ f2.
+ Definition annot_of_cnf (f : cnf) : list Annot :=
+ List.fold_left (fun acc e => annot_of_clause e +++ acc ) f nil.
- (** TX is Prop in Coq and EConstr.constr in Ocaml.
- AF i s unit in Coq and Names.Id.t in Ocaml
- *)
- Definition TFormula (TX: Type) (AF: Type) := @GFormula Term TX Annot AF.
+ Definition ror_cnf_opt f1 f2 :=
+ if is_cnf_tt f1
+ then (cnf_tt , nil)
+ else if is_cnf_tt f2
+ then (cnf_tt, nil)
+ else if is_cnf_ff f2
+ then (f1,nil)
+ else ror_cnf f1 f2.
- Definition is_cnf_tt (c : cnf) : bool :=
- match c with
- | nil => true
- | _ => false
- end.
- Definition is_cnf_ff (c : cnf) : bool :=
- match c with
- | nil::nil => true
- | _ => false
+ Definition ocons {A : Type} (o : option A) (l : list A) : list A :=
+ match o with
+ | None => l
+ | Some e => e ::l
end.
- Definition and_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
- if is_cnf_ff f1 || is_cnf_ff f2
- then cnf_ff
- else and_cnf f1 f2.
-
- Definition or_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
- if is_cnf_tt f1 || is_cnf_tt f2
- then cnf_tt
- else if is_cnf_ff f2
- then f1 else or_cnf f1 f2.
+ Definition ratom (c : cnf) (a : Annot) : cnf * list Annot :=
+ if is_cnf_ff c || is_cnf_tt c
+ then (c,a::nil)
+ else (c,nil). (* t is embedded in c *)
+
+ Section REC.
+ Context {TX : kind -> Type} {AF : Type}.
+
+ Variable RXCNF : forall (polarity: bool) (k: kind) (f: TFormula TX AF k) , cnf * list Annot.
+
+ Definition rxcnf_and (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) :=
+ let '(e1,t1) := RXCNF polarity e1 in
+ let '(e2,t2) := RXCNF polarity e2 in
+ if polarity
+ then (and_cnf_opt e1 e2, t1 +++ t2)
+ else let (f',t') := ror_cnf_opt e1 e2 in
+ (f', t1 +++ t2 +++ t').
+
+ Definition rxcnf_or (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) :=
+ let '(e1,t1) := RXCNF polarity e1 in
+ let '(e2,t2) := RXCNF polarity e2 in
+ if polarity
+ then let (f',t') := ror_cnf_opt e1 e2 in
+ (f', t1 +++ t2 +++ t')
+ else (and_cnf_opt e1 e2, t1 +++ t2).
+
+ Definition rxcnf_impl (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) :=
+ let '(e1 , t1) := (RXCNF (negb polarity) e1) in
+ if polarity
+ then
+ if is_cnf_ff e1
+ then
+ RXCNF polarity e2
+ else (* compute disjunction *)
+ let '(e2 , t2) := (RXCNF polarity e2) in
+ let (f',t') := ror_cnf_opt e1 e2 in
+ (f', t1 +++ t2 +++ t') (* record the hypothesis *)
+ else
+ let '(e2 , t2) := (RXCNF polarity e2) in
+ (and_cnf_opt e1 e2, t1 +++ t2).
+
+ Definition rxcnf_iff (polarity:bool) (k: kind) (e1 e2 : TFormula TX AF k) :=
+ let '(c1,t1) := RXCNF (negb polarity) e1 in
+ let '(c2,t2) := RXCNF false e2 in
+ let '(c3,t3) := RXCNF polarity e1 in
+ let '(c4,t4) := RXCNF true e2 in
+ let (f',t') := ror_cnf_opt (and_cnf_opt c1 c2) (and_cnf_opt c3 c4) in
+ (f', t1+++ t2+++t3 +++ t4 +++ t')
+ .
+
+ End REC.
+
+ Fixpoint rxcnf {TX : kind -> Type} {AF: Type}(polarity : bool) (k: kind) (f : TFormula TX AF k) : cnf * list Annot :=
- Fixpoint xcnf {TX AF: Type} (pol : bool) (f : TFormula TX AF) {struct f}: cnf :=
match f with
- | TT => if pol then cnf_tt else cnf_ff
- | FF => if pol then cnf_ff else cnf_tt
- | X p => if pol then cnf_ff else cnf_ff (* This is not complete - cannot negate any proposition *)
- | A x t => if pol then normalise x t else negate x t
- | N e => xcnf (negb pol) e
- | Cj e1 e2 =>
- (if pol then and_cnf_opt else or_cnf_opt) (xcnf pol e1) (xcnf pol e2)
- | D e1 e2 => (if pol then or_cnf_opt else and_cnf_opt) (xcnf pol e1) (xcnf pol e2)
- | I e1 _ e2
- => (if pol then or_cnf_opt else and_cnf_opt) (xcnf (negb pol) e1) (xcnf pol e2)
+ | TT _ => if polarity then (cnf_tt,nil) else (cnf_ff,nil)
+ | FF _ => if polarity then (cnf_ff,nil) else (cnf_tt,nil)
+ | X b p => if polarity then (cnf_ff,nil) else (cnf_ff,nil)
+ | A _ x t => ratom (if polarity then normalise x t else negate x t) t
+ | NOT e => rxcnf (negb polarity) e
+ | AND e1 e2 => rxcnf_and rxcnf polarity e1 e2
+ | OR e1 e2 => rxcnf_or rxcnf polarity e1 e2
+ | IMPL e1 a e2 => rxcnf_impl rxcnf polarity e1 e2
+ | IFF e1 e2 => rxcnf_iff rxcnf polarity e1 e2
+ | EQ e1 e2 => rxcnf_iff rxcnf polarity e1 e2
end.
- Section CNFAnnot.
-
- (** Records annotations used to optimise the cnf.
- Those need to be kept when pruning the formula.
- For efficiency, this is a separate function.
- *)
-
- Fixpoint radd_term (t : Term' * Annot) (cl : clause) : clause + list Annot :=
- match cl with
- | nil => (* if t is unsat, the clause is empty BUT t is needed. *)
- match deduce (fst t) (fst t) with
- | Some u => if unsat u then inr ((snd t)::nil) else inl (t::nil)
- | None => inl (t::nil)
- end
- | t'::cl => (* if t /\ t' is unsat, the clause is empty BUT t & t' are needed *)
- match deduce (fst t) (fst t') with
- | Some u => if unsat u then inr ((snd t)::(snd t')::nil)
- else match radd_term t cl with
- | inl cl' => inl (t'::cl')
- | inr l => inr l
- end
- | None => match radd_term t cl with
- | inl cl' => inl (t'::cl')
- | inr l => inr l
- end
- end
- end.
+ Section Abstraction.
+ Variable TX : kind -> Type.
+ Variable AF : Type.
- Fixpoint ror_clause cl1 cl2 :=
- match cl1 with
- | nil => inl cl2
- | t::cl => match radd_term t cl2 with
- | inl cl' => ror_clause cl cl'
- | inr l => inr l
- end
- end.
+ Class to_constrT : Type :=
+ {
+ mkTT : forall (k: kind), TX k;
+ mkFF : forall (k: kind), TX k;
+ mkA : forall (k: kind), Term -> Annot -> TX k;
+ mkAND : forall (k: kind), TX k -> TX k -> TX k;
+ mkOR : forall (k: kind), TX k -> TX k -> TX k;
+ mkIMPL : forall (k: kind), TX k -> TX k -> TX k;
+ mkIFF : forall (k: kind), TX k -> TX k -> TX k;
+ mkNOT : forall (k: kind), TX k -> TX k;
+ mkEQ : TX isBool -> TX isBool -> TX isProp
- Definition xror_clause_cnf t f :=
- List.fold_left (fun '(acc,tg) e =>
- match ror_clause t e with
- | inl cl => (cl :: acc,tg)
- | inr l => (acc,tg+++l)
- end) f (nil,nil).
-
- Definition ror_clause_cnf t f :=
- match t with
- | nil => (f,nil)
- | _ => xror_clause_cnf t f
- end.
+ }.
+ Context {to_constr : to_constrT}.
- Fixpoint ror_cnf (f f':list clause) :=
+ Fixpoint aformula (k: kind) (f : TFormula TX AF k) : TX k :=
match f with
- | nil => (cnf_tt,nil)
- | e :: rst =>
- let (rst_f',t) := ror_cnf rst f' in
- let (e_f', t') := ror_clause_cnf e f' in
- (rst_f' +++ e_f', t +++ t')
+ | TT b => mkTT b
+ | FF b => mkFF b
+ | X b p => p
+ | A b x t => mkA b x t
+ | AND f1 f2 => mkAND (aformula f1) (aformula f2)
+ | OR f1 f2 => mkOR (aformula f1) (aformula f2)
+ | IMPL f1 o f2 => mkIMPL (aformula f1) (aformula f2)
+ | IFF f1 f2 => mkIFF (aformula f1) (aformula f2)
+ | NOT f => mkNOT (aformula f)
+ | EQ f1 f2 => mkEQ (aformula f1) (aformula f2)
end.
- Definition annot_of_clause (l : clause) : list Annot :=
- List.map snd l.
-
- Definition annot_of_cnf (f : cnf) : list Annot :=
- List.fold_left (fun acc e => annot_of_clause e +++ acc ) f nil.
+ Definition is_X (k: kind) (f : TFormula TX AF k) : option (TX k) :=
+ match f with
+ | X _ p => Some p
+ | _ => None
+ end.
- Definition ror_cnf_opt f1 f2 :=
- if is_cnf_tt f1
- then (cnf_tt , nil)
- else if is_cnf_tt f2
- then (cnf_tt, nil)
- else if is_cnf_ff f2
- then (f1,nil)
- else ror_cnf f1 f2.
+ Definition is_X_inv : forall (k: kind) (f: TFormula TX AF k) x,
+ is_X f = Some x -> f = X k x.
+ Proof.
+ destruct f ; simpl ; try congruence.
+ Qed.
+ Variable needA : Annot -> bool.
- Definition ocons {A : Type} (o : option A) (l : list A) : list A :=
- match o with
- | None => l
- | Some e => e ::l
+ Definition abs_and (k: kind) (f1 f2 : TFormula TX AF k)
+ (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k -> TFormula TX AF k) :=
+ match is_X f1 , is_X f2 with
+ | Some _ , _ | _ , Some _ => X k (aformula (c k f1 f2))
+ | _ , _ => c k f1 f2
end.
- Definition ratom (c : cnf) (a : Annot) : cnf * list Annot :=
- if is_cnf_ff c || is_cnf_tt c
- then (c,a::nil)
- else (c,nil). (* t is embedded in c *)
-
- Fixpoint rxcnf {TX AF: Type}(polarity : bool) (f : TFormula TX AF) : cnf * list Annot :=
- match f with
- | TT => if polarity then (cnf_tt,nil) else (cnf_ff,nil)
- | FF => if polarity then (cnf_ff,nil) else (cnf_tt,nil)
- | X p => if polarity then (cnf_ff,nil) else (cnf_ff,nil)
- | A x t => ratom (if polarity then normalise x t else negate x t) t
- | N e => rxcnf (negb polarity) e
- | Cj e1 e2 =>
- let '(e1,t1) := rxcnf polarity e1 in
- let '(e2,t2) := rxcnf polarity e2 in
- if polarity
- then (and_cnf_opt e1 e2, t1 +++ t2)
- else let (f',t') := ror_cnf_opt e1 e2 in
- (f', t1 +++ t2 +++ t')
- | D e1 e2 =>
- let '(e1,t1) := rxcnf polarity e1 in
- let '(e2,t2) := rxcnf polarity e2 in
- if polarity
- then let (f',t') := ror_cnf_opt e1 e2 in
- (f', t1 +++ t2 +++ t')
- else (and_cnf_opt e1 e2, t1 +++ t2)
- | I e1 a e2 =>
- let '(e1 , t1) := (rxcnf (negb polarity) e1) in
- if polarity
- then
- if is_cnf_ff e1
- then
- rxcnf polarity e2
- else (* compute disjunction *)
- let '(e2 , t2) := (rxcnf polarity e2) in
- let (f',t') := ror_cnf_opt e1 e2 in
- (f', t1 +++ t2 +++ t') (* record the hypothesis *)
- else
- let '(e2 , t2) := (rxcnf polarity e2) in
- (and_cnf_opt e1 e2, t1 +++ t2)
+ Definition abs_or (k: kind) (f1 f2 : TFormula TX AF k)
+ (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k -> TFormula TX AF k) :=
+ match is_X f1 , is_X f2 with
+ | Some _ , Some _ => X k (aformula (c k f1 f2))
+ | _ , _ => c k f1 f2
end.
+ Definition abs_not (k: kind) (f1 : TFormula TX AF k)
+ (c : forall (k: kind), TFormula TX AF k -> TFormula TX AF k) :=
+ match is_X f1 with
+ | Some _ => X k (aformula (c k f1 ))
+ | _ => c k f1
+ end.
- Section Abstraction.
- Variable TX : Type.
- Variable AF : Type.
-
- Class to_constrT : Type :=
- {
- mkTT : TX;
- mkFF : TX;
- mkA : Term -> Annot -> TX;
- mkCj : TX -> TX -> TX;
- mkD : TX -> TX -> TX;
- mkI : TX -> TX -> TX;
- mkN : TX -> TX
- }.
-
- Context {to_constr : to_constrT}.
-
- Fixpoint aformula (f : TFormula TX AF) : TX :=
- match f with
- | TT => mkTT
- | FF => mkFF
- | X p => p
- | A x t => mkA x t
- | Cj f1 f2 => mkCj (aformula f1) (aformula f2)
- | D f1 f2 => mkD (aformula f1) (aformula f2)
- | I f1 o f2 => mkI (aformula f1) (aformula f2)
- | N f => mkN (aformula f)
- end.
+ Definition mk_arrow (o : option AF) (k: kind) (f1 f2: TFormula TX AF k) :=
+ match o with
+ | None => IMPL f1 None f2
+ | Some _ => if is_X f1 then f2 else IMPL f1 o f2
+ end.
- Definition is_X (f : TFormula TX AF) : option TX :=
- match f with
- | X p => Some p
- | _ => None
- end.
+ Fixpoint abst_simpl (k: kind) (f : TFormula TX AF k) : TFormula TX AF k:=
+ match f with
+ | TT k => TT k
+ | FF k => FF k
+ | X k p => X k p
+ | A k x t => if needA t then A k x t else X k (mkA k x t)
+ | AND f1 f2 => AND (abst_simpl f1) (abst_simpl f2)
+ | OR f1 f2 => OR (abst_simpl f1) (abst_simpl f2)
+ | IMPL f1 o f2 => IMPL (abst_simpl f1) o (abst_simpl f2)
+ | NOT f => NOT (abst_simpl f)
+ | IFF f1 f2 => IFF (abst_simpl f1) (abst_simpl f2)
+ | EQ f1 f2 => EQ (abst_simpl f1) (abst_simpl f2)
+ end.
- Definition is_X_inv : forall f x,
- is_X f = Some x -> f = X x.
- Proof.
- destruct f ; simpl ; congruence.
- Qed.
+ Section REC.
+ Variable REC : forall (pol : bool) (k: kind) (f : TFormula TX AF k), TFormula TX AF k.
+ Definition abst_and (pol : bool) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:=
+ (if pol then abs_and else abs_or) k (REC pol f1) (REC pol f2) AND.
- Variable needA : Annot -> bool.
+ Definition abst_or (pol : bool) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:=
+ (if pol then abs_or else abs_and) k (REC pol f1) (REC pol f2) OR.
- Definition abs_and (f1 f2 : TFormula TX AF)
- (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) :=
- match is_X f1 , is_X f2 with
- | Some _ , _ | _ , Some _ => X (aformula (c f1 f2))
- | _ , _ => c f1 f2
- end.
+ Definition abst_impl (pol : bool) (o :option AF) (k: kind) (f1 f2:TFormula TX AF k) : TFormula TX AF k:=
+ (if pol then abs_or else abs_and) k (REC (negb pol) f1) (REC pol f2) (mk_arrow o).
- Definition abs_or (f1 f2 : TFormula TX AF)
- (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) :=
+ Definition or_is_X (k: kind) (f1 f2: TFormula TX AF k) : bool :=
match is_X f1 , is_X f2 with
- | Some _ , Some _ => X (aformula (c f1 f2))
- | _ , _ => c f1 f2
+ | Some _ , _
+ | _ , Some _ => true
+ | _ , _ => false
end.
- Definition mk_arrow (o : option AF) (f1 f2: TFormula TX AF) :=
- match o with
- | None => I f1 None f2
- | Some _ => if is_X f1 then f2 else I f1 o f2
- end.
+ Definition abs_iff (k: kind) (nf1 ff2 f1 tf2 : TFormula TX AF k) (r: kind) (def : TFormula TX AF r) : TFormula TX AF r :=
+ if andb (or_is_X nf1 ff2) (or_is_X f1 tf2)
+ then X r (aformula def)
+ else def.
- Fixpoint abst_form (pol : bool) (f : TFormula TX AF) :=
- match f with
- | TT => if pol then TT else X mkTT
- | FF => if pol then X mkFF else FF
- | X p => X p
- | A x t => if needA t then A x t else X (mkA x t)
- | Cj f1 f2 =>
- let f1 := abst_form pol f1 in
- let f2 := abst_form pol f2 in
- if pol then abs_and f1 f2 Cj
- else abs_or f1 f2 Cj
- | D f1 f2 =>
- let f1 := abst_form pol f1 in
- let f2 := abst_form pol f2 in
- if pol then abs_or f1 f2 D
- else abs_and f1 f2 D
- | I f1 o f2 =>
- let f1 := abst_form (negb pol) f1 in
- let f2 := abst_form pol f2 in
- if pol
- then abs_or f1 f2 (mk_arrow o)
- else abs_and f1 f2 (mk_arrow o)
- | N f => let f := abst_form (negb pol) f in
- match is_X f with
- | Some a => X (mkN a)
- | _ => N f
- end
- end.
+ Definition abst_iff (pol : bool) (k: kind) (f1 f2: TFormula TX AF k) : TFormula TX AF k :=
+ abs_iff (REC (negb pol) f1) (REC false f2) (REC pol f1) (REC true f2) (IFF (abst_simpl f1) (abst_simpl f2)).
+ Definition abst_eq (pol : bool) (f1 f2: TFormula TX AF isBool) : TFormula TX AF isProp :=
+ abs_iff (REC (negb pol) f1) (REC false f2) (REC pol f1) (REC true f2) (EQ (abst_simpl f1) (abst_simpl f2)).
+ End REC.
+ Fixpoint abst_form (pol : bool) (k: kind) (f : TFormula TX AF k) : TFormula TX AF k:=
+ match f with
+ | TT k => if pol then TT k else X k (mkTT k)
+ | FF k => if pol then X k (mkFF k) else FF k
+ | X k p => X k p
+ | A k x t => if needA t then A k x t else X k (mkA k x t)
+ | AND f1 f2 => abst_and abst_form pol f1 f2
+ | OR f1 f2 => abst_or abst_form pol f1 f2
+ | IMPL f1 o f2 => abst_impl abst_form pol o f1 f2
+ | NOT f => abs_not (abst_form (negb pol) f) NOT
+ | IFF f1 f2 => abst_iff abst_form pol f1 f2
+ | EQ f1 f2 => abst_eq abst_form pol f1 f2
+ end.
- Lemma if_same : forall {A: Type} (b:bool) (t:A),
- (if b then t else t) = t.
- Proof.
- destruct b ; reflexivity.
- Qed.
+ Lemma if_same : forall {A: Type} (b: bool) (t:A),
+ (if b then t else t) = t.
+ Proof.
+ destruct b ; reflexivity.
+ Qed.
- Lemma is_cnf_tt_cnf_ff :
- is_cnf_tt cnf_ff = false.
- Proof.
- reflexivity.
- Qed.
+ Lemma is_cnf_tt_cnf_ff :
+ is_cnf_tt cnf_ff = false.
+ Proof.
+ reflexivity.
+ Qed.
- Lemma is_cnf_ff_cnf_ff :
- is_cnf_ff cnf_ff = true.
- Proof.
- reflexivity.
- Qed.
+ Lemma is_cnf_ff_cnf_ff :
+ is_cnf_ff cnf_ff = true.
+ Proof.
+ reflexivity.
+ Qed.
Lemma is_cnf_tt_inv : forall f1,
@@ -587,9 +844,9 @@ Section S.
reflexivity.
Qed.
- Lemma abs_and_pol : forall f1 f2 pol,
+ Lemma abs_and_pol : forall (k: kind) (f1 f2: TFormula TX AF k) pol,
and_cnf_opt (xcnf pol f1) (xcnf pol f2) =
- xcnf pol (abs_and f1 f2 (if pol then Cj else D)).
+ xcnf pol (abs_and f1 f2 (if pol then AND else OR)).
Proof.
unfold abs_and; intros.
destruct (is_X f1) eqn:EQ1.
@@ -607,9 +864,9 @@ Section S.
destruct pol ; simpl; auto.
Qed.
- Lemma abs_or_pol : forall f1 f2 pol,
+ Lemma abs_or_pol : forall (k: kind) (f1 f2:TFormula TX AF k) pol,
or_cnf_opt (xcnf pol f1) (xcnf pol f2) =
- xcnf pol (abs_or f1 f2 (if pol then D else Cj)).
+ xcnf pol (abs_or f1 f2 (if pol then OR else AND)).
Proof.
unfold abs_or; intros.
destruct (is_X f1) eqn:EQ1.
@@ -629,8 +886,8 @@ Section S.
Variable needA_all : forall a, needA a = true.
- Lemma xcnf_true_mk_arrow_l : forall o t f,
- xcnf true (mk_arrow o (X t) f) = xcnf true f.
+ Lemma xcnf_true_mk_arrow_l : forall b o t (f:TFormula TX AF b),
+ xcnf true (mk_arrow o (X b t) f) = xcnf true f.
Proof.
destruct o ; simpl; auto.
intros. rewrite or_cnf_opt_cnf_ff. reflexivity.
@@ -647,8 +904,8 @@ Section S.
apply if_cnf_tt.
Qed.
- Lemma xcnf_true_mk_arrow_r : forall o t f,
- xcnf true (mk_arrow o f (X t)) = xcnf false f.
+ Lemma xcnf_true_mk_arrow_r : forall b o t (f:TFormula TX AF b),
+ xcnf true (mk_arrow o f (X b t)) = xcnf false f.
Proof.
destruct o ; simpl; auto.
- intros.
@@ -660,9 +917,167 @@ Section S.
apply or_cnf_opt_cnf_ff_r.
Qed.
+ Lemma and_cnf_opt_cnf_ff_r : forall f,
+ and_cnf_opt f cnf_ff = cnf_ff.
+ Proof.
+ intros.
+ unfold and_cnf_opt.
+ rewrite is_cnf_ff_cnf_ff.
+ rewrite orb_comm. reflexivity.
+ Qed.
+
+ Lemma and_cnf_opt_cnf_ff : forall f,
+ and_cnf_opt cnf_ff f = cnf_ff.
+ Proof.
+ intros.
+ unfold and_cnf_opt.
+ rewrite is_cnf_ff_cnf_ff.
+ reflexivity.
+ Qed.
+
+
+ Lemma and_cnf_opt_cnf_tt : forall f,
+ and_cnf_opt f cnf_tt = f.
+ Proof.
+ intros.
+ unfold and_cnf_opt.
+ simpl. rewrite orb_comm.
+ simpl.
+ destruct (is_cnf_ff f) eqn:EQ ; auto.
+ apply is_cnf_ff_inv in EQ.
+ auto.
+ Qed.
+
+ Lemma is_bool_abst_simpl : forall b (f:TFormula TX AF b),
+ is_bool (abst_simpl f) = is_bool f.
+ Proof.
+ induction f ; simpl ; auto.
+ rewrite needA_all.
+ reflexivity.
+ Qed.
+
+ Lemma abst_simpl_correct : forall b (f:TFormula TX AF b) pol,
+ xcnf pol f = xcnf pol (abst_simpl f).
+ Proof.
+ induction f; simpl;intros;
+ unfold mk_and,mk_or,mk_impl, mk_iff;
+ rewrite <- ?IHf;
+ try (rewrite <- !IHf1; rewrite <- !IHf2);
+ try reflexivity.
+ - rewrite needA_all.
+ reflexivity.
+ - rewrite is_bool_abst_simpl.
+ destruct (is_bool f2); auto.
+ - rewrite is_bool_abst_simpl.
+ destruct (is_bool f2); auto.
+ Qed.
+
+ Ltac is_X :=
+ match goal with
+ | |-context[is_X ?X] =>
+ let f := fresh "EQ" in
+ destruct (is_X X) eqn:f ;
+ [apply is_X_inv in f|]
+ end.
+
+ Ltac cnf_simpl :=
+ repeat match goal with
+ | |- context[and_cnf_opt cnf_ff _ ] => rewrite and_cnf_opt_cnf_ff
+ | |- context[and_cnf_opt _ cnf_ff] => rewrite and_cnf_opt_cnf_ff_r
+ | |- context[and_cnf_opt _ cnf_tt] => rewrite and_cnf_opt_cnf_tt
+ | |- context[or_cnf_opt cnf_ff _] => rewrite or_cnf_opt_cnf_ff
+ | |- context[or_cnf_opt _ cnf_ff] => rewrite or_cnf_opt_cnf_ff_r
+ end.
+
+ Lemma or_is_X_inv : forall (k: kind) (f1 f2 : TFormula TX AF k),
+ or_is_X f1 f2 = true ->
+ exists k1, is_X f1 = Some k1 \/ is_X f2 = Some k1.
+ Proof.
+ unfold or_is_X.
+ intros k f1 f2.
+ repeat is_X.
+ exists t ; intuition.
+ exists t ; intuition.
+ exists t ; intuition.
+ congruence.
+ Qed.
+
+ Lemma mk_iff_is_bool : forall (k: kind) (f1 f2:TFormula TX AF k) pol,
+ match is_bool f2 with
+ | Some isb => xcnf (if isb then pol else negb pol) f1
+ | None => mk_iff xcnf pol f1 f2
+ end = mk_iff xcnf pol f1 f2.
+ Proof.
+ intros.
+ destruct (is_bool f2) eqn:EQ; auto.
+ apply is_bool_inv in EQ.
+ subst.
+ unfold mk_iff.
+ destruct b ; simpl; cnf_simpl; reflexivity.
+ Qed.
+
+ Lemma abst_iff_correct : forall
+ (k: kind)
+ (f1 f2 : GFormula k)
+ (IHf1 : forall pol : bool, xcnf pol f1 = xcnf pol (abst_form pol f1))
+ (IHf2 : forall pol : bool, xcnf pol f2 = xcnf pol (abst_form pol f2))
+ (pol : bool),
+ xcnf pol (IFF f1 f2) = xcnf pol (abst_iff abst_form pol f1 f2).
+ Proof.
+ intros; simpl.
+ assert (D1 :mk_iff xcnf pol f1 f2 = mk_iff xcnf pol (abst_simpl f1) (abst_simpl f2)).
+ {
+ simpl.
+ unfold mk_iff.
+ rewrite <- !abst_simpl_correct.
+ reflexivity.
+ }
+ rewrite mk_iff_is_bool.
+ unfold abst_iff,abs_iff.
+ destruct ( or_is_X (abst_form (negb pol) f1) (abst_form false f2) &&
+ or_is_X (abst_form pol f1) (abst_form true f2)
+ ) eqn:EQ1.
+ + simpl.
+ rewrite andb_true_iff in EQ1.
+ destruct EQ1 as (EQ1 & EQ2).
+ apply or_is_X_inv in EQ1.
+ apply or_is_X_inv in EQ2.
+ destruct EQ1 as (b1 & EQ1).
+ destruct EQ2 as (b2 & EQ2).
+ rewrite if_same.
+ unfold mk_iff.
+ rewrite !IHf1.
+ rewrite !IHf2.
+ destruct EQ1 as [EQ1 | EQ1] ; apply is_X_inv in EQ1;
+ destruct EQ2 as [EQ2 | EQ2] ; apply is_X_inv in EQ2;
+ rewrite EQ1; rewrite EQ2; simpl;
+ repeat rewrite if_same ; cnf_simpl; auto.
+ + simpl.
+ rewrite mk_iff_is_bool.
+ unfold mk_iff.
+ rewrite <- ! abst_simpl_correct.
+ reflexivity.
+ Qed.
+
+ Lemma abst_eq_correct : forall
+ (f1 f2 : GFormula isBool)
+ (IHf1 : forall pol : bool, xcnf pol f1 = xcnf pol (abst_form pol f1))
+ (IHf2 : forall pol : bool, xcnf pol f2 = xcnf pol (abst_form pol f2))
+ (pol : bool),
+ xcnf pol (EQ f1 f2) = xcnf pol (abst_form pol (EQ f1 f2)).
+ Proof.
+ intros.
+ change (xcnf pol (IFF f1 f2) = xcnf pol (abst_form pol (EQ f1 f2))).
+ rewrite abst_iff_correct by assumption.
+ simpl. unfold abst_iff, abst_eq.
+ unfold abs_iff.
+ destruct (or_is_X (abst_form (negb pol) f1) (abst_form false f2) &&
+ or_is_X (abst_form pol f1) (abst_form true f2)
+ ) ; auto.
+ Qed.
- Lemma abst_form_correct : forall f pol,
+ Lemma abst_form_correct : forall b (f:TFormula TX AF b) pol,
xcnf pol f = xcnf pol (abst_form pol f).
Proof.
induction f;intros.
@@ -671,27 +1086,24 @@ Section S.
- simpl. reflexivity.
- simpl. rewrite needA_all.
reflexivity.
- - simpl.
+ - simpl. unfold mk_and.
specialize (IHf1 pol).
specialize (IHf2 pol).
rewrite IHf1.
rewrite IHf2.
destruct pol.
- +
- apply abs_and_pol; auto.
- +
- apply abs_or_pol; auto.
- - simpl.
+ + apply abs_and_pol; auto.
+ + apply abs_or_pol.
+ - simpl. unfold mk_or.
specialize (IHf1 pol).
specialize (IHf2 pol).
rewrite IHf1.
rewrite IHf2.
destruct pol.
- +
- apply abs_or_pol; auto.
- +
- apply abs_and_pol; auto.
+ + apply abs_or_pol; auto.
+ + apply abs_and_pol; auto.
- simpl.
+ unfold abs_not.
specialize (IHf (negb pol)).
destruct (is_X (abst_form (negb pol) f)) eqn:EQ1.
+ apply is_X_inv in EQ1.
@@ -699,381 +1111,438 @@ Section S.
simpl in *.
destruct pol ; auto.
+ simpl. congruence.
- - simpl.
+ - simpl. unfold mk_impl.
specialize (IHf1 (negb pol)).
specialize (IHf2 pol).
destruct pol.
- +
- simpl in *.
- unfold abs_or.
- destruct (is_X (abst_form false f1)) eqn:EQ1;
- destruct (is_X (abst_form true f2)) eqn:EQ2 ; simpl.
- * apply is_X_inv in EQ1.
- apply is_X_inv in EQ2.
- rewrite EQ1 in *.
- rewrite EQ2 in *.
- rewrite IHf1. rewrite IHf2.
- simpl. reflexivity.
- * apply is_X_inv in EQ1.
- rewrite EQ1 in *.
- rewrite IHf1.
- simpl.
- rewrite xcnf_true_mk_arrow_l.
- rewrite or_cnf_opt_cnf_ff.
- congruence.
- * apply is_X_inv in EQ2.
- rewrite EQ2 in *.
- rewrite IHf2.
- simpl.
- rewrite xcnf_true_mk_arrow_r.
- rewrite or_cnf_opt_cnf_ff_r.
- congruence.
- * destruct o ; simpl ; try congruence.
- rewrite EQ1.
- simpl. congruence.
- + simpl in *.
- unfold abs_and.
- destruct (is_X (abst_form true f1)) eqn:EQ1;
- destruct (is_X (abst_form false f2)) eqn:EQ2 ; simpl.
- * apply is_X_inv in EQ1.
+ +
+ simpl in *.
+ unfold abs_or.
+ destruct (is_X (abst_form false f1)) eqn:EQ1;
+ destruct (is_X (abst_form true f2)) eqn:EQ2 ; simpl.
+ * apply is_X_inv in EQ1.
+ apply is_X_inv in EQ2.
+ rewrite EQ1 in *.
+ rewrite EQ2 in *.
+ rewrite IHf1. rewrite IHf2.
+ simpl. reflexivity.
+ * apply is_X_inv in EQ1.
+ rewrite EQ1 in *.
+ rewrite IHf1.
+ simpl.
+ rewrite xcnf_true_mk_arrow_l.
+ rewrite or_cnf_opt_cnf_ff.
+ congruence.
+ * apply is_X_inv in EQ2.
+ rewrite EQ2 in *.
+ rewrite IHf2.
+ simpl.
+ rewrite xcnf_true_mk_arrow_r.
+ rewrite or_cnf_opt_cnf_ff_r.
+ congruence.
+ * destruct o ; simpl ; try congruence.
+ rewrite EQ1.
+ simpl. congruence.
+ + simpl in *.
+ unfold abs_and.
+ destruct (is_X (abst_form true f1)) eqn:EQ1;
+ destruct (is_X (abst_form false f2)) eqn:EQ2 ; simpl.
+ * apply is_X_inv in EQ1.
apply is_X_inv in EQ2.
rewrite EQ1 in *.
rewrite EQ2 in *.
rewrite IHf1. rewrite IHf2.
simpl. reflexivity.
- * apply is_X_inv in EQ1.
+ * apply is_X_inv in EQ1.
rewrite EQ1 in *.
rewrite IHf1.
simpl. reflexivity.
- * apply is_X_inv in EQ2.
+ * apply is_X_inv in EQ2.
rewrite EQ2 in *.
rewrite IHf2.
simpl. unfold and_cnf_opt.
rewrite orb_comm. reflexivity.
- * destruct o; simpl.
- rewrite EQ1. simpl.
- congruence.
- congruence.
- Qed.
-
- End Abstraction.
-
-
- End CNFAnnot.
-
-
- Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl.
- Proof.
- induction a' ; simpl.
- - intros.
- destruct (deduce (fst a) (fst a)).
- destruct (unsat t). congruence.
- inversion H. reflexivity.
- inversion H ;reflexivity.
- - intros.
- destruct (deduce (fst a0) (fst a)).
- destruct (unsat t). congruence.
- destruct (radd_term a0 a') eqn:RADD; try congruence.
- inversion H. subst.
- apply IHa' in RADD.
- rewrite RADD.
- reflexivity.
- destruct (radd_term a0 a') eqn:RADD; try congruence.
- inversion H. subst.
- apply IHa' in RADD.
- rewrite RADD.
- reflexivity.
- Qed.
-
- Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl.
- Proof.
- induction a' ; simpl.
- - intros.
- destruct (deduce (fst a) (fst a)).
- destruct (unsat t). congruence.
- inversion H. reflexivity.
- inversion H ;reflexivity.
- - intros.
- destruct (deduce (fst a0) (fst a)).
- destruct (unsat t). congruence.
- destruct (add_term a0 a') eqn:RADD; try congruence.
- inversion H. subst.
- apply IHa' in RADD.
- rewrite RADD.
- reflexivity.
- destruct (add_term a0 a') eqn:RADD; try congruence.
- inversion H. subst.
- apply IHa' in RADD.
- rewrite RADD.
- reflexivity.
+ * destruct o; simpl.
+ rewrite EQ1. simpl.
+ congruence.
+ congruence.
+ - apply abst_iff_correct; auto.
+ - apply abst_eq_correct; auto.
Qed.
- Lemma xror_clause_clause : forall a f,
- fst (xror_clause_cnf a f) = xor_clause_cnf a f.
- Proof.
- unfold xror_clause_cnf.
- unfold xor_clause_cnf.
- assert (ACC: fst (@nil clause,@nil Annot) = nil).
- reflexivity.
- intros.
- set (F1:= (fun '(acc, tg) (e : clause) =>
- match ror_clause a e with
- | inl cl => (cl :: acc, tg)
- | inr l => (acc, tg +++ l)
- end)).
- set (F2:= (fun (acc : list clause) (e : clause) =>
- match or_clause a e with
- | Some cl => cl :: acc
- | None => acc
- end)).
- revert ACC.
- generalize (@nil clause,@nil Annot).
- generalize (@nil clause).
- induction f ; simpl ; auto.
- intros.
- apply IHf.
- unfold F1 , F2.
- destruct p ; simpl in * ; subst.
- clear.
- revert a0.
- induction a; simpl; auto.
- intros.
- destruct (radd_term a a1) eqn:RADD.
- apply radd_term_term in RADD.
- rewrite RADD.
- auto.
- destruct (add_term a a1) eqn:RADD'.
- apply radd_term_term' in RADD'.
- congruence.
- reflexivity.
- Qed.
+ End Abstraction.
- Lemma ror_clause_clause : forall a f,
- fst (ror_clause_cnf a f) = or_clause_cnf a f.
- Proof.
- unfold ror_clause_cnf,or_clause_cnf.
- destruct a ; auto.
- apply xror_clause_clause.
- Qed.
- Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2.
- Proof.
- induction f1 ; simpl ; auto.
- intros.
- specialize (IHf1 f2).
- destruct(ror_cnf f1 f2).
- rewrite <- ror_clause_clause.
- destruct(ror_clause_cnf a f2).
- simpl.
- rewrite <- IHf1.
- reflexivity.
- Qed.
+ End CNFAnnot.
- Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2.
- Proof.
- unfold ror_cnf_opt, or_cnf_opt.
- intros.
- destruct (is_cnf_tt f1).
- - simpl ; auto.
- - simpl. destruct (is_cnf_tt f2) ; simpl ; auto.
- destruct (is_cnf_ff f2) eqn:EQ.
- reflexivity.
- apply ror_cnf_cnf.
- Qed.
- Lemma ratom_cnf : forall f a,
- fst (ratom f a) = f.
- Proof.
- unfold ratom.
- intros.
- destruct (is_cnf_ff f || is_cnf_tt f); auto.
- Qed.
-
-
-
- Lemma rxcnf_xcnf : forall {TX AF:Type} (f:TFormula TX AF) b,
- fst (rxcnf b f) = xcnf b f.
- Proof.
- induction f ; simpl ; auto.
- - destruct b; simpl ; auto.
- - destruct b; simpl ; auto.
- - destruct b ; simpl ; auto.
- - intros. rewrite ratom_cnf. reflexivity.
- - intros.
- specialize (IHf1 b).
- specialize (IHf2 b).
- destruct (rxcnf b f1).
- destruct (rxcnf b f2).
- simpl in *.
- subst. destruct b ; auto.
- rewrite <- ror_opt_cnf_cnf.
- destruct (ror_cnf_opt (xcnf false f1) (xcnf false f2)).
- reflexivity.
- - intros.
- specialize (IHf1 b).
- specialize (IHf2 b).
- rewrite <- IHf1.
- rewrite <- IHf2.
- destruct (rxcnf b f1).
- destruct (rxcnf b f2).
- simpl in *.
- subst. destruct b ; auto.
- rewrite <- ror_opt_cnf_cnf.
- destruct (ror_cnf_opt (xcnf true f1) (xcnf true f2)).
- reflexivity.
- - intros.
- specialize (IHf1 (negb b)).
- specialize (IHf2 b).
- rewrite <- IHf1.
- rewrite <- IHf2.
- destruct (rxcnf (negb b) f1).
- destruct (rxcnf b f2).
- simpl in *.
- subst.
- destruct b;auto.
- generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
- destruct (is_cnf_ff (xcnf (negb true) f1)).
- + intros.
- rewrite H by auto.
- unfold or_cnf_opt.
- simpl.
- destruct (is_cnf_tt (xcnf true f2)) eqn:EQ;auto.
- apply is_cnf_tt_inv in EQ; auto.
- destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1.
- apply is_cnf_ff_inv in EQ1. congruence.
- reflexivity.
- +
- rewrite <- ror_opt_cnf_cnf.
- destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)).
- intros.
- reflexivity.
- Qed.
+ Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl.
+ Proof.
+ induction a' ; simpl.
+ - intros.
+ destruct (deduce (fst a) (fst a)).
+ destruct (unsat t). congruence.
+ inversion H. reflexivity.
+ inversion H ;reflexivity.
+ - intros.
+ destruct (deduce (fst a0) (fst a)).
+ destruct (unsat t). congruence.
+ destruct (radd_term a0 a') eqn:RADD; try congruence.
+ inversion H. subst.
+ apply IHa' in RADD.
+ rewrite RADD.
+ reflexivity.
+ destruct (radd_term a0 a') eqn:RADD; try congruence.
+ inversion H. subst.
+ apply IHa' in RADD.
+ rewrite RADD.
+ reflexivity.
+ Qed.
+ Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl.
+ Proof.
+ induction a' ; simpl.
+ - intros.
+ destruct (deduce (fst a) (fst a)).
+ destruct (unsat t). congruence.
+ inversion H. reflexivity.
+ inversion H ;reflexivity.
+ - intros.
+ destruct (deduce (fst a0) (fst a)).
+ destruct (unsat t). congruence.
+ destruct (add_term a0 a') eqn:RADD; try congruence.
+ inversion H. subst.
+ apply IHa' in RADD.
+ rewrite RADD.
+ reflexivity.
+ destruct (add_term a0 a') eqn:RADD; try congruence.
+ inversion H. subst.
+ apply IHa' in RADD.
+ rewrite RADD.
+ reflexivity.
+ Qed.
- Variable eval' : Env -> Term' -> Prop.
+ Lemma xror_clause_clause : forall a f,
+ fst (xror_clause_cnf a f) = xor_clause_cnf a f.
+ Proof.
+ unfold xror_clause_cnf.
+ unfold xor_clause_cnf.
+ assert (ACC: fst (@nil clause,@nil Annot) = nil).
+ reflexivity.
+ intros.
+ set (F1:= (fun '(acc, tg) (e : clause) =>
+ match ror_clause a e with
+ | inl cl => (cl :: acc, tg)
+ | inr l => (acc, tg +++ l)
+ end)).
+ set (F2:= (fun (acc : list clause) (e : clause) =>
+ match or_clause a e with
+ | Some cl => cl :: acc
+ | None => acc
+ end)).
+ revert ACC.
+ generalize (@nil clause,@nil Annot).
+ generalize (@nil clause).
+ induction f ; simpl ; auto.
+ intros.
+ apply IHf.
+ unfold F1 , F2.
+ destruct p ; simpl in * ; subst.
+ clear.
+ revert a0.
+ induction a; simpl; auto.
+ intros.
+ destruct (radd_term a a1) eqn:RADD.
+ apply radd_term_term in RADD.
+ rewrite RADD.
+ auto.
+ destruct (add_term a a1) eqn:RADD'.
+ apply radd_term_term' in RADD'.
+ congruence.
+ reflexivity.
+ Qed.
- Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d).
+ Lemma ror_clause_clause : forall a f,
+ fst (ror_clause_cnf a f) = or_clause_cnf a f.
+ Proof.
+ unfold ror_clause_cnf,or_clause_cnf.
+ destruct a ; auto.
+ apply xror_clause_clause.
+ Qed.
+ Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2.
+ Proof.
+ induction f1 ; simpl ; auto.
+ intros.
+ specialize (IHf1 f2).
+ destruct(ror_cnf f1 f2).
+ rewrite <- ror_clause_clause.
+ destruct(ror_clause_cnf a f2).
+ simpl.
+ rewrite <- IHf1.
+ reflexivity.
+ Qed.
- Variable unsat_prop : forall t, unsat t = true ->
- forall env, eval' env t -> False.
+ Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2.
+ Proof.
+ unfold ror_cnf_opt, or_cnf_opt.
+ intros.
+ destruct (is_cnf_tt f1).
+ - simpl ; auto.
+ - simpl. destruct (is_cnf_tt f2) ; simpl ; auto.
+ destruct (is_cnf_ff f2) eqn:EQ.
+ reflexivity.
+ apply ror_cnf_cnf.
+ Qed.
+ Lemma ratom_cnf : forall f a,
+ fst (ratom f a) = f.
+ Proof.
+ unfold ratom.
+ intros.
+ destruct (is_cnf_ff f || is_cnf_tt f); auto.
+ Qed.
+ Lemma rxcnf_and_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
+ (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
+ (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2),
+ forall pol : bool, fst (rxcnf_and rxcnf pol f1 f2) = mk_and xcnf pol f1 f2.
+ Proof.
+ intros.
+ unfold mk_and, rxcnf_and.
+ specialize (IHf1 pol).
+ specialize (IHf2 pol).
+ destruct (rxcnf pol f1).
+ destruct (rxcnf pol f2).
+ simpl in *.
+ subst. destruct pol ; auto.
+ rewrite <- ror_opt_cnf_cnf.
+ destruct (ror_cnf_opt (xcnf false f1) (xcnf false f2)).
+ reflexivity.
+ Qed.
- Variable deduce_prop : forall t t' u,
- deduce t t' = Some u -> forall env,
- eval' env t -> eval' env t' -> eval' env u.
+ Lemma rxcnf_or_xcnf :
+ forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
+ (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
+ (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2),
+ forall pol : bool, fst (rxcnf_or rxcnf pol f1 f2) = mk_or xcnf pol f1 f2.
+ Proof.
+ intros.
+ unfold rxcnf_or, mk_or.
+ specialize (IHf1 pol).
+ specialize (IHf2 pol).
+ destruct (rxcnf pol f1).
+ destruct (rxcnf pol f2).
+ simpl in *.
+ subst. destruct pol ; auto.
+ rewrite <- ror_opt_cnf_cnf.
+ destruct (ror_cnf_opt (xcnf true f1) (xcnf true f2)).
+ reflexivity.
+ Qed.
+ Lemma rxcnf_impl_xcnf :
+ forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
+ (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
+ (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2),
+ forall pol : bool, fst (rxcnf_impl rxcnf pol f1 f2) = mk_impl xcnf pol f1 f2.
+ Proof.
+ intros.
+ unfold rxcnf_impl, mk_impl, mk_or.
+ specialize (IHf1 (negb pol)).
+ specialize (IHf2 pol).
+ rewrite <- IHf1.
+ rewrite <- IHf2.
+ destruct (rxcnf (negb pol) f1).
+ destruct (rxcnf pol f2).
+ simpl in *.
+ subst.
+ destruct pol;auto.
+ generalize (is_cnf_ff_inv (xcnf (negb true) f1)).
+ destruct (is_cnf_ff (xcnf (negb true) f1)).
+ + intros.
+ rewrite H by auto.
+ unfold or_cnf_opt.
+ simpl.
+ destruct (is_cnf_tt (xcnf true f2)) eqn:EQ;auto.
+ apply is_cnf_tt_inv in EQ; auto.
+ destruct (is_cnf_ff (xcnf true f2)) eqn:EQ1.
+ apply is_cnf_ff_inv in EQ1. congruence.
+ reflexivity.
+ +
+ rewrite <- ror_opt_cnf_cnf.
+ destruct (ror_cnf_opt (xcnf (negb true) f1) (xcnf true f2)).
+ intros.
+ reflexivity.
+ Qed.
- Definition eval_tt (env : Env) (tt : Term' * Annot) := eval' env (fst tt).
- Definition eval_clause (env : Env) (cl : clause) := ~ make_conj (eval_tt env) cl.
+ Lemma rxcnf_iff_xcnf :
+ forall {TX : kind -> Type} {AF:Type} (k: kind) (f1 f2:TFormula TX AF k)
+ (IHf1 : forall pol : bool, fst (rxcnf pol f1) = xcnf pol f1)
+ (IHf2 : forall pol : bool, fst (rxcnf pol f2) = xcnf pol f2),
+ forall pol : bool, fst (rxcnf_iff rxcnf pol f1 f2) = mk_iff xcnf pol f1 f2.
+ Proof.
+ intros.
+ unfold rxcnf_iff.
+ unfold mk_iff.
+ rewrite <- (IHf1 (negb pol)).
+ rewrite <- (IHf1 pol).
+ rewrite <- (IHf2 false).
+ rewrite <- (IHf2 true).
+ destruct (rxcnf (negb pol) f1).
+ destruct (rxcnf false f2).
+ destruct (rxcnf pol f1).
+ destruct (rxcnf true f2).
+ destruct (ror_cnf_opt (and_cnf_opt c c0) (and_cnf_opt c1 c2)) eqn:EQ.
+ simpl.
+ change c3 with (fst (c3,l3)).
+ rewrite <- EQ. rewrite ror_opt_cnf_cnf.
+ reflexivity.
+ Qed.
- Definition eval_cnf (env : Env) (f:cnf) := make_conj (eval_clause env) f.
+ Lemma rxcnf_xcnf : forall {TX : kind -> Type} {AF:Type} (k: kind) (f:TFormula TX AF k) pol,
+ fst (rxcnf pol f) = xcnf pol f.
+ Proof.
+ induction f ; simpl ; auto.
+ - destruct pol; simpl ; auto.
+ - destruct pol; simpl ; auto.
+ - destruct pol ; simpl ; auto.
+ - intros. rewrite ratom_cnf. reflexivity.
+ - apply rxcnf_and_xcnf; auto.
+ - apply rxcnf_or_xcnf; auto.
+ - apply rxcnf_impl_xcnf; auto.
+ - intros.
+ rewrite mk_iff_is_bool.
+ apply rxcnf_iff_xcnf; auto.
+ - intros.
+ rewrite mk_iff_is_bool.
+ apply rxcnf_iff_xcnf; auto.
+ Qed.
- Lemma eval_cnf_app : forall env x y, eval_cnf env (x+++y) <-> eval_cnf env x /\ eval_cnf env y.
- Proof.
- unfold eval_cnf.
- intros.
- rewrite make_conj_rapp.
- rewrite make_conj_app ; auto.
- tauto.
- Qed.
+ Variable eval' : Env -> Term' -> Prop.
+ Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d).
- Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False.
- Proof.
- unfold cnf_ff, eval_cnf,eval_clause.
- simpl. tauto.
- Qed.
+ Variable unsat_prop : forall t, unsat t = true ->
+ forall env, eval' env t -> False.
- Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True.
- Proof.
- unfold cnf_tt, eval_cnf,eval_clause.
- simpl. tauto.
- Qed.
+ Variable deduce_prop : forall t t' u,
+ deduce t t' = Some u -> forall env,
+ eval' env t -> eval' env t' -> eval' env u.
+ Definition eval_tt (env : Env) (tt : Term' * Annot) := eval' env (fst tt).
- Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y).
- Proof.
- unfold and_cnf_opt.
- intros.
- destruct (is_cnf_ff x) eqn:F1.
- { apply is_cnf_ff_inv in F1.
- simpl. subst.
- unfold and_cnf.
- rewrite eval_cnf_app.
- rewrite eval_cnf_ff.
- tauto.
- }
- simpl.
- destruct (is_cnf_ff y) eqn:F2.
- { apply is_cnf_ff_inv in F2.
- simpl. subst.
- unfold and_cnf.
- rewrite eval_cnf_app.
- rewrite eval_cnf_ff.
- tauto.
- }
- tauto.
- Qed.
+ Definition eval_clause (env : Env) (cl : clause) := ~ make_conj (eval_tt env) cl.
+ Definition eval_cnf (env : Env) (f:cnf) := make_conj (eval_clause env) f.
+ Lemma eval_cnf_app : forall env x y, eval_cnf env (x+++y) <-> eval_cnf env x /\ eval_cnf env y.
+ Proof.
+ unfold eval_cnf.
+ intros.
+ rewrite make_conj_rapp.
+ rewrite make_conj_app ; auto.
+ tauto.
+ Qed.
- Definition eval_opt_clause (env : Env) (cl: option clause) :=
- match cl with
- | None => True
- | Some cl => eval_clause env cl
- end.
+ Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False.
+ Proof.
+ unfold cnf_ff, eval_cnf,eval_clause.
+ simpl. tauto.
+ Qed.
+ Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True.
+ Proof.
+ unfold cnf_tt, eval_cnf,eval_clause.
+ simpl. tauto.
+ Qed.
- Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl).
+ Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y).
Proof.
- induction cl.
- - (* BC *)
- simpl.
- case_eq (deduce (fst t) (fst t)) ; try tauto.
+ unfold and_cnf_opt.
intros.
- generalize (@deduce_prop _ _ _ H env).
- case_eq (unsat t0) ; try tauto.
- { intros.
- generalize (@unsat_prop _ H0 env).
- unfold eval_clause.
- rewrite make_conj_cons.
- simpl; intros.
+ destruct (is_cnf_ff x) eqn:F1.
+ { apply is_cnf_ff_inv in F1.
+ simpl. subst.
+ unfold and_cnf.
+ rewrite eval_cnf_app.
+ rewrite eval_cnf_ff.
tauto.
}
- - (* IC *)
simpl.
- case_eq (deduce (fst t) (fst a));
- intros.
- generalize (@deduce_prop _ _ _ H env).
- case_eq (unsat t0); intros.
- {
- generalize (@unsat_prop _ H0 env).
- simpl.
- unfold eval_clause.
- repeat rewrite make_conj_cons.
- tauto.
- }
- destruct (add_term t cl) ; simpl in * ; try tauto.
- {
- intros.
- unfold eval_clause in *.
- repeat rewrite make_conj_cons in *.
+ destruct (is_cnf_ff y) eqn:F2.
+ { apply is_cnf_ff_inv in F2.
+ simpl. subst.
+ unfold and_cnf.
+ rewrite eval_cnf_app.
+ rewrite eval_cnf_ff.
tauto.
}
+ destruct (is_cnf_tt y) eqn:F3.
{
- unfold eval_clause in *.
- repeat rewrite make_conj_cons in *.
+ apply is_cnf_tt_inv in F3.
+ subst.
+ unfold and_cnf.
+ rewrite eval_cnf_app.
+ rewrite eval_cnf_tt.
tauto.
}
- destruct (add_term t cl) ; simpl in *;
- unfold eval_clause in * ;
- repeat rewrite make_conj_cons in *; tauto.
+ tauto.
+ Qed.
+
+ Definition eval_opt_clause (env : Env) (cl: option clause) :=
+ match cl with
+ | None => True
+ | Some cl => eval_clause env cl
+ end.
+
+ Lemma add_term_correct : forall env t cl , eval_opt_clause env (add_term t cl) <-> eval_clause env (t::cl).
+ Proof.
+ induction cl.
+ - (* BC *)
+ simpl.
+ case_eq (deduce (fst t) (fst t)) ; try tauto.
+ intros.
+ generalize (@deduce_prop _ _ _ H env).
+ case_eq (unsat t0) ; try tauto.
+ { intros.
+ generalize (@unsat_prop _ H0 env).
+ unfold eval_clause.
+ rewrite make_conj_cons.
+ simpl; intros.
+ tauto.
+ }
+ - (* IC *)
+ simpl.
+ case_eq (deduce (fst t) (fst a));
+ intros.
+ generalize (@deduce_prop _ _ _ H env).
+ case_eq (unsat t0); intros.
+ {
+ generalize (@unsat_prop _ H0 env).
+ simpl.
+ unfold eval_clause.
+ repeat rewrite make_conj_cons.
+ tauto.
+ }
+ destruct (add_term t cl) ; simpl in * ; try tauto.
+ {
+ intros.
+ unfold eval_clause in *.
+ repeat rewrite make_conj_cons in *.
+ tauto.
+ }
+ {
+ unfold eval_clause in *.
+ repeat rewrite make_conj_cons in *.
+ tauto.
+ }
+ destruct (add_term t cl) ; simpl in *;
+ unfold eval_clause in * ;
+ repeat rewrite make_conj_cons in *; tauto.
Qed.
@@ -1096,10 +1565,10 @@ Section S.
assert (eval_tt env a \/ ~ eval_tt env a) by (apply no_middle_eval').
destruct (add_term a cl'); simpl in *.
+
- rewrite IHcl.
- unfold eval_clause in *.
- rewrite !make_conj_cons in *.
- tauto.
+ rewrite IHcl.
+ unfold eval_clause in *.
+ rewrite !make_conj_cons in *.
+ tauto.
+ unfold eval_clause in *.
repeat rewrite make_conj_cons in *.
tauto.
@@ -1131,8 +1600,8 @@ Section S.
generalize (or_clause_correct t a env).
destruct (or_clause t a).
+
- rewrite make_conj_cons.
- simpl. tauto.
+ rewrite make_conj_cons.
+ simpl. tauto.
+ simpl. tauto.
}
destruct t ; auto.
@@ -1211,113 +1680,108 @@ Section S.
}
Qed.
+ Variable eval : Env -> forall (k: kind), Term -> rtyp k.
- Variable eval : Env -> Term -> Prop.
+ Variable normalise_correct : forall env b t tg, eval_cnf env (normalise t tg) -> hold b (eval env b t).
- Variable normalise_correct : forall env t tg, eval_cnf env (normalise t tg) -> eval env t.
+ Variable negate_correct : forall env b t tg, eval_cnf env (negate t tg) -> hold b (eNOT b (eval env b t)).
- Variable negate_correct : forall env t tg, eval_cnf env (negate t tg) -> ~ eval env t.
+ Definition e_rtyp (k: kind) (x : rtyp k) : rtyp k := x.
- Lemma xcnf_correct : forall (f : @GFormula Term Prop Annot unit) pol env, eval_cnf env (xcnf pol f) -> eval_f (fun x => x) (eval env) (if pol then f else N f).
+ Lemma hold_eTT : forall k, hold k (eTT k).
Proof.
- induction f.
- - (* TT *)
- unfold eval_cnf.
- simpl.
- destruct pol ; simpl ; auto.
- - (* FF *)
- unfold eval_cnf.
- destruct pol; simpl ; auto.
- unfold eval_clause ; simpl.
- tauto.
- - (* P *)
- simpl.
- destruct pol ; intros ;simpl.
- unfold eval_cnf in H.
- (* Here I have to drop the proposition *)
- simpl in H.
- unfold eval_clause in H ; simpl in H.
- tauto.
- (* Here, I could store P in the clause *)
- unfold eval_cnf in H;simpl in H.
- unfold eval_clause in H ; simpl in H.
- tauto.
- - (* A *)
- simpl.
- destruct pol ; simpl.
- intros.
- eapply normalise_correct ; eauto.
- (* A 2 *)
- intros.
- eapply negate_correct ; eauto.
- - (* Cj *)
- destruct pol ; simpl.
- + (* pol = true *)
- intros.
- rewrite eval_cnf_and_opt in H.
- unfold and_cnf in H.
- rewrite eval_cnf_app in H.
- destruct H.
- split.
- apply (IHf1 _ _ H).
- apply (IHf2 _ _ H0).
- + (* pol = false *)
- intros.
- rewrite or_cnf_opt_correct in H.
- rewrite or_cnf_correct in H.
- destruct H as [H | H].
- generalize (IHf1 false env H).
- simpl.
- tauto.
- generalize (IHf2 false env H).
- simpl.
- tauto.
- - (* D *)
- simpl.
- destruct pol.
- + (* pol = true *)
- intros.
- rewrite or_cnf_opt_correct in H.
- rewrite or_cnf_correct in H.
- destruct H as [H | H].
- generalize (IHf1 _ env H).
- simpl.
- tauto.
- generalize (IHf2 _ env H).
- simpl.
- tauto.
- + (* pol = true *)
- intros.
- rewrite eval_cnf_and_opt in H.
- unfold and_cnf.
- rewrite eval_cnf_app in H.
- destruct H as [H0 H1].
- simpl.
- generalize (IHf1 _ _ H0).
- generalize (IHf2 _ _ H1).
- simpl.
- tauto.
- - (**)
- simpl.
- destruct pol ; simpl.
- intros.
- apply (IHf false) ; auto.
- intros.
- generalize (IHf _ _ H).
- tauto.
- - (* I *)
- simpl; intros.
+ destruct k ; simpl; auto.
+ Qed.
+
+ Hint Resolve hold_eTT : tauto.
+
+ Lemma hold_eFF : forall k,
+ hold k (eNOT k (eFF k)).
+ Proof.
+ destruct k ; simpl;auto.
+ Qed.
+
+ Hint Resolve hold_eFF : tauto.
+
+ Lemma hold_eAND : forall k r1 r2,
+ hold k (eAND k r1 r2) <-> (hold k r1 /\ hold k r2).
+ Proof.
+ destruct k ; simpl.
+ - intros. apply iff_refl.
+ - apply andb_true_iff.
+ Qed.
+
+ Lemma hold_eOR : forall k r1 r2,
+ hold k (eOR k r1 r2) <-> (hold k r1 \/ hold k r2).
+ Proof.
+ destruct k ; simpl.
+ - intros. apply iff_refl.
+ - apply orb_true_iff.
+ Qed.
+
+ Lemma hold_eNOT : forall k e,
+ hold k (eNOT k e) <-> not (hold k e).
+ Proof.
+ destruct k ; simpl.
+ - intros. apply iff_refl.
+ - intros. unfold is_true.
+ rewrite negb_true_iff.
+ destruct e ; intuition congruence.
+ Qed.
+
+ Lemma hold_eIMPL : forall k e1 e2,
+ hold k (eIMPL k e1 e2) <-> (hold k e1 -> hold k e2).
+ Proof.
+ destruct k ; simpl.
+ - intros. apply iff_refl.
+ - intros.
+ unfold is_true.
+ destruct e1,e2 ; simpl ; intuition congruence.
+ Qed.
+
+ Lemma hold_eIFF : forall k e1 e2,
+ hold k (eIFF k e1 e2) <-> (hold k e1 <-> hold k e2).
+ Proof.
+ destruct k ; simpl.
+ - intros. apply iff_refl.
+ - intros.
+ unfold is_true.
+ rewrite eqb_true_iff.
+ destruct e1,e2 ; simpl ; intuition congruence.
+ Qed.
+
+
+
+ Lemma xcnf_impl :
+ forall
+ (k: kind)
+ (f1 : GFormula k)
+ (o : option unit)
+ (f2 : GFormula k)
+ (IHf1 : forall (pol : bool) (env : Env),
+ eval_cnf env (xcnf pol f1) ->
+ hold k (eval_f e_rtyp (eval env) (if pol then f1 else NOT f1)))
+ (IHf2 : forall (pol : bool) (env : Env),
+ eval_cnf env (xcnf pol f2) ->
+ hold k (eval_f e_rtyp (eval env) (if pol then f2 else NOT f2))),
+ forall (pol : bool) (env : Env),
+ eval_cnf env (xcnf pol (IMPL f1 o f2)) ->
+ hold k (eval_f e_rtyp (eval env) (if pol then IMPL f1 o f2 else NOT (IMPL f1 o f2))).
+ Proof.
+ simpl; intros. unfold mk_impl in H.
destruct pol.
+ simpl.
- intro.
- rewrite or_cnf_opt_correct in H.
- rewrite or_cnf_correct in H.
- destruct H as [H | H].
- generalize (IHf1 _ _ H).
- simpl in *.
- tauto.
- generalize (IHf2 _ _ H).
- auto.
+ rewrite hold_eIMPL.
+ intro.
+ rewrite or_cnf_opt_correct in H.
+ rewrite or_cnf_correct in H.
+ destruct H as [H | H].
+ generalize (IHf1 _ _ H).
+ simpl in *.
+ rewrite hold_eNOT.
+ tauto.
+ generalize (IHf2 _ _ H).
+ auto.
+ (* pol = false *)
rewrite eval_cnf_and_opt in H.
unfold and_cnf in H.
@@ -1327,9 +1791,190 @@ Section S.
generalize (IHf1 _ _ H0).
generalize (IHf2 _ _ H1).
simpl.
+ rewrite ! hold_eNOT.
+ rewrite ! hold_eIMPL.
tauto.
Qed.
+ Lemma hold_eIFF_IMPL : forall k e1 e2,
+ hold k (eIFF k e1 e2) <-> (hold k (eAND k (eIMPL k e1 e2) (eIMPL k e2 e1))).
+ Proof.
+ intros.
+ rewrite hold_eIFF.
+ rewrite hold_eAND.
+ rewrite! hold_eIMPL.
+ tauto.
+ Qed.
+
+ Lemma hold_eEQ : forall e1 e2,
+ hold isBool (eIFF isBool e1 e2) <-> e1 = e2.
+ Proof.
+ simpl.
+ destruct e1,e2 ; simpl ; intuition congruence.
+ Qed.
+
+
+ Lemma xcnf_iff : forall
+ (k : kind)
+ (f1 f2 : @GFormula Term rtyp Annot unit k)
+ (IHf1 : forall (pol : bool) (env : Env),
+ eval_cnf env (xcnf pol f1) ->
+ hold k (eval_f e_rtyp (eval env) (if pol then f1 else NOT f1)))
+ (IHf2 : forall (pol : bool) (env : Env),
+ eval_cnf env (xcnf pol f2) ->
+ hold k (eval_f e_rtyp (eval env) (if pol then f2 else NOT f2))),
+ forall (pol : bool) (env : Env),
+ eval_cnf env (xcnf pol (IFF f1 f2)) ->
+ hold k (eval_f e_rtyp (eval env) (if pol then IFF f1 f2 else NOT (IFF f1 f2))).
+ Proof.
+ simpl.
+ intros.
+ rewrite mk_iff_is_bool in H.
+ unfold mk_iff in H.
+ destruct pol;
+ rewrite or_cnf_opt_correct in H;
+ rewrite or_cnf_correct in H;
+ rewrite! eval_cnf_and_opt in H;
+ unfold and_cnf in H;
+ rewrite! eval_cnf_app in H;
+ generalize (IHf1 false env);
+ generalize (IHf1 true env);
+ generalize (IHf2 false env);
+ generalize (IHf2 true env);
+ simpl.
+ -
+ rewrite hold_eIFF_IMPL.
+ rewrite hold_eAND.
+ rewrite! hold_eIMPL.
+ rewrite! hold_eNOT.
+ tauto.
+ - rewrite! hold_eNOT.
+ rewrite hold_eIFF_IMPL.
+ rewrite hold_eAND.
+ rewrite! hold_eIMPL.
+ tauto.
+ Qed.
+
+ Lemma xcnf_correct : forall (k: kind) (f : @GFormula Term rtyp Annot unit k) pol env,
+ eval_cnf env (xcnf pol f) -> hold k (eval_f e_rtyp (eval env) (if pol then f else NOT f)).
+ Proof.
+ induction f.
+ - (* TT *)
+ unfold eval_cnf.
+ simpl.
+ destruct pol ; intros; simpl; auto with tauto.
+ rewrite eval_cnf_ff in H. tauto.
+ - (* FF *)
+ destruct pol ; simpl in *; intros; auto with tauto.
+ + rewrite eval_cnf_ff in H. tauto.
+ - (* P *)
+ simpl.
+ destruct pol ; intros ;simpl.
+ + rewrite eval_cnf_ff in H. tauto.
+ + rewrite eval_cnf_ff in H. tauto.
+ - (* A *)
+ simpl.
+ destruct pol ; simpl.
+ intros.
+ eapply normalise_correct ; eauto.
+ (* A 2 *)
+ intros.
+ eapply negate_correct ; eauto.
+ - (* AND *)
+ destruct pol ; simpl.
+ + (* pol = true *)
+ intros.
+ rewrite eval_cnf_and_opt in H.
+ unfold and_cnf in H.
+ rewrite eval_cnf_app in H.
+ destruct H.
+ apply hold_eAND; split.
+ apply (IHf1 _ _ H).
+ apply (IHf2 _ _ H0).
+ + (* pol = false *)
+ intros.
+ apply hold_eNOT.
+ rewrite hold_eAND.
+ rewrite or_cnf_opt_correct in H.
+ rewrite or_cnf_correct in H.
+ destruct H as [H | H].
+ generalize (IHf1 false env H).
+ simpl.
+ rewrite hold_eNOT.
+ tauto.
+ generalize (IHf2 false env H).
+ simpl.
+ rewrite hold_eNOT.
+ tauto.
+ - (* OR *)
+ simpl.
+ destruct pol.
+ + (* pol = true *)
+ intros. unfold mk_or in H.
+ rewrite or_cnf_opt_correct in H.
+ rewrite or_cnf_correct in H.
+ destruct H as [H | H].
+ generalize (IHf1 _ env H).
+ simpl.
+ rewrite hold_eOR.
+ tauto.
+ generalize (IHf2 _ env H).
+ simpl.
+ rewrite hold_eOR.
+ tauto.
+ + (* pol = true *)
+ intros. unfold mk_or in H.
+ rewrite eval_cnf_and_opt in H.
+ unfold and_cnf.
+ rewrite eval_cnf_app in H.
+ destruct H as [H0 H1].
+ simpl.
+ generalize (IHf1 _ _ H0).
+ generalize (IHf2 _ _ H1).
+ simpl.
+ rewrite ! hold_eNOT.
+ rewrite ! hold_eOR.
+ tauto.
+ - (**)
+ simpl.
+ destruct pol ; simpl.
+ intros.
+ apply (IHf false) ; auto.
+ intros.
+ generalize (IHf _ _ H).
+ rewrite ! hold_eNOT.
+ tauto.
+ - (* IMPL *)
+ apply xcnf_impl; auto.
+ - apply xcnf_iff ; auto.
+ - simpl.
+ destruct (is_bool f2) eqn:EQ.
+ + apply is_bool_inv in EQ.
+ destruct b; subst; intros;
+ apply IHf1 in H;
+ destruct pol ; simpl in * ; auto.
+ * unfold is_true in H.
+ rewrite negb_true_iff in H.
+ congruence.
+ *
+ unfold is_true in H.
+ rewrite negb_true_iff in H.
+ congruence.
+ * unfold is_true in H.
+ congruence.
+ + intros.
+ rewrite <- mk_iff_is_bool in H.
+ apply xcnf_iff in H; auto.
+ simpl in H.
+ destruct pol ; simpl in *.
+ rewrite <- hold_eEQ.
+ simpl; auto.
+ rewrite <- hold_eEQ.
+ simpl; auto.
+ unfold is_true in *.
+ rewrite negb_true_iff in H.
+ congruence.
+ Qed.
Variable Witness : Type.
Variable checker : list (Term'*Annot) -> Witness -> bool.
@@ -1370,28 +2015,26 @@ Section S.
tauto.
Qed.
-
- Definition tauto_checker (f:@GFormula Term Prop Annot unit) (w:list Witness) : bool :=
+ Definition tauto_checker (f:@GFormula Term rtyp Annot unit isProp) (w:list Witness) : bool :=
cnf_checker (xcnf true f) w.
- Lemma tauto_checker_sound : forall t w, tauto_checker t w = true -> forall env, eval_f (fun x => x) (eval env) t.
+ Lemma tauto_checker_sound : forall t w, tauto_checker t w = true -> forall env, eval_f e_rtyp (eval env) t.
Proof.
unfold tauto_checker.
intros.
- change (eval_f (fun x => x) (eval env) t) with (eval_f (fun x => x) (eval env) (if true then t else TT)).
+ change (eval_f e_rtyp (eval env) t) with (eval_f e_rtyp (eval env) (if true then t else TT isProp)).
apply (xcnf_correct t true).
eapply cnf_checker_sound ; eauto.
Qed.
- Definition eval_bf {A : Type} (ea : A -> Prop) (f: BFormula A) := eval_f (fun x => x) ea f.
-
+ Definition eval_bf {A : Type} (ea : forall (k: kind), A -> rtyp k) (k: kind) (f: BFormula A k) := eval_f e_rtyp ea f.
- Lemma eval_bf_map : forall T U (fct: T-> U) env f ,
- eval_bf env (map_bformula fct f) = eval_bf (fun x => env (fct x)) f.
-Proof.
- induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto.
- rewrite <- IHf. auto.
-Qed.
+ Lemma eval_bf_map : forall T U (fct: T-> U) env (k: kind) (f:BFormula T k) ,
+ eval_bf env (map_bformula fct f) = eval_bf (fun b x => env b (fct x)) f.
+ Proof.
+ induction f ; simpl ; try (rewrite IHf1 ; rewrite IHf2) ; auto.
+ rewrite <- IHf. auto.
+ Qed.
End S.
diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v
index bff9671fee..935757f30a 100644
--- a/theories/micromega/ZMicromega.v
+++ b/theories/micromega/ZMicromega.v
@@ -176,7 +176,7 @@ Proof.
rewrite ZNpower. congruence.
Qed.
-Definition Zeval_op2 (o : Op2) : Z -> Z -> Prop :=
+Definition Zeval_pop2 (o : Op2) : Z -> Z -> Prop :=
match o with
| OpEq => @eq Z
| OpNEq => fun x y => ~ x = y
@@ -187,14 +187,62 @@ match o with
end.
-Definition Zeval_formula (env : PolEnv Z) (f : Formula Z):=
+Definition Zeval_bop2 (o : Op2) : Z -> Z -> bool :=
+match o with
+| OpEq => Z.eqb
+| OpNEq => fun x y => negb (Z.eqb x y)
+| OpLe => Z.leb
+| OpGe => Z.geb
+| OpLt => Z.ltb
+| OpGt => Z.gtb
+end.
+
+Lemma pop2_bop2 :
+ forall (op : Op2) (q1 q2 : Z), is_true (Zeval_bop2 op q1 q2) <-> Zeval_pop2 op q1 q2.
+Proof.
+ unfold is_true.
+ destruct op ; simpl; intros.
+ - apply Z.eqb_eq.
+ - rewrite <- Z.eqb_eq.
+ rewrite negb_true_iff.
+ destruct (q1 =? q2) ; intuition congruence.
+ - apply Z.leb_le.
+ - rewrite Z.geb_le. rewrite Z.ge_le_iff. tauto.
+ - apply Z.ltb_lt.
+ - rewrite <- Zgt_is_gt_bool; tauto.
+Qed.
+
+Definition Zeval_op2 (k: Tauto.kind) : Op2 -> Z -> Z -> Tauto.rtyp k:=
+ if k as k0 return (Op2 -> Z -> Z -> Tauto.rtyp k0)
+ then Zeval_pop2 else Zeval_bop2.
+
+
+Lemma Zeval_op2_hold : forall k op q1 q2,
+ Tauto.hold k (Zeval_op2 k op q1 q2) <-> Zeval_pop2 op q1 q2.
+Proof.
+ destruct k.
+ simpl ; tauto.
+ simpl. apply pop2_bop2.
+Qed.
+
+
+Definition Zeval_formula (env : PolEnv Z) (k: Tauto.kind) (f : Formula Z):=
let (lhs, op, rhs) := f in
- (Zeval_op2 op) (Zeval_expr env lhs) (Zeval_expr env rhs).
+ (Zeval_op2 k op) (Zeval_expr env lhs) (Zeval_expr env rhs).
Definition Zeval_formula' :=
eval_formula Z.add Z.mul Z.sub Z.opp (@eq Z) Z.le Z.lt (fun x => x) (fun x => x) (pow_N 1 Z.mul).
-Lemma Zeval_formula_compat' : forall env f, Zeval_formula env f <-> Zeval_formula' env f.
+Lemma Zeval_formula_compat : forall env k f, Tauto.hold k (Zeval_formula env k f) <-> Zeval_formula env Tauto.isProp f.
+Proof.
+ destruct k ; simpl.
+ - tauto.
+ - destruct f ; simpl.
+ rewrite <- Zeval_op2_hold with (k:=Tauto.isBool).
+ simpl. tauto.
+Qed.
+
+Lemma Zeval_formula_compat' : forall env f, Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f.
Proof.
intros.
unfold Zeval_formula.
@@ -312,7 +360,7 @@ Definition xnnormalise (t : Formula Z) : NFormula Z :=
Lemma xnnormalise_correct :
forall env f,
- eval_nformula env (xnnormalise f) <-> Zeval_formula env f.
+ eval_nformula env (xnnormalise f) <-> Zeval_formula env Tauto.isProp f.
Proof.
intros.
rewrite Zeval_formula_compat'.
@@ -393,6 +441,7 @@ Proof.
Qed.
+
Require Import Coq.micromega.Tauto BinNums.
Definition cnf_of_list {T: Type} (tg : T) (l : list (NFormula Z)) :=
@@ -435,7 +484,7 @@ Definition normalise {T : Type} (t:Formula Z) (tg:T) : cnf (NFormula Z) T :=
if Zunsat f then cnf_ff _ _
else cnf_of_list tg (xnormalise f).
-Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env t.
+Lemma normalise_correct : forall (T: Type) env t (tg:T), eval_cnf eval_nformula env (normalise t tg) <-> Zeval_formula env Tauto.isProp t.
Proof.
intros.
rewrite <- xnnormalise_correct.
@@ -449,6 +498,7 @@ Proof.
apply xnormalise_correct.
Qed.
+
Definition xnegate (f:NFormula Z) : list (NFormula Z) :=
let (e,o) := f in
match o with
@@ -478,7 +528,7 @@ Proof.
- tauto.
Qed.
-Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env t.
+Lemma negate_correct : forall T env t (tg:T), eval_cnf eval_nformula env (negate t tg) <-> ~ Zeval_formula env Tauto.isProp t.
Proof.
intros.
rewrite <- xnnormalise_correct.
@@ -492,10 +542,10 @@ Proof.
apply xnegate_correct.
Qed.
-Definition cnfZ (Annot: Type) (TX : Type) (AF : Type) (f : TFormula (Formula Z) Annot TX AF) :=
+Definition cnfZ (Annot: Type) (TX : Tauto.kind -> Type) (AF : Type) (k: Tauto.kind) (f : TFormula (Formula Z) Annot TX AF k) :=
rxcnf Zunsat Zdeduce normalise negate true f.
-Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z)) : bool :=
+Definition ZweakTautoChecker (w: list ZWitness) (f : BFormula (Formula Z) Tauto.isProp) : bool :=
@tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZWitness (fun cl => ZWeakChecker (List.map fst cl)) f w.
(* To get a complete checker, the proof format has to be enriched *)
@@ -1672,9 +1722,7 @@ Proof.
apply Nat.lt_succ_diag_r.
Qed.
-
-
-Definition ZTautoChecker (f : BFormula (Formula Z)) (w: list ZArithProof): bool :=
+Definition ZTautoChecker (f : BFormula (Formula Z) Tauto.isProp) (w: list ZArithProof): bool :=
@tauto_checker (Formula Z) (NFormula Z) unit Zunsat Zdeduce normalise negate ZArithProof (fun cl => ZChecker (List.map fst cl)) f w.
Lemma ZTautoChecker_sound : forall f w, ZTautoChecker f w = true -> forall env, eval_bf (Zeval_formula env) f.
@@ -1692,10 +1740,12 @@ Proof.
-
intros.
rewrite normalise_correct in H.
- auto.
+ rewrite Zeval_formula_compat; auto.
-
intros.
rewrite negate_correct in H ; auto.
+ rewrite Tauto.hold_eNOT.
+ rewrite Zeval_formula_compat; auto.
- intros t w0.
unfold eval_tt.
intros.
@@ -1703,8 +1753,6 @@ Proof.
eapply ZChecker_sound; eauto.
tauto.
Qed.
-
-
Fixpoint xhyps_of_pt (base:nat) (acc : list nat) (pt:ZArithProof) : list nat :=
match pt with
| DoneProof => acc
diff --git a/theories/micromega/ZifyBool.v b/theories/micromega/ZifyBool.v
index c693824f89..d41ac6cf2f 100644
--- a/theories/micromega/ZifyBool.v
+++ b/theories/micromega/ZifyBool.v
@@ -9,177 +9,88 @@
(************************************************************************)
Require Import Bool ZArith.
Require Import Zify ZifyClasses.
+Require Import ZifyInst.
Local Open Scope Z_scope.
-(* Instances of [ZifyClasses] for dealing with boolean operators.
- Various encodings of boolean are possible. One objective is to
- have an encoding that is terse but also lia friendly.
- *)
+(* Instances of [ZifyClasses] for dealing with boolean operators. *)
-(** [Z_of_bool] is the injection function for boolean *)
-Definition Z_of_bool (b : bool) : Z := if b then 1 else 0.
-
-(** [bool_of_Z] is a compatible reverse operation *)
-Definition bool_of_Z (z : Z) : bool := negb (Z.eqb z 0).
-
-Lemma Z_of_bool_bound : forall x, 0 <= Z_of_bool x <= 1.
-Proof.
- destruct x ; simpl; compute; intuition congruence.
-Qed.
-
-Instance Inj_bool_Z : InjTyp bool Z :=
- { inj := Z_of_bool ; pred :=(fun x => 0 <= x <= 1) ; cstr := Z_of_bool_bound}.
-Add InjTyp Inj_bool_Z.
+Instance Inj_bool_bool : InjTyp bool bool :=
+ { inj := (fun x => x) ; pred := (fun x => True) ; cstr := (fun _ => I)}.
+Add InjTyp Inj_bool_bool.
(** Boolean operators *)
Instance Op_andb : BinOp andb :=
- { TBOp := Z.min ;
- TBOpInj := ltac: (destruct n,m; reflexivity)}.
+ { TBOp := andb ;
+ TBOpInj := ltac: (reflexivity)}.
Add BinOp Op_andb.
Instance Op_orb : BinOp orb :=
- { TBOp := Z.max ;
- TBOpInj := ltac:(destruct n,m; reflexivity)}.
+ { TBOp := orb ;
+ TBOpInj := ltac:(reflexivity)}.
Add BinOp Op_orb.
Instance Op_implb : BinOp implb :=
- { TBOp := fun x y => Z.max (1 - x) y;
- TBOpInj := ltac:(destruct n,m; reflexivity) }.
+ { TBOp := implb;
+ TBOpInj := ltac:(reflexivity) }.
Add BinOp Op_implb.
+Definition xorb_eq : forall b1 b2,
+ xorb b1 b2 = andb (orb b1 b2) (negb (eqb b1 b2)).
+Proof.
+ destruct b1,b2 ; reflexivity.
+Qed.
+
Instance Op_xorb : BinOp xorb :=
- { TBOp := fun x y => Z.max (x - y) (y - x);
- TBOpInj := ltac:(destruct n,m; reflexivity) }.
+ { TBOp := fun x y => andb (orb x y) (negb (eqb x y));
+ TBOpInj := xorb_eq }.
Add BinOp Op_xorb.
Instance Op_negb : UnOp negb :=
- { TUOp := fun x => 1 - x ; TUOpInj := ltac:(destruct x; reflexivity)}.
+ { TUOp := negb ; TUOpInj := ltac:(reflexivity)}.
Add UnOp Op_negb.
Instance Op_eq_bool : BinRel (@eq bool) :=
- {TR := @eq Z ; TRInj := ltac:(destruct n,m; simpl ; intuition congruence) }.
+ {TR := @eq bool ; TRInj := ltac:(reflexivity) }.
Add BinRel Op_eq_bool.
Instance Op_true : CstOp true :=
- { TCst := 1 ; TCstInj := eq_refl }.
+ { TCst := true ; TCstInj := eq_refl }.
Add CstOp Op_true.
Instance Op_false : CstOp false :=
- { TCst := 0 ; TCstInj := eq_refl }.
+ { TCst := false ; TCstInj := eq_refl }.
Add CstOp Op_false.
-(** Comparisons are encoded using the predicates [isZero] and [isLeZero].*)
-
-Definition isZero (z : Z) := Z_of_bool (Z.eqb z 0).
-
-Definition isLeZero (x : Z) := Z_of_bool (Z.leb x 0).
-
-Instance Op_isZero : UnOp isZero :=
- { TUOp := isZero; TUOpInj := ltac: (reflexivity) }.
-Add UnOp Op_isZero.
-
-Instance Op_isLeZero : UnOp isLeZero :=
- { TUOp := isLeZero; TUOpInj := ltac: (reflexivity) }.
-Add UnOp Op_isLeZero.
-
-(* Some intermediate lemma *)
-
-Lemma Z_eqb_isZero : forall n m,
- Z_of_bool (n =? m) = isZero (n - m).
-Proof.
- intros ; unfold isZero.
- destruct ( n =? m) eqn:EQ.
- - simpl. rewrite Z.eqb_eq in EQ.
- rewrite EQ. rewrite Z.sub_diag.
- reflexivity.
- -
- destruct (n - m =? 0) eqn:EQ'.
- rewrite Z.eqb_neq in EQ.
- rewrite Z.eqb_eq in EQ'.
- apply Zminus_eq in EQ'.
- congruence.
- reflexivity.
-Qed.
-
-Lemma Z_leb_sub : forall x y, x <=? y = ((x - y) <=? 0).
-Proof.
- intros.
- destruct (x <=?y) eqn:B1 ;
- destruct (x - y <=?0) eqn:B2 ; auto.
- - rewrite Z.leb_le in B1.
- rewrite Z.leb_nle in B2.
- rewrite Z.le_sub_0 in B2. tauto.
- - rewrite Z.leb_nle in B1.
- rewrite Z.leb_le in B2.
- rewrite Z.le_sub_0 in B2. tauto.
-Qed.
-
-Lemma Z_ltb_leb : forall x y, x <? y = (x +1 <=? y).
-Proof.
- intros.
- destruct (x <?y) eqn:B1 ;
- destruct (x + 1 <=?y) eqn:B2 ; auto.
- - rewrite Z.ltb_lt in B1.
- rewrite Z.leb_nle in B2.
- apply Zorder.Zlt_le_succ in B1.
- unfold Z.succ in B1.
- tauto.
- - rewrite Z.ltb_nlt in B1.
- rewrite Z.leb_le in B2.
- apply Zorder.Zle_lt_succ in B2.
- unfold Z.succ in B2.
- apply Zorder.Zplus_lt_reg_r in B2.
- tauto.
-Qed.
-
-
(** Comparison over Z *)
Instance Op_Zeqb : BinOp Z.eqb :=
- { TBOp := fun x y => isZero (Z.sub x y) ; TBOpInj := Z_eqb_isZero}.
+ { TBOp := Z.eqb ; TBOpInj := ltac:(reflexivity)}.
Instance Op_Zleb : BinOp Z.leb :=
- { TBOp := fun x y => isLeZero (x-y) ;
- TBOpInj :=
- ltac: (intros;unfold isLeZero;
- rewrite Z_leb_sub;
- auto) }.
+ { TBOp := Z.leb;
+ TBOpInj := ltac: (reflexivity);
+ }.
Add BinOp Op_Zleb.
Instance Op_Zgeb : BinOp Z.geb :=
- { TBOp := fun x y => isLeZero (y-x) ;
- TBOpInj := ltac:(
- intros;
- unfold isLeZero;
- rewrite Z.geb_leb;
- rewrite Z_leb_sub;
- auto) }.
+ { TBOp := Z.geb;
+ TBOpInj := ltac:(reflexivity)
+ }.
Add BinOp Op_Zgeb.
Instance Op_Zltb : BinOp Z.ltb :=
- { TBOp := fun x y => isLeZero (x+1-y) ;
- TBOpInj := ltac:(
- intros;
- unfold isLeZero;
- rewrite Z_ltb_leb;
- rewrite <- Z_leb_sub;
- reflexivity) }.
+ { TBOp := Z.ltb ;
+ TBOpInj := ltac:(reflexivity)
+ }.
Instance Op_Zgtb : BinOp Z.gtb :=
- { TBOp := fun x y => isLeZero (y-x+1) ;
- TBOpInj := ltac:(
- intros;
- unfold isLeZero;
- rewrite Z.gtb_ltb;
- rewrite Z_ltb_leb;
- rewrite Z_leb_sub;
- rewrite Z.add_sub_swap;
- reflexivity) }.
+ { TBOp := Z.gtb;
+ TBOpInj := ltac:(reflexivity)
+ }.
Add BinOp Op_Zgtb.
(** Comparison over nat *)
-
Lemma Z_of_nat_eqb_iff : forall n m,
(n =? m)%nat = (Z.of_nat n =? Z.of_nat m).
Proof.
@@ -211,68 +122,18 @@ Proof.
Qed.
Instance Op_nat_eqb : BinOp Nat.eqb :=
- { TBOp := fun x y => isZero (Z.sub x y) ;
- TBOpInj := ltac:(
- intros; simpl;
- rewrite <- Z_eqb_isZero;
- f_equal; apply Z_of_nat_eqb_iff) }.
+ { TBOp := Z.eqb;
+ TBOpInj := Z_of_nat_eqb_iff }.
Add BinOp Op_nat_eqb.
Instance Op_nat_leb : BinOp Nat.leb :=
- { TBOp := fun x y => isLeZero (x-y) ;
- TBOpInj := ltac:(
- intros;
- rewrite Z_of_nat_leb_iff;
- unfold isLeZero;
- rewrite Z_leb_sub;
- auto) }.
+ { TBOp := Z.leb ;
+ TBOpInj := Z_of_nat_leb_iff
+ }.
Add BinOp Op_nat_leb.
Instance Op_nat_ltb : BinOp Nat.ltb :=
- { TBOp := fun x y => isLeZero (x+1-y) ;
- TBOpInj := ltac:(
- intros;
- rewrite Z_of_nat_ltb_iff;
- unfold isLeZero;
- rewrite Z_ltb_leb;
- rewrite <- Z_leb_sub;
- reflexivity) }.
+ { TBOp := Z.ltb;
+ TBOpInj := Z_of_nat_ltb_iff
+ }.
Add BinOp Op_nat_ltb.
-
-(** Injected boolean operators *)
-
-Lemma Z_eqb_ZSpec_ok : forall x, 0 <= isZero x <= 1 /\
- (x = 0 <-> isZero x = 1).
-Proof.
- intros.
- unfold isZero.
- destruct (x =? 0) eqn:EQ.
- - apply Z.eqb_eq in EQ.
- simpl. intuition try congruence;
- compute ; congruence.
- - apply Z.eqb_neq in EQ.
- simpl. intuition try congruence;
- compute ; congruence.
-Qed.
-
-
-Instance Z_eqb_ZSpec : UnOpSpec isZero :=
- {| UPred := fun n r => 0 <= r <= 1 /\ (n = 0 <-> isZero n = 1) ; USpec := Z_eqb_ZSpec_ok |}.
-Add Spec Z_eqb_ZSpec.
-
-Lemma leZeroSpec_ok : forall x, x <= 0 /\ isLeZero x = 1 \/ x > 0 /\ isLeZero x = 0.
-Proof.
- intros.
- unfold isLeZero.
- destruct (x <=? 0) eqn:EQ.
- - apply Z.leb_le in EQ.
- simpl. intuition congruence.
- - simpl.
- apply Z.leb_nle in EQ.
- apply Zorder.Znot_le_gt in EQ.
- tauto.
-Qed.
-
-Instance leZeroSpec : UnOpSpec isLeZero :=
- {| UPred := fun n r => (n<=0 /\ r = 1) \/ (n > 0 /\ r = 0) ; USpec := leZeroSpec_ok|}.
-Add Spec leZeroSpec.
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index 3eb4c924ae..65083791ca 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -34,19 +34,19 @@ Class InjTyp (S : Type) (T : Type) :=
(** [BinOp Op] declares a source operator [Op: S1 -> S2 -> S3].
*)
-Class BinOp {S1 S2 S3:Type} {T:Type} (Op : S1 -> S2 -> S3) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} {I3 : InjTyp S3 T} :=
+Class BinOp {S1 S2 S3 T1 T2 T3:Type} (Op : S1 -> S2 -> S3) {I1 : InjTyp S1 T1} {I2 : InjTyp S2 T2} {I3 : InjTyp S3 T3} :=
mkbop {
(* [TBOp] is the target operator after injection of operands. *)
- TBOp : T -> T -> T;
+ TBOp : T1 -> T2 -> T3;
(* [TBOpInj] states the correctness of the injection. *)
TBOpInj : forall (n:S1) (m:S2), inj (Op n m) = TBOp (inj n) (inj m)
}.
(** [Unop Op] declares a source operator [Op : S1 -> S2]. *)
-Class UnOp {S1 S2 T:Type} (Op : S1 -> S2) {I1 : InjTyp S1 T} {I2 : InjTyp S2 T} :=
+Class UnOp {S1 S2 T1 T2:Type} (Op : S1 -> S2) {I1 : InjTyp S1 T1} {I2 : InjTyp S2 T2} :=
mkuop {
(* [TUOp] is the target operator after injection of operands. *)
- TUOp : T -> T;
+ TUOp : T1 -> T2;
(* [TUOpInj] states the correctness of the injection. *)
TUOpInj : forall (x:S1), inj (Op x) = TUOp (inj x)
}.
@@ -141,9 +141,6 @@ Record injprop :=
injprop_ok : source_prop <-> target_prop}.
-
-
-
(** Lemmas for building rewrite rules. *)
Definition PropOp_iff (Op : Prop -> Prop -> Prop) :=
@@ -152,22 +149,22 @@ Definition PropOp_iff (Op : Prop -> Prop -> Prop) :=
Definition PropUOp_iff (Op : Prop -> Prop) :=
forall (p1 q1 :Prop), (p1 <-> q1) -> (Op p1 <-> Op q1).
-Lemma mkapp2 (S1 S2 S3 T : Type) (Op : S1 -> S2 -> S3)
- (I1 : S1 -> T) (I2 : S2 -> T) (I3 : S3 -> T)
- (TBOP : T -> T -> T)
+Lemma mkapp2 (S1 S2 S3 T1 T2 T3 : Type) (Op : S1 -> S2 -> S3)
+ (I1 : S1 -> T1) (I2 : S2 -> T2) (I3 : S3 -> T3)
+ (TBOP : T1 -> T2 -> T3)
(TBOPINJ : forall n m, I3 (Op n m) = TBOP (I1 n) (I2 m))
- (s1 : S1) (t1 : T) (P1: I1 s1 = t1)
- (s2 : S2) (t2 : T) (P2: I2 s2 = t2): I3 (Op s1 s2) = TBOP t1 t2.
+ (s1 : S1) (t1 : T1) (P1: I1 s1 = t1)
+ (s2 : S2) (t2 : T2) (P2: I2 s2 = t2): I3 (Op s1 s2) = TBOP t1 t2.
Proof.
subst. apply TBOPINJ.
Qed.
-Lemma mkapp (S1 S2 T : Type) (OP : S1 -> S2)
- (I1 : S1 -> T)
- (I2 : S2 -> T)
- (TUOP : T -> T)
+Lemma mkapp (S1 S2 T1 T2 : Type) (OP : S1 -> S2)
+ (I1 : S1 -> T1)
+ (I2 : S2 -> T2)
+ (TUOP : T1 -> T2)
(TUOPINJ : forall n, I2 (OP n) = TUOP (I1 n))
- (s1: S1) (t1: T) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1.
+ (s1: S1) (t1: T1) (P1: I1 s1 = t1): I2 (OP s1) = TUOP t1.
Proof.
subst. apply TUOPINJ.
Qed.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:38:52 +0000