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 or_clause_cnf (t:clause) (f:cnf) : cnf :=
List.fold_right (fun e acc =>
match or_clause t e with
| None => acc
| Some cl => cl :: acc
end) nil f.
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.
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 else or_cnf) (xcnf pol e1) (xcnf pol e2)
| D e1 e2 => (if pol then or_cnf else and_cnf) (xcnf pol e1) (xcnf pol e2)
| I e1 _ e2 => (if pol then or_cnf else and_cnf) (xcnf (negb pol) e1) (xcnf pol e2)
end.
Section CNFAnnot.
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 else or_cnf) (xcnf pol e1) (xcnf pol e2)
| D e1 e2 => (if pol then or_cnf else and_cnf) (xcnf pol e1) (xcnf pol e2)
| I e1 _ e2 => (if pol then or_cnf else and_cnf) (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 ror_clause_cnf t f :=
List.fold_right (fun e '(acc,tg) =>
match ror_clause t e with
| inl cl => (cl :: acc,tg)
| inr l => (acc,tg++l)
end) (nil,nil) f .
Fixpoint ror_cnf f f' :=
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.
Fixpoint rxcnf {TX AF: Type}(polarity : bool) (f : TFormula TX AF) :=
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 => ((if polarity then normalise x t else negate x t),nil)
| 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 (e1 ++ e2, t1 ++ t2)
else let (f',t') := ror_cnf 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 e1 e2 in
(f', t1 ++ t2 ++ t')
else (e1 ++ e2, t1 ++ t2)
| I e1 _ e2 =>
let (e1 , t1) := (rxcnf (negb polarity) e1) in
let (e2 , t2) := (rxcnf polarity e2) in
if polarity
then let (f',t') := ror_cnf e1 e2 in
(f', t1 ++ t2 ++ t')
else (and_cnf e1 e2, t1 ++ t2)
end.
End CNFAnnot.
Variable eval : Env -> Term -> Prop.
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 env t t' u,
eval' env t -> eval' env t' -> deduce t t' = Some u -> 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.
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 or_cnf_correct : forall env f f', eval_cnf env (or_cnf f f') -> (eval_cnf env f) \/ (eval_cnf env f').
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.