Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype finset.
Require Import tactics base.

Import Prenex Implicits.

Definition var := nat.

Inductive form :=
  Var : var -> form
| NegVar : var -> form
| And : form -> form -> form
| Or : form -> form -> form
.

Lemma eq_form_dec : forall s t : form , { s = t } + { s <> t}.

Definition form_eqMixin := EqMixin (compareP eq_form_dec).
Canonical Structure form_eqType := Eval hnf in @EqType form form_eqMixin.

Fixpoint pickle t :=
  match t with
    | Var n => Node (0,n) [::]
    | NegVar n => Node (1,n) [::]
    | And s t => Node (2,2) [:: pickle s ; pickle t]
    | Or s t => Node (3,3) [:: pickle s ; pickle t]
  end.

Fixpoint unpickle t :=
  match t with
    | Node (O,n) [::] => Some (Var n)
    | Node (1,n) [::] => Some (NegVar n)
    | Node (2,2) [:: s' ; t'] =>
      if unpickle s' is Some s then
        if unpickle t' is Some t then Some (And s t)
          else None else None
    | Node (3,3) [:: s' ; t'] =>
      if unpickle s' is Some s then
        if unpickle t' is Some t then Some (Or s t)
          else None else None
    | _ => None
  end.

Lemma inv : pcancel pickle unpickle.

Definition form_countMixin := PcanCountMixin inv.
Definition form_choiceMixin := CountChoiceMixin form_countMixin.
Canonical Structure form_ChoiceType := Eval hnf in ChoiceType form form_choiceMixin.
Canonical Structure form_CountType := Eval hnf in CountType form form_countMixin.

Definition model := var -> bool.

Reserved Notation "M |= s" (at level 35).
Fixpoint eval M s : bool :=
  match s with
    | Var x => M x
    | NegVar x => ~~ M x
    | And s t => M |= s && M |= t
    | Or s t => M |= s || M |= t
  end
where "M |= s" := (eval M s).

Definition valid s := forall M , M |= s.
Definition sat s := exists M , M |= s.
Definition equiv s t := forall M , M |= s = M |= t.

Fixpoint Neg (s : form) :=
  match s with
    | Var n => NegVar n
    | NegVar n => Var n
    | And s t => Or (Neg s) (Neg t)
    | Or s t => And (Neg s) (Neg t)
  end.

Lemma Neg_involutive s : Neg (Neg s) = s .

Lemma eval_Neg M s : M |= Neg s = ~~ M |= s.

Lemma valid_unsat s : valid s <-> ~ sat (Neg s).

Lemma equiv_valid s t : equiv s t <-> valid (Or (And s t) (And (Neg s) (Neg t))).

Lemma equiv_sat_valid s t : equiv s t -> (sat s <-> sat t) /\ (valid s <-> valid t).

Lemma dec_sat2valid : decidable sat -> decidable valid.

Lemma dec_valid2equiv : decidable valid -> decidable2 equiv.

Fixpoint synclos s :=
  s :: match s with
         | Var n => [::]
         | NegVar s => [::]
         | And s t => synclos s ++ synclos t
         | Or s t => synclos s ++ synclos t
       end.

Lemma synclos_refl s : s \in synclos s.

Lemma synclos_trans s t u : s \in synclos t -> t \in synclos u -> s \in synclos u.

Ltac synclos := apply : synclos_trans => // ; by rewrite /= in_cons mem_cat synclos_refl.

Implicit Arguments SeqSub [T s].
Notation "[ss s ; H ]" := (SeqSub s H) (at level 0).

Section FormulaUniverse.
  Variable s : form.
  Definition F := seq_sub (synclos s).

  Definition Hcond (t : F) (H : {set F}) :=
    match val t with
      | NegVar v => ~~ (Var v \in' H)
      | And u v => u \in' H && v \in' H
      | Or u v => u \in' H || v \in' H
      | _ => true
    end.

  Definition hintikka (H : {set F}) : bool := forallb t , (t \in H) ==> Hcond t H.

  Lemma model_existence (t : F) : (existsb H, hintikka H && (t \in H)) -> sat (val t).

  Lemma small_models (t : F) : sat (val t) -> existsb H , hintikka H && (t \in H).

  Theorem decidability t : sat (val t) <-> existsb H, hintikka H && (t \in H).

End FormulaUniverse.

Corollary sat_dec : decidable sat.

Corollary valid_dec : decidable valid.

Corollary equic_dec : decidable2 equiv.