KM.Syntax.syntax

From stdpp Require Import base countable.
From Stdlib Require Import List Arith Ensembles.
Export ListNotations.

(* First, let us define propositional formulas. *)

(* TODO: parameterize with arbitrary countable type *)
Notation variable := nat.

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

(* We define negation and top. *)

Definition Neg (A : form) := Imp A (Bot).
Definition Top := Imp Bot Bot.

(* We use the following notations for modal formulas. *)

Notation "# p" := (Var p) (at level 1).
Notation "¬ φ" := (Imp φ Bot) (at level 75, φ at level 75).
Notation " ⊥ " := Bot.
Notation " ⊤ " := Top.
Notation " φ ∧ ψ" := (And φ ψ) (at level 80, ψ at level 80).
Notation " φ ∨ ψ" := (Or φ ψ) (at level 85, ψ at level 85).
Notation " φ → ψ" := (Imp φ ψ) (at level 99, ψ at level 200).
Notation "□ φ" := (Box φ) (at level 75, φ at level 75).
Notation "φ ↔ ψ" := ((φ → ψ) ∧ (ψ → φ)) (at level 95, ψ at next level).
Notation "⊥" := Bot (at level 0).

(* Next, we define the set of subformulas of a formula, and
    extend this notion to lists of formulas. *)

Fixpoint subform (φ : form) : Ensemble form :=
match φ with
| Var p => Singleton _ (Var p)
| ⊥ => Singleton _ ⊥
| ψ ∧ χ => Union _ (Singleton _ (ψ ∧ χ)) (Union _ (subform ψ) (subform χ))
| ψ ∨ χ => Union _ (Singleton _ (ψ ∨ χ)) (Union _ (subform ψ) (subform χ))
| ψ → χ => Union _ (Singleton _ (ψ → χ)) (Union _ (subform ψ) (subform χ))
| □ ψ => Union _ (Singleton _ (□ ψ)) (subform ψ)
end.

Lemma subform_id : forall φ, (subform φ) φ.
Proof.
destruct φ ; cbn. 1-2: split. all: left ; split.
Qed.

Fixpoint subformlist (φ : form) : list form :=
match φ with
| Var p => (Var p) :: nil
| ⊥ => [⊥]
| ψ ∧ χ => (ψ ∧ χ) :: (subformlist ψ) ++ (subformlist χ)
| ψ ∨ χ => (ψ ∨ χ) :: (subformlist ψ) ++ (subformlist χ)
| ψ → χ => (Imp ψ χ) :: (subformlist ψ) ++ (subformlist χ)
| □ ψ => (□ ψ) :: (subformlist ψ)
end.

Lemma subform_trans : forall φ ψ χ, List.In φ (subformlist ψ) ->
  List.In χ (subformlist φ) -> List.In χ (subformlist ψ).
Proof.
intros φ ψ χ. revert ψ χ φ. induction ψ.
- intros. simpl. simpl in H. destruct H ; subst ; auto.
- intros. simpl. simpl in H. destruct H ; subst ; auto.
- intros. simpl. simpl in H. destruct H ; subst ; auto.
  apply in_app_or in H ; destruct H. right. apply in_or_app ; left.
  apply IHψ1 with (φ:=φ) ; auto. right. apply in_or_app ; right.
  apply IHψ2 with (φ:=φ) ; auto.
- intros. simpl. simpl in H. destruct H ; subst ; auto.
  apply in_app_or in H ; destruct H. right. apply in_or_app ; left.
  apply IHψ1 with (φ:=φ) ; auto. right. apply in_or_app ; right.
  apply IHψ2 with (φ:=φ) ; auto.
- intros. simpl. simpl in H. destruct H ; subst ; auto.
  apply in_app_or in H ; destruct H. right. apply in_or_app ; left.
  apply IHψ1 with (φ:=φ) ; auto. right. apply in_or_app ; right.
  apply IHψ2 with (φ:=φ) ; auto.
- intros. simpl. simpl in H. destruct H ; subst ; auto. right.
  apply IHψ with (φ:=φ) ; auto.
Qed.

Global Instance form_eq_dec : EqDecision form.
Proof. intros x y. solve_decision. Defined.

Global Instance In_form_dec l (A : form): Decision (List.In A l).
Proof. intros. apply ListDec.In_dec, form_eq_dec. Defined.

(* We define the notion of uniform substitution. *)

Fixpoint subst (σ : variable -> form) (φ : form) : form :=
match φ with
| # p => (σ p)
| ⊥ => ⊥
| ψ ∧ χ => (subst σ ψ) ∧ (subst σ χ)
| ψ ∨ χ => (subst σ ψ) ∨ (subst σ χ)
| ψ → χ => (subst σ ψ) → (subst σ χ)
| □ ψ => □ (subst σ ψ)
end.

Definition first_subst ϕ ψ := subst (fun n => match n with | 0 => ϕ | S n => # (S n) end) ψ.

Lemma first_subst_idem ϕ : ϕ = first_subst #0 ϕ.
Proof.
induction ϕ ; cbn ; unfold first_subst in * ; auto.
2-4: rewrite <- IHϕ1, <- IHϕ2 ; auto.
destruct n ; cbn ; auto.
rewrite <- IHϕ; auto.
Qed.

Fixpoint list_Imp (A : form) (l : list form) : form :=
match l with
 | nil => A
 | h :: t => h → (list_Imp A t)
end.

Definition Box_list (l : list form) : list form := map Box l.