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.