Library Coq.micromega.Tauto
Require Import List.
Require Import Refl.
Require Import Bool.
Set Implicit Arguments.
Section S.
Context {TA : Type}. Context {TX : Type}. Context {AA : Type}. Context {AF : Type}.
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.
Section MAPX.
Variable F : TX -> TX.
Fixpoint mapX (f : GFormula) : GFormula :=
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)
end.
End MAPX.
Section FOLDANNOT.
Variable ACC : Type.
Variable F : ACC -> AA -> ACC.
Fixpoint foldA (f : GFormula) (acc : ACC) : ACC :=
match f with
| 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
end.
End FOLDANNOT.
Definition cons_id (id : option AF) (l : list AF) :=
match id with
| None => l
| Some id => id :: l
end.
Fixpoint ids_of_formula f :=
match f with
| I f id f' => cons_id id (ids_of_formula f')
| _ => nil
end.
Fixpoint collect_annot (f : GFormula) : 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
end.
Variable ex : TX -> Prop.
Section EVAL.
Variable ea : TA -> Prop.
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.
End EVAL.
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).
End S.
Typical boolean formulae
Definition BFormula (A : Type) := @GFormula A Prop unit unit.
Section MAPATOMS.
Context {TA TA':Type}.
Context {TX : 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.
End MAPATOMS.
Lemma map_simpl : forall A B f l, @map A B f l = match l with
| nil => nil
| a :: l=> (f a) :: (@map A B f l)
end.
Section S.
Section MAPATOMS.
Context {TA TA':Type}.
Context {TX : 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.
End MAPATOMS.
Lemma map_simpl : forall A B f l, @map A B f l = match l with
| nil => nil
| a :: l=> (f a) :: (@map A B f l)
end.
Section S.
A cnf tracking annotations of atoms.
Type parameters
Variable Env : Type.
Variable Term : Type.
Variable Term' : Type.
Variable Annot : Type.
Variable unsat : Term' -> bool. Variable deduce : Term' -> Term' -> option Term'.
Definition clause := list (Term' * Annot).
Definition cnf := list clause.
Variable normalise : Term -> Annot -> cnf.
Variable negate : Term -> Annot -> cnf.
Definition cnf_tt : cnf := @nil clause.
Definition cnf_ff : cnf := cons (@nil (Term' * Annot)) nil.
Variable Term : Type.
Variable Term' : Type.
Variable Annot : Type.
Variable unsat : Term' -> bool. Variable deduce : Term' -> Term' -> option Term'.
Definition clause := list (Term' * Annot).
Definition cnf := list clause.
Variable normalise : Term -> Annot -> cnf.
Variable negate : Term -> Annot -> cnf.
Definition cnf_tt : cnf := @nil clause.
Definition cnf_ff : cnf := cons (@nil (Term' * Annot)) nil.
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)
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
| 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 i s unit in Coq and Names.Id.t in Ocaml
Definition TFormula (TX: 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 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.
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
| 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)
end.
Section CNFAnnot.
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 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.
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
| 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)
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 =>
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 =>
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 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.
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.
Fixpoint ror_cnf (f f':list clause) :=
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')
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 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 ocons {A : Type} (o : option A) (l : list A) : list A :=
match o with
| None => l
| Some e => e ::l
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).
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
let '(e2 , t2) := (rxcnf polarity e2) in
let (f',t') := ror_cnf_opt e1 e2 in
(f', t1 +++ t2 +++ t')
else
let '(e2 , t2) := (rxcnf polarity e2) in
(and_cnf_opt e1 e2, t1 +++ t2)
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 is_X (f : TFormula TX AF) : option TX :=
match f with
| X p => Some p
| _ => None
end.
Definition is_X_inv : forall f x,
is_X f = Some x -> f = X x.
Variable needA : Annot -> bool.
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 abs_or (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 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.
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.
Lemma if_same : forall {A: Type} (b:bool) (t:A),
(if b then t else t) = t.
Lemma is_cnf_tt_cnf_ff :
is_cnf_tt cnf_ff = false.
Lemma is_cnf_ff_cnf_ff :
is_cnf_ff cnf_ff = true.
Lemma is_cnf_tt_inv : forall f1,
is_cnf_tt f1 = true -> f1 = cnf_tt.
Lemma is_cnf_ff_inv : forall f1,
is_cnf_ff f1 = true -> f1 = cnf_ff.
Lemma if_cnf_tt : forall f, (if is_cnf_tt f then cnf_tt else f) = f.
Lemma or_cnf_opt_cnf_ff : forall f,
or_cnf_opt cnf_ff f = f.
Lemma abs_and_pol : forall f1 f2 pol,
and_cnf_opt (xcnf pol f1) (xcnf pol f2) =
xcnf pol (abs_and f1 f2 (if pol then Cj else D)).
Lemma abs_or_pol : forall f1 f2 pol,
or_cnf_opt (xcnf pol f1) (xcnf pol f2) =
xcnf pol (abs_or f1 f2 (if pol then D else Cj)).
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 or_cnf_opt_cnf_ff_r : forall f,
or_cnf_opt f cnf_ff = f.
Lemma xcnf_true_mk_arrow_r : forall o t f,
xcnf true (mk_arrow o f (X t)) = xcnf false f.
Lemma abst_form_correct : forall f pol,
xcnf pol f = xcnf pol (abst_form pol f).
End Abstraction.
End CNFAnnot.
Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl.
Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl.
Lemma xror_clause_clause : forall a f,
fst (xror_clause_cnf a f) = xor_clause_cnf a f.
Lemma ror_clause_clause : forall a f,
fst (ror_clause_cnf a f) = or_clause_cnf a f.
Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2.
Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2.
Lemma ratom_cnf : forall f a,
fst (ratom f a) = f.
Lemma rxcnf_xcnf : forall {TX AF:Type} (f:TFormula TX AF) b,
fst (rxcnf b f) = xcnf b f.
Variable eval' : Env -> Term' -> Prop.
Variable no_middle_eval' : forall env d, (eval' env d) \/ ~ (eval' env d).
Variable unsat_prop : forall t, unsat t = true ->
forall env, eval' env t -> False.
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).
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.
Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False.
Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True.
Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x y).
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).
Lemma no_middle_eval_tt : forall env a,
eval_tt env a \/ ~ eval_tt env a.
Hint Resolve no_middle_eval_tt : tauto.
Lemma or_clause_correct : forall cl cl' env, eval_opt_clause env (or_clause cl cl') <-> eval_clause env cl \/ eval_clause env cl'.
Lemma or_clause_cnf_correct : forall env t f, eval_cnf env (or_clause_cnf t f) <-> (eval_clause env t) \/ (eval_cnf env f).
Lemma eval_cnf_cons : forall env a f, (~ make_conj (eval_tt env) a /\ eval_cnf env f) <-> eval_cnf env (a::f).
Lemma eval_cnf_cons_iff : forall env a f, ((~ make_conj (eval_tt env) a) /\ eval_cnf env f) <-> eval_cnf env (a::f).
Lemma or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') <-> (eval_cnf env f) \/ (eval_cnf env f').
Lemma or_cnf_opt_correct : forall env f f', eval_cnf env (or_cnf_opt f f') <-> eval_cnf env (or_cnf f f').
Variable eval : Env -> Term -> Prop.
Variable normalise_correct : forall env t tg, eval_cnf env (normalise t tg) -> eval env t.
Variable negate_correct : forall env t tg, eval_cnf env (negate t tg) -> ~ eval env t.
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).
Variable Witness : Type.
Variable checker : list (Term'*Annot) -> Witness -> bool.
Variable checker_sound : forall t w, checker t w = true -> forall env, make_impl (eval_tt env) t False.
Fixpoint cnf_checker (f : cnf) (l : list Witness) {struct f}: bool :=
match f with
| nil => true
| e::f => match l with
| nil => false
| c::l => match checker e c with
| true => cnf_checker f l
| _ => false
end
end
end.
Lemma cnf_checker_sound : forall t w, cnf_checker t w = true -> forall env, eval_cnf env t.
Definition tauto_checker (f:@GFormula Term Prop Annot unit) (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.
Definition eval_bf {A : Type} (ea : A -> Prop) (f: BFormula A) := eval_f (fun x => x) 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.
End S.