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

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.
Proof. elim => //=; try solve [ move => ? -> ? -> //= | move => ? -> //= ].
Qed.

Lemma eq_form_dec : forall s t : form , { s = t } + { s <> t}.
Proof. decide equality; apply : eq_comparable. Qed.

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.

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.
Proof. case: s ; move => * //= ; by rewrite in_cons eq_refl. Qed.

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.
Proof. elim: s; trans_tac. Qed.