From stdpp Require Import countable.

Definition variable := nat.

Inductive form : Type :=
| Var : variable -> form
| Bot : form
| And : form -> form -> form
| Or : form -> form -> form
| Implies : form -> form -> form.

Fixpoint occurs_in (x : variable) (φ : form) :=
match φ with
| Var y => x = y
| Bot => False
| And φ ψ => (occurs_in x φ) \/ (occurs_in x ψ)
| Or φ ψ => (occurs_in x φ) \/ (occurs_in x ψ)
| Implies φ ψ => (occurs_in x φ) \/ (occurs_in x ψ)
end.

Notation "¬ φ" := (Implies φ Bot) (at level 75, φ at level 75).
Notation " ⊥ " := Bot.
Notation " ⊤ " := (Implies Bot Bot).
Notation " A ∧ B" := (And A B) (at level 80, B at level 80).
Notation " A ∨ B" := (Or A B) (at level 85, B at level 85).
Notation " A → B" := (Implies A B) (at level 99, B at level 200).
Infix " φ ⇔ ψ " := (And (Implies φ ψ) (Implies ψ φ)) (at level 100).
Global Instance fomula_bottom : base.Bottom form := Bot.

Global Coercion Var : variable >-> form.

Global Instance form_top : base.Top form := ⊤.

Global Instance form_eq_dec : EqDecision form.
Proof. solve_decision. Defined.

Section CountablyManyFormulas.

Local Fixpoint form_to_gen_tree (φ : form) : gen_tree nat :=
match φ with
| ⊥ => GenLeaf 0
| Var v => GenLeaf (1 + v)
| φ ∧ ψ => GenNode 0 [form_to_gen_tree φ ; form_to_gen_tree ψ]
| φ ∨ ψ => GenNode 1 [form_to_gen_tree φ ; form_to_gen_tree ψ]
| φ → ψ => GenNode 2 [form_to_gen_tree φ ; form_to_gen_tree ψ]
end.

Local Fixpoint gen_tree_to_form (t : gen_tree nat) : option form :=
match t with
| GenLeaf 0 => Some ⊥
| GenLeaf (S n) => Some (Var n)
| GenNode 0 [t1 ; t2] =>
    gen_tree_to_form t1 ≫= fun φ => gen_tree_to_form t2 ≫= fun ψ =>
      Some (φ ∧ ψ)
| GenNode 1 [t1 ; t2] =>
    gen_tree_to_form t1 ≫= fun φ => gen_tree_to_form t2 ≫= fun ψ =>
      Some (φ ∨ ψ)
| GenNode 2 [t1 ; t2] =>
    gen_tree_to_form t1 ≫= fun φ => gen_tree_to_form t2 ≫= fun ψ =>
      Some (φ → ψ)
| _=> None
end.

Global Instance form_count : Countable form.
Proof.
  apply inj_countable with (f := form_to_gen_tree) (g := gen_tree_to_form).
  intro φ; induction φ; simpl; trivial; now rewrite IHφ1, IHφ2.
Defined.

End CountablyManyFormulas.

Inductive subform : form -> form -> Prop :=
| SubEq : ∀ φ, subform φ φ
| SubAnd : ∀ φ ψ1 ψ2, (subform φ ψ1 + subform φ ψ2) -> subform φ (ψ1 ∧ ψ2)
| SubOr : ∀ φ ψ1 ψ2, (subform φ ψ1 + subform φ ψ2) -> subform φ (ψ1 ∨ ψ2)
| SubImpl : ∀ φ ψ1 ψ2, (subform φ ψ1 + subform φ ψ2) -> subform φ (ψ1→ ψ2).
Local Hint Constructors subform : dyckhoff.

Fixpoint weight (φ : form) : nat := match φ with
| ⊥ => 1
| Var _ => 1
| φ ∧ ψ => 2 + weight φ + weight ψ
| φ ∨ ψ => 3 + weight φ + weight ψ
| φ → ψ => 1 + weight φ + weight ψ
end.

Lemma weight_pos φ : weight φ > 0.
Proof. destruct φ; simpl; lia. Qed.

Definition weight_ind (P : form -> Type) :
 (forall ψ, (∀ φ, (weight φ < weight ψ) -> P φ) -> P ψ) ->
 (∀ φ, P φ).
Proof.
  intros Hc φ. remember (weight φ) as w.
  assert(Hw : weight φ ≤ w) by now subst. clear Heqw.
  revert φ Hw. induction w; intros φ Hw.
  - destruct φ; simpl in Hw; lia.
  - destruct φ; simpl in Hw; trivial;
    apply Hc; intros φ Hw'; apply IHw; simpl in Hw'; lia.
Defined.

Definition form_order φ ψ := weight φ > weight ψ.

Notation "φ ≺f ψ" := (form_order ψ φ) (at level 149).