# Library Coq.micromega.CheckerMaker

Require Import Setoid.
Require Import Decidable.
Require Import List.
Require Import Refl.
Section CheckerMaker.
Variable Formula : Type.
Variable Env : Type.
Variable eval : Env -> Formula -> Prop.
Variable Formula' : Type.
Variable eval' : Env -> Formula' -> Prop.
Variable normalise : Formula -> Formula'.
Variable negate : Formula -> Formula'.
Hypothesis normalise_sound :
forall (env : Env) (t : Formula), eval env t -> eval' env (normalise t).
Hypothesis negate_correct :
forall (env : Env) (t : Formula), eval env t <-> ~ (eval' env (negate t)).
Variable Witness : Type.
Variable check_formulas' : list Formula' -> Witness -> bool.
Hypothesis check_formulas'_sound :
forall (l : list Formula') (w : Witness),
check_formulas' l w = true ->
forall env : Env, make_impl (eval' env) l False.
Definition normalise_list : list Formula -> list Formula' := map normalise.
Definition negate_list : list Formula -> list Formula' := map negate.
Definition check_formulas (l : list Formula) (w : Witness) : bool :=
check_formulas' (map normalise l) w.
Lemma normalise_sound_contr : forall (env : Env) (l : list Formula),
make_impl (eval' env) (map normalise l) False -> make_impl (eval env) l False.
Theorem check_formulas_sound :
forall (l : list Formula) (w : Witness),
check_formulas l w = true -> forall env : Env, make_impl (eval env) l False.
Fixpoint check_conj_formulas'
(t1 : list Formula') (wits : list Witness) (t2 : list Formula') {struct wits} : bool :=
match t2 with
| nil => true
| t':: rt2 =>
match wits with
| nil => false
| w :: rwits =>
match check_formulas' (t':: t1) w with
| true => check_conj_formulas' t1 rwits rt2
| false => false
end
end
end.
Definition check_conj_formulas
(t1 : list Formula) (wits : list Witness) (t2 : list Formula) : bool :=
check_conj_formulas' (normalise_list t1) wits (negate_list t2).
Theorem check_conj_formulas_sound :
forall (t1 : list Formula) (t2 : list Formula) (wits : list Witness),
check_conj_formulas t1 wits t2 = true ->
forall env : Env, make_impl (eval env) t1 (make_conj (eval env) t2).
End CheckerMaker.