KM.Algebra.algebraic_semantic
From Stdlib Require Import List.
Require Import syntax.
Require Import KM_Algebras.
Section alg_semantics.
Require Import syntax.
Require Import KM_Algebras.
Section alg_semantics.
Fixpoint interp (A : KMalg) (amap : nat -> nodes) ϕ :=
match ϕ with
| # n => amap n
| ⊥ => zero
| ψ ∧ χ => meet (interp A amap ψ) (interp A amap χ)
| ψ ∨ χ => join (interp A amap ψ) (interp A amap χ)
| ψ → χ => rpc (interp A amap ψ) (interp A amap χ)
| □ ψ => box (interp A amap ψ)
end.
We define the notion of semantic consequence via a set of equations.
We need to explain how consecutions of equations (pairs of formulas) are
satisfied in an algebra with an interpretation.
Definition alg_eqconseq_eq (Eq : form -> form -> Prop) ϕ ψ := forall A amap,
(forall χ δ, Eq χ δ -> (interp A amap χ) ≡ (interp A amap δ)) ->
(interp A amap ϕ) ≡ (interp A amap ψ).
Then, we use the notion of satisfiability of equations to intepret consecutions
of formulas. To do so, we use equations in one place: the variable we use to
capture this one place is 0. We substitute the variable 0 in an equation in
one place using first_subst.
We finally get the consequence relation via equations. This consequence relation
on KM algebras captures KM.
Definition alg_eqconseq Eq Γ ϕ :=
forall χ δ, Eq χ δ ->
alg_eqconseq_eq (fun A B => exists C D, Eq C D /\ exists γ, Γ γ /\ first_subst γ C = A /\ first_subst γ D = B)
(first_subst ϕ χ) (first_subst ϕ δ).
End alg_semantics.
Section alg_sem_properties.
We show a technical lemma for the commutativity of
interp and first_subst.
Lemma first_subst_interp : forall A amap ϕ χ,
interp A amap (first_subst χ ϕ) =
interp A (fun n => match n with | 0 => (interp A amap χ) | _ => amap n end) ϕ.
Proof.
intros A amap ; induction ϕ ; intros ; cbn ; auto.
- cbn. destruct n ; auto.
- rewrite <- IHϕ1. rewrite <- IHϕ2. auto.
- rewrite <- IHϕ1. rewrite <- IHϕ2. auto.
- rewrite <- IHϕ1. rewrite <- IHϕ2. auto.
- rewrite <- IHϕ. auto.
Qed.
End alg_sem_properties.