KM.Algebra.alg_soundness

From Stdlib Require Import List Ensembles.

Require Import syntax.
Require Import KM_Algebras.
Require Import algebraic_semantic.
Require Import KMH_export.

Section Soundness.

Soundness of KM w.r.t. algebraic semantics

Axioms are all higher than one in any algebras with any interpretation.

Lemma Axioms_one : forall ϕ, Axioms ϕ -> forall A amap, aleq A one (interp A amap ϕ).
Proof.
intros ϕ Ax A amap.
inversion Ax.
+ inversion H ; cbn ; subst.
  - apply alg_A1.
  - apply alg_A2.
  - apply alg_A3.
  - apply alg_A4.
  - apply alg_A5.
  - apply alg_A6.
  - apply alg_A7.
  - apply alg_A8.
  - apply alg_A9.
+ inversion H ; cbn ; subst.
  - apply alg_MA1.
  - apply alg_MA2.
  - apply alg_MA3.
Qed.

Then, we proceed to show that KMH is sound with respect to the equational semantic consequence, with respect to the set of equations sEq: { x = ⊤ }

Definition sEq ϕ ψ := ϕ = # 0 /\ ψ = ⊤.

Theorem alg_soundness_KMH Γ ϕ : KMH_prv Γ ϕ -> alg_eqconseq sEq Γ ϕ.
Proof.
intro. induction H ; intros χ δ E ; inversion E ; subst ; cbn in * ; intros KM amap J.
- apply J. exists (# 0). exists ⊤.
  split ; auto. cbn. exists A ; auto.
- cbn. rewrite <- Top_rpczz. apply aleq_antisym. symmetry ; apply greatest.
  apply Axioms_one ; auto.
- cbn.
  assert (forall χ δ : form, (fun A B : form => exists C D : form ,
  sEq C D /\ (exists γ : form , Γ γ /\ first_subst γ C = A /\ first_subst γ D = B )) χ δ ->
  interp KM amap χ ≡ interp KM amap δ).
  { intros. destruct H1 as (C & D & H2 & F & H4 & H5 & H6). inversion H2 ; subst.
    cbn. pose (J F ⊤) ; cbn in e. apply e. exists (# 0), ⊤. split ; auto.
    exists F ; cbn ; repeat split ; auto. }
  pose (IHKMH_prv1 _ _ E _ _ H1). cbn in e.
  pose (IHKMH_prv2 _ _ E _ _ H1). cbn in e0.
  rewrite <- Top_rpczz. apply aleq_antisym. symmetry ; apply greatest.
  rewrite <- Top_rpczz in e,e0.
  apply aleq_trans with (meet (interp KM amap A) (rpc (interp KM amap A) (interp KM amap B))).
  * apply glb ; [ rewrite <- e0 | rewrite <- e] ; apply aleq_refl.
  * apply mp.
- cbn.
  assert (forall χ δ : form, (fun A B : form => exists C D : form ,
  sEq C D /\ (exists γ : form , (@Empty_set _) γ /\ first_subst γ C = A /\ first_subst γ D = B )) χ δ ->
  interp KM amap χ ≡ interp KM amap δ).
  { intros. destruct H0 as (C & D & H2 & F & H4 & H5 & H6). inversion H4. }
  pose (IHKMH_prv _ _ E _ _ H0). cbn in e. rewrite <- Top_rpczz.
  rewrite <- Top_rpczz in e.
  apply aleq_antisym. symmetry ; apply greatest.
  rewrite <- e. apply coreflec.
Qed.

End Soundness.