KM.Sequent.Equiv_KMH
From Stdlib Require Import Ensembles.
Require Import syntax syntax_facts. (* Syntax *)
Require Import Sequents SequentProps Order Cut DecisionProcedure. (* Sequent calculus *)
Require Import KMH_export. (* Hilbert calculus *)
Section Soundness.
(* First we need some theorems about KMH_prv relating to the
syntactic definitions pertaining to G4CK. *)
Lemma open_boxes_GL_rule (Γ : env) φ :
KMH_prv (fun γ => γ ∈ ((⊗ Γ) • (□ φ))) φ -> KMH_prv (fun γ => γ ∈ Γ) (□ φ).
Proof.
intro H.
assert (KMH_prv (Ensembles.Union _ (λ γ : form, γ ∈ ⊗ Γ) (Ensembles.Singleton _ (□ φ))) φ).
{ eapply KMH_monot ; [ exact H | intros ψ Hin].
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
- left ; ms.
- apply gmultiset_elem_of_singleton in H0 ; subst ; right ; ms. }
apply KMH_Deduction_Theorem in H0. apply K_rule in H0.
apply MP with (□ (□ φ → φ)).
- eapply MP ; [ apply Ax ; right ; eapply K ; reflexivity | apply Nec ; apply Ax ; right ; eapply L ; reflexivity].
- apply (KMH_comp _ _ H0) ; intros ψ [χ [H1 H2]] ; subst.
assert (χ ∈ (⊗ Γ)) by ms.
apply elem_of_open_boxes in H2 ; destruct H2 as [H2 | [δ [H2 H3]]] ; subst.
+ eapply MP ; [ apply Axcoreflection | apply Id ; ms].
+ apply Id ; ms.
Qed.
Lemma list_disj_perm : forall l l', l ≡ₚ l' -> forall Γ, KMH_prv Γ (list_disj l) -> KMH_prv Γ (list_disj l').
Proof.
induction 1 ; cbn ; intros ; auto.
- apply ND_OrE with x (list_disj l) ; [auto | apply Ax ; left ; eapply IA3 ; reflexivity | ].
apply KMH_Deduction_Theorem. apply ND_OrI2. apply IHPermutation ; apply Id ; right ; split.
- apply ND_OrE with y (x ∨ list_disj l) ; auto.
+ apply KMH_Deduction_Theorem ; apply ND_OrI2,ND_OrI1,Id ; right ; split.
+ apply KMH_Deduction_Theorem. apply ND_OrE with x (list_disj l).
* apply Id ; right ; split.
* apply Ax ; left ; eapply IA3 ; reflexivity.
* apply KMH_Deduction_Theorem. do 2 apply ND_OrI2 ; apply Id ; right ; split.
Qed.
Theorem G4KM_sound_KMH Γ Δ : Γ ⊢ Δ -> KMH_prv (fun γ => γ ∈ Γ) (list_disj (elements Δ)) (* could use "disjunction" from optimisation on Δ *).
Proof.
induction 1.
(* Atom *)
- apply list_disj_in_prv with (# p).
+ apply elem_of_list_In. apply gmultiset_elem_of_elements ; ms.
+ apply Id ; unfold Ensembles.In ; ms.
(* ExFalso *)
- apply ND_BotE. apply Id ; unfold Ensembles.In ; ms.
(* AndR *)
- apply list_disj_perm with ((φ ∧ ψ) :: elements Δ) ; [ rewrite elements_env_add ; auto | cbn ].
apply list_disj_perm with (l':=φ :: elements Δ) in IHProvable1 ; [ cbn in IHProvable1 | rewrite elements_env_add ; auto].
apply list_disj_perm with (l':=ψ :: elements Δ) in IHProvable2 ; [ cbn in IHProvable2 | rewrite elements_env_add ; auto].
apply ND_OrE with φ (list_disj (elements Δ)) ; auto.
+ apply ND_OrE with ψ (list_disj (elements Δ)) ; auto.
* do 2 apply KMH_Deduction_Theorem. apply ND_OrI1,ND_AndI ; apply Id ; [ right ; split | left ; right ; split].
* do 2 apply KMH_Deduction_Theorem. apply ND_OrI2 ; apply Id ; left ; right ; split.
+ apply KMH_Deduction_Theorem ; apply ND_OrI2 ; apply Id ; right ; split.
(* AndL *)
- apply KMH_monot with (Γ:= Ensembles.Union _ (fun γ => γ ∈ Γ) (Ensembles.Singleton _ (φ ∧ ψ))).
+ apply KMH_Detachment_Theorem. eapply MP ; [ apply Imp_And | ].
do 2 (apply KMH_Deduction_Theorem).
apply (KMH_monot _ _ (IHProvable)).
intros χ Hχ. unfold Ensembles.In in *.
apply gmultiset_elem_of_disj_union in Hχ ; destruct Hχ.
* apply gmultiset_elem_of_disj_union in H0 ; destruct H0.
-- do 2 left ; auto.
-- left ; right. ms.
* right ; ms.
+ intros χ Hχ. unfold Ensembles.In in *. inversion Hχ ; subst.
* ms.
* inversion H0 ; subst ; ms.
(* OrR *)
- apply list_disj_perm with ((φ ∨ ψ) :: elements Δ) ; [ rewrite elements_env_add ; auto | cbn ].
apply list_disj_perm with (l':=ψ :: φ :: elements Δ) in IHProvable ; [ cbn in IHProvable | do 2 rewrite elements_env_add ; auto].
apply ND_OrE with ψ (φ ∨ list_disj (elements Δ)) ; auto.
+ apply KMH_Deduction_Theorem. apply ND_OrI1,ND_OrI2 ; apply Id ; right ; split.
+ apply KMH_Deduction_Theorem. apply ND_OrE with φ (list_disj (elements Δ)) ; auto.
* apply Id ; right ; split.
* apply KMH_Deduction_Theorem. apply ND_OrI1,ND_OrI1 ; apply Id ; right ; split.
* apply KMH_Deduction_Theorem. apply ND_OrI2 ; apply Id ; right ; split.
(* OrL *)
- apply ND_OrE with φ ψ.
+ apply Id. apply gmultiset_elem_of_disj_union ; right.
apply gmultiset_elem_of_singleton ; auto.
+ apply KMH_Deduction_Theorem. apply (KMH_monot _ _ IHProvable1).
intros χ Hχ. apply gmultiset_elem_of_disj_union in Hχ ; destruct Hχ.
* left ; ms.
* right ; ms.
+ apply KMH_Deduction_Theorem. apply (KMH_monot _ _ IHProvable2).
intros χ Hχ. apply gmultiset_elem_of_disj_union in Hχ ; destruct Hχ.
* left ; ms.
* right ; ms.
(* ImpR *)
- apply list_disj_perm with ((φ → ψ) :: elements Δ) ; [ rewrite elements_env_add ; auto | cbn ].
apply list_disj_perm with (l':=ψ :: elements Δ) in IHProvable1 ; [ cbn in IHProvable1 | rewrite elements_env_add ; auto].
apply list_disj_perm with (l':=ψ :: []) in IHProvable2 ; [ cbn in IHProvable2 | rewrite elements_env_add ; auto].
apply ND_OrE with φ (φ → ψ).
+ apply ND_OrE with φ (φ → φ → ψ).
* eapply MP ; [ apply Ax ; right ; eapply NA ; reflexivity | ].
apply open_boxes_GL_rule. apply KMH_Deduction_Theorem.
apply KMH_monot with (λ γ : form, γ ∈ (⊗ Γ • φ)).
-- apply ND_OrE with ψ ⊥ ; [ auto | apply imp_Id_gen | apply EFQ].
-- intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
++ left ; ms.
++ right ; ms.
* apply KMH_Deduction_Theorem. apply ND_OrI1. apply Id ; right ; split.
* apply KMH_Deduction_Theorem. apply ND_OrI2. apply KMH_Deduction_Theorem.
eapply MP ; [ eapply MP ; [ apply Id ; left ; right ; split | apply Id ; right ; split ] | apply Id ; right ; split ].
+ apply KMH_Deduction_Theorem. apply ND_OrE with ψ (list_disj (elements Δ)).
* apply KMH_monot with (λ γ : form, γ ∈ (Γ • φ)) ; [ auto | ].
intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
-- left ; ms.
-- right ; ms.
* apply KMH_Deduction_Theorem. apply ND_OrI1. apply KMH_Deduction_Theorem.
apply Id ; left ; right ; split.
* apply KMH_Deduction_Theorem ; apply ND_OrI2 ; apply Id ; right ; split.
+ apply KMH_Deduction_Theorem. apply ND_OrI1 ; apply Id ; right ; split.
(* AtomImpL *)
- apply (KMH_comp _ _ IHProvable). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply gmultiset_elem_of_disj_union in H0 ; destruct H0.
* apply Id ; ms.
* apply Id ; ms.
+ eapply MP ; apply Id.
* apply gmultiset_elem_of_disj_union ; right.
apply gmultiset_elem_of_singleton in H0 ; subst.
apply gmultiset_elem_of_singleton ; auto.
* ms.
(* AndImpL *)
- apply (KMH_comp _ _ IHProvable). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply Id ; ms.
+ apply gmultiset_elem_of_singleton in H0 ; subst.
eapply MP ; [apply And_Imp | apply Id]. ms.
(* OrImpL *)
- apply (KMH_comp _ _ IHProvable). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply gmultiset_elem_of_disj_union in H0 ; destruct H0.
* apply Id ; ms.
* apply gmultiset_elem_of_singleton in H0 ; subst.
apply KMH_Deduction_Theorem.
eapply MP ; [ apply Id ; left ; apply gmultiset_elem_of_disj_union ; right ; apply gmultiset_elem_of_singleton ; auto | ].
apply ND_OrI1 ; apply Id ; right ; split.
+ apply gmultiset_elem_of_singleton in H0 ; subst.
apply KMH_Deduction_Theorem.
eapply MP ; [ apply Id ; left ; apply gmultiset_elem_of_disj_union ; right ; apply gmultiset_elem_of_singleton ; auto | ].
apply ND_OrI2 ; apply Id ; right ; split.
(* ImpImpL *)
- apply list_disj_perm with (l':=φ2 :: elements Δ) in IHProvable1 ; [ cbn in IHProvable1 | rewrite elements_env_add ; auto].
apply list_disj_perm with (l':=φ2 :: []) in IHProvable2 ; [ cbn in IHProvable2 | rewrite elements_env_add ; auto].
assert (J: KMH_prv (λ γ : form, γ ∈ (Γ • (φ3 ∨ (list_disj (elements Δ))))) (list_disj (elements Δ))).
{ apply ND_OrE with φ3 (list_disj (elements Δ)).
- apply Id ; ms.
- apply KMH_Deduction_Theorem ; apply (KMH_comp _ _ IHProvable3) ; intros χ Hin ; apply Id.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ left ; ms.
+ right ; ms.
- apply imp_Id_gen. }
apply (KMH_comp _ _ J). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply Id ; ms.
+ apply gmultiset_elem_of_singleton in H2 ; subst.
apply MP with ((φ1 → φ2) ∨ list_disj (elements Δ)).
* apply KMH_Deduction_Theorem. apply ND_OrE with (φ1 → φ2) (list_disj (elements Δ)).
-- apply Id ; right ; split.
-- apply KMH_Deduction_Theorem. apply ND_OrI1.
apply MP with (φ1 → φ2) ; [ apply Id ; left ; left ; ms | apply Id ; right ; split ].
-- apply KMH_Deduction_Theorem,ND_OrI2,Id ; right ; split.
* apply ND_OrE with φ1 (φ1 → φ2).
-- apply ND_OrE with φ1 (φ1 → φ1 → φ2).
++ eapply MP ; [ apply Ax ; right ; eapply NA ; reflexivity | ].
apply open_boxes_GL_rule. apply KMH_Deduction_Theorem.
apply KMH_monot with (λ γ : form, γ ∈ (⊗ Γ • ((φ1 → φ2) → φ3) • φ1)).
** apply ND_OrE with φ2 ⊥ ; [ | apply imp_Id_gen | apply EFQ].
apply (KMH_comp _ _ IHProvable2).
intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
--- apply gmultiset_elem_of_disj_union in H2 ; destruct H2.
+++ apply Id ; ms.
+++ apply gmultiset_elem_of_singleton in H2 ; subst.
apply KMH_Deduction_Theorem.
apply MP with (φ1 → φ2) ; [ apply Id ; left ; ms | apply KMH_Deduction_Theorem,Id ; left ; right ; split].
--- apply gmultiset_elem_of_singleton in H2 ; subst. apply Id ; ms.
** intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
--- left ; ms.
--- right ; ms.
++ apply KMH_Deduction_Theorem. apply ND_OrI1. apply Id ; right ; split.
++ apply KMH_Deduction_Theorem. apply ND_OrI2. apply KMH_Deduction_Theorem.
eapply MP ; [ eapply MP ; [ apply Id ; left ; right ; split | apply Id ; right ; split ] | apply Id ; right ; split ].
-- apply KMH_Deduction_Theorem. apply ND_OrE with φ2 (list_disj (elements Δ)).
++ apply KMH_monot with (λ γ : form, γ ∈ (Γ • ((φ1 → φ2) → φ3) • φ1)) ; [ | ].
** apply (KMH_comp _ _ IHProvable1).
intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
--- apply gmultiset_elem_of_disj_union in H2 ; destruct H2.
+++ apply Id ; ms.
+++ apply gmultiset_elem_of_singleton in H2 ; subst.
apply KMH_Deduction_Theorem.
apply MP with (φ1 → φ2) ; [ apply Id ; left ; ms | apply KMH_Deduction_Theorem,Id ; left ; right ; split].
--- apply gmultiset_elem_of_singleton in H2 ; subst. apply Id ; ms.
** intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
--- left ; ms.
--- right ; ms.
++ apply KMH_Deduction_Theorem. apply ND_OrI1. apply KMH_Deduction_Theorem.
apply Id ; left ; right ; split.
++ apply KMH_Deduction_Theorem ; apply ND_OrI2 ; apply Id ; right ; split.
-- apply KMH_Deduction_Theorem. apply ND_OrI1 ; apply Id ; right ; split.
(* BoxImpL *)
- apply (KMH_comp _ _ IHProvable2). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply Id ; ms.
+ apply gmultiset_elem_of_singleton in H1 ; subst.
eapply MP ; [apply Id ; apply gmultiset_elem_of_disj_union ; right ; apply gmultiset_elem_of_singleton ; auto | ].
apply open_boxes_GL_rule. rewrite open_boxes_add ; cbn.
apply list_disj_perm with (l':=[φ1]) in IHProvable1 ; [ cbn in IHProvable1 | rewrite elements_env_add ; auto].
apply KMH_comp with (λ γ : form, γ ∈ (⊗ Γ • □ φ1 • φ2)).
* apply ND_OrE with φ1 ⊥ ; [ auto | apply imp_Id_gen | apply EFQ].
* intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
-- apply gmultiset_elem_of_disj_union in H1 ; destruct H1.
++ apply Id ; ms.
++ apply gmultiset_elem_of_singleton in H1 ; subst. apply Id ; ms.
-- apply gmultiset_elem_of_singleton in H1 ; subst.
apply MP with (□ φ1); apply Id ; ms.
(* BoxR *)
- apply list_disj_perm with ((□ φ) :: elements Δ) ; [ rewrite elements_env_add ; auto | cbn ].
apply list_disj_perm with (l':= [φ]) in IHProvable ; [ cbn in IHProvable | rewrite elements_env_add ; auto].
apply ND_OrI1. apply open_boxes_GL_rule. apply ND_OrE with φ ⊥ ; [ auto | apply imp_Id_gen | apply EFQ].
Qed.
End Soundness.
Section Completeness.
(* Then we can show that if there is an axiomatic proof, then
there exists (in Prop) a sequent proof. *)
Theorem G4KM_compl_KMH Γ φ : KMH_prv (fun γ => γ ∈ Γ) φ -> Γ ⊢ ∅ • φ.
Proof.
enough (KMH_prv (fun γ => γ ∈ Γ) φ -> exists (P : Γ ⊢ ∅ • φ), True).
{ intro D. apply H in D. destruct (Proof_tree_dec (elements Γ) [φ]).
+ rewrite (proper_Provable _ (list_to_set_disj (elements Γ))) with (y:=∅ • φ) ;
[ destruct s ; auto | rewrite <- elements_list_to_set_disj ; auto | auto].
+ exfalso. destruct D as [D Vrai] ; auto. apply f.
rewrite (proper_Provable _ Γ) with (y:=∅ • φ) ; auto. rewrite <- elements_list_to_set_disj ; auto. }
{ intro. remember (λ γ : form, γ ∈ Γ) as Γ'.
revert Γ HeqΓ'. induction H ; intros ; subst.
(* Id *)
- assert (Γ0 ⊢KM ∅ • A). exhibit H 0. apply generalised_axiom.
exists H0 ; auto.
(* Axiom *)
- destruct H as [H | H] ; [ destruct H ; subst | destruct H ; subst].
+ assert (Γ0 ⊢KM ∅ • (A0 → B → A0)). do 2 (apply Int_ImpR).
exchl 0 ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • ((A0 → B → C) → (A0 → B) → A0 → C)).
{ do 3 (apply Int_ImpR). exchl 0. apply ImpL.
* apply generalised_axiom.
* exchl 1 ; exchl 0. apply ImpL.
-- exchl 0 ; apply generalised_axiom.
-- apply ImpL ; apply generalised_axiom. }
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (A0 → A0 ∨ B)). apply Int_ImpR,OrR ; exchr 0 ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (B → A0 ∨ B)). apply Int_ImpR,OrR ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • ((A0 → C) → (B → C) → A0 ∨ B → C)).
{ do 3 (apply Int_ImpR). apply OrL.
* exchl 1 ; exchl 0. apply ImpL ; apply generalised_axiom.
* exchl 0. apply ImpL ; apply generalised_axiom. }
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (A0 ∧ B → A0)). apply Int_ImpR,AndL ; exchl 0 ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (A0 ∧ B → B)). apply Int_ImpR,AndL ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • ((A0 → B) → (A0 → C) → A0 → B ∧ C)).
{ do 3 (apply Int_ImpR). apply AndR.
* exchl 1 ; exchl 0. apply ImpL ; apply generalised_axiom.
* exchl 0. apply ImpL ; apply generalised_axiom. }
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (⊥ → A0)). apply Int_ImpR,ExFalso. exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (□ (A0 → B) → □ A0 → □ B)). do 2 (apply Int_ImpR). apply BoxR.
repeat rewrite open_boxes_add ; auto ; simpl (⊙ (□ (A0 → B))). simpl (⊙ (□ A0)).
exchl 1 ; exchl 0 ; apply ImpL ; try apply generalised_axiom. exchl 0 ; apply generalised_axiom.
exists ; auto.
+ assert (Γ0 ⊢KM ∅ • ((□ A0 → A0) → A0)). apply Int_ImpR.
apply ImpLBox ; apply generalised_axiom.
exists ; auto.
+ assert (Γ0 ⊢KM ∅ • (□ A0 → B ∨ (B → A0))).
{ apply Int_ImpR. apply OrR. apply ImpR.
* exchr 0 ; apply generalised_axiom.
* rewrite open_boxes_add ; simpl (⊙ (□ A0)) ; exchl 0 ; apply generalised_axiom. }
exists ; auto.
(* MP *)
- destruct (IHKMH_prv2 Γ0) ; auto. destruct (IHKMH_prv1 Γ0) ; auto.
assert (Γ0 ⊢KM ∅ • B).
{ apply additive_cut with (A → B) ; auto.
apply ImpL ; [ exchr 0 ; apply weakeningr ; auto | apply generalised_axiom]. }
exists H3 ; auto.
(* Nec *)
- destruct (IHKMH_prv (⊗ ∅)) ; auto.
+ apply Extensionality_Ensembles ; split ; intros x Hx.
* inversion Hx.
* unfold Ensembles.In in Hx. apply elem_of_open_boxes in Hx as [H0 | [ψ [H0 H1]]] ; subst ; [inversion H0 | inversion H1].
+ assert (Γ0 ⊢KM ∅ • □ A). rewrite <- gmultiset_disj_union_right_id. apply generalised_weakeninglL.
apply BoxR ; apply weakeningl ; auto.
exists H1 ; auto. }
Qed.
End Completeness.
Require Import syntax syntax_facts. (* Syntax *)
Require Import Sequents SequentProps Order Cut DecisionProcedure. (* Sequent calculus *)
Require Import KMH_export. (* Hilbert calculus *)
Section Soundness.
(* First we need some theorems about KMH_prv relating to the
syntactic definitions pertaining to G4CK. *)
Lemma open_boxes_GL_rule (Γ : env) φ :
KMH_prv (fun γ => γ ∈ ((⊗ Γ) • (□ φ))) φ -> KMH_prv (fun γ => γ ∈ Γ) (□ φ).
Proof.
intro H.
assert (KMH_prv (Ensembles.Union _ (λ γ : form, γ ∈ ⊗ Γ) (Ensembles.Singleton _ (□ φ))) φ).
{ eapply KMH_monot ; [ exact H | intros ψ Hin].
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
- left ; ms.
- apply gmultiset_elem_of_singleton in H0 ; subst ; right ; ms. }
apply KMH_Deduction_Theorem in H0. apply K_rule in H0.
apply MP with (□ (□ φ → φ)).
- eapply MP ; [ apply Ax ; right ; eapply K ; reflexivity | apply Nec ; apply Ax ; right ; eapply L ; reflexivity].
- apply (KMH_comp _ _ H0) ; intros ψ [χ [H1 H2]] ; subst.
assert (χ ∈ (⊗ Γ)) by ms.
apply elem_of_open_boxes in H2 ; destruct H2 as [H2 | [δ [H2 H3]]] ; subst.
+ eapply MP ; [ apply Axcoreflection | apply Id ; ms].
+ apply Id ; ms.
Qed.
Lemma list_disj_perm : forall l l', l ≡ₚ l' -> forall Γ, KMH_prv Γ (list_disj l) -> KMH_prv Γ (list_disj l').
Proof.
induction 1 ; cbn ; intros ; auto.
- apply ND_OrE with x (list_disj l) ; [auto | apply Ax ; left ; eapply IA3 ; reflexivity | ].
apply KMH_Deduction_Theorem. apply ND_OrI2. apply IHPermutation ; apply Id ; right ; split.
- apply ND_OrE with y (x ∨ list_disj l) ; auto.
+ apply KMH_Deduction_Theorem ; apply ND_OrI2,ND_OrI1,Id ; right ; split.
+ apply KMH_Deduction_Theorem. apply ND_OrE with x (list_disj l).
* apply Id ; right ; split.
* apply Ax ; left ; eapply IA3 ; reflexivity.
* apply KMH_Deduction_Theorem. do 2 apply ND_OrI2 ; apply Id ; right ; split.
Qed.
Theorem G4KM_sound_KMH Γ Δ : Γ ⊢ Δ -> KMH_prv (fun γ => γ ∈ Γ) (list_disj (elements Δ)) (* could use "disjunction" from optimisation on Δ *).
Proof.
induction 1.
(* Atom *)
- apply list_disj_in_prv with (# p).
+ apply elem_of_list_In. apply gmultiset_elem_of_elements ; ms.
+ apply Id ; unfold Ensembles.In ; ms.
(* ExFalso *)
- apply ND_BotE. apply Id ; unfold Ensembles.In ; ms.
(* AndR *)
- apply list_disj_perm with ((φ ∧ ψ) :: elements Δ) ; [ rewrite elements_env_add ; auto | cbn ].
apply list_disj_perm with (l':=φ :: elements Δ) in IHProvable1 ; [ cbn in IHProvable1 | rewrite elements_env_add ; auto].
apply list_disj_perm with (l':=ψ :: elements Δ) in IHProvable2 ; [ cbn in IHProvable2 | rewrite elements_env_add ; auto].
apply ND_OrE with φ (list_disj (elements Δ)) ; auto.
+ apply ND_OrE with ψ (list_disj (elements Δ)) ; auto.
* do 2 apply KMH_Deduction_Theorem. apply ND_OrI1,ND_AndI ; apply Id ; [ right ; split | left ; right ; split].
* do 2 apply KMH_Deduction_Theorem. apply ND_OrI2 ; apply Id ; left ; right ; split.
+ apply KMH_Deduction_Theorem ; apply ND_OrI2 ; apply Id ; right ; split.
(* AndL *)
- apply KMH_monot with (Γ:= Ensembles.Union _ (fun γ => γ ∈ Γ) (Ensembles.Singleton _ (φ ∧ ψ))).
+ apply KMH_Detachment_Theorem. eapply MP ; [ apply Imp_And | ].
do 2 (apply KMH_Deduction_Theorem).
apply (KMH_monot _ _ (IHProvable)).
intros χ Hχ. unfold Ensembles.In in *.
apply gmultiset_elem_of_disj_union in Hχ ; destruct Hχ.
* apply gmultiset_elem_of_disj_union in H0 ; destruct H0.
-- do 2 left ; auto.
-- left ; right. ms.
* right ; ms.
+ intros χ Hχ. unfold Ensembles.In in *. inversion Hχ ; subst.
* ms.
* inversion H0 ; subst ; ms.
(* OrR *)
- apply list_disj_perm with ((φ ∨ ψ) :: elements Δ) ; [ rewrite elements_env_add ; auto | cbn ].
apply list_disj_perm with (l':=ψ :: φ :: elements Δ) in IHProvable ; [ cbn in IHProvable | do 2 rewrite elements_env_add ; auto].
apply ND_OrE with ψ (φ ∨ list_disj (elements Δ)) ; auto.
+ apply KMH_Deduction_Theorem. apply ND_OrI1,ND_OrI2 ; apply Id ; right ; split.
+ apply KMH_Deduction_Theorem. apply ND_OrE with φ (list_disj (elements Δ)) ; auto.
* apply Id ; right ; split.
* apply KMH_Deduction_Theorem. apply ND_OrI1,ND_OrI1 ; apply Id ; right ; split.
* apply KMH_Deduction_Theorem. apply ND_OrI2 ; apply Id ; right ; split.
(* OrL *)
- apply ND_OrE with φ ψ.
+ apply Id. apply gmultiset_elem_of_disj_union ; right.
apply gmultiset_elem_of_singleton ; auto.
+ apply KMH_Deduction_Theorem. apply (KMH_monot _ _ IHProvable1).
intros χ Hχ. apply gmultiset_elem_of_disj_union in Hχ ; destruct Hχ.
* left ; ms.
* right ; ms.
+ apply KMH_Deduction_Theorem. apply (KMH_monot _ _ IHProvable2).
intros χ Hχ. apply gmultiset_elem_of_disj_union in Hχ ; destruct Hχ.
* left ; ms.
* right ; ms.
(* ImpR *)
- apply list_disj_perm with ((φ → ψ) :: elements Δ) ; [ rewrite elements_env_add ; auto | cbn ].
apply list_disj_perm with (l':=ψ :: elements Δ) in IHProvable1 ; [ cbn in IHProvable1 | rewrite elements_env_add ; auto].
apply list_disj_perm with (l':=ψ :: []) in IHProvable2 ; [ cbn in IHProvable2 | rewrite elements_env_add ; auto].
apply ND_OrE with φ (φ → ψ).
+ apply ND_OrE with φ (φ → φ → ψ).
* eapply MP ; [ apply Ax ; right ; eapply NA ; reflexivity | ].
apply open_boxes_GL_rule. apply KMH_Deduction_Theorem.
apply KMH_monot with (λ γ : form, γ ∈ (⊗ Γ • φ)).
-- apply ND_OrE with ψ ⊥ ; [ auto | apply imp_Id_gen | apply EFQ].
-- intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
++ left ; ms.
++ right ; ms.
* apply KMH_Deduction_Theorem. apply ND_OrI1. apply Id ; right ; split.
* apply KMH_Deduction_Theorem. apply ND_OrI2. apply KMH_Deduction_Theorem.
eapply MP ; [ eapply MP ; [ apply Id ; left ; right ; split | apply Id ; right ; split ] | apply Id ; right ; split ].
+ apply KMH_Deduction_Theorem. apply ND_OrE with ψ (list_disj (elements Δ)).
* apply KMH_monot with (λ γ : form, γ ∈ (Γ • φ)) ; [ auto | ].
intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
-- left ; ms.
-- right ; ms.
* apply KMH_Deduction_Theorem. apply ND_OrI1. apply KMH_Deduction_Theorem.
apply Id ; left ; right ; split.
* apply KMH_Deduction_Theorem ; apply ND_OrI2 ; apply Id ; right ; split.
+ apply KMH_Deduction_Theorem. apply ND_OrI1 ; apply Id ; right ; split.
(* AtomImpL *)
- apply (KMH_comp _ _ IHProvable). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply gmultiset_elem_of_disj_union in H0 ; destruct H0.
* apply Id ; ms.
* apply Id ; ms.
+ eapply MP ; apply Id.
* apply gmultiset_elem_of_disj_union ; right.
apply gmultiset_elem_of_singleton in H0 ; subst.
apply gmultiset_elem_of_singleton ; auto.
* ms.
(* AndImpL *)
- apply (KMH_comp _ _ IHProvable). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply Id ; ms.
+ apply gmultiset_elem_of_singleton in H0 ; subst.
eapply MP ; [apply And_Imp | apply Id]. ms.
(* OrImpL *)
- apply (KMH_comp _ _ IHProvable). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply gmultiset_elem_of_disj_union in H0 ; destruct H0.
* apply Id ; ms.
* apply gmultiset_elem_of_singleton in H0 ; subst.
apply KMH_Deduction_Theorem.
eapply MP ; [ apply Id ; left ; apply gmultiset_elem_of_disj_union ; right ; apply gmultiset_elem_of_singleton ; auto | ].
apply ND_OrI1 ; apply Id ; right ; split.
+ apply gmultiset_elem_of_singleton in H0 ; subst.
apply KMH_Deduction_Theorem.
eapply MP ; [ apply Id ; left ; apply gmultiset_elem_of_disj_union ; right ; apply gmultiset_elem_of_singleton ; auto | ].
apply ND_OrI2 ; apply Id ; right ; split.
(* ImpImpL *)
- apply list_disj_perm with (l':=φ2 :: elements Δ) in IHProvable1 ; [ cbn in IHProvable1 | rewrite elements_env_add ; auto].
apply list_disj_perm with (l':=φ2 :: []) in IHProvable2 ; [ cbn in IHProvable2 | rewrite elements_env_add ; auto].
assert (J: KMH_prv (λ γ : form, γ ∈ (Γ • (φ3 ∨ (list_disj (elements Δ))))) (list_disj (elements Δ))).
{ apply ND_OrE with φ3 (list_disj (elements Δ)).
- apply Id ; ms.
- apply KMH_Deduction_Theorem ; apply (KMH_comp _ _ IHProvable3) ; intros χ Hin ; apply Id.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ left ; ms.
+ right ; ms.
- apply imp_Id_gen. }
apply (KMH_comp _ _ J). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply Id ; ms.
+ apply gmultiset_elem_of_singleton in H2 ; subst.
apply MP with ((φ1 → φ2) ∨ list_disj (elements Δ)).
* apply KMH_Deduction_Theorem. apply ND_OrE with (φ1 → φ2) (list_disj (elements Δ)).
-- apply Id ; right ; split.
-- apply KMH_Deduction_Theorem. apply ND_OrI1.
apply MP with (φ1 → φ2) ; [ apply Id ; left ; left ; ms | apply Id ; right ; split ].
-- apply KMH_Deduction_Theorem,ND_OrI2,Id ; right ; split.
* apply ND_OrE with φ1 (φ1 → φ2).
-- apply ND_OrE with φ1 (φ1 → φ1 → φ2).
++ eapply MP ; [ apply Ax ; right ; eapply NA ; reflexivity | ].
apply open_boxes_GL_rule. apply KMH_Deduction_Theorem.
apply KMH_monot with (λ γ : form, γ ∈ (⊗ Γ • ((φ1 → φ2) → φ3) • φ1)).
** apply ND_OrE with φ2 ⊥ ; [ | apply imp_Id_gen | apply EFQ].
apply (KMH_comp _ _ IHProvable2).
intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
--- apply gmultiset_elem_of_disj_union in H2 ; destruct H2.
+++ apply Id ; ms.
+++ apply gmultiset_elem_of_singleton in H2 ; subst.
apply KMH_Deduction_Theorem.
apply MP with (φ1 → φ2) ; [ apply Id ; left ; ms | apply KMH_Deduction_Theorem,Id ; left ; right ; split].
--- apply gmultiset_elem_of_singleton in H2 ; subst. apply Id ; ms.
** intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
--- left ; ms.
--- right ; ms.
++ apply KMH_Deduction_Theorem. apply ND_OrI1. apply Id ; right ; split.
++ apply KMH_Deduction_Theorem. apply ND_OrI2. apply KMH_Deduction_Theorem.
eapply MP ; [ eapply MP ; [ apply Id ; left ; right ; split | apply Id ; right ; split ] | apply Id ; right ; split ].
-- apply KMH_Deduction_Theorem. apply ND_OrE with φ2 (list_disj (elements Δ)).
++ apply KMH_monot with (λ γ : form, γ ∈ (Γ • ((φ1 → φ2) → φ3) • φ1)) ; [ | ].
** apply (KMH_comp _ _ IHProvable1).
intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
--- apply gmultiset_elem_of_disj_union in H2 ; destruct H2.
+++ apply Id ; ms.
+++ apply gmultiset_elem_of_singleton in H2 ; subst.
apply KMH_Deduction_Theorem.
apply MP with (φ1 → φ2) ; [ apply Id ; left ; ms | apply KMH_Deduction_Theorem,Id ; left ; right ; split].
--- apply gmultiset_elem_of_singleton in H2 ; subst. apply Id ; ms.
** intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
--- left ; ms.
--- right ; ms.
++ apply KMH_Deduction_Theorem. apply ND_OrI1. apply KMH_Deduction_Theorem.
apply Id ; left ; right ; split.
++ apply KMH_Deduction_Theorem ; apply ND_OrI2 ; apply Id ; right ; split.
-- apply KMH_Deduction_Theorem. apply ND_OrI1 ; apply Id ; right ; split.
(* BoxImpL *)
- apply (KMH_comp _ _ IHProvable2). intros χ Hin.
apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
+ apply Id ; ms.
+ apply gmultiset_elem_of_singleton in H1 ; subst.
eapply MP ; [apply Id ; apply gmultiset_elem_of_disj_union ; right ; apply gmultiset_elem_of_singleton ; auto | ].
apply open_boxes_GL_rule. rewrite open_boxes_add ; cbn.
apply list_disj_perm with (l':=[φ1]) in IHProvable1 ; [ cbn in IHProvable1 | rewrite elements_env_add ; auto].
apply KMH_comp with (λ γ : form, γ ∈ (⊗ Γ • □ φ1 • φ2)).
* apply ND_OrE with φ1 ⊥ ; [ auto | apply imp_Id_gen | apply EFQ].
* intros χ Hin. apply gmultiset_elem_of_disj_union in Hin ; destruct Hin.
-- apply gmultiset_elem_of_disj_union in H1 ; destruct H1.
++ apply Id ; ms.
++ apply gmultiset_elem_of_singleton in H1 ; subst. apply Id ; ms.
-- apply gmultiset_elem_of_singleton in H1 ; subst.
apply MP with (□ φ1); apply Id ; ms.
(* BoxR *)
- apply list_disj_perm with ((□ φ) :: elements Δ) ; [ rewrite elements_env_add ; auto | cbn ].
apply list_disj_perm with (l':= [φ]) in IHProvable ; [ cbn in IHProvable | rewrite elements_env_add ; auto].
apply ND_OrI1. apply open_boxes_GL_rule. apply ND_OrE with φ ⊥ ; [ auto | apply imp_Id_gen | apply EFQ].
Qed.
End Soundness.
Section Completeness.
(* Then we can show that if there is an axiomatic proof, then
there exists (in Prop) a sequent proof. *)
Theorem G4KM_compl_KMH Γ φ : KMH_prv (fun γ => γ ∈ Γ) φ -> Γ ⊢ ∅ • φ.
Proof.
enough (KMH_prv (fun γ => γ ∈ Γ) φ -> exists (P : Γ ⊢ ∅ • φ), True).
{ intro D. apply H in D. destruct (Proof_tree_dec (elements Γ) [φ]).
+ rewrite (proper_Provable _ (list_to_set_disj (elements Γ))) with (y:=∅ • φ) ;
[ destruct s ; auto | rewrite <- elements_list_to_set_disj ; auto | auto].
+ exfalso. destruct D as [D Vrai] ; auto. apply f.
rewrite (proper_Provable _ Γ) with (y:=∅ • φ) ; auto. rewrite <- elements_list_to_set_disj ; auto. }
{ intro. remember (λ γ : form, γ ∈ Γ) as Γ'.
revert Γ HeqΓ'. induction H ; intros ; subst.
(* Id *)
- assert (Γ0 ⊢KM ∅ • A). exhibit H 0. apply generalised_axiom.
exists H0 ; auto.
(* Axiom *)
- destruct H as [H | H] ; [ destruct H ; subst | destruct H ; subst].
+ assert (Γ0 ⊢KM ∅ • (A0 → B → A0)). do 2 (apply Int_ImpR).
exchl 0 ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • ((A0 → B → C) → (A0 → B) → A0 → C)).
{ do 3 (apply Int_ImpR). exchl 0. apply ImpL.
* apply generalised_axiom.
* exchl 1 ; exchl 0. apply ImpL.
-- exchl 0 ; apply generalised_axiom.
-- apply ImpL ; apply generalised_axiom. }
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (A0 → A0 ∨ B)). apply Int_ImpR,OrR ; exchr 0 ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (B → A0 ∨ B)). apply Int_ImpR,OrR ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • ((A0 → C) → (B → C) → A0 ∨ B → C)).
{ do 3 (apply Int_ImpR). apply OrL.
* exchl 1 ; exchl 0. apply ImpL ; apply generalised_axiom.
* exchl 0. apply ImpL ; apply generalised_axiom. }
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (A0 ∧ B → A0)). apply Int_ImpR,AndL ; exchl 0 ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (A0 ∧ B → B)). apply Int_ImpR,AndL ; apply generalised_axiom.
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • ((A0 → B) → (A0 → C) → A0 → B ∧ C)).
{ do 3 (apply Int_ImpR). apply AndR.
* exchl 1 ; exchl 0. apply ImpL ; apply generalised_axiom.
* exchl 0. apply ImpL ; apply generalised_axiom. }
exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (⊥ → A0)). apply Int_ImpR,ExFalso. exists H ; auto.
+ assert (Γ0 ⊢KM ∅ • (□ (A0 → B) → □ A0 → □ B)). do 2 (apply Int_ImpR). apply BoxR.
repeat rewrite open_boxes_add ; auto ; simpl (⊙ (□ (A0 → B))). simpl (⊙ (□ A0)).
exchl 1 ; exchl 0 ; apply ImpL ; try apply generalised_axiom. exchl 0 ; apply generalised_axiom.
exists ; auto.
+ assert (Γ0 ⊢KM ∅ • ((□ A0 → A0) → A0)). apply Int_ImpR.
apply ImpLBox ; apply generalised_axiom.
exists ; auto.
+ assert (Γ0 ⊢KM ∅ • (□ A0 → B ∨ (B → A0))).
{ apply Int_ImpR. apply OrR. apply ImpR.
* exchr 0 ; apply generalised_axiom.
* rewrite open_boxes_add ; simpl (⊙ (□ A0)) ; exchl 0 ; apply generalised_axiom. }
exists ; auto.
(* MP *)
- destruct (IHKMH_prv2 Γ0) ; auto. destruct (IHKMH_prv1 Γ0) ; auto.
assert (Γ0 ⊢KM ∅ • B).
{ apply additive_cut with (A → B) ; auto.
apply ImpL ; [ exchr 0 ; apply weakeningr ; auto | apply generalised_axiom]. }
exists H3 ; auto.
(* Nec *)
- destruct (IHKMH_prv (⊗ ∅)) ; auto.
+ apply Extensionality_Ensembles ; split ; intros x Hx.
* inversion Hx.
* unfold Ensembles.In in Hx. apply elem_of_open_boxes in Hx as [H0 | [ψ [H0 H1]]] ; subst ; [inversion H0 | inversion H1].
+ assert (Γ0 ⊢KM ∅ • □ A). rewrite <- gmultiset_disj_union_right_id. apply generalised_weakeninglL.
apply BoxR ; apply weakeningl ; auto.
exists H1 ; auto. }
Qed.
End Completeness.