# testfree-PDL.testfree_PDL_def

(* (c) Copyright Joachim Bard, Saarland University                        *)
(* Distributed under the terms of the CeCILL-B license                    *)

Require Import Relations.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.
From libs Require Import edone bcase fset base modular_hilbert.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

# Formulas

Definition var := nat.

Inductive prg :=
| pV of var
| pCon of prg & prg
| pCh of prg & prg
| pStar of prg.

Notation "p ^*" := (pStar p) (at level 30).
Notation "p0 ;; p1" := (pCon p0 p1) (at level 40, format "p0 ;; p1").
Notation "p0 + p1" := (pCh p0 p1).

Lemma eq_prg_dec (p q : prg) : { p = q } + { p <> q }.
Proof. decide equality. decide equality. Qed.

Inductive form :=
| fF
| fV of var
| fImp of form & form
| fAX of prg & form.

Notation "[ p ] s" := (fAX p s) (right associativity, at level 0, format "[ p ] s").

Lemma eq_form_dec (s t : form) : { s = t} + { s <> t}.
Proof. decide equality. apply eq_comparable. apply eq_prg_dec. Qed.

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

To use formulas and other types built around formulas as base type for the finite set libaray, we need to show that formulas are countable. We do this by embedding formulas into the Ssreflect's generic trees

Module formChoice.
Import GenTree.

Fixpoint pickle_prg (p : prg) :=
match p with
| pV v => Leaf v
| pCon p1 p2 => Node 0 [:: pickle_prg p1 ; pickle_prg p2]
| pCh p1 p2 => Node 1 [:: pickle_prg p1 ; pickle_prg p2]
| pStar p => Node 2 [:: pickle_prg p]
end.

Fixpoint unpickle_prg t :=
match t with
| Leaf v => Some (pV v)
| Node 0 [:: t ; t'] =>
obind (fun p => obind (fun p' => Some (pCon p p')) (unpickle_prg t')) (unpickle_prg t)
| Node 1 [:: t ; t'] =>
obind (fun p => obind (fun p' => Some (pCh p p')) (unpickle_prg t')) (unpickle_prg t)
| Node 2 [:: t] => obind (fun p => Some (pStar p)) (unpickle_prg t)
| _ => None
end.

Lemma pickle_prgP : pcancel pickle_prg unpickle_prg.
Proof.
elim => //= [p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IH].
- by rewrite IH0 IH1.
- by rewrite IH0 IH1.
- by rewrite IH.
Qed.

Fixpoint pickle (s : form) :=
match s with
| fV v => Leaf v
| fF => Node 0 [::]
| fImp s t => Node 1 [:: pickle s ; pickle t]
| fAX p s => Node 2 [:: pickle_prg p ; pickle s]
end.

Fixpoint unpickle t :=
match t with
| Leaf v => Some (fV v)
| Node 0 [::] => Some (fF)
| Node 1 [:: t ; t' ] =>
obind (fun s => obind (fun s' => Some (fImp s s')) (unpickle t')) (unpickle t)
| Node 2 [:: p ; t ] =>
obind (fun q => obind (fun s => Some (fAX q s)) (unpickle t)) (unpickle_prg p)
| _ => None
end.

Lemma pickleP : pcancel pickle unpickle.
Proof.
move => s. elim: s => //=.
- by move => s -> t ->.
- move => p f IH. by rewrite IH pickle_prgP.
Qed.

End formChoice.

Definition form_countMixin := PcanCountMixin formChoice.pickleP.
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.

Section Reachability.
Variables (X: Type) (e: var -> X -> X -> Prop).

Inductive star (R: X -> X -> Prop) (x : X) : X -> Prop :=
| Star0 : star R x x
| StarL y z : R x z -> star R z y -> star R x y.

Fixpoint reach (p: prg) : X -> X -> Prop :=
match p with
| pV a => e a
| pCon p0 p1 => (fun v w => exists2 u, reach p0 v u & reach p1 u w)
| pCh p0 p1 => (fun v w => reach p0 v w \/ reach p1 v w)
| pStar p => star (reach p)
end.

Variables (fX: finType) (f: var -> rel fX).

Definition starb (R: rel fX) : rel fX := connect R.

Fixpoint reachb (p: prg) : rel fX :=
match p with
| pV a => f a
| pCon p0 p1 => (fun v w => [exists (u | reachb p0 v u), reachb p1 u w])
| pCh p0 p1 => (fun v w => reachb p0 v w || reachb p1 v w)
| pStar p => (fun v w => starb (reachb p) v w)
end.

End Reachability.

## Models

We distinguish three classes of models
• raw models or transition systems (ts): The inductive satisfaction relation eval is defined on this class
• finite models (fmodel): models where the type of states is finite and everything else is decidable
• classical models, i.e., models where eval is logically decidable (cmodel): This is the largest class of models for which we can show soundness of the hilbert system.

Definition stable X Y (R : X -> Y -> Prop) := forall x y, ~ ~ R x y -> R x y.
Definition ldec X Y (R : X -> Y -> Prop) := forall x y, R x y \/ ~ R x y.

Record ts := TS {
state :> Type;
trans : var -> state -> state -> Prop;
label : var -> state -> Prop
}.
Prenex Implicits trans.

Record fmodel := FModel {
fstate :> finType;
ftrans : var -> rel fstate;
flabel : var -> pred fstate
}.
Prenex Implicits ftrans.

Make ts inferable for states of fmodels
Canonical ts_of_fmodel (M : fmodel) : ts := TS (@ftrans M) (@flabel M).
Coercion ts_of_fmodel : fmodel >-> ts.

Fixpoint eval (M: ts) (s: form) :=
match s with
| fF => (fun _ => False)
| fV x => label x
| fImp s t => (fun v => eval M s v -> eval M t v)
| fAX p s => (fun v => forall w, @reach M trans p v w -> eval M s w)
end.

Record cmodel := CModel { sts_of :> ts; modelP : ldec (@eval sts_of) }.

Section Hilbert.
Local Notation "s ---> t" := (fImp s t).

Inductive prv : form -> Prop :=
| rMP s t : prv (s ---> t) -> prv s -> prv t
| axK s t : prv (s ---> t ---> s)
| axS s t u : prv ((u ---> s ---> t) ---> (u ---> s) ---> u ---> t)
| axDN s : prv (((s ---> fF) ---> fF) ---> s)

| rNec p s : prv s -> prv ([p]s)
| axN p s t : prv ([p](s ---> t) ---> [p]s ---> [p]t)

| axConE p0 p1 s: prv ([p0;;p1]s ---> [p0][p1]s)
| axCon p0 p1 s: prv ([p0][p1]s ---> [p0;;p1]s)
| axChEl p0 p1 s: prv ([p0 + p1]s ---> [p0]s)
| axChEr p0 p1 s: prv ([p0 + p1]s ---> [p1]s)
| axCh p0 p1 s: prv ([p0]s ---> [p1]s ---> [p0 + p1]s)
| axStarEl p s : prv ([p^*]s ---> s)
| axStarEr p s : prv ([p^*]s ---> [p][p^*]s)
| rStar_ind p u s : prv (u ---> [p]u) -> prv (u ---> s) -> prv (u ---> [p^*]s)
.

Canonical Structure prv_mSystem := MSystem rMP axK axS.
Canonical Structure prv_pSystem := PSystem axDN.

Lemma rNorm p s t : prv (s ---> t) -> prv ([p]s ---> [p]t).
Proof. move => H. rule axN. exact: rNec. Qed.

Lemma axStar p s : prv (s ---> [p][p^*]s ---> [p^*]s).
Proof.
do 2 Intro. apply: rStar_ind.
- Rev* 0. drop. apply: rNorm. apply: bigAI => t. rewrite !inE.
case/orP; move/eqP => ->. exact: axStarEr. exact: axStarEl.
- Rev* 1. drop. exact: axI.
Qed.

Definition EX p s := (~~: [p] ~~: s).

Lemma axnEXF p : prv (~~: EX p Bot).
Proof. rewrite /EX. rewrite -> axDNE. apply: rNec. exact: axI. Qed.

Lemma rEXn p s t : prv (s ---> t) -> prv (EX p s ---> EX p t).
Proof. move => H. rule ax_contraNN. apply: rNorm. by rule ax_contraNN. Qed.

Lemma axDBD p s t : prv (EX p s ---> [p]t ---> EX p (s :/\: t)).
Proof.
do 3 Intro. Apply* 2. do 2 Rev. rewrite <- axN. apply: rNorm.
do 3 Intro. Apply* 1. ApplyH axAI.
Qed.

Lemma dmAX p s : prv (~~:[p]s ---> EX p (~~:s)).
Proof. rewrite /EX. rewrite <- (ax_contraNN _ ([p]s)). apply: rNorm. exact: axDN. Qed.

Lemma axABBA p s t : prv ([p]s :/\: [p]t ---> [p](s :/\: t)).
Proof.
rule axAcase. rewrite <- axN, <- axN. apply: rNec. exact: axAI.
Qed.

Lemma bigABBA (T: eqType) (xs: seq T) (F: T -> form) p :
prv ((\and_(s <- xs) [p](F s)) ---> [p](\and_(s <- xs) F s)).
Proof.
elim: xs => [|t xs IH].
- drop. rewrite big_nil. apply: rNec. exact: axI.
- rewrite !big_cons. rewrite -> IH, axABBA. exact: axI.
Qed.

Lemma axEOOE p s t : prv (EX p (s :\/: t) ---> EX p s :\/: EX p t).
Proof.
rewrite /EX. rewrite <- dmA. rewrite <- (ax_contraNN _ ([p]~~: (s:\/:t))).
rewrite -> axABBA. apply: rNorm. rewrite <- dmO. exact: axI.
Qed.

Lemma bigEOOE (T: eqType) (xs: seq T) (F: T -> form) p :
prv (EX p (\or_(s <- xs) F s) ---> \or_(s <- xs) EX p (F s)).
Proof.
elim: xs => [|t xs IH].
- rewrite !big_nil. exact: axnEXF.
- rewrite !big_cons. rewrite -> axEOOE, IH. exact: axI.
Qed.

Definition valid s := forall (M: cmodel) (v: M), eval s v.

Soundness

Lemma LI_sound s p: valid (s ---> [p]s) -> valid (s ---> [p^*]s).
Proof.
move => LI M v H w /= vRw. elim: vRw H => // {v w} v w u vRu _ IH H. apply: IH. exact: LI.
Qed.

Lemma soundness s: prv s -> valid s.
Proof.
elim => {s}; try by move => *; firstorder.
- move => s M v /=. case: (modelP s v); by auto.
- move => p s M v /=. apply. by constructor.
- move => p s M v H u vRu w uRw /=. apply: H. exact: StarL.
- move => p u s _ IHu _ IHs M v Hu w vRw. apply: IHs. exact: LI_sound.
Qed.

Lemma xm_soundness (xm: forall P, P \/ ~P) s: prv s -> forall (M: ts) (v: M), eval s v.
Proof.
move => H M v. assert (ldec_ts: ldec (@eval M)) by (move => *; apply: xm).
exact: (@soundness _ H (CModel ldec_ts)).
Qed.

End Hilbert.

## Soundness for Finite Models

Section FiniteModels.
Variables (M: fmodel).

Lemma starP p (v w: M) :
(forall (x y: M), reflect (reach ftrans p x y) (reachb ftrans p x y))
-> reflect (star (reach ftrans p) v w) (starb (reachb ftrans p) v w).
Proof.
move => H. unfold starb. apply: iffP connectP _ _.
- move => [A vw E]. elim: A v vw E => [v vw -> | x A IHA v /andP [vRx G] E] //. constructor.
apply: StarL. apply/H. exact: vRx. by apply: IHA.
- elim => [x | x y z xRz zRy [zy step E]]; first by exists [::] => //. exists (z::zy) => //=.
rewrite step andbT. by apply/H.
Qed.

Lemma reachP p (v w: M) : reflect (reach ftrans p v w) (reachb ftrans p v w).
Proof.
elim: p v w => [x|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp] v w /=.
- exact idP.
- apply: iffP (@exists_inP _ _ _) _ _; move => [u /IH0 H0 /IH1 H1]; by exists u.
- apply: iffP (@orP _ _) _ _; move => [/IH0 H | /IH1 H]; by auto.
- by apply: starP IHp.
Qed.

Fixpoint evalb (s: form) : pred M :=
match s with
| fF => xpred0
| fV x => flabel x
| fImp s t => (fun v => evalb s v ==> evalb t v)
| fAX p s => (fun v => [forall (w | reachb ftrans p v w), evalb s w])
end.

Lemma evalP (v: M) s : reflect (@eval M s v) (evalb s v).
Proof.
elim: s v => [|x|s IHs t IHt|p s IHs] v /=.
- by constructor.
- by apply: idP.
- apply: iffP (@implyP _ _) _ _ => H /IHs Hs; apply/IHt; by auto.
- apply: iffP (@forall_inP _ _ _) _ _ => H w /reachP vRw; apply/IHs; by auto.
Qed.

Lemma fin_modelP : ldec (@eval M).
Proof. move => s v. case: (decP (evalP v s)); auto. Qed.

End FiniteModels.

Definition cmodel_of_fmodel (M : fmodel) := CModel (@fin_modelP M).
Coercion cmodel_of_fmodel : fmodel >-> cmodel.

Theorem finite_soundness s : prv s -> forall (M: fmodel) (v: M), eval s v.
Proof. move => H M v. exact: (@soundness _ H (cmodel_of_fmodel M) v). Qed.

# Clauses and Hintikka Sets

## Signed Formulas

Definition sform := (form * bool) %type.
Notation "s ^-" := (s, false) (at level 20, format "s ^-").
Notation "s ^+" := (s, true) (at level 20, format "s ^+").

Definition body s := match s with [pV _]t^+ => t^+ | [pV _]t^- => t^- | _ => s end.

Definition positive (s: sform) := if s is t^+ then true else false.
Definition positives C := [fset s.1 | s <- [fset t in C | positive t]].

Lemma posE C s : (s \in positives C) = (s^+ \in C).
Proof.
apply/fimsetP/idP => [ [[t [|]]] | H].
- by rewrite inE /= andbT => ? ->.
- by rewrite inE /= andbF.
- exists (s^+) => //. by rewrite inE.
Qed.

Definition negative (s:sform) := ~~ positive s.
Definition negatives C := [fset s.1 | s <- [fset t in C | negative t]].

Lemma negE C s : (s \in negatives C) = (s^- \in C).
Proof.
apply/fimsetP/idP => [ [[t [|]]] | H].
- by rewrite inE /= andbC.
- by rewrite inE /negative andbT => ? ->.
- exists (s^-) => //. by rewrite inE.
Qed.

Definition isBox (a: var) s :=
match s with
| [pV b]t^+ => a == b
| _ => false
end.

Inductive isBox_spec a s : bool -> Type :=
| isBox_true t : s = [pV a]t^+ -> isBox_spec a s true
| isBox_false : isBox_spec a s false.

Lemma isBoxP a s : isBox_spec a s (isBox a s).
Proof.
move: s => [ [|?|? ?|[b|? ?|? ?|?] ?] [|]] /=; try constructor.
case H: (a == b); try constructor.
rewrite (eqP H). by exact: isBox_true.
Qed.

Definition isDia a s :=
match s with
| [pV b]t^- => a == b
| _ => false
end.

Inductive isDia_spec a s : bool -> Type :=
| isDia_true t : s = [pV a]t^- -> isDia_spec a s true
| isDia_false : isDia_spec a s false.

Lemma isDiaP a s : isDia_spec a s (isDia a s).
Proof.
move: s => [ [|?|? ?|[b|? ?|? ?|?] ?] [|]] /=; try constructor.
case H: (a == b); try constructor.
rewrite (eqP H). by exact: isDia_true.
Qed.

## Subformula Closure

Definition clause := {fset sform}.

Fixpoint ssubbox p s :=
[p]s |` match p with
| pV _ => fset0
| p0;;p1 => ssubbox p0 ([p1]s) `|` ssubbox p1 s
| p0 + p1 => ssubbox p0 s `|` ssubbox p1 s
| p^* => ssubbox p ([p^*]s)
end.

Fixpoint ssub s :=
s |` match s with
| fImp s t => ssub s `|` ssub t
| [p]s => ssub s `|` ssubbox p s
| _ => fset0
end.

Lemma ssubbox_refl p s : [p]s \in ssubbox p s.
Proof.
case: p => [v|p0 p1|p0 p1|p] /=; exact: fset1U1.
Qed.

Lemma ssub_refl s : s \in ssub s.
Proof.
case: s => [|x|s t|[a|p0 p1|p0 p1|p] s]; exact: fset1U1.
Qed.

Definition sf_closed' (F : {fset form}) s :=
match s with
| fImp s t => (s \in F) && (t \in F)
| [pV _]s => s \in F
| [p0;;p1]s => [&& [p0][p1]s \in F, [p1]s \in F & s \in F]
| [p0 + p1]s => [&& [p0]s \in F, [p1]s \in F & s \in F]
| [p^*]s => ([p][p^*]s \in F) && (s \in F)
| _ => true
end.

Arguments sf_closed' F !s.

Definition sf_closed (F :{fset form}) := forall s, s \in F -> sf_closed' F s.

Lemma sf_closed_box X p s : sf_closed X -> [p]s \in X -> s \in X.
Proof.
case: p => [a|p0 p1|p0 p1|p] sfc_X inX; move: (sfc_X _ inX) => //=; last (by case/andP);
by case/and3P.
Qed.

Lemma sf_closed'_mon X Y s : sf_closed' X s -> X `<=` Y -> sf_closed' Y s.
Proof.
elim: s => [|x|s IHs t IHt|[a|p0 p1|p0 p1|p] s IHs ] H /subP sub //=;
rewrite ?sub //=; by [case/andP: H | case/and3P: H].
Qed.

Lemma sf_ssubbox F p s : sf_closed F -> [p]s \in F -> ssubbox p s `<=` F.
Proof.
elim: p s => [v|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp] s sfc_F inF //=;
rewrite ?fsetU0 ?fsubUset ?fsub1 ?inF ?IH0 ?IH1 ?IHp ?andbT //=;
move: (sfc_F _ inF) => /=; bcase.
Qed.

Lemma sf_ssub F s : sf_closed F -> s \in F -> ssub s `<=` F.
Proof.
elim: s => [|p|s IHs t IHt|[a|p0 p1|p0 p1|p] s IHs] sfc_F inF //=;
rewrite ?fsetU0 ?fsubUset ?fsub1 ?inF ?IHs ?IHt ?sf_ssubbox ?andbT //=;
move: (sfc_F _ inF) => /=; bcase.
Qed.

Lemma sfc_ssubbox p s :
forall u, u \in ssubbox p s -> sf_closed' (ssub s `|` ssubbox p s) u.
Proof.
elim: p s => [a|p0 IH0 p1 IH1|p0 IH0 p1 IH1|p IHp] s /= u; rewrite !inE ?orbF.
- move/eqP => -> /=. by rewrite inE ssub_refl.
- case/or3P => [/eqP -> | H | H] /=.
+ by rewrite !inE !ssubbox_refl ssub_refl.
+ apply: sf_closed'_mon. apply: IH0 => //. rewrite !fsubUset fsub1 !inE ssubbox_refl.
by rewrite fsubUl /= !fsetUA fsubUr /= -fsetUA fsetUC -fsetUA fsubUl.
+ apply: sf_closed'_mon. apply IH1 => //. by rewrite fsubUset fsubUl !fsetUA fsubUr.
- case/or3P => [/eqP -> | H | H] /=.
+ by rewrite !inE !ssubbox_refl ssub_refl.
+ apply: sf_closed'_mon. apply: IH0 => //. rewrite fsubUset fsubUl fsetUA fsetUC.
by rewrite -fsetUA fsubUl.
+ apply: sf_closed'_mon. apply: IH1 => //. by rewrite fsubUset fsubUl !fsetUA fsubUr.
- case/orP => [/eqP -> | H] /=.
+ by rewrite !inE ssubbox_refl ssub_refl.
+ apply: sf_closed'_mon. apply: IHp => //. rewrite !fsubUset fsub1 !inE fsubUl fsetUA.
by rewrite fsubUr andbT andbC /= andbT andbb orbC.
Qed.

Lemma sfc_ssub s : sf_closed (ssub s).
Proof.
elim: s => [|x|s IHs t IHt|[a|p0 p1|p0 p1|p] s IHs] //= u; rewrite !inE ?orbF.
- by move/eqP => ->.
- by move/eqP => ->.
- case/orP => [/eqP -> | /orP [H | H]] /=.
+ by rewrite !inE !ssub_refl.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon (fsubUl _ _). exact: IHs.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon (fsubUr _ _). exact: IHt.
- case/orP => [/eqP ->|/orP [H|/eqP H]] /=.
+ by rewrite !inE !ssub_refl.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon (fsubUl _ _). exact: IHs.
+ apply: sf_closed'_mon (fsubUr _ _). by rewrite H /= inE ssub_refl.
- case/or3P => [/eqP -> | H | /or3P [/eqP -> | H | H]] /=;
try rewrite !inE !ssub_refl !ssubbox_refl //=.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon (fsubUl _ _). exact: IHs.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon. by apply: sfc_ssubbox.
apply/subP => x. rewrite !inE.
by move/orP => [/or3P [/eqP -> | inF | inF] | inF]; rewrite ?inF ?ssubbox_refl.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon. by apply: sfc_ssubbox.
by rewrite fsubUset fsubUl !fsetUA fsubUr.
- case/or3P => [/eqP -> | H | /or3P [/eqP -> | H | H]] /=;
try rewrite !inE !ssub_refl !ssubbox_refl //=.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon (fsubUl _ _). exact: IHs.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon. by apply: sfc_ssubbox.
rewrite fsubUset fsubUl /=. apply/subP => x inF. by rewrite !inE inF.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon. by apply: sfc_ssubbox.
by rewrite fsubUset fsubUl !fsetUA fsubUr.
- case/or4P => [/eqP ->| H |/eqP -> | H] /=; try by rewrite !inE ?ssub_refl ?ssubbox_refl.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon (fsubUl _ _). exact: IHs.
+ apply: sf_closed'_mon (fsubUr _ _). apply: sf_closed'_mon. by apply: sfc_ssubbox.
rewrite fsubUset fsetUA fsubUr andbT !fsubUset fsub1 !inE fsubUr -fsetUA fsubUl.
by rewrite andbT andbb.
Qed.

Lemma sfcU (X Y : {fset form}) : sf_closed X -> sf_closed Y -> sf_closed (X `|` Y).
Proof.
rewrite /sf_closed => /= H1 H2 s.
case/fsetUP => [/H1 | /H2] H; apply: sf_closed'_mon H _; auto with fset.
Qed.

Definition sfc F := \bigcup_(s in F) ssub s.

Lemma sfc_bigcup (T : choiceType) (X : {fset T}) F :
(forall s, sf_closed (F s)) -> sf_closed (\bigcup_(s in X) F s).
Proof.
move => H. apply: big_rec => [s|i D _]; by [rewrite inE | exact: sfcU].
Qed.

Lemma closed_sfc F : sf_closed (sfc F).
Proof. exact: sfc_bigcup sfc_ssub. Qed.

Lemma sub_sfc F : F `<=` (sfc F).
Proof.
apply/subP => s inC. apply/cupP.
exists s. by rewrite inC ssub_refl.
Qed.

Definition flipcl F : clause := \bigcup_(s in F) [fset s^+; s^-].

Lemma flipcl_refl F s : s \in F -> forall b, (s, b) \in flipcl F.
Proof. move => inF [|]; apply/cupP; exists s; by rewrite inF /= !inE. Qed.

Definition drop_sign (s: sform) := match s with (t, _) => t end.

Lemma flip_drop_sign F s : s \in flipcl F -> drop_sign s \in F.
Proof. case/cupP => t. case/and3P => inF _. rewrite !inE. case/orP; by move/eqP => ->. Qed.

Definition flip (s : sform) := match s with t^+ => t^- | t^- => t^+ end.

Definition flip_closed (C: clause) := forall s, s \in C -> (flip s) \in C.

Lemma closed_flipcl F : flip_closed (flipcl F).
Proof.
move => s. case/cupP => t. case/and3P => inF _ H. apply/cupP. exists t. move: H. rewrite inF /= !inE.
case/orP; move/eqP => -> /=; by rewrite eqxx.
Qed.

## Hintikka Sets

Definition lcons (L : clause) :=
(fF^+ \notin L) && [all s in L, flip s \notin L].

Section Hintikka.
Variable (F: {fset form}).
Hypothesis (sfc_F: sf_closed F).

Definition maximal (C: clause) := [all s in F, (s^+ \in C) || (s^- \in C)].

Definition hintikka' s (L: clause) :=
match s with
| fImp s t^+ => (s^- \in L) || (t^+ \in L)
| fImp s t^- => (s^+ \in L) && (t^- \in L)
| ([p0;;p1]s, b) => ([p0][p1]s, b) \in L
| [p0 + p1]s^+ => ([p0]s^+ \in L) && ([p1]s^+ \in L)
| [p0 + p1]s^- => ([p0]s^- \in L) || ([p1]s^- \in L)
| [p^*]s^+ => (s^+ \in L) && ([p][p^*]s^+ \in L)
| [p^*]s^- => (s^- \in L) || ([p][p^*]s^- \in L)
| _ => true
end.

Definition hintikka L := lcons L && [all s in L, hintikka' s L].

Variable (C: clause).
Hypothesis (hint_C: hintikka C).

Lemma hint_imp_pos s t : fImp s t^+ \in C -> s^- \in C \/ t^+ \in C.
Proof. case/andP: hint_C => _ /allP H inC. move: (H _ inC). case/orP; by auto. Qed.

Lemma hint_imp_neg s t : fImp s t^- \in C -> s^+ \in C /\ t^- \in C.
Proof. case/andP: hint_C => _ /allP H inC. move: (H _ inC). by case/andP. Qed.

Lemma hint_box_con p0 p1 s b : ([p0;;p1]s, b) \in C -> ([p0][p1]s, b) \in C.
Proof. case/andP: hint_C => _ /allP H inC. by move: (H _ inC). Qed.

Lemma hint_box_ch p0 p1 s : [p0 + p1]s^+ \in C -> [p0]s^+ \in C /\ [p1]s^+ \in C.
Proof. case/andP: hint_C => _ /allP H inC. move: (H _ inC). by case/andP. Qed.

Lemma hint_dia_ch p0 p1 s : [p0 + p1]s^- \in C -> [p0]s^- \in C \/ [p1]s^- \in C.
Proof. case/andP: hint_C => _ /allP H inC. move: (H _ inC). case/orP; by auto. Qed.

Lemma hint_box_star p s : [p^*]s^+ \in C -> s^+ \in C /\ [p][p^*]s^+ \in C.
Proof. case/andP: hint_C => _ /allP H inC. move: (H _ inC). by case/andP. Qed.

Lemma hint_dia_star p s : [p^*]s^- \in C -> s^- \in C \/ [p][p^*]s^- \in C.
Proof. case/andP: hint_C => _ /allP H inC. move: (H _ inC). case/orP; by auto. Qed.

End Hintikka.

## Request

Definition R a C := [fset body s | s <- [fset t in C | isBox a t]].

Lemma RE C a s : (s^+ \in R a C) = ([pV a]s^+ \in C).
Proof.
apply/fimsetP/idP => [ [t] | H].
- rewrite inE andbC. by case: (isBoxP a t) => //= t' -> /= ? [->].
- exists ([pV a]s^+) => //. by rewrite inE H /=.
Qed.

Lemma Rpos a s C : s^- \notin R a C.
Proof.
apply/negP. case/fimsetP => t. rewrite inE andbC.
by case (isBoxP a t) => // t' ->.
Qed.

Lemma RU a (C C' : clause) : R a (C `|` C') = (R a C `|` R a C').
Proof. by rewrite /R sepU fimsetU. Qed.

Lemma R1 a (s : sform) :
R a [fset s] = if s is [pV b]u^+ then if (a == b) then [fset u^+] else fset0 else fset0.
Proof.
case: s => [[|x|s t|[b|p0 p1|p0 p1|p] s] [|]]; rewrite /R sep1 /= ?fimset1 ?fimset0 //.
case: (a == b); by rewrite ?fimset1 ?fimset0.
Qed.

Lemma R0 a : R a fset0 = fset0.
Proof. by rewrite /R sep0 fimset0. Qed.

Lemma RinU F a : sf_closed F ->
forall C, C \in powerset (flipcl F) -> R a C \in powerset (flipcl F).
Proof.
move => sfc_F C. rewrite !powersetE => /subP H. apply/subP => s.
case: s => s [|]; last by rewrite (negbTE (Rpos _ _ _)).
rewrite RE /flipcl => /H /flip_drop_sign /= inF. apply/cupP. exists s. rewrite !inE /= andbT.
exact: (sfc_F [pV a]s).
Qed.

## Associated Formuals

Definition interp s := match s with (s, true) => s | (s, false) => @Neg prv_pSystem s end.

Notation "[ 'af' C ]" := (\and_(s <- C) interp s) (at level 0, format "[ 'af' C ]").

Lemma satA (M: cmodel) (w: M) (C: clause) :
(forall s, s \in C -> eval (interp s) w) <-> eval [af C] w.
Proof.
case: C => xs i /=.
change ((forall s, s \in xs -> eval (interp s) w) <-> eval [af xs] w).
elim: xs {i} => [|/= s xs IH]. rewrite big_nil forall_nil /=. tauto.
rewrite big_cons forall_cons IH {2}/And /=.
move: (modelP (interp s) w) (modelP [af xs] w); tauto.
Qed.

Lemma box_request (C: clause) a : prv ([af C] ---> [pV a][af R a C]).
Proof.
rewrite <- bigABBA. apply: bigAI. case => [s [|]]; last by rewrite (negbTE (Rpos _ _ _)).
rewrite RE. exact: bigAE.
Qed.

Fixpoint p_size (p: prg) :=
match p with
| pV _ => 1
| pCon p0 p1 => (p_size p0 + p_size p1).+1
| pCh p0 p1 => (p_size p0 + p_size p1).+1
| pStar p => (p_size p).+1
end.

Fixpoint f_size (s: form) :=
match s with
| fF => 1
| fV p => 1
| fImp s t => (f_size s + f_size t).+1
| fAX p s => (f_size s + p_size p).+1
end.

Lemma size_ssubbox p (s: form) : size (ssubbox p s) <= p_size p.
Proof.
elim: p s => // [a|p0 IH0 p1 IH1| p0 IH0 p1 IH1| p IHp] s.
- apply: leq_trans (fsizeU1 _ _) _. by rewrite sizes0.
- apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _.
- apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _.
- apply: leq_trans (fsizeU1 _ _) _. exact: leq_ltn_trans.
Qed.

Lemma size_ssub (s: form) : size (ssub s) <= f_size s.
Proof.
elim: s => //= [|p|s IHs t IHt|[a|p0 p1|p0 p1|p] s IHs ];
try by rewrite fsetU0 fset1Es.
- apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _.
- apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _ => /=.
apply: leq_add => //. apply: leq_trans (fsizeU1 _ _) _. by rewrite sizes0.
- apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _ => /=.
apply: leq_add => //. apply: leq_trans (fsizeU1 _ _) _. apply: leq_trans (fsizeU _ _) _.
apply: leq_add. exact: size_ssubbox. exact: size_ssubbox.
- apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _ => /=.
apply: leq_add => //. apply: leq_trans (fsizeU1 _ _) _. apply: leq_trans (fsizeU _ _) _.
apply: leq_add. exact: size_ssubbox. exact: size_ssubbox.
- apply: leq_trans (fsizeU1 _ _) _. apply: leq_ltn_trans (fsizeU _ _) _ => /=.
apply: leq_add => //. apply: leq_trans (fsizeU1 _ _) _. exact: size_ssubbox.
Qed.

Lemma size_flipcl F : size (flipcl F) <= 2 * size F.
Proof.
rewrite /flipcl. elim (elements F) => [|s xs IH] /=.
- rewrite big_nil sizes0. done.
- rewrite big_cons. apply: leq_trans; first exact: fsizeU.
rewrite mulnS. apply: leq_add; last exact: IH.
apply: leq_trans; first exact: fsizeU1.
by rewrite fset1Es.
Qed.