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.
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.

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.

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.