Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import choice fintype finfun finset path fingraph bigop.

Require Import edone bcase fset.

Require Import base CTL_def.

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

Inductive annot :=
| aAU of form * form * {fset clause}
| aAXU of form * form * {fset clause}
| aAR of form * form * {fset clause}
| aAXR of form * form * {fset clause}
| aVoid.

Lemma eq_annot_dec (E1 E2 : annot) : {E1 = E2} + {E1 <> E2}.
Proof. decide equality; apply: eq_comparable. Qed.

Definition annot_eqMixin := EqMixin (compareP eq_annot_dec).
Canonical Structure annot_eqType := Eval hnf in @EqType annot annot_eqMixin.

Definition aR (E : annot) := if E is aAXU (p, H) then aAU (p,H) else aVoid.

Module Annot.
  Definition pickle A :=
    match A with
      | aAU s => (1,pickle s)
      | aAXU s => (2,pickle s)
      | aVoid => (3,0)
      | aAR s => (4,pickle s)
      | aAXR s => (5,pickle s)
    end.

  Prenex Implicits Some.

  Definition unpickle p :=
    match p with
      | (1,n) => obind (Some \o aAU) (unpickle n)
      | (2,n) => obind (Some \o aAXU) (unpickle n)
      | (3,_) => Some aVoid
      | (4,n) => obind (Some \o aAR) (unpickle n)
      | (5,n) => obind (Some \o aAXR) (unpickle n)
      | _ => None
    end.

  Lemma pickleP : pcancel pickle unpickle.
  Proof. move => s. case: s => //= p; by rewrite pickleK. Qed.
End Annot.

Definition annot_countMixin := PcanCountMixin (Annot.pickleP).
Definition annot_choiceMixin := CountChoiceMixin annot_countMixin.
Canonical Structure annot_choiceType := Eval hnf in ChoiceType annot annot_choiceMixin.
Canonical Structure annot_CountType := Eval hnf in CountType annot annot_countMixin.

Implicit Types (C : clause) (E : annot).

Definition pr' E :=
  match E with
    | aVoid => fset0
    | aAU (s, t, H) => [fset fAU s t^+]
    | aAXU (s, t, H) => [fset fAX (fAU s t)^+]
    | aAR (s, t, H) => [fset fAR s t^-]
    | aAXR (s, t, H) => [fset fAX (fAR s t)^-]
  end.

Definition pr A := let: (C,E) := A in pr' E `|` C.

Lemma prV C : pr (C, aVoid) = C.
Proof. by rewrite /= fset0U. Qed.

Inductive tab : clause * annot -> Prop :=
| tab_F C E :
    tab (fF^+ |` C, E)
| tab_p p C E :
    tab ([fset fV p^+ , fV p^- & C], E)
| tab_Ip s t C E :
    tab (s^- |` C, E) -> tab (t^+ |` C, E) -> tab (fImp s t^+ |` C, E)
| tab_In s t C E :
    tab ([fset s^+ , t^- & C], E) -> tab (fImp s t^- |` C, E)
| tab_AXn s C E :
    tab (s^- |` R C, aR E) -> tab (fAX s^- |` C , E)
| tab_AUp s t C E :
    tab (t^+ |` C,E) -> tab ([fset s^+, fAX (fAU s t)^+ & C],E) -> tab (fAU s t^+ |` C,E)
| tab_AUn s t C E :
    tab ([fset s^-, t^- & C], E) -> tab ([fset t^-, fAX (fAU s t)^- & C],E) -> tab (fAU s t^- |` C, E)
| tab_foc s t C :
    tab (C,aAU (s, t, fset0)) -> tab (fAU s t^+ |` C , aVoid)
| tab_AUh s t H C :
    tab (t^+ |` C, aVoid) -> tab (s^+ |` C, aAXU (s, t, C |` H)) -> tab (C, aAU (s, t, H))
| tab_rep s t H C :
    tab (C, aAU (s, t, C |` H))
| tab_jmp C E :
    tab (R C, aR E) -> tab (C,E)
| tab_ARp s t C E :
    tab ([fset s^+, t^+ & C],E) -> tab ([fset t^+, fAX (fAR s t)^+ & C],E) -> tab (fAR s t^+ |` C,E)
| tab_ARn s t C E :
    tab (t^- |` C,E) -> tab ([fset s^-, fAX (fAR s t)^- & C],E) -> tab (fAR s t^- |` C,E)
| tab_foc' s t C :
    tab (C, aAR (s,t,fset0)) -> tab (fAR s t^- |` C, aVoid)
| tab_ARh s t H C :
    tab (t^- |` C, aVoid) -> tab (s^- |` C, aAXR (s,t,C |` H)) -> tab (C, aAR (s,t,H))
| tab_rep' s t H C :
    tab (C,aAR(s,t,C |` H))
| tab_aAXR s t H C :
    tab (R C, aAR (s,t,H)) -> tab (C, aAXR (s,t,H))
.