# Library Coq.micromega.Tauto

Require Import List.
Require Import Refl.
Require Import Bool.
Inductive BFormula (A:Type) : Type :=
| TT : BFormula A
| FF : BFormula A
| X : Prop -> BFormula A
| A : A -> BFormula A
| Cj : BFormula A -> BFormula A -> BFormula A
| D : BFormula A-> BFormula A -> BFormula A
| N : BFormula A -> BFormula A
| I : BFormula A-> BFormula A-> BFormula A.
Fixpoint eval_f (A:Type) (ev:A -> Prop ) (f:BFormula A) {struct f}: Prop :=
match f with
| TT => True
| FF => False
| A a => ev a
| X p => p
| Cj e1 e2 => ( eval_f ev e1 ) /\ ( eval_f ev e2 )
| D e1 e2 => ( eval_f ev e1 ) \/ ( eval_f ev e2 )
| N e => ~ ( eval_f ev e )
| I f1 f2 => (eval_f ev f1) -> (eval_f ev f2)
end.
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.
Variable Env : Type.
Variable Term : Type.
Variable eval : Env -> Term -> Prop.
Variable Term' : Type.
Variable eval' : Env -> Term' -> Prop.
Variable no_middle_eval' : forall env d, ( eval' env d ) \/ ~ ( eval' env d ).
Definition clause := list Term'.
Definition cnf := list clause.
Variable normalise : Term -> cnf.
Variable negate : Term -> cnf.
Definition tt : cnf := @nil clause.
Definition ff : cnf := cons (@nil Term') nil.
Definition or_clause_cnf (t:clause) (f:cnf) : cnf :=
List.map (fun x => (t ++ x)) f.
Fixpoint or_cnf (f : cnf) (f' : cnf) {struct f}: cnf :=
match f with
| nil => tt
| e :: rst => ( or_cnf rst f' ) ++ ( or_clause_cnf e f' )
end.
Definition and_cnf (f1 : cnf) (f2 : cnf) : cnf :=
f1 ++ f2.
Fixpoint xcnf (pol : bool) (f : BFormula Term) {struct f}: cnf :=
match f with
| TT => if pol then tt else ff
| FF => if pol then ff else tt
| X p => if pol then ff else ff
| A x => if pol then normalise x else negate x
| 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.
Definition eval_cnf (env : Term' -> Prop) (f:cnf) := make_conj (fun cl => ~ make_conj env cl) f.
Lemma eval_cnf_app : forall env x y, eval_cnf (eval' env) (x ++ y) -> eval_cnf (eval' env) x /\ eval_cnf (eval' env) y.
Lemma or_clause_correct : forall env t f, eval_cnf (eval' env) (or_clause_cnf t f) -> ( ~ make_conj (eval' env) t ) \/ ( eval_cnf (eval' env) f ).
Lemma eval_cnf_cons : forall env a f, (~ make_conj (eval' env) a) -> eval_cnf (eval' env) f -> eval_cnf (eval' env) (a :: f).
Lemma or_cnf_correct : forall env f f', eval_cnf (eval' env) (or_cnf f f') -> ( eval_cnf (eval' env) f ) \/ ( eval_cnf (eval' env) f' ).
Variable normalise_correct : forall env t, eval_cnf (eval' env) (normalise t) -> eval env t.
Variable negate_correct : forall env t, eval_cnf (eval' env) (negate t) -> ~ eval env t.
Lemma xcnf_correct : forall f pol env, eval_cnf (eval' env) (xcnf pol f) -> eval_f (eval env) (if pol then f else N f).
Variable Witness : Type.
Variable checker : list Term' -> Witness -> bool.
Variable checker_sound : forall t w, checker t w = true -> forall env, make_impl (eval' 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 (eval' env) t.
Definition tauto_checker (f:BFormula Term) (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 (eval env) t.
End S.