KM.Algebra.KMH_algebraizable
From Stdlib Require Import Ensembles.
Require Import syntax.
Require Import KM_Algebras.
Require Import algebraic_semantic.
Require Import KMH_export.
Require Import alg_soundness.
Require Import KMH_alg_completeness.
Section algebraizable.
Require Import syntax.
Require Import KM_Algebras.
Require Import algebraic_semantic.
Require Import KMH_export.
Require Import alg_soundness.
Require Import KMH_alg_completeness.
Section algebraizable.
Algebraisability of KM
Theorem KMH_Alg1 Γ ϕ : KMH_prv Γ ϕ <-> alg_eqconseq sEq Γ ϕ.
Proof.
split ; [apply alg_soundness_KMH | apply alg_completeness_KMH ; auto].
Qed.
The second shows that the equational consequence relation over KM-algebras
is mirrored in KM.
Theorem KMH_Alg2 Eq ϕ ψ : alg_eqconseq_eq Eq ϕ ψ <->
KMH_prv (fun χ => exists δ γ, Eq δ γ /\ χ = (δ ↔ γ)) (ϕ ↔ ψ).
Proof.
split ; intro.
- apply alg_completeness_KMH ; auto.
+ intros χ γ H0 A amap H1. inversion H0 ; subst ; cbn in *.
rewrite <- Top_rpczz.
pose (H A amap). rewrite e ; clear e.
* apply aleq_antisym.
-- apply high_one.
-- apply glb.
++ apply ord_resid. apply meet_elim2.
++ apply ord_resid. apply meet_elim2.
* intros.
assert (interp A amap (χ ↔ δ) ≡ interp A amap ⊤).
{ apply H1. exists (# 0), ⊤. split ; unfold sEq ; auto.
exists (χ ↔ δ) ; cbn ; repeat split.
exists χ,δ ; auto. }
cbn in H3. apply aleq_antisym.
-- eapply aleq_trans.
++ apply glb.
** apply high_one.
** apply aleq_refl.
++ apply ord_resid. rewrite <- Top_rpczz in H3. rewrite <- H3. apply meet_elim1.
-- eapply aleq_trans.
++ apply glb.
** apply high_one.
** apply aleq_refl.
++ apply ord_resid. rewrite <- Top_rpczz in H3. rewrite <- H3. apply meet_elim2.
- intros A amap H0. apply alg_soundness_KMH in H.
assert (alg_soundness.sEq # 0 ⊤).
{ unfold alg_soundness.sEq ; split ; auto. }
pose (H (# 0) ⊤ H1 A amap). cbn in e.
rewrite <- Top_rpczz in e.
assert (meet (rpc (interp A amap ϕ) (interp A amap ψ))
(rpc (interp A amap ψ) (interp A amap ϕ)) ≡ one).
{ apply e. intros χ δ (γ & ρ & H2 & ω & (σ & φ & (H4 & H7)) & (H5 & H6)).
inversion H2 ; subst ; cbn in *.
apply H0 in H4. rewrite H4. rewrite <- Top_rpczz.
apply aleq_antisym.
+ apply high_one.
+ apply glb.
* apply ord_resid. apply meet_elim2.
* apply ord_resid. apply meet_elim2. }
apply aleq_antisym.
+ eapply aleq_trans.
* apply glb.
-- apply high_one.
-- apply aleq_refl.
* apply ord_resid. rewrite <- H2. apply meet_elim1.
+ eapply aleq_trans.
* apply glb.
-- apply high_one.
-- apply aleq_refl.
* apply ord_resid. rewrite <- H2. apply meet_elim2.
Qed.
The third property shows that the defining equations
for algebraisability are respected in KM.
Theorem KMH_Alg3 ϕ : KMH_prv (Singleton _ ϕ) (ϕ ↔ ⊤) /\
KMH_prv (Singleton _ (ϕ ↔ ⊤)) ϕ.
Proof.
split.
- eapply MP.
+ eapply MP.
* eapply MP.
-- apply Ax ; left ; eapply IA8 ; reflexivity.
-- eapply Thm_irrel.
* eapply MP.
-- apply And_Imp.
-- eapply MP.
++ apply Thm_irrel.
++ apply Id ; split.
+ apply prv_Top.
- eapply MP.
+ eapply MP.
* apply Ax ; left ; eapply IA7 ; reflexivity.
* apply Id ; split.
+ apply prv_Top.
Qed.
The fourth property shows that the equivalence formulas
for algebraisability are respected on KM-algebras.
Theorem KMH_Alg4 ϕ ψ : alg_eqconseq_eq (fun δ γ => δ = ϕ /\ γ = ψ) (ϕ ↔ ψ) ⊤ /\
alg_eqconseq_eq (fun δ γ => δ = (ϕ ↔ ψ) /\ γ = ⊤) ϕ ψ.
Proof.
split.
- intros A amap H. cbn. rewrite <- Top_rpczz.
assert (interp A amap ϕ ≡ interp A amap ψ).
{ apply H ; auto. }
rewrite H0.
apply aleq_antisym.
+ apply high_one.
+ apply glb.
* apply ord_resid. apply meet_elim2.
* apply ord_resid. apply meet_elim2.
- intros A amap H.
assert (interp A amap (ϕ ↔ ψ) ≡ interp A amap ⊤).
{ apply H ; auto. }
cbn in H0. rewrite <- Top_rpczz in H0.
apply aleq_antisym.
+ eapply aleq_trans.
* apply glb.
-- apply high_one.
-- apply aleq_refl.
* apply ord_resid. rewrite <- H0. apply meet_elim1.
+ eapply aleq_trans.
* apply glb.
-- apply high_one.
-- apply aleq_refl.
* apply ord_resid. rewrite <- H0. apply meet_elim2.
Qed.
End algebraizable.