# Syntax

Definition var := nat.

Inductive form :=
Var : var -> form
| Bot : form
| Imp : form -> form -> form
| Box : form -> form
| PBox : form -> form.

Notation "s ---> t" := (Imp s t) (at level 35, right associativity).
Definition Neg s := s ---> Bot.
Definition Top := Bot ---> Bot.
Notation "□" := Box (at level 0).
Notation "¬" := Neg (at level 0).
Notation "□+" := PBox (at level 0).

## A countType instance for formulas

We need a countType instance for formulas so that we can use it as a base type for Ssreflect's finite types and finite sets. This also allows us to use constructive choice for boolean predicates over formulas.

Fixpoint pickle t :=
match t with
| Var n => Node (0,n) [::]
| Bot => Node (1,1) [::]
| Imp s t => Node (4,4) [:: pickle s ; pickle t]
| Box s => Node (5,5) [:: pickle s]
| PBox s => Node (6,6) [:: pickle s]
end.

Fixpoint unpickle t :=
match t with
| Node (O,n) [::] => Some (Var n)
| Node (1,1) [::] => Some Bot
| Node (4,4) [:: s' ; t'] =>
if unpickle s' is Some s then
if unpickle t' is Some t then Some (Imp s t)
else None else None
| Node (5,5) [:: s'] =>
if unpickle s' is Some s then Some (Box s) else None
| Node (6,6) [:: s'] =>
if unpickle s' is Some s then Some (PBox s) else None
| _ => None
end.

Lemma inv : pcancel pickle unpickle.

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.

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.

## Subformulas

Fixpoint sub (s:form) :=
s :: match s with
| Var x => [::]
| Bot => [::]
| Imp s t => sub s ++ sub t
| Box t => sub t
| PBox t => sub t
end.

Lemma sub_refl s : s \in sub s.

Hint Rewrite in_cons in_nil mem_cat orbT orbF sub_refl eq_refl : synclos.

Ltac trans_tac :=
repeat first
[ intro | progress simpl in * | reflexivity
| progress autorewrite with synclos in *
| match goal with
| [ H : is_true false |- _] => discriminate H
| [ H : ?P -> ?Q , H0 : ?P |- _ ] => move: (H H0) => {H} H
| [ H : is_true (_ || _) |- _ ]=> case/orP : H
| [ H : is_true (_ == _) |- _ ] => move/eqP : H => H ; subst
| [ H : is_true ?e |- context[?e] ] => rewrite H
end].

Lemma sub_trans s t u : t \in sub s -> u \in sub t -> u \in sub s.