# Library P

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

Import Prenex Implicits.

# Syntax

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.

We need to construct a countType instance for form. We do this by by providing an injectiton (and its inverse) into finitely branching trees. This is required to construct finite types from sequences of formulas

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.

# Semantics

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.

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

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

Propositon 2.1

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.

Syntactic Closuse

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.

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