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

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

History-Based Gentzen System for CTL

As for formulas, we need to show that the type of annotations is a countable type.

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).

gen_jmp placed last, so that the constructor tactic tries more specific rules first