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 xor_clause_cnf (t:clause) (f:cnf) : cnf :=
      List.fold_left (fun acc e =>
                         match or_clause t e with
                         | None => acc
                         | Some cl => cl :: acc
                         end) f nil .

    Definition or_clause_cnf (t: clause) (f:cnf) : cnf :=
      match t with
      | nil => f
      | _ => xor_clause_cnf t f
      end.

    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.

    Definition is_cnf_tt (c : cnf) : bool :=
      match c with
      | nil => true
      | _ => false
      end.

    Definition is_cnf_ff (c : cnf) : bool :=
      match c with
      | nil::nil => true
      | _ => false
      end.

    Definition and_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
      if is_cnf_ff f1 || is_cnf_ff f2
      then cnf_ff
      else and_cnf f1 f2.

    Definition or_cnf_opt (f1 : cnf) (f2 : cnf) : cnf :=
      if is_cnf_tt f1 || is_cnf_tt f2
      then cnf_tt
      else if is_cnf_ff f2
           then f1 else or_cnf f1 f2.

    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_opt else or_cnf_opt) (xcnf pol e1) (xcnf pol e2)
      | D e1 e2 => (if pol then or_cnf_opt else and_cnf_opt) (xcnf pol e1) (xcnf pol e2)
      | I e1 _ e2
        => (if pol then or_cnf_opt else and_cnf_opt) (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 xror_clause_cnf t f :=
        List.fold_left (fun '(acc,tg) e =>
                           match ror_clause t e with
                           | inl cl => (cl :: acc,tg)
                           | inr l => (acc,tg+++l)
                           end) f (nil,nil).

      Definition ror_clause_cnf t f :=
        match t with
        | nil => (f,nil)
        | _ => xror_clause_cnf t f
        end.

      Fixpoint ror_cnf (f f':list clause) :=
        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.

      Definition annot_of_clause (l : clause) : list Annot :=
        List.map snd l.

      Definition annot_of_cnf (f : cnf) : list Annot :=
        List.fold_left (fun acc e => annot_of_clause e +++ acc ) f nil.

      Definition ror_cnf_opt f1 f2 :=
        if is_cnf_tt f1
        then (cnf_tt , nil)
        else if is_cnf_tt f2
             then (cnf_tt, nil)
             else if is_cnf_ff f2
                  then (f1,nil)
                  else ror_cnf f1 f2.

      Definition ocons {A : Type} (o : option A) (l : list A) : list A :=
        match o with
        | None => l
        | Some e => e ::l
        end.

      Definition ratom (c : cnf) (a : Annot) : cnf * list Annot :=
        if is_cnf_ff c || is_cnf_tt c
        then (c,a::nil)
        else (c,nil).
      Fixpoint rxcnf {TX AF: Type}(polarity : bool) (f : TFormula TX AF) : cnf * list Annot :=
        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 => ratom (if polarity then normalise x t else negate x t) t
        | 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 (and_cnf_opt e1 e2, t1 +++ t2)
          else let (f',t') := ror_cnf_opt 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_opt e1 e2 in
            (f', t1 +++ t2 +++ t')
          else (and_cnf_opt e1 e2, t1 +++ t2)
        | I e1 a e2 =>
          let '(e1 , t1) := (rxcnf (negb polarity) e1) in
          if polarity
          then
            if is_cnf_ff e1
            then
              rxcnf polarity e2
            else
              let '(e2 , t2) := (rxcnf polarity e2) in
              let (f',t') := ror_cnf_opt e1 e2 in
              (f', t1 +++ t2 +++ t')
          else
            let '(e2 , t2) := (rxcnf polarity e2) in
            (and_cnf_opt e1 e2, t1 +++ t2)
        end.

      Section Abstraction.
        Variable TX : Type.
        Variable AF : Type.

        Class to_constrT : Type :=
          {
            mkTT : TX;
            mkFF : TX;
            mkA : Term -> Annot -> TX;
            mkCj : TX -> TX -> TX;
            mkD : TX -> TX -> TX;
            mkI : TX -> TX -> TX;
            mkN : TX -> TX
          }.

        Context {to_constr : to_constrT}.

        Fixpoint aformula (f : TFormula TX AF) : TX :=
          match f with
          | TT => mkTT
          | FF => mkFF
          | X p => p
          | A x t => mkA x t
          | Cj f1 f2 => mkCj (aformula f1) (aformula f2)
          | D f1 f2 => mkD (aformula f1) (aformula f2)
          | I f1 o f2 => mkI (aformula f1) (aformula f2)
          | N f => mkN (aformula f)
          end.

        Definition is_X (f : TFormula TX AF) : option TX :=
          match f with
          | X p => Some p
          | _ => None
          end.

        Definition is_X_inv : forall f x,
            is_X f = Some x -> f = X x.

        Variable needA : Annot -> bool.

        Definition abs_and (f1 f2 : TFormula TX AF)
                   (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) :=
          match is_X f1 , is_X f2 with
          | Some _ , _ | _ , Some _ => X (aformula (c f1 f2))
          | _ , _ => c f1 f2
          end.

        Definition abs_or (f1 f2 : TFormula TX AF)
                   (c : TFormula TX AF -> TFormula TX AF -> TFormula TX AF) :=
          match is_X f1 , is_X f2 with
          | Some _ , Some _ => X (aformula (c f1 f2))
          | _ , _ => c f1 f2
          end.

        Definition mk_arrow (o : option AF) (f1 f2: TFormula TX AF) :=
          match o with
          | None => I f1 None f2
          | Some _ => if is_X f1 then f2 else I f1 o f2
          end.

        Fixpoint abst_form (pol : bool) (f : TFormula TX AF) :=
          match f with
          | TT => if pol then TT else X mkTT
          | FF => if pol then X mkFF else FF
          | X p => X p
          | A x t => if needA t then A x t else X (mkA x t)
          | Cj f1 f2 =>
            let f1 := abst_form pol f1 in
            let f2 := abst_form pol f2 in
            if pol then abs_and f1 f2 Cj
            else abs_or f1 f2 Cj
          | D f1 f2 =>
            let f1 := abst_form pol f1 in
            let f2 := abst_form pol f2 in
            if pol then abs_or f1 f2 D
            else abs_and f1 f2 D
          | I f1 o f2 =>
            let f1 := abst_form (negb pol) f1 in
            let f2 := abst_form pol f2 in
            if pol
            then abs_or f1 f2 (mk_arrow o)
            else abs_and f1 f2 (mk_arrow o)
          | N f => let f := abst_form (negb pol) f in
                   match is_X f with
                   | Some a => X (mkN a)
                   | _ => N f
                   end
          end.

        Lemma if_same : forall {A: Type} (b:bool) (t:A),
            (if b then t else t) = t.

        Lemma is_cnf_tt_cnf_ff :
          is_cnf_tt cnf_ff = false.

        Lemma is_cnf_ff_cnf_ff :
          is_cnf_ff cnf_ff = true.

      Lemma is_cnf_tt_inv : forall f1,
          is_cnf_tt f1 = true -> f1 = cnf_tt.

      Lemma is_cnf_ff_inv : forall f1,
          is_cnf_ff f1 = true -> f1 = cnf_ff.

      Lemma if_cnf_tt : forall f, (if is_cnf_tt f then cnf_tt else f) = f.

      Lemma or_cnf_opt_cnf_ff : forall f,
          or_cnf_opt cnf_ff f = f.

      Lemma abs_and_pol : forall f1 f2 pol,
          and_cnf_opt (xcnf pol f1) (xcnf pol f2) =
          xcnf pol (abs_and f1 f2 (if pol then Cj else D)).

      Lemma abs_or_pol : forall f1 f2 pol,
          or_cnf_opt (xcnf pol f1) (xcnf pol f2) =
          xcnf pol (abs_or f1 f2 (if pol then D else Cj)).

      Variable needA_all : forall a, needA a = true.

      Lemma xcnf_true_mk_arrow_l : forall o t f,
        xcnf true (mk_arrow o (X t) f) = xcnf true f.

      Lemma or_cnf_opt_cnf_ff_r : forall f,
          or_cnf_opt f cnf_ff = f.

      Lemma xcnf_true_mk_arrow_r : forall o t f,
          xcnf true (mk_arrow o f (X t)) = xcnf false f.

      Lemma abst_form_correct : forall f pol,
          xcnf pol f = xcnf pol (abst_form pol f).

      End Abstraction.

      End CNFAnnot.

      Lemma radd_term_term : forall a' a cl, radd_term a a' = inl cl -> add_term a a' = Some cl.

      Lemma radd_term_term' : forall a' a cl, add_term a a' = Some cl -> radd_term a a' = inl cl.

      Lemma xror_clause_clause : forall a f,
          fst (xror_clause_cnf a f) = xor_clause_cnf a f.

      Lemma ror_clause_clause : forall a f,
          fst (ror_clause_cnf a f) = or_clause_cnf a f.

      Lemma ror_cnf_cnf : forall f1 f2, fst (ror_cnf f1 f2) = or_cnf f1 f2.

      Lemma ror_opt_cnf_cnf : forall f1 f2, fst (ror_cnf_opt f1 f2) = or_cnf_opt f1 f2.

      Lemma ratom_cnf : forall f a,
          fst (ratom f a) = f.

      Lemma rxcnf_xcnf : forall {TX AF:Type} (f:TFormula TX AF) b,
        fst (rxcnf b f) = xcnf b f.

    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 t t' u,
        deduce t t' = Some u -> forall env,
        eval' env t -> eval' env t' -> 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.

    Lemma eval_cnf_ff : forall env, eval_cnf env cnf_ff <-> False.

    Lemma eval_cnf_tt : forall env, eval_cnf env cnf_tt <-> True.

    Lemma eval_cnf_and_opt : forall env x y, eval_cnf env (and_cnf_opt x y) <-> eval_cnf env (and_cnf x 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 eval_cnf_cons_iff : 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').

  Lemma or_cnf_opt_correct : forall env f f', eval_cnf env (or_cnf_opt f f') <-> eval_cnf env (or_cnf f f').

  Variable eval : Env -> Term -> Prop.

  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.