KM.GHC.properties
From Stdlib Require Import List ListDec Arith Lia Ensembles.
Export ListNotations.
Require Import syntax.
Require Import KMH.
Require Import logics.
Section theorems_and_meta.
Lemma Thm_irrel : forall A B Γ , KMH_prv Γ (A → (B → A)).
Proof.
intros A B Γ. apply Ax. left ; eapply IA1 ; reflexivity.
Qed.
Lemma imp_Id_gen : forall A Γ , KMH_prv Γ (A → A).
Proof.
intros.
eapply MP. eapply MP.
apply Ax. left ; apply IA2 with A (Top → ⊥ → Top) A ; reflexivity.
apply Ax. left ; apply IA1 with A (Top → ⊥ → Top) ; reflexivity.
eapply MP.
apply Ax. left ; apply IA1 with (Top → ⊥ → Top) A ; reflexivity.
apply Ax. left ; apply IA1 with Top ⊥ ; reflexivity.
Qed.
Lemma comm_And_obj : forall A B Γ ,
KMH_prv Γ (And A B → And B A).
Proof.
intros A B Γ . eapply MP. eapply MP.
apply Ax. left ; apply IA8 with (And A B) B A ; reflexivity.
apply Ax. left ; apply IA7 with A B ; reflexivity.
apply Ax. left ; apply IA6 with A B ; reflexivity.
Qed.
Lemma comm_Or_obj : forall A B Γ, KMH_prv Γ (Or A B → Or B A).
Proof.
intros A B Γ. eapply MP. eapply MP.
apply Ax. left ; apply IA5 with A B (Or B A) ; reflexivity.
apply Ax. left ; apply IA4 with B A ; reflexivity.
apply Ax. left ; apply IA3 with B A ; reflexivity.
Qed.
Lemma comm_Or : forall A B Γ, KMH_prv Γ (Or A B) -> KMH_prv Γ (Or B A).
Proof.
intros A B Γ D. eapply MP. apply comm_Or_obj. auto.
Qed.
Lemma EFQ : forall A Γ, KMH_prv Γ (Bot → A).
Proof.
intros A Γ. apply Ax. left ; eapply IA9 ; reflexivity.
Qed.
Lemma Imp_trans_help7 : forall x y z Γ, KMH_prv Γ ((x → (y → (z → y)))).
Proof.
intros. eapply MP. all: apply Ax ; left ; eapply IA1 ; reflexivity.
Qed.
Lemma Imp_trans_help8 : forall x y z Γ,
KMH_prv Γ ((((x → (y → z)) → (x → y)) → ((x → (y → z)) → (x → z)))).
Proof.
intros. eapply MP. all: apply Ax ; left ; eapply IA2 ; reflexivity.
Qed.
Lemma Imp_trans_help9 : forall x y z u Γ,
KMH_prv Γ ((x → ((y → (z → u)) → ((y → z) → (y → u))))).
Proof.
intros. eapply MP. all: apply Ax ; left.
eapply IA1 ; reflexivity. eapply IA2 ; reflexivity.
Qed.
Lemma Imp_trans_help14 : forall x y z u Γ,
KMH_prv Γ ((x → (y → (z → (u → z))))).
Proof.
intros. eapply MP. apply Ax ; left ; eapply IA1 ; reflexivity. apply Imp_trans_help7.
Qed.
Lemma Imp_trans_help35 : forall x y z Γ, KMH_prv Γ ((x → ((y → x) → z)) → (x → z)).
Proof.
intros. eapply MP. apply Imp_trans_help8. apply Imp_trans_help7.
Qed.
Lemma Imp_trans_help37 : forall x y z u Γ, KMH_prv Γ (((x → ((y → (z → y)) → u)) → (x → u))).
Proof.
intros. eapply MP. apply Imp_trans_help8. apply Imp_trans_help14.
Qed.
Lemma Imp_trans_help54 : forall x y z u Γ,
KMH_prv Γ ((((x → (y → z)) → (((x → y) → (x → z)) → u)) → ((x → (y → z)) → u))).
Proof.
intros. eapply MP. apply Imp_trans_help8. apply Imp_trans_help9.
Qed.
Lemma Imp_trans_help170 : forall x y z Γ, KMH_prv Γ ((x → y) → ((z → x) → (z → y))).
Proof.
intros. eapply MP. apply Imp_trans_help35. apply Imp_trans_help9.
Qed.
Lemma Imp_trans_help410 : forall x y z Γ,
KMH_prv Γ ((((x → y) → z) → (y → z))).
Proof.
intros. eapply MP. apply Imp_trans_help37. apply Imp_trans_help170.
Qed.
Lemma Imp_trans_help427 : forall x y z u Γ,
KMH_prv Γ ((x → (((y → z) → u) → (z → u)))).
Proof.
intros. eapply MP. apply Ax ; left ; eapply IA1 ; reflexivity. apply Imp_trans_help410.
Qed.
Lemma Imp_trans : forall A B C Γ, KMH_prv Γ ((A → B) → (B → C) → (A → C)).
Proof.
intros. eapply MP. eapply MP. apply Imp_trans_help54. apply Imp_trans_help427.
apply Imp_trans_help170.
Qed.
Lemma monotR_Or : forall A B Γ ,
KMH_prv Γ (A → B) ->
forall C, KMH_prv Γ ((Or A C) → (Or B C)).
Proof.
intros A B Γ D C. eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
eapply MP. eapply MP. apply Imp_trans. exact D.
apply Ax ; left ; eapply IA3 ; reflexivity.
apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma monotL_Or : forall A B Γ,
KMH_prv Γ (A → B) ->
forall C, KMH_prv Γ ((Or C A) → (Or C B)).
Proof.
intros A B Γ D C. eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
apply Ax ; left ; eapply IA3 ; reflexivity.
eapply MP. eapply MP. apply Imp_trans. exact D.
apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma monot_Or2 : forall A B Γ, KMH_prv Γ (A → B) ->
forall C, KMH_prv Γ ((Or A C) → (Or C B)).
Proof.
intros A B Γ D C.
eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
eapply MP. eapply MP. apply Imp_trans. exact D.
apply Ax ; left ; eapply IA4 ; reflexivity.
apply Ax ; left ; eapply IA3 ; reflexivity.
Qed.
Lemma prv_Top : forall Γ , KMH_prv Γ Top.
Proof.
intros. apply imp_Id_gen.
Qed.
Lemma absorp_Or1 : forall A Γ ,
KMH_prv Γ (Or A (Bot)) ->
KMH_prv Γ A.
Proof.
intros A Γ D. eapply MP. eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
apply imp_Id_gen. apply EFQ. auto.
Qed.
Lemma Imp_And : forall A B C Γ, KMH_prv Γ ((A → (B → C)) → ((And A B) → C)).
Proof.
intros A B C Γ. eapply MP. eapply MP. apply Imp_trans. eapply MP. apply Imp_trans.
apply Ax ; left ; eapply IA6 ; reflexivity.
eapply MP. eapply MP.
apply Ax ; left ; eapply IA2 ; reflexivity.
apply Ax ; left ; eapply IA2 ; reflexivity.
eapply MP.
apply Ax ; left ; eapply IA1 ; reflexivity.
apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.
Lemma Contr_Bot : forall A Γ, KMH_prv Γ (And A (Neg A) → (Bot)).
Proof.
intros A Γ . eapply MP. eapply MP. apply Imp_trans.
apply comm_And_obj. eapply MP. apply Imp_And.
apply imp_Id_gen.
Qed.
Theorem KMH_Detachment_Theorem : forall A B Γ,
KMH_prv Γ (A → B) ->
KMH_prv (Union _ Γ (Singleton _ (A))) B.
Proof.
intros A B Γ D. eapply MP. apply (KMH_monot Γ (A → B)) ; auto.
intros C HC. apply Union_introl ; auto.
apply Id. apply Union_intror. apply In_singleton.
Qed.
Theorem KMH_Deduction_Theorem : forall A B Γ,
KMH_prv (Union _ Γ (Singleton _ (A))) B ->
KMH_prv Γ (A → B).
Proof.
intros. remember (Union form Γ (Singleton form A)) as L.
revert L B H A Γ HeqL.
intros L B D. induction D ; intros C Γ0 id ; subst.
(* Id *)
- inversion H ; subst ; cbn.
+ eapply MP. apply Thm_irrel. apply Id ; auto.
+ inversion H0 ; subst. apply imp_Id_gen.
(* Ax *)
- eapply MP. apply Thm_irrel. apply Ax ; assumption.
(* MP *)
- eapply MP. eapply MP. apply Imp_trans. eapply MP.
eapply MP. apply Ax ; left ; eapply IA8 ; reflexivity. apply imp_Id_gen.
apply IHD2 ; auto. eapply MP. apply Imp_And. apply IHD1 ; auto.
(* DNw *)
- eapply MP. apply Thm_irrel. eapply Nec ; auto.
Qed.
Lemma And_Imp : forall A B C Γ, KMH_prv Γ (((And A B) → C) → (A → (B → C))).
Proof.
intros. repeat apply KMH_Deduction_Theorem.
eapply MP. apply Id. apply Union_introl. apply Union_introl. apply Union_intror. apply In_singleton.
eapply MP. eapply MP. eapply MP.
apply Ax ; left ; eapply IA8 ; reflexivity.
apply KMH_Deduction_Theorem.
apply Id ; apply Union_introl ; apply Union_introl ; apply Union_intror ; apply In_singleton.
apply KMH_Deduction_Theorem.
apply Id ; apply Union_introl ; apply Union_intror ; apply In_singleton.
apply prv_Top.
Qed.
Lemma meta_Imp_trans : forall A B C Γ, KMH_prv Γ (A → B) -> KMH_prv Γ (B → C) ->
KMH_prv Γ (A → C).
Proof.
intros A B C Γ H H0. eapply MP.
- eapply MP.
+ eapply Imp_trans.
+ exact H.
- auto.
Qed.
Lemma Or_imp_assoc : forall A B C D Γ,
KMH_prv Γ (A → ((B ∨ C) ∨ D)) ->
KMH_prv Γ (A → (B ∨ (C ∨ D))).
Proof.
intros. eapply MP.
- eapply MP.
+ apply Imp_trans.
+ exact H.
- eapply MP.
+ eapply MP.
* apply Ax ; left ; eapply IA5 ; reflexivity.
* eapply MP.
-- eapply MP.
++ apply Ax ; left ; eapply IA5 ; reflexivity.
++ apply Ax ; left ; eapply IA3 ; reflexivity.
-- eapply MP.
++ eapply MP.
** apply Imp_trans.
** apply Ax ; left ; eapply IA3 ; reflexivity.
++ apply Ax ; left ; eapply IA4 ; reflexivity.
+ eapply MP.
* eapply MP.
-- apply Imp_trans.
-- apply Ax ; left ; eapply IA4 ; reflexivity.
* apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma assoc_And_obj : forall A B C Γ, KMH_prv Γ ((A ∧ (B ∧ C)) → ((A ∧ B) ∧ C)) /\
KMH_prv Γ (((A ∧ B) ∧ C) → (A ∧ (B ∧ C))).
Proof.
intros A B C Γ. split.
- eapply MP.
+ eapply MP.
* apply Ax ; left ; eapply IA8 ; reflexivity.
* eapply MP.
-- eapply MP.
++ apply Ax ; left ; eapply IA8 ; reflexivity.
++ apply Ax ; left ; eapply IA6 ; reflexivity.
-- eapply meta_Imp_trans.
++ apply Ax ; left ; eapply IA7 ; reflexivity.
++ apply Ax ; left ; eapply IA6 ; reflexivity.
+ eapply meta_Imp_trans.
* apply Ax ; left ; eapply IA7 ; reflexivity.
* apply Ax ; left ; eapply IA7 ; reflexivity.
- eapply MP.
+ eapply MP.
* apply Ax ; left ; eapply IA8 ; reflexivity.
* eapply meta_Imp_trans.
-- apply Ax ; left ; eapply IA6 ; reflexivity.
-- apply Ax ; left ; eapply IA6 ; reflexivity.
+ eapply MP.
* eapply MP.
-- apply Ax ; left ; eapply IA8 ; reflexivity.
-- eapply meta_Imp_trans.
++ apply Ax ; left ; eapply IA6 ; reflexivity.
++ apply Ax ; left ; eapply IA7 ; reflexivity.
* apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.
Lemma Explosion : forall Γ A B,
KMH_prv Γ ((B → Bot) → (B → A)).
Proof.
intros. repeat apply KMH_Deduction_Theorem. eapply MP.
apply Ax ; left ; eapply IA9 ; reflexivity.
eapply MP. apply Id ; apply Union_introl ; apply Union_intror ; apply In_singleton.
apply Id ; apply Union_intror ; apply In_singleton.
Qed.
Lemma Imp_list_Imp : forall l Γ A B,
KMH_prv Γ (list_Imp (A → B) l) <->
KMH_prv Γ (A → list_Imp B l).
Proof.
induction l ; cbn ; intros.
- split ; intro ; auto.
- split ; intro.
* repeat apply KMH_Deduction_Theorem.
apply KMH_Detachment_Theorem in H. apply IHl in H.
apply KMH_Detachment_Theorem in H. apply (KMH_monot _ _ H).
intros C HC. inversion HC ; subst. inversion H0 ; subst.
left. left ; auto. right ; auto. left ; right ; auto.
* apply KMH_Deduction_Theorem. apply IHl.
apply KMH_Deduction_Theorem. repeat apply KMH_Detachment_Theorem in H.
apply (KMH_monot _ _ H).
intros C HC. inversion HC ; subst. inversion H0 ; subst.
left. left ; auto. right ; auto. left ; right ; auto.
Qed.
Lemma KMH_Imp_list_Detachment_Deduction_Theorem : forall l (Γ: Ensemble _) A,
(forall B, (Γ B -> List.In B l) * (List.In B l -> Γ B)) ->
(KMH_prv Γ A <-> KMH_prv (Empty_set _) (list_Imp A l)).
Proof.
induction l ; cbn ; intros ; split ; intros.
- apply (KMH_monot _ _ H0). intros B HB ; apply H in HB ; contradiction.
- apply (KMH_monot _ _ H0). intros B HB ; contradiction.
- destruct (In_form_dec l a).
* apply IHl in H0. eapply MP. apply Thm_irrel. auto.
intros. split ; intro. destruct (H B). destruct (o H2) ; subst ; auto.
apply H ; auto.
* apply Imp_list_Imp. apply (IHl (fun y => (In _ Γ y) /\ (y <> a))).
intros. split ; intro. destruct H1. destruct (H B).
apply o in H1. destruct H1 ; subst. exfalso. apply H2 ; auto.
auto. split ; auto. apply H ; auto. intro. subst. auto.
apply KMH_Deduction_Theorem ; auto.
apply (KMH_monot _ _ H0). intros x Hx.
destruct (form_eq_dec a x). subst. apply Union_intror. apply In_singleton.
apply Union_introl. split ; auto.
- destruct (In_form_dec l a).
* apply Imp_list_Imp in H0. eapply MP. apply IHl ; auto.
intros. split ; intro. destruct (H B). destruct (o H1).
subst. auto. auto. apply H. auto. exact H0. apply Id ; apply H ; auto.
* apply Imp_list_Imp in H0. apply (IHl (fun y => (In _ Γ y) /\ (y <> a))) in H0.
apply KMH_Detachment_Theorem in H0. apply (KMH_monot _ _ H0). intros x Hx.
inversion Hx ; subst. inversion H1 ; subst ; auto. inversion H1 ; subst ; apply H ; auto.
intros. split ; intro. destruct H2. destruct (H B).
destruct (o H2) ; subst ; try contradiction ; auto.
split ; auto. apply H ; auto. intro. subst. auto.
Qed.
Lemma K_list_Imp : forall l Γ A,
KMH_prv Γ (Box (list_Imp A l) → list_Imp (Box A) (Box_list l)).
Proof.
induction l ; cbn ; intros.
- apply imp_Id_gen.
- repeat apply KMH_Deduction_Theorem. eapply MP. auto. eapply MP.
eapply MP. apply Ax ; right ; eapply K ; reflexivity.
apply Id ; left ; right ; apply In_singleton. apply Id ; right ;
apply In_singleton.
Qed.
Lemma Box_distrib_list_Imp : forall l A,
KMH_prv (Empty_set _) (list_Imp A l) ->
KMH_prv (Empty_set _) (list_Imp (Box A) (Box_list l)).
Proof.
induction l ; cbn ; intros.
- eapply Nec ; auto.
- eapply MP. eapply MP. apply Imp_trans. eapply MP.
apply Ax ; right ; eapply K ; reflexivity.
eapply Nec ; auto. exact H. apply K_list_Imp.
Qed.
Lemma In_list_In_Box_list : forall l A,
List.In A l -> List.In (Box A) (Box_list l).
Proof.
induction l ; intros ; cbn.
- inversion H.
- inversion H ; subst ; auto.
Qed.
Lemma In_Box_list_In_list : forall l A,
List.In A (Box_list l) -> (exists B, List.In B l /\ A = Box B).
Proof.
induction l ; cbn ; intros.
- inversion H.
- destruct H ; subst. exists a. split ; auto. apply IHl in H.
destruct H. destruct H. subst. exists x ; auto.
Qed.
Lemma K_rule : forall Γ A, KMH_prv Γ A ->
KMH_prv (fun x => (exists B, In _ Γ B /\ x = Box B)) (Box A).
Proof.
intros. apply KMH_finite in H. cbn in H.
destruct H as (X & HX1 & HX2 & (l & Hl)).
apply (KMH_monot (fun x1 : form => exists B : form, List.In B l /\ x1 = Box B)) ; cbn.
apply (KMH_Imp_list_Detachment_Deduction_Theorem l X A) in HX2.
apply Box_distrib_list_Imp in HX2.
epose (KMH_Imp_list_Detachment_Deduction_Theorem (Box_list l) _ (Box A)).
apply i in HX2 ; auto. exact HX2. intros. split ; intro. destruct H0. destruct H0. subst.
apply In_list_In_Box_list ; auto. apply In_Box_list_In_list in H0 ; auto.
intro. split ; intros ; apply Hl ; auto. intros C HC. inversion HC. destruct H. subst. unfold In.
exists x ; split ; auto. apply HX1. apply Hl ; auto.
Qed.
Lemma Axcoreflection : forall Γ A, KMH_prv Γ (A → □ A).
Proof.
intros. apply meta_Imp_trans with (A ∧ (□ A)).
- apply meta_Imp_trans with ((□ ((A ∧ □ A)))→ (A ∧ □ A)).
+ eapply MP ; [ apply And_Imp | ].
eapply MP ; [eapply MP ; [apply Ax ; left ; eapply IA8 ; reflexivity | ] | ].
* apply Ax ; left ; eapply IA6 ; reflexivity.
* apply meta_Imp_trans with (□ (A ∧ (□ A))).
-- apply Ax ; left ; eapply IA7 ; reflexivity.
-- eapply MP ; [ apply Ax ; right ; eapply K ; reflexivity | ].
apply Nec. apply Ax ; left ; eapply IA6 ; reflexivity.
+ apply Ax ; right ; eapply L ; reflexivity.
- apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.
Section list_of_disjunctions.
Fixpoint list_disj (l : list form) :=
match l with
| nil => Bot
| h :: t => Or h (list_disj t)
end.
Lemma list_disj_map_Box : forall l, (forall A, List.In A l -> exists B, A = □ B) ->
exists l', l = map Box l'.
Proof.
induction l ; cbn ; intros ; auto.
- exists [] ; auto.
- destruct (H a) ; auto ; subst.
destruct (IHl). intros. apply H ; auto. subst.
exists (x :: x0). cbn ; auto.
Qed.
Lemma IdL_list_disj_obj : forall Γ l0 l1,
KMH_prv Γ (list_disj l0 → list_disj (l0 ++ l1)).
Proof.
induction l0 ; intros.
- simpl. apply EFQ.
- simpl. apply monotL_Or. apply IHl0.
Qed.
Lemma IdR_list_disj_obj : forall Γ l0 l1,
KMH_prv Γ (list_disj l1 → list_disj (l0 ++ l1)).
Proof.
induction l0 ; intros.
- simpl. apply imp_Id_gen.
- simpl. eapply MP. eapply MP. apply Imp_trans.
apply IHl0. apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma IdL_list_disj : forall Γ l0 l1,
KMH_prv Γ (list_disj l0) ->
KMH_prv Γ (list_disj (l0 ++ l1)).
Proof.
intros. eapply MP. apply IdL_list_disj_obj. auto.
Qed.
Lemma IdR_list_disj : forall Γ l0 l1,
KMH_prv Γ (list_disj l1) ->
KMH_prv Γ (list_disj (l0 ++ l1)).
Proof.
intros. eapply MP. apply IdR_list_disj_obj. auto.
Qed.
Lemma forall_list_disj : forall l Γ A,
KMH_prv Γ (list_disj l) ->
(forall B, List.In B l -> KMH_prv Γ (B → A)) ->
KMH_prv Γ A.
Proof.
induction l ; cbn ; intros ; auto.
- eapply MP. apply EFQ. auto.
- eapply MP. eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
apply H0. left ; reflexivity.
apply KMH_Deduction_Theorem. apply IHl.
apply Id. right ; apply In_singleton.
intros. apply KMH_monot with Γ. apply H0 ; auto.
intros C HC ; left ; auto. auto.
Qed.
Lemma list_disj_Box_obj : forall l Γ,
KMH_prv Γ (list_disj (map Box l) → □ (list_disj l)).
Proof.
induction l ; cbn ; intros.
- apply EFQ.
- eapply MP. eapply MP. apply Ax ; left ; eapply IA5 ; reflexivity.
eapply MP. apply Ax ; right ; eapply K ; reflexivity.
apply Nec. apply Ax ; left ; eapply IA3 ; reflexivity.
eapply MP. eapply MP. apply Imp_trans.
apply IHl. eapply MP. apply Ax ; right ; eapply K ; reflexivity.
apply Nec. apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma list_disj_Box : forall l Γ,
KMH_prv Γ (list_disj (map Box l)) ->
KMH_prv Γ (□ (list_disj l)).
Proof.
intros. eapply MP. apply list_disj_Box_obj. auto.
Qed.
End list_of_disjunctions.
Section list_of_conjunctions.
Fixpoint list_conj (l : list form) :=
match l with
| nil => Top
| h :: t => And h (list_conj t)
end.
Lemma forall_list_conj : forall l Γ,
(forall B, List.In B l -> KMH_prv Γ B) ->
KMH_prv Γ (list_conj l).
Proof.
induction l ; cbn ; intros ; auto.
- apply prv_Top.
- eapply MP. eapply MP. eapply MP.
apply Ax ; left ; eapply IA8 ; reflexivity. apply imp_Id_gen.
eapply MP. apply Thm_irrel. apply IHl. intros ; auto.
apply H ; auto.
Qed.
Lemma prv_list_left_conj : forall l Γ A,
KMH_prv (Union _ Γ (fun x => List.In x l)) A ->
KMH_prv (Union _ Γ (Singleton _ (list_conj l))) A.
Proof.
induction l ; cbn ; intros.
- apply (KMH_monot _ _ H). intros B HB. inversion HB ; subst.
+ left ; auto.
+ inversion H0.
- apply KMH_comp with (Union _ (Union _ Γ (Singleton _ a)) (Singleton _ (list_conj l))).
+ apply IHl. apply (KMH_monot _ _ H). intros B HB. inversion HB ; subst.
* left ; left ; auto.
* inversion H0 ; subst. left ; right ; apply In_singleton. right ; cbn ; auto.
+ intros. inversion H0 ; subst. inversion H1 ; subst. apply Id. left ; auto.
inversion H2 ; subst. apply KMH_Detachment_Theorem. apply Ax ; left ; eapply IA6 ; reflexivity.
inversion H1 ; subst. apply KMH_Detachment_Theorem. apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.
End list_of_conjunctions.
End theorems_and_meta.
Section Natural_Deduction.
Lemma ND_BotE Γ φ : KMH_prv Γ ⊥ -> KMH_prv Γ φ.
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA9 ; reflexivity | exact Hp ].
Qed.
Lemma ND_AndI Γ φ ψ : KMH_prv Γ φ -> KMH_prv Γ ψ -> KMH_prv Γ (φ ∧ ψ).
Proof.
intros Hp1 Hp2.
eapply MP ; [ eapply MP ; [ eapply MP ; [ eapply Ax ; left ; eapply IA8 ; reflexivity | apply imp_Id_gen ]| ] | ].
eapply MP ; [ apply Thm_irrel | exact Hp2].
exact Hp1.
Qed.
Lemma ND_AndE1 Γ φ ψ : KMH_prv Γ (φ ∧ ψ) -> KMH_prv Γ φ.
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA6 ; reflexivity | exact Hp ].
Qed.
Lemma ND_AndE2 Γ φ ψ : KMH_prv Γ (φ ∧ ψ) -> KMH_prv Γ ψ.
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA7 ; reflexivity | exact Hp ].
Qed.
Lemma ND_OrI1 Γ φ ψ : KMH_prv Γ φ -> KMH_prv Γ (φ ∨ ψ).
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA3 ; reflexivity | exact Hp ].
Qed.
Lemma ND_OrI2 Γ φ ψ : KMH_prv Γ ψ -> KMH_prv Γ (φ ∨ ψ).
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA4 ; reflexivity | exact Hp ].
Qed.
Lemma ND_OrE Γ φ ψ χ : KMH_prv Γ (φ ∨ ψ) ->
KMH_prv Γ (φ → χ) -> KMH_prv Γ (ψ → χ) ->
KMH_prv Γ χ.
Proof.
intros Hp1 Hp2 Hp3.
eapply MP ; [ eapply MP ; [ eapply MP ; [ eapply Ax ; left ; eapply IA5 ; reflexivity | exact Hp2 ]| exact Hp3 ] | exact Hp1].
Qed.
End Natural_Deduction.
Section more_for_eq_seq.
Lemma list_disj_in_prv : forall l Γ A,
List.In A l ->
KMH_prv Γ A ->
KMH_prv Γ (list_disj l).
Proof.
induction l ; cbn ; intros ; auto ; try contradiction.
destruct H ; subst.
- apply ND_OrI1 ; auto.
- apply ND_OrI2 ; apply IHl with A ; auto.
Qed.
End more_for_eq_seq.
Export ListNotations.
Require Import syntax.
Require Import KMH.
Require Import logics.
Section theorems_and_meta.
Lemma Thm_irrel : forall A B Γ , KMH_prv Γ (A → (B → A)).
Proof.
intros A B Γ. apply Ax. left ; eapply IA1 ; reflexivity.
Qed.
Lemma imp_Id_gen : forall A Γ , KMH_prv Γ (A → A).
Proof.
intros.
eapply MP. eapply MP.
apply Ax. left ; apply IA2 with A (Top → ⊥ → Top) A ; reflexivity.
apply Ax. left ; apply IA1 with A (Top → ⊥ → Top) ; reflexivity.
eapply MP.
apply Ax. left ; apply IA1 with (Top → ⊥ → Top) A ; reflexivity.
apply Ax. left ; apply IA1 with Top ⊥ ; reflexivity.
Qed.
Lemma comm_And_obj : forall A B Γ ,
KMH_prv Γ (And A B → And B A).
Proof.
intros A B Γ . eapply MP. eapply MP.
apply Ax. left ; apply IA8 with (And A B) B A ; reflexivity.
apply Ax. left ; apply IA7 with A B ; reflexivity.
apply Ax. left ; apply IA6 with A B ; reflexivity.
Qed.
Lemma comm_Or_obj : forall A B Γ, KMH_prv Γ (Or A B → Or B A).
Proof.
intros A B Γ. eapply MP. eapply MP.
apply Ax. left ; apply IA5 with A B (Or B A) ; reflexivity.
apply Ax. left ; apply IA4 with B A ; reflexivity.
apply Ax. left ; apply IA3 with B A ; reflexivity.
Qed.
Lemma comm_Or : forall A B Γ, KMH_prv Γ (Or A B) -> KMH_prv Γ (Or B A).
Proof.
intros A B Γ D. eapply MP. apply comm_Or_obj. auto.
Qed.
Lemma EFQ : forall A Γ, KMH_prv Γ (Bot → A).
Proof.
intros A Γ. apply Ax. left ; eapply IA9 ; reflexivity.
Qed.
Lemma Imp_trans_help7 : forall x y z Γ, KMH_prv Γ ((x → (y → (z → y)))).
Proof.
intros. eapply MP. all: apply Ax ; left ; eapply IA1 ; reflexivity.
Qed.
Lemma Imp_trans_help8 : forall x y z Γ,
KMH_prv Γ ((((x → (y → z)) → (x → y)) → ((x → (y → z)) → (x → z)))).
Proof.
intros. eapply MP. all: apply Ax ; left ; eapply IA2 ; reflexivity.
Qed.
Lemma Imp_trans_help9 : forall x y z u Γ,
KMH_prv Γ ((x → ((y → (z → u)) → ((y → z) → (y → u))))).
Proof.
intros. eapply MP. all: apply Ax ; left.
eapply IA1 ; reflexivity. eapply IA2 ; reflexivity.
Qed.
Lemma Imp_trans_help14 : forall x y z u Γ,
KMH_prv Γ ((x → (y → (z → (u → z))))).
Proof.
intros. eapply MP. apply Ax ; left ; eapply IA1 ; reflexivity. apply Imp_trans_help7.
Qed.
Lemma Imp_trans_help35 : forall x y z Γ, KMH_prv Γ ((x → ((y → x) → z)) → (x → z)).
Proof.
intros. eapply MP. apply Imp_trans_help8. apply Imp_trans_help7.
Qed.
Lemma Imp_trans_help37 : forall x y z u Γ, KMH_prv Γ (((x → ((y → (z → y)) → u)) → (x → u))).
Proof.
intros. eapply MP. apply Imp_trans_help8. apply Imp_trans_help14.
Qed.
Lemma Imp_trans_help54 : forall x y z u Γ,
KMH_prv Γ ((((x → (y → z)) → (((x → y) → (x → z)) → u)) → ((x → (y → z)) → u))).
Proof.
intros. eapply MP. apply Imp_trans_help8. apply Imp_trans_help9.
Qed.
Lemma Imp_trans_help170 : forall x y z Γ, KMH_prv Γ ((x → y) → ((z → x) → (z → y))).
Proof.
intros. eapply MP. apply Imp_trans_help35. apply Imp_trans_help9.
Qed.
Lemma Imp_trans_help410 : forall x y z Γ,
KMH_prv Γ ((((x → y) → z) → (y → z))).
Proof.
intros. eapply MP. apply Imp_trans_help37. apply Imp_trans_help170.
Qed.
Lemma Imp_trans_help427 : forall x y z u Γ,
KMH_prv Γ ((x → (((y → z) → u) → (z → u)))).
Proof.
intros. eapply MP. apply Ax ; left ; eapply IA1 ; reflexivity. apply Imp_trans_help410.
Qed.
Lemma Imp_trans : forall A B C Γ, KMH_prv Γ ((A → B) → (B → C) → (A → C)).
Proof.
intros. eapply MP. eapply MP. apply Imp_trans_help54. apply Imp_trans_help427.
apply Imp_trans_help170.
Qed.
Lemma monotR_Or : forall A B Γ ,
KMH_prv Γ (A → B) ->
forall C, KMH_prv Γ ((Or A C) → (Or B C)).
Proof.
intros A B Γ D C. eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
eapply MP. eapply MP. apply Imp_trans. exact D.
apply Ax ; left ; eapply IA3 ; reflexivity.
apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma monotL_Or : forall A B Γ,
KMH_prv Γ (A → B) ->
forall C, KMH_prv Γ ((Or C A) → (Or C B)).
Proof.
intros A B Γ D C. eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
apply Ax ; left ; eapply IA3 ; reflexivity.
eapply MP. eapply MP. apply Imp_trans. exact D.
apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma monot_Or2 : forall A B Γ, KMH_prv Γ (A → B) ->
forall C, KMH_prv Γ ((Or A C) → (Or C B)).
Proof.
intros A B Γ D C.
eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
eapply MP. eapply MP. apply Imp_trans. exact D.
apply Ax ; left ; eapply IA4 ; reflexivity.
apply Ax ; left ; eapply IA3 ; reflexivity.
Qed.
Lemma prv_Top : forall Γ , KMH_prv Γ Top.
Proof.
intros. apply imp_Id_gen.
Qed.
Lemma absorp_Or1 : forall A Γ ,
KMH_prv Γ (Or A (Bot)) ->
KMH_prv Γ A.
Proof.
intros A Γ D. eapply MP. eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
apply imp_Id_gen. apply EFQ. auto.
Qed.
Lemma Imp_And : forall A B C Γ, KMH_prv Γ ((A → (B → C)) → ((And A B) → C)).
Proof.
intros A B C Γ. eapply MP. eapply MP. apply Imp_trans. eapply MP. apply Imp_trans.
apply Ax ; left ; eapply IA6 ; reflexivity.
eapply MP. eapply MP.
apply Ax ; left ; eapply IA2 ; reflexivity.
apply Ax ; left ; eapply IA2 ; reflexivity.
eapply MP.
apply Ax ; left ; eapply IA1 ; reflexivity.
apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.
Lemma Contr_Bot : forall A Γ, KMH_prv Γ (And A (Neg A) → (Bot)).
Proof.
intros A Γ . eapply MP. eapply MP. apply Imp_trans.
apply comm_And_obj. eapply MP. apply Imp_And.
apply imp_Id_gen.
Qed.
Theorem KMH_Detachment_Theorem : forall A B Γ,
KMH_prv Γ (A → B) ->
KMH_prv (Union _ Γ (Singleton _ (A))) B.
Proof.
intros A B Γ D. eapply MP. apply (KMH_monot Γ (A → B)) ; auto.
intros C HC. apply Union_introl ; auto.
apply Id. apply Union_intror. apply In_singleton.
Qed.
Theorem KMH_Deduction_Theorem : forall A B Γ,
KMH_prv (Union _ Γ (Singleton _ (A))) B ->
KMH_prv Γ (A → B).
Proof.
intros. remember (Union form Γ (Singleton form A)) as L.
revert L B H A Γ HeqL.
intros L B D. induction D ; intros C Γ0 id ; subst.
(* Id *)
- inversion H ; subst ; cbn.
+ eapply MP. apply Thm_irrel. apply Id ; auto.
+ inversion H0 ; subst. apply imp_Id_gen.
(* Ax *)
- eapply MP. apply Thm_irrel. apply Ax ; assumption.
(* MP *)
- eapply MP. eapply MP. apply Imp_trans. eapply MP.
eapply MP. apply Ax ; left ; eapply IA8 ; reflexivity. apply imp_Id_gen.
apply IHD2 ; auto. eapply MP. apply Imp_And. apply IHD1 ; auto.
(* DNw *)
- eapply MP. apply Thm_irrel. eapply Nec ; auto.
Qed.
Lemma And_Imp : forall A B C Γ, KMH_prv Γ (((And A B) → C) → (A → (B → C))).
Proof.
intros. repeat apply KMH_Deduction_Theorem.
eapply MP. apply Id. apply Union_introl. apply Union_introl. apply Union_intror. apply In_singleton.
eapply MP. eapply MP. eapply MP.
apply Ax ; left ; eapply IA8 ; reflexivity.
apply KMH_Deduction_Theorem.
apply Id ; apply Union_introl ; apply Union_introl ; apply Union_intror ; apply In_singleton.
apply KMH_Deduction_Theorem.
apply Id ; apply Union_introl ; apply Union_intror ; apply In_singleton.
apply prv_Top.
Qed.
Lemma meta_Imp_trans : forall A B C Γ, KMH_prv Γ (A → B) -> KMH_prv Γ (B → C) ->
KMH_prv Γ (A → C).
Proof.
intros A B C Γ H H0. eapply MP.
- eapply MP.
+ eapply Imp_trans.
+ exact H.
- auto.
Qed.
Lemma Or_imp_assoc : forall A B C D Γ,
KMH_prv Γ (A → ((B ∨ C) ∨ D)) ->
KMH_prv Γ (A → (B ∨ (C ∨ D))).
Proof.
intros. eapply MP.
- eapply MP.
+ apply Imp_trans.
+ exact H.
- eapply MP.
+ eapply MP.
* apply Ax ; left ; eapply IA5 ; reflexivity.
* eapply MP.
-- eapply MP.
++ apply Ax ; left ; eapply IA5 ; reflexivity.
++ apply Ax ; left ; eapply IA3 ; reflexivity.
-- eapply MP.
++ eapply MP.
** apply Imp_trans.
** apply Ax ; left ; eapply IA3 ; reflexivity.
++ apply Ax ; left ; eapply IA4 ; reflexivity.
+ eapply MP.
* eapply MP.
-- apply Imp_trans.
-- apply Ax ; left ; eapply IA4 ; reflexivity.
* apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma assoc_And_obj : forall A B C Γ, KMH_prv Γ ((A ∧ (B ∧ C)) → ((A ∧ B) ∧ C)) /\
KMH_prv Γ (((A ∧ B) ∧ C) → (A ∧ (B ∧ C))).
Proof.
intros A B C Γ. split.
- eapply MP.
+ eapply MP.
* apply Ax ; left ; eapply IA8 ; reflexivity.
* eapply MP.
-- eapply MP.
++ apply Ax ; left ; eapply IA8 ; reflexivity.
++ apply Ax ; left ; eapply IA6 ; reflexivity.
-- eapply meta_Imp_trans.
++ apply Ax ; left ; eapply IA7 ; reflexivity.
++ apply Ax ; left ; eapply IA6 ; reflexivity.
+ eapply meta_Imp_trans.
* apply Ax ; left ; eapply IA7 ; reflexivity.
* apply Ax ; left ; eapply IA7 ; reflexivity.
- eapply MP.
+ eapply MP.
* apply Ax ; left ; eapply IA8 ; reflexivity.
* eapply meta_Imp_trans.
-- apply Ax ; left ; eapply IA6 ; reflexivity.
-- apply Ax ; left ; eapply IA6 ; reflexivity.
+ eapply MP.
* eapply MP.
-- apply Ax ; left ; eapply IA8 ; reflexivity.
-- eapply meta_Imp_trans.
++ apply Ax ; left ; eapply IA6 ; reflexivity.
++ apply Ax ; left ; eapply IA7 ; reflexivity.
* apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.
Lemma Explosion : forall Γ A B,
KMH_prv Γ ((B → Bot) → (B → A)).
Proof.
intros. repeat apply KMH_Deduction_Theorem. eapply MP.
apply Ax ; left ; eapply IA9 ; reflexivity.
eapply MP. apply Id ; apply Union_introl ; apply Union_intror ; apply In_singleton.
apply Id ; apply Union_intror ; apply In_singleton.
Qed.
Lemma Imp_list_Imp : forall l Γ A B,
KMH_prv Γ (list_Imp (A → B) l) <->
KMH_prv Γ (A → list_Imp B l).
Proof.
induction l ; cbn ; intros.
- split ; intro ; auto.
- split ; intro.
* repeat apply KMH_Deduction_Theorem.
apply KMH_Detachment_Theorem in H. apply IHl in H.
apply KMH_Detachment_Theorem in H. apply (KMH_monot _ _ H).
intros C HC. inversion HC ; subst. inversion H0 ; subst.
left. left ; auto. right ; auto. left ; right ; auto.
* apply KMH_Deduction_Theorem. apply IHl.
apply KMH_Deduction_Theorem. repeat apply KMH_Detachment_Theorem in H.
apply (KMH_monot _ _ H).
intros C HC. inversion HC ; subst. inversion H0 ; subst.
left. left ; auto. right ; auto. left ; right ; auto.
Qed.
Lemma KMH_Imp_list_Detachment_Deduction_Theorem : forall l (Γ: Ensemble _) A,
(forall B, (Γ B -> List.In B l) * (List.In B l -> Γ B)) ->
(KMH_prv Γ A <-> KMH_prv (Empty_set _) (list_Imp A l)).
Proof.
induction l ; cbn ; intros ; split ; intros.
- apply (KMH_monot _ _ H0). intros B HB ; apply H in HB ; contradiction.
- apply (KMH_monot _ _ H0). intros B HB ; contradiction.
- destruct (In_form_dec l a).
* apply IHl in H0. eapply MP. apply Thm_irrel. auto.
intros. split ; intro. destruct (H B). destruct (o H2) ; subst ; auto.
apply H ; auto.
* apply Imp_list_Imp. apply (IHl (fun y => (In _ Γ y) /\ (y <> a))).
intros. split ; intro. destruct H1. destruct (H B).
apply o in H1. destruct H1 ; subst. exfalso. apply H2 ; auto.
auto. split ; auto. apply H ; auto. intro. subst. auto.
apply KMH_Deduction_Theorem ; auto.
apply (KMH_monot _ _ H0). intros x Hx.
destruct (form_eq_dec a x). subst. apply Union_intror. apply In_singleton.
apply Union_introl. split ; auto.
- destruct (In_form_dec l a).
* apply Imp_list_Imp in H0. eapply MP. apply IHl ; auto.
intros. split ; intro. destruct (H B). destruct (o H1).
subst. auto. auto. apply H. auto. exact H0. apply Id ; apply H ; auto.
* apply Imp_list_Imp in H0. apply (IHl (fun y => (In _ Γ y) /\ (y <> a))) in H0.
apply KMH_Detachment_Theorem in H0. apply (KMH_monot _ _ H0). intros x Hx.
inversion Hx ; subst. inversion H1 ; subst ; auto. inversion H1 ; subst ; apply H ; auto.
intros. split ; intro. destruct H2. destruct (H B).
destruct (o H2) ; subst ; try contradiction ; auto.
split ; auto. apply H ; auto. intro. subst. auto.
Qed.
Lemma K_list_Imp : forall l Γ A,
KMH_prv Γ (Box (list_Imp A l) → list_Imp (Box A) (Box_list l)).
Proof.
induction l ; cbn ; intros.
- apply imp_Id_gen.
- repeat apply KMH_Deduction_Theorem. eapply MP. auto. eapply MP.
eapply MP. apply Ax ; right ; eapply K ; reflexivity.
apply Id ; left ; right ; apply In_singleton. apply Id ; right ;
apply In_singleton.
Qed.
Lemma Box_distrib_list_Imp : forall l A,
KMH_prv (Empty_set _) (list_Imp A l) ->
KMH_prv (Empty_set _) (list_Imp (Box A) (Box_list l)).
Proof.
induction l ; cbn ; intros.
- eapply Nec ; auto.
- eapply MP. eapply MP. apply Imp_trans. eapply MP.
apply Ax ; right ; eapply K ; reflexivity.
eapply Nec ; auto. exact H. apply K_list_Imp.
Qed.
Lemma In_list_In_Box_list : forall l A,
List.In A l -> List.In (Box A) (Box_list l).
Proof.
induction l ; intros ; cbn.
- inversion H.
- inversion H ; subst ; auto.
Qed.
Lemma In_Box_list_In_list : forall l A,
List.In A (Box_list l) -> (exists B, List.In B l /\ A = Box B).
Proof.
induction l ; cbn ; intros.
- inversion H.
- destruct H ; subst. exists a. split ; auto. apply IHl in H.
destruct H. destruct H. subst. exists x ; auto.
Qed.
Lemma K_rule : forall Γ A, KMH_prv Γ A ->
KMH_prv (fun x => (exists B, In _ Γ B /\ x = Box B)) (Box A).
Proof.
intros. apply KMH_finite in H. cbn in H.
destruct H as (X & HX1 & HX2 & (l & Hl)).
apply (KMH_monot (fun x1 : form => exists B : form, List.In B l /\ x1 = Box B)) ; cbn.
apply (KMH_Imp_list_Detachment_Deduction_Theorem l X A) in HX2.
apply Box_distrib_list_Imp in HX2.
epose (KMH_Imp_list_Detachment_Deduction_Theorem (Box_list l) _ (Box A)).
apply i in HX2 ; auto. exact HX2. intros. split ; intro. destruct H0. destruct H0. subst.
apply In_list_In_Box_list ; auto. apply In_Box_list_In_list in H0 ; auto.
intro. split ; intros ; apply Hl ; auto. intros C HC. inversion HC. destruct H. subst. unfold In.
exists x ; split ; auto. apply HX1. apply Hl ; auto.
Qed.
Lemma Axcoreflection : forall Γ A, KMH_prv Γ (A → □ A).
Proof.
intros. apply meta_Imp_trans with (A ∧ (□ A)).
- apply meta_Imp_trans with ((□ ((A ∧ □ A)))→ (A ∧ □ A)).
+ eapply MP ; [ apply And_Imp | ].
eapply MP ; [eapply MP ; [apply Ax ; left ; eapply IA8 ; reflexivity | ] | ].
* apply Ax ; left ; eapply IA6 ; reflexivity.
* apply meta_Imp_trans with (□ (A ∧ (□ A))).
-- apply Ax ; left ; eapply IA7 ; reflexivity.
-- eapply MP ; [ apply Ax ; right ; eapply K ; reflexivity | ].
apply Nec. apply Ax ; left ; eapply IA6 ; reflexivity.
+ apply Ax ; right ; eapply L ; reflexivity.
- apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.
Section list_of_disjunctions.
Fixpoint list_disj (l : list form) :=
match l with
| nil => Bot
| h :: t => Or h (list_disj t)
end.
Lemma list_disj_map_Box : forall l, (forall A, List.In A l -> exists B, A = □ B) ->
exists l', l = map Box l'.
Proof.
induction l ; cbn ; intros ; auto.
- exists [] ; auto.
- destruct (H a) ; auto ; subst.
destruct (IHl). intros. apply H ; auto. subst.
exists (x :: x0). cbn ; auto.
Qed.
Lemma IdL_list_disj_obj : forall Γ l0 l1,
KMH_prv Γ (list_disj l0 → list_disj (l0 ++ l1)).
Proof.
induction l0 ; intros.
- simpl. apply EFQ.
- simpl. apply monotL_Or. apply IHl0.
Qed.
Lemma IdR_list_disj_obj : forall Γ l0 l1,
KMH_prv Γ (list_disj l1 → list_disj (l0 ++ l1)).
Proof.
induction l0 ; intros.
- simpl. apply imp_Id_gen.
- simpl. eapply MP. eapply MP. apply Imp_trans.
apply IHl0. apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma IdL_list_disj : forall Γ l0 l1,
KMH_prv Γ (list_disj l0) ->
KMH_prv Γ (list_disj (l0 ++ l1)).
Proof.
intros. eapply MP. apply IdL_list_disj_obj. auto.
Qed.
Lemma IdR_list_disj : forall Γ l0 l1,
KMH_prv Γ (list_disj l1) ->
KMH_prv Γ (list_disj (l0 ++ l1)).
Proof.
intros. eapply MP. apply IdR_list_disj_obj. auto.
Qed.
Lemma forall_list_disj : forall l Γ A,
KMH_prv Γ (list_disj l) ->
(forall B, List.In B l -> KMH_prv Γ (B → A)) ->
KMH_prv Γ A.
Proof.
induction l ; cbn ; intros ; auto.
- eapply MP. apply EFQ. auto.
- eapply MP. eapply MP. eapply MP.
apply Ax ; left ; eapply IA5 ; reflexivity.
apply H0. left ; reflexivity.
apply KMH_Deduction_Theorem. apply IHl.
apply Id. right ; apply In_singleton.
intros. apply KMH_monot with Γ. apply H0 ; auto.
intros C HC ; left ; auto. auto.
Qed.
Lemma list_disj_Box_obj : forall l Γ,
KMH_prv Γ (list_disj (map Box l) → □ (list_disj l)).
Proof.
induction l ; cbn ; intros.
- apply EFQ.
- eapply MP. eapply MP. apply Ax ; left ; eapply IA5 ; reflexivity.
eapply MP. apply Ax ; right ; eapply K ; reflexivity.
apply Nec. apply Ax ; left ; eapply IA3 ; reflexivity.
eapply MP. eapply MP. apply Imp_trans.
apply IHl. eapply MP. apply Ax ; right ; eapply K ; reflexivity.
apply Nec. apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.
Lemma list_disj_Box : forall l Γ,
KMH_prv Γ (list_disj (map Box l)) ->
KMH_prv Γ (□ (list_disj l)).
Proof.
intros. eapply MP. apply list_disj_Box_obj. auto.
Qed.
End list_of_disjunctions.
Section list_of_conjunctions.
Fixpoint list_conj (l : list form) :=
match l with
| nil => Top
| h :: t => And h (list_conj t)
end.
Lemma forall_list_conj : forall l Γ,
(forall B, List.In B l -> KMH_prv Γ B) ->
KMH_prv Γ (list_conj l).
Proof.
induction l ; cbn ; intros ; auto.
- apply prv_Top.
- eapply MP. eapply MP. eapply MP.
apply Ax ; left ; eapply IA8 ; reflexivity. apply imp_Id_gen.
eapply MP. apply Thm_irrel. apply IHl. intros ; auto.
apply H ; auto.
Qed.
Lemma prv_list_left_conj : forall l Γ A,
KMH_prv (Union _ Γ (fun x => List.In x l)) A ->
KMH_prv (Union _ Γ (Singleton _ (list_conj l))) A.
Proof.
induction l ; cbn ; intros.
- apply (KMH_monot _ _ H). intros B HB. inversion HB ; subst.
+ left ; auto.
+ inversion H0.
- apply KMH_comp with (Union _ (Union _ Γ (Singleton _ a)) (Singleton _ (list_conj l))).
+ apply IHl. apply (KMH_monot _ _ H). intros B HB. inversion HB ; subst.
* left ; left ; auto.
* inversion H0 ; subst. left ; right ; apply In_singleton. right ; cbn ; auto.
+ intros. inversion H0 ; subst. inversion H1 ; subst. apply Id. left ; auto.
inversion H2 ; subst. apply KMH_Detachment_Theorem. apply Ax ; left ; eapply IA6 ; reflexivity.
inversion H1 ; subst. apply KMH_Detachment_Theorem. apply Ax ; left ; eapply IA7 ; reflexivity.
Qed.
End list_of_conjunctions.
End theorems_and_meta.
Section Natural_Deduction.
Lemma ND_BotE Γ φ : KMH_prv Γ ⊥ -> KMH_prv Γ φ.
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA9 ; reflexivity | exact Hp ].
Qed.
Lemma ND_AndI Γ φ ψ : KMH_prv Γ φ -> KMH_prv Γ ψ -> KMH_prv Γ (φ ∧ ψ).
Proof.
intros Hp1 Hp2.
eapply MP ; [ eapply MP ; [ eapply MP ; [ eapply Ax ; left ; eapply IA8 ; reflexivity | apply imp_Id_gen ]| ] | ].
eapply MP ; [ apply Thm_irrel | exact Hp2].
exact Hp1.
Qed.
Lemma ND_AndE1 Γ φ ψ : KMH_prv Γ (φ ∧ ψ) -> KMH_prv Γ φ.
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA6 ; reflexivity | exact Hp ].
Qed.
Lemma ND_AndE2 Γ φ ψ : KMH_prv Γ (φ ∧ ψ) -> KMH_prv Γ ψ.
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA7 ; reflexivity | exact Hp ].
Qed.
Lemma ND_OrI1 Γ φ ψ : KMH_prv Γ φ -> KMH_prv Γ (φ ∨ ψ).
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA3 ; reflexivity | exact Hp ].
Qed.
Lemma ND_OrI2 Γ φ ψ : KMH_prv Γ ψ -> KMH_prv Γ (φ ∨ ψ).
Proof.
intros Hp.
eapply MP ; [ eapply Ax ; left ; eapply IA4 ; reflexivity | exact Hp ].
Qed.
Lemma ND_OrE Γ φ ψ χ : KMH_prv Γ (φ ∨ ψ) ->
KMH_prv Γ (φ → χ) -> KMH_prv Γ (ψ → χ) ->
KMH_prv Γ χ.
Proof.
intros Hp1 Hp2 Hp3.
eapply MP ; [ eapply MP ; [ eapply MP ; [ eapply Ax ; left ; eapply IA5 ; reflexivity | exact Hp2 ]| exact Hp3 ] | exact Hp1].
Qed.
End Natural_Deduction.
Section more_for_eq_seq.
Lemma list_disj_in_prv : forall l Γ A,
List.In A l ->
KMH_prv Γ A ->
KMH_prv Γ (list_disj l).
Proof.
induction l ; cbn ; intros ; auto ; try contradiction.
destruct H ; subst.
- apply ND_OrI1 ; auto.
- apply ND_OrI2 ; apply IHl with A ; auto.
Qed.
End more_for_eq_seq.