Library Coq.micromega.Tauto
Require Import List.
Require Import Refl.
Require Import Bool.
Set Implicit Arguments.
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 eval_f_morph : forall A (ev ev' : A -> Prop) (f : BFormula A),
(forall a, ev a <-> ev' a) -> (eval_f ev f <-> eval_f ev' f).
Fixpoint map_bformula (T U : Type) (fct : T -> U) (f : BFormula T) : BFormula U :=
match f with
| TT _ => TT _
| FF _ => FF _
| X _ p => X _ p
| A a => A (fct a)
| 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 f2 => I (map_bformula fct f1) (map_bformula fct f2)
end.
Lemma eval_f_map : forall T U (fct: T-> U) env f ,
eval_f env (map_bformula fct f) = eval_f (fun x => env (fct x)) f.
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).
Variable unsat : Term' -> bool.
Variable unsat_prop : forall t, unsat t = true ->
forall env, eval' env t -> False.
Variable deduce : Term' -> Term' -> option Term'.
Variable deduce_prop : forall env t t' u,
eval' env t -> eval' env t' -> deduce t t' = Some u -> eval' env u.
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.
Fixpoint add_term (t: Term') (cl : clause) : option clause :=
match cl with
| nil =>
match deduce t t with
| None => Some (t ::nil)
| Some u => if unsat u then None else Some (t::nil)
end
| t'::cl =>
match deduce t 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 => 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_clause (env : Env) (cl : clause) := ~ make_conj (eval' 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 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' 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, eval_cnf env (normalise t) -> eval env t.
Variable negate_correct : forall env t, eval_cnf env (negate t) -> ~ eval env t.
Lemma xcnf_correct : forall f pol env, eval_cnf 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 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.