CPPsiteProjPackage.CPP_BiInt_meta_interactions2
Require Import List.
Export ListNotations.
Require Import CPP_genT.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_meta_interactions1.
Theorem BIH_Detachment_Theorem : forall s,
(BIH_rules s) ->
(forall A B Γ , (fst s = Γ ) ->
(snd s = A --> B) ->
BIH_rules (Union _ Γ (Singleton _ (A)), B)).
Proof.
intros s D. induction D.
(* Id *)
- intros A B Γ id1 id2. inversion H. subst. simpl in id2. subst.
simpl. apply MP with (ps:=[(Union _ Γ0 (Singleton _ A), Imp A B);(Union _ Γ0 (Singleton _ A), A)]).
2: apply MPRule_I. intros. inversion H1. subst. apply Id.
apply IdRule_I. apply Union_introl. assumption. inversion H2. subst.
apply Id. apply IdRule_I. apply Union_intror. apply In_singleton. inversion H3.
(* Ax *)
- intros A B Γ id1 id2. inversion H. subst. simpl in id2. subst. simpl.
apply MP with (ps:=[(Union _ Γ0 (Singleton _ A), Imp A B);(Union _ Γ0 (Singleton _ A), A)]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax.
apply AxRule_I. assumption. inversion H2. subst. apply Id. apply IdRule_I.
apply Union_intror. apply In_singleton. inversion H3.
(* MP *)
- intros A B Γ id1 id2. inversion H1. subst. simpl in id2. subst. simpl.
assert (J01: List.In (Γ0, A0 --> A --> B) [(Γ0, A0 --> A --> B); (Γ0, A0)]). apply in_eq.
assert (J1: Γ0 = Γ0). reflexivity.
assert (J2: A0 --> A --> B = A0 --> A --> B). reflexivity.
pose (H0 (Γ0, A0 --> A --> B) J01 A0 (Imp A B) Γ0 J1 J2).
assert (BIH_rules (Γ0, A --> B)).
assert (J3: (forall A1 : BPropF, fst (Union _ Γ0 (Singleton _ A0), A --> B) A1 ->
BIH_rules (Γ0, A1))).
intro. simpl. intro. inversion H2. subst. apply Id.
apply IdRule_I. assumption. subst. inversion H3. subst.
assert (J02: List.In (Γ0, A1) [(Γ0, A1 --> A --> B); (Γ0, A1)]). apply in_cons. apply in_eq.
pose (H (Γ0, A1) J02). assumption.
pose (BIH_comp (Union _ Γ0 (Singleton _ A0), A --> B) b Γ0 J3). simpl in b0. assumption.
apply MP with (ps:=[(Union _ Γ0 (Singleton _ A), (Imp A B));(Union _ Γ0 (Singleton _ A), A)]).
2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Union _ Γ0 (Singleton _ A), Imp A0 (Imp A B));(Union _ Γ0 (Singleton _ A), A0)]).
2: apply MPRule_I. intros. inversion H4. subst.
assert (J4: Included _ (fst (Γ0, A0 --> A --> B)) (Union _ Γ0 (Singleton _ A))).
simpl. intro. intro. apply Union_introl. assumption. pose (H (Γ0, A0 --> A --> B) J01).
pose (BIH_monot (Γ0, A0 --> A --> B) b0 (Union _ Γ0 (Singleton _ A)) J4). assumption.
inversion H5. subst.
assert (J4: Included _ (fst (Γ0, A0 --> A --> B)) (Union _ Γ0 (Singleton _ A))).
simpl. intro. intro. apply Union_introl. assumption.
pose (BIH_monot (Γ0, A0)). apply b0. apply H. apply in_cons. apply in_eq.
auto. inversion H6. inversion H4. subst. apply Id. apply IdRule_I. apply Union_intror.
apply In_singleton. inversion H5.
(* DNw *)
- intros A B Γ id1 id2. inversion H1. subst. simpl in id2. subst. inversion id2. subst. simpl.
assert (J01: List.In (Empty_set (BPropF), A0) [(Empty_set (BPropF), A0)]). apply in_eq.
apply H in J01. remember (Union (BPropF) Γ0 (Singleton (BPropF) (wNeg A0))) as Γ .
apply MP with (ps:=[(Γ , (And (wNeg A0) (Neg (wNeg A0))) --> Bot); (Γ , And (wNeg A0) (Neg (wNeg A0)))]).
2: apply MPRule_I. intros. inversion H2. rewrite <- H3. apply wContr_Bot. inversion H3.
rewrite <- H4.
apply MP with (ps:=[(Γ ,(Top --> (And (wNeg A0) (Neg (wNeg A0)))));(Γ , Top)]).
2: apply MPRule_I. intros. inversion H5. rewrite <- H6.
apply MP with (ps:=[(Γ ,(Top --> (Neg (wNeg A0))) --> (Top --> (And (wNeg A0) (Neg (wNeg A0)))));(Γ , Top --> (Neg (wNeg A0)))]).
2: apply MPRule_I. intros. inversion H7. rewrite <- H8.
apply MP with (ps:=[(Γ ,(Top --> (wNeg A0)) --> (Top --> (Neg (wNeg A0))) --> (Top --> (And (wNeg A0) (Neg (wNeg A0)))));(Γ , Top --> (wNeg A0))]).
2: apply MPRule_I. intros. inversion H9. rewrite <- H10. apply Ax. apply AxRule_I.
apply RA7_I. exists (Top). exists (wNeg A0). exists (Neg (wNeg A0)). auto. inversion H10. 2: inversion H11.
rewrite <- H11.
apply MP with (ps:=[(Γ , wNeg A0 --> Top --> wNeg A0);(Γ , wNeg A0)]). intros. 2: apply MPRule_I.
inversion H12. rewrite <- H13. apply wThm_irrel. inversion H13. 2: inversion H14. rewrite <- H14.
apply Id. apply IdRule_I. subst. apply Union_intror. apply In_singleton.
inversion H8. rewrite <- H9.
apply MP with (ps:=[(Γ , Neg (wNeg A0) --> Top --> Neg (wNeg A0));(Γ , Neg (wNeg A0))]). intros. 2: apply MPRule_I.
inversion H10. rewrite <- H11. apply wThm_irrel. inversion H11. 2: inversion H12. rewrite <- H12.
apply DNw with (ps:=[(Empty_set (BPropF), A0)]) ; auto. apply DNwRule_I. inversion H9.
inversion H6. subst. apply wTop. inversion H7. inversion H4.
Qed.
Theorem BIH_Deduction_Theorem : forall s,
(BIH_rules s) ->
(forall A B Γ , (fst s = Union _ Γ (Singleton _ (A))) ->
(snd s = B) ->
BIH_rules (Γ , A --> B)).
Proof.
intros s D. induction D.
(* Id *)
- intros A B Γ id1 id2. inversion H. subst. simpl in id1. subst. simpl. inversion H0.
+ subst. apply MP with (ps:=[(Γ , A0 --> A --> A0);(Γ , A0)]). 2: apply MPRule_I. intros. inversion H2. subst.
apply wThm_irrel. inversion H3. subst. apply Id. apply IdRule_I. assumption.
inversion H4.
+ subst. inversion H1. subst. apply wimp_Id_gen.
(* Ax *)
- intros A B Γ id1 id2. inversion H. subst. simpl in id1. subst. simpl.
apply MP with (ps:=[(Γ , A0 --> A --> A0);(Γ , A0)]). 2: apply MPRule_I. intros. inversion H1. subst.
apply wThm_irrel. inversion H2. subst.
apply Ax. apply AxRule_I. assumption. inversion H3.
(* MP *)
- intros A B Γ id1 id2. inversion H1. subst. simpl in id1. subst. simpl.
assert (J1: Union _ Γ (Singleton _ A) = Union _ Γ (Singleton _ A)). reflexivity.
assert (J2: A0 --> B0 = A0 --> B0). reflexivity.
assert (J20: List.In (Union (BPropF) Γ (Singleton (BPropF) A), A0 --> B0) [(Union (BPropF) Γ (Singleton (BPropF) A), A0 --> B0); (Union (BPropF) Γ (Singleton (BPropF) A), A0)]).
apply in_eq.
pose (H0 (Union (BPropF) Γ (Singleton (BPropF) A), A0 --> B0) J20
A (Imp A0 B0) Γ J1 J2).
assert (J3: A0 = A0). reflexivity.
apply MP with (ps:=[(Γ , (And A A0 --> B0) --> (A --> B0));(Γ , And A A0 --> B0)]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (A --> And A A0) --> (And A A0 --> B0) --> (A --> B0));(Γ , A --> And A A0)]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (And A A0). exists B0. auto.
inversion H4. subst. 2: inversion H5.
apply MP with (ps:=[(Γ , (A --> A0) --> (A --> And A A0));(Γ , A --> A0)]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (A --> A) --> (A --> A0) --> (A --> And A A0));(Γ , A --> A)]).
2: apply MPRule_I. intros. inversion H6. subst. apply Ax.
apply AxRule_I. apply RA7_I. exists A. exists A. exists A0. auto. inversion H7.
subst. apply wimp_Id_gen. inversion H8. inversion H6. subst. 2: inversion H7.
assert (J30: List.In (Union (BPropF) Γ (Singleton (BPropF) A), A0) [(Union (BPropF) Γ (Singleton (BPropF) A), A0 --> B0); (Union (BPropF) Γ (Singleton (BPropF) A), A0)]).
apply in_cons. apply in_eq. assert (J40: A0 = A0). reflexivity.
pose (H0 (Union (BPropF) Γ (Singleton (BPropF) A), A0) J30
A A0 Γ J1 J40). auto. inversion H3. subst.
apply MP with (ps:=[(Γ , (A --> A0 --> B0) --> (And A A0 --> B0));(Γ , (A --> A0 --> B0))]).
2: apply MPRule_I. intros. inversion H4. subst. apply Ax.
apply AxRule_I. apply RA8_I. exists A. exists A0. exists B0. auto.
inversion H5. subst. assumption. inversion H6. inversion H4.
(* DNw *)
- intros A B Γ id1 id2. inversion H1. subst. simpl in id1. subst. simpl.
assert (J1: BIH_rules (Empty_set _, Neg (wNeg A0))).
apply DNw with (ps:=[(Empty_set _, A0)]). 2: apply DNwRule_I. assumption.
assert (J2: Included _ (fst (Empty_set _, Neg (wNeg A0))) Γ ). intro. intro. inversion H2.
pose (BIH_monot (Empty_set _, Neg (wNeg A0)) J1 Γ J2). simpl in b.
apply MP with (ps:=[(Γ , Neg (wNeg A0) --> A --> Neg (wNeg A0)); (Γ , Neg (wNeg A0))]).
2: apply MPRule_I. intros. inversion H2. subst. apply wThm_irrel.
inversion H3. subst. 2: inversion H4. assumption.
Qed.
Theorem gen_BIH_Detachment_Theorem : forall A B Γ ,
pair_derrec (Γ , Singleton _ (A --> B)) ->
pair_derrec (Union _ Γ (Singleton _ (A)), Singleton _ (B)).
Proof.
intros A B Γ wpair. unfold pair_derrec. exists [B]. repeat split.
apply NoDup_cons. intro. inversion H. apply NoDup_nil. intros. inversion H.
subst. simpl. apply In_singleton. inversion H0. simpl.
apply MP with (ps:=[ (Union _ Γ (Singleton _ A), Imp B (Or B (Bot))); (Union _ Γ (Singleton _ A), B)]).
2: apply MPRule_I. intros. inversion H. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists B. exists (Bot). auto. inversion H0. subst. 2: inversion H1.
destruct wpair. destruct H1. destruct H2. simpl in H3. destruct x.
apply MP with (ps:=[(Union _ Γ (Singleton _ A), Imp (Bot) B);(Union _ Γ (Singleton _ A), (Bot))]).
2: apply MPRule_I. intros. inversion H4. subst. apply wEFQ. inversion H5. subst. 2: inversion H6.
assert (J1: Included _ (fst (Γ , Bot)) (Union _ Γ (Singleton _ A))). intro. intro. apply Union_introl.
assumption.
pose (BIH_monot (Γ , Bot) H3 (Union _ Γ (Singleton _ A)) J1). assumption.
destruct x. simpl in H3. assert (b=A --> B). pose (H2 b). assert (List.In b [b]). apply in_eq.
apply s in H4. inversion H4. reflexivity. subst. apply absorp_Or1 in H3.
assert (J1: Γ = Γ ). reflexivity.
assert (J2: A --> B = A --> B). reflexivity.
pose (BIH_Detachment_Theorem (Γ , A --> B) H3 A B Γ J1 J2). assumption.
exfalso. simpl in H1. inversion H1. apply H6. subst. pose (H2 b).
assert (List.In b (b :: b0 :: x)). apply in_eq. pose (s H4). inversion s0. subst.
pose (H2 b0). assert (List.In b0 (A --> B :: b0 :: x)). apply in_cons. apply in_eq.
pose (s1 H5). inversion s2. subst. apply in_eq.
Qed.
Theorem gen_BIH_Deduction_Theorem : forall A B Γ ,
pair_derrec (Union _ Γ (Singleton _ (A)), Singleton _ (B)) ->
pair_derrec (Γ , Singleton _ (A --> B)).
Proof.
intros A B Γ wpair. unfold pair_derrec. simpl. exists [(A --> B)]. repeat split.
apply NoDup_cons. intro. inversion H. apply NoDup_nil. intros. inversion H.
subst. simpl. apply In_singleton. inversion H0. simpl.
apply MP with (ps:=[(Γ , Imp (A --> B) (Or (A --> B) (Bot))); (Γ , (A --> B))]).
2: apply MPRule_I. intros. inversion H. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists (A --> B). exists (Bot). auto. inversion H0. subst. 2: inversion H1.
destruct wpair. destruct H1. destruct H2. simpl in H3. simpl in H2. destruct x. simpl in H3.
assert (J1: Union _ Γ (Singleton _ A) = Union _ Γ (Singleton _ A)). reflexivity.
assert (J2: Bot = Bot). reflexivity.
pose (BIH_Deduction_Theorem (Union _ Γ (Singleton _ A), Bot) H3 A (Bot) Γ J1 J2).
apply MP with (ps:=[(Γ , (Bot --> B) --> (A --> B));(Γ , Bot --> B)]).
2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Γ , (A --> Bot) --> (Bot --> B) --> (A --> B));(Γ , A --> Bot)]).
2: apply MPRule_I. intros. inversion H5. subst. apply Ax. apply AxRule_I. apply RA1_I. exists A.
exists (Bot). exists B. auto. inversion H6. subst. 2: inversion H7. assumption.
inversion H5. subst. 2: inversion H6. apply wEFQ.
destruct x. simpl in H3. assert (b=B). pose (H2 b). assert (List.In b [b]). apply in_eq.
apply s in H4. inversion H4. reflexivity. subst. apply absorp_Or1 in H3.
assert (J1: Union _ Γ (Singleton _ A) = Union _ Γ (Singleton _ A)). reflexivity.
assert (J2: B = B). reflexivity.
pose (BIH_Deduction_Theorem (Union _ Γ (Singleton _ A), B) H3 A B Γ J1 J2). assumption.
exfalso. simpl in H2. inversion H1. apply H6. subst. pose (H2 b).
assert (List.In b (b :: b0 :: x)). apply in_eq. pose (s H4). inversion s0. subst.
pose (H2 b0). assert (List.In b0 (b :: b0 :: x)). apply in_cons. apply in_eq.
pose (s1 H5). inversion s2. subst. apply in_eq.
Qed.
Theorem BIH_Dual_Detachment_Theorem : forall A B Δ ,
(BIH_rules (Singleton _ (Excl A B), list_disj Δ )) ->
(BIH_rules (Singleton _ (A), Or B (list_disj Δ ))).
Proof.
intros A B Δ D.
assert (J1: Singleton _ (Excl A B) = Union _ (Empty_set _) (Singleton _ (Excl A B))).
apply Extensionality_Ensembles. split. intro. intro. inversion H. subst. apply Union_intror.
apply In_singleton. intro. intro. inversion H. inversion H0. inversion H0. subst. apply In_singleton.
assert (J2: list_disj Δ = list_disj Δ ). reflexivity.
pose (BIH_Deduction_Theorem (Singleton _ (Excl A B), list_disj Δ ) D (Excl A B) (list_disj Δ )
(Empty_set _) J1 J2).
apply wdual_residuation in b.
assert (J3: @Empty_set (BPropF) = @Empty_set _). reflexivity.
assert (J4: A --> Or B (list_disj Δ ) = A --> Or B (list_disj Δ )). reflexivity.
pose (BIH_Detachment_Theorem (Empty_set _, A --> Or B (list_disj Δ )) b A (Or B (list_disj Δ ))
(Empty_set _) J3 J4). assert (Union _ (Empty_set _) (Singleton _ A) = Singleton _ A).
apply Extensionality_Ensembles. split. intro. intro. inversion H. inversion H0.
assumption. intro. intro. apply Union_intror. assumption. rewrite H in b0. assumption.
Qed.
Theorem BIH_Dual_Deduction_Theorem : forall A B Δ ,
(BIH_rules (Singleton _ (A), Or B (list_disj Δ ))) ->
(BIH_rules (Singleton _ (Excl A B), list_disj Δ )).
Proof.
intros A B Δ D.
assert (J1: Singleton _ A = Union _ (Empty_set _) (Singleton _ A)). apply Extensionality_Ensembles.
split. intro. intro. apply Union_intror. assumption. intro. intro. inversion H. inversion H0. assumption.
assert (J2: Or B (list_disj Δ ) = Or B (list_disj Δ )). reflexivity.
pose (BIH_Deduction_Theorem (Singleton _ A, Or B (list_disj Δ )) D A (Or B (list_disj Δ ))
(Empty_set _) J1 J2). apply wdual_residuation in b.
assert (J3: @Empty_set (BPropF) = Empty_set _). reflexivity.
assert (J4: Excl A B --> list_disj Δ = Excl A B --> list_disj Δ ). reflexivity.
pose (BIH_Detachment_Theorem (Empty_set _, Excl A B --> list_disj Δ ) b (Excl A B)
(list_disj Δ ) (Empty_set _) J3 J4).
assert (Union _ (Empty_set _) (Singleton _ (Excl A B)) = Singleton _ (Excl A B)).
apply Extensionality_Ensembles. split. intro. intro. inversion H. inversion H0.
assumption. intro. intro. apply Union_intror. assumption.
rewrite H in b0. assumption.
Qed.
Lemma In_remove : forall (A : BPropF) B (l : list (BPropF)), List.In A (remove eq_dec_form B l) -> List.In A l.
Proof.
intros A B. induction l.
- simpl. auto.
- intro. simpl in H. destruct (eq_dec_form B a).
* subst. apply in_cons. apply IHl. assumption.
* inversion H.
+ subst. apply in_eq.
+ subst. apply in_cons. apply IHl. auto.
Qed.
Lemma InT_remove : forall (A : BPropF) B (l : list (BPropF)), InT A (remove eq_dec_form B l) -> InT A l.
Proof.
intros A B. induction l.
- simpl. auto.
- intro. simpl in H. destruct (eq_dec_form B a).
* subst. apply InT_cons. apply IHl. assumption.
* inversion H.
+ subst. apply InT_eq.
+ subst. apply InT_cons. apply IHl. auto.
Qed.
Lemma NoDup_remove : forall A (l : list (BPropF)), NoDup l -> NoDup (remove eq_dec_form A l).
Proof.
intro A. induction l.
- intro. simpl. apply NoDup_nil.
- intro H. simpl. destruct (eq_dec_form A a).
* subst. apply IHl. inversion H. assumption.
* inversion H. subst. apply NoDup_cons. intro. apply H2. apply In_remove with (B:= A).
assumption. apply IHl. assumption.
Qed.
Lemma remove_disj : forall l B Γ , BIH_rules (Γ , list_disj l --> Or B (list_disj (remove eq_dec_form B l))).
Proof.
induction l.
- intros. simpl. apply Ax. apply AxRule_I. apply RA3_I.
exists B. exists (Bot). auto.
- intros. pose (IHl B Γ ). simpl. destruct (eq_dec_form B a).
* subst. simpl.
apply MP with (ps:=[(Γ , ((list_disj l) --> Or a (list_disj (remove eq_dec_form a l))) --> (Or a (list_disj l) --> Or a (list_disj (remove eq_dec_form a l))));
(Γ , (list_disj l) --> Or a (list_disj (remove eq_dec_form a l)))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (a --> Or a (list_disj (remove eq_dec_form a l))) --> ((list_disj l) --> Or a (list_disj (remove eq_dec_form a l))) --> (Or a (list_disj l) --> Or a (list_disj (remove eq_dec_form a l))));
(Γ , a --> Or a (list_disj (remove eq_dec_form a l)))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA4_I. exists a. exists (list_disj l). exists (Or a (list_disj (remove eq_dec_form a l))).
auto. inversion H1. subst. apply Ax. apply AxRule_I.
apply RA2_I. exists a. exists (list_disj (remove eq_dec_form a l)).
auto. inversion H2. inversion H0. subst. assumption. inversion H1.
* simpl.
apply MP with (ps:=[(Γ , (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (Or a (list_disj l) --> Or B (Or a (list_disj (remove eq_dec_form B l)))));
(Γ , (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Or a (list_disj l) --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (Or a (list_disj l) --> Or B (Or a (list_disj (remove eq_dec_form B l)))));
(Γ , (Or a (list_disj l) --> Or a (Or B (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists (Or a (list_disj l)). exists (Or a (Or B (list_disj (remove eq_dec_form B l)))).
exists (Or B (Or a (list_disj (remove eq_dec_form B l)))). auto. inversion H1. subst.
apply MP with (ps:=[(Γ , (list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (Or a (list_disj l) --> Or a (Or B (list_disj (remove eq_dec_form B l)))));
(Γ , list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l))))]). 2: apply MPRule_I.
intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (a --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (Or a (list_disj l) --> Or a (Or B (list_disj (remove eq_dec_form B l)))));
(Γ , a --> Or a (Or B (list_disj (remove eq_dec_form B l))))]). 2: apply MPRule_I.
intros. inversion H3. subst. apply Ax. apply AxRule_I. apply RA4_I.
exists a. exists (list_disj l). exists (Or a (Or B (list_disj (remove eq_dec_form B l)))).
auto. inversion H4. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists a. exists (Or B (list_disj (remove eq_dec_form B l))). auto. inversion H5.
inversion H3. subst.
apply MP with (ps:=[(Γ , ((Or B (list_disj (remove eq_dec_form B l))) --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l)))));
(Γ , (Or B (list_disj (remove eq_dec_form B l))) --> Or a (Or B (list_disj (remove eq_dec_form B l))))]).
2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Γ , (list_disj l --> (Or B (list_disj (remove eq_dec_form B l)))) --> ((Or B (list_disj (remove eq_dec_form B l))) --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l)))));
(Γ , (list_disj l --> (Or B (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H5. subst. apply Ax. apply AxRule_I. apply RA1_I. exists (list_disj l).
exists (Or B (list_disj (remove eq_dec_form B l))). exists (Or a (Or B (list_disj (remove eq_dec_form B l)))).
auto. inversion H6. subst. assumption. inversion H7. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists a. exists (Or B (list_disj (remove eq_dec_form B l))).
auto. inversion H6. inversion H4. inversion H2. inversion H0. subst.
apply MP with (ps:=[(Γ , ((Or B (list_disj (remove eq_dec_form B l)) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l))))));
(Γ , ((Or B (list_disj (remove eq_dec_form B l)) --> Or B (Or a (list_disj (remove eq_dec_form B l))))))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Γ , (a --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> ((Or B (list_disj (remove eq_dec_form B l)) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l))))));
(Γ , (a --> Or B (Or a (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I.
apply RA4_I. exists a. exists (Or B (list_disj (remove eq_dec_form B l))).
exists (Or B (Or a (list_disj (remove eq_dec_form B l)))). auto. inversion H3. subst.
apply MP with (ps:=[(Γ , ((Or a (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (a --> Or B (Or a (list_disj (remove eq_dec_form B l)))));
(Γ , (Or a (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l))))]).
2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Γ , (a --> (Or a (list_disj (remove eq_dec_form B l)))) --> ((Or a (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (a --> Or B (Or a (list_disj (remove eq_dec_form B l)))));
(Γ , (a --> (Or a (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H5. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists a. exists (Or a (list_disj (remove eq_dec_form B l))).
exists (Or B (Or a (list_disj (remove eq_dec_form B l)))). auto. inversion H6. subst.
apply Ax. apply AxRule_I.
apply RA2_I. exists a. exists (list_disj (remove eq_dec_form B l)).
auto. inversion H7. inversion H5. subst. apply Ax. apply AxRule_I.
apply RA3_I. exists B. exists (Or a (list_disj (remove eq_dec_form B l))).
auto. inversion H6. inversion H4. inversion H2. subst. apply wmonotL_Or.
apply Ax. apply AxRule_I.
apply RA3_I. exists a. exists (list_disj (remove eq_dec_form B l)).
auto. inversion H3. inversion H1.
Qed.
Theorem gen_BIH_Dual_Detachment_Theorem : forall A B Δ ,
pair_derrec (Singleton _ (Excl A B), Δ ) ->
pair_derrec (Singleton _ (A), Union _ (Singleton _ (B)) Δ ).
Proof.
intros A B Δ wpair. destruct wpair. destruct H. destruct H0. simpl in H0. simpl in H1.
exists (B :: (remove eq_dec_form B x)). repeat split.
apply NoDup_cons. apply remove_In. apply NoDup_remove. assumption.
intros. inversion H2. subst. apply Union_introl. apply In_singleton. subst.
apply Union_intror. apply H0. apply In_remove with (B:=B). assumption.
simpl.
pose (BIH_Dual_Detachment_Theorem A B x H1).
apply MP with (ps:=[(Singleton _ A, Imp (Or B (list_disj x)) (Or B (list_disj (remove eq_dec_form B x))));
(Singleton _ A, (Or B (list_disj x)))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Singleton _ A, Imp (Imp (list_disj x) (Or B (list_disj (remove eq_dec_form B x)))) ((Imp (Or B (list_disj x)) (Or B (list_disj (remove eq_dec_form B x))))));
(Singleton _ A, Imp (list_disj x) (Or B (list_disj (remove eq_dec_form B x))))]). 2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Singleton _ A, Imp (Imp (B) (Or B (list_disj (remove eq_dec_form B x)))) (Imp (Imp (list_disj x) (Or B (list_disj (remove eq_dec_form B x)))) ((Imp (Or B (list_disj x)) (Or B (list_disj (remove eq_dec_form B x)))))));
(Singleton _ A, Imp B (Or B (list_disj (remove eq_dec_form B x))))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA4_I.
exists B. exists (list_disj x). exists (Or B (list_disj (remove eq_dec_form B x))).
auto. inversion H5. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists B. exists (list_disj (remove eq_dec_form B x)). auto. inversion H6.
inversion H4. subst. apply remove_disj. inversion H5. inversion H3. subst. assumption.
inversion H4.
Qed.
Theorem gen_BIH_Dual_Deduction_Theorem : forall A B Δ ,
pair_derrec (Singleton _ (A), Union _ (Singleton _ (B)) Δ ) ->
pair_derrec (Singleton _ (Excl A B), Δ ).
Proof.
intros A B Δ wpair. destruct wpair. destruct H. destruct H0. simpl in H0. simpl in H1.
exists (remove eq_dec_form B x). repeat split.
apply NoDup_remove. assumption.
intros. simpl. pose (H0 A0). pose (In_remove _ _ _ H2). apply u in i.
inversion i. exfalso. subst. inversion H3. subst.
pose (remove_In eq_dec_form x A0). apply n. assumption. assumption.
simpl.
pose (BIH_Dual_Deduction_Theorem A B (remove eq_dec_form B x)). apply b.
apply MP with (ps:=[(Singleton _ A, Imp (list_disj x) (Or B (list_disj (remove eq_dec_form B x))));
(Singleton _ A, list_disj x)]). 2: apply MPRule_I. intros. inversion H2. subst. apply remove_disj.
inversion H3. subst. assumption. inversion H4.
Qed.
(* To help for the results about sBIH. *)
Lemma eq_dec_nat : forall (n m : nat), (n = m) + (n <> m).
Proof.
induction n.
- destruct m.
* auto.
* auto.
- intro m. destruct m.
* auto.
* destruct IHn with (m:=m).
+ left. lia.
+ right. lia.
Qed.
Lemma wT_for_DN : forall A n m Γ , (le m n) -> (BIH_rules (Γ , (DN_form n A) --> (DN_form m A))).
Proof.
intro A. induction n.
- intros. assert (m = 0). lia. rewrite H0. simpl. apply wimp_Id_gen.
- intros. destruct (eq_dec_nat m (S n)).
* subst. apply wimp_Id_gen.
* assert (m <= n). lia. pose (IHn m Γ H0).
apply MP with (ps:=[(Γ , (DN_form n A --> DN_form m A) --> (DN_form (S n) A --> DN_form m A));(Γ , (DN_form n A --> DN_form m A))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Γ , (DN_form (S n) A --> DN_form n A) --> (DN_form n A --> DN_form m A) --> (DN_form (S n) A --> DN_form m A));(Γ , (DN_form (S n) A --> DN_form n A))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA1_I. exists (DN_form (S n) A).
exists (DN_form n A). exists (DN_form m A). auto. inversion H3. subst. apply wDN_to_form.
inversion H4. inversion H2. subst. assumption. inversion H3.
Qed.
Lemma wExcl_mon : forall A B C,
(BIH_rules (Empty_set _, A --> B)) ->
(BIH_rules (Empty_set _, (Excl A C) --> (Excl B C))).
Proof.
intros. apply wdual_residuation.
apply MP with (ps:=[(Empty_set _, (B --> Or C (Excl B C)) --> (A --> Or C (Excl B C)));
(Empty_set _, (B --> Or C (Excl B C)))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Empty_set _, (A --> B) --> (B --> Or C (Excl B C)) --> (A --> Or C (Excl B C)));
(Empty_set _, (A --> B))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists B.
exists (Or C (Excl B C)). auto. inversion H2. subst. assumption. inversion H3.
inversion H1. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists B. exists C. auto. inversion H2.
Qed.
Lemma wmon_Excl : forall A B C,
(BIH_rules (Empty_set _, A --> B)) ->
(BIH_rules (Empty_set _, (Excl C B) --> (Excl C A))).
Proof.
intros. apply wdual_residuation.
apply MP with (ps:=[(Empty_set _, (Or A (Excl C A) --> Or B (Excl C A)) --> (C --> Or B (Excl C A)));
(Empty_set _, (Or A (Excl C A) --> Or B (Excl C A)))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Empty_set _, (C --> Or A (Excl C A)) --> (Or A (Excl C A) --> Or B (Excl C A)) --> (C --> Or B (Excl C A)));
(Empty_set _, C --> Or A (Excl C A))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists C. exists (Or A (Excl C A)).
exists (Or B (Excl C A)). auto. inversion H2. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists C. exists A.
auto. inversion H3. inversion H1. subst. 2: inversion H2.
apply MP with (ps:=[(Empty_set _, ((Excl C A) --> Or B (Excl C A)) --> (Or A (Excl C A) --> Or B (Excl C A)));
(Empty_set _, ((Excl C A) --> Or B (Excl C A)))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or B (Excl C A)) --> ((Excl C A) --> Or B (Excl C A)) --> (Or A (Excl C A) --> Or B (Excl C A)));
(Empty_set _, (A --> Or B (Excl C A)))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists A. exists (Excl C A).
exists (Or B (Excl C A)). auto. inversion H4. subst.
apply MP with (ps:=[(Empty_set _, (B --> Or B (Excl C A)) --> (A --> Or B (Excl C A)));
(Empty_set _, (B --> Or B (Excl C A)))]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Empty_set _, (A --> B) --> (B --> Or B (Excl C A)) --> (A --> Or B (Excl C A)));
(Empty_set _, (A --> B))]).
2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists B.
exists (Or B (Excl C A)). auto. inversion H7. subst. assumption.
inversion H8. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA2_I. exists B. exists (Excl C A). auto.
inversion H7. inversion H5. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists B. exists (Excl C A). auto.
inversion H4.
Qed.
Lemma wOr_Neg : forall A B C Γ ,
(BIH_rules (Γ , A --> (Or B C))) ->
(BIH_rules (Γ , (And (Neg B) A) --> C)).
Proof.
intros.
apply MP with (ps:=[(Γ , ((And (Neg B) (Or B C)) --> C) --> (And (Neg B) A --> C));(Γ , And (Neg B) (Or B C) --> C)]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ , ((And (Neg B) A) --> (And (Neg B) (Or B C))) --> ((And (Neg B) (Or B C)) --> C) --> (And (Neg B) A --> C));
(Γ , ((And (Neg B) A) --> (And (Neg B) (Or B C))))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And (Neg B) A). exists (And (Neg B) (Or B C)).
exists C. auto. inversion H2. subst.
apply MP with (ps:=[(Γ , (And (Neg B) A --> (Or B C)) --> (And (Neg B) A --> And (Neg B) (Or B C)));
(Γ , (And (Neg B) A --> (Or B C)))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Γ , (And (Neg B) A --> (Neg B)) --> (And (Neg B) A --> (Or B C)) --> (And (Neg B) A --> And (Neg B) (Or B C)));
(Γ , (And (Neg B) A --> (Neg B)))]).
2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (And (Neg B) A). exists (Neg B).
exists (Or B C). auto. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA5_I. exists (Neg B). exists A. auto.
inversion H6. inversion H4. subst.
apply MP with (ps:=[(Γ , (A --> Or B C) --> (And (Neg B) A --> Or B C));
(Γ , (A --> Or B C))]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (And (Neg B) A --> A) --> (A --> Or B C) --> (And (Neg B) A --> Or B C));
(Γ , (And (Neg B) A --> A))]).
2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And (Neg B) A). exists A.
exists (Or B C). auto. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA6_I. exists (Neg B). exists A. auto.
inversion H8. inversion H6. subst. assumption. inversion H7. inversion H5. inversion H3.
inversion H1. subst.
apply MP with (ps:=[(Γ , (And (Or B C) (Neg B) --> C) --> (And (Neg B) (Or B C) --> C));
(Γ , (And (Or B C) (Neg B) --> C))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (And (Neg B) (Or B C) --> And (Or B C) (Neg B)) --> (And (Or B C) (Neg B) --> C) --> (And (Neg B) (Or B C) --> C));
(Γ , And (Neg B) (Or B C) --> And (Or B C) (Neg B))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And (Neg B) (Or B C)). exists (And (Or B C) (Neg B)).
exists C. auto. inversion H4. subst.
apply MP with (ps:=[(Γ , (And (Neg B) (Or B C) --> (Neg B)) --> (And (Neg B) (Or B C) --> And (Or B C) (Neg B)));
(Γ , (And (Neg B) (Or B C) --> (Neg B)))]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (And (Neg B) (Or B C) --> (Or B C)) --> (And (Neg B) (Or B C) --> (Neg B)) --> (And (Neg B) (Or B C) --> And (Or B C) (Neg B)));
(Γ , (And (Neg B) (Or B C) --> (Or B C)))]).
2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (And (Neg B) (Or B C)). exists (Or B C).
exists (Neg B). auto. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA6_I. exists (Neg B). exists (Or B C).
auto. inversion H8. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA5_I. exists (Neg B). exists (Or B C).
auto. inversion H7. inversion H5. inversion H3. subst.
apply MP with (ps:=[(Γ , ((Or B C) --> (Neg B) --> C) --> (And (Or B C) (Neg B) --> C));
(Γ , ((Or B C) --> (Neg B) --> C))]).
2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA8_I. exists (Or B C). exists (Neg B). exists C.
auto. inversion H5. subst.
apply MP with (ps:=[(Γ , (C --> Neg B --> C) --> (Or B C --> Neg B --> C));
(Γ , (C --> Neg B --> C))]).
2: apply MPRule_I. intros. inversion H6. subst.
apply MP with (ps:=[(Γ , (B --> Neg B --> C) --> (C --> Neg B --> C) --> (Or B C --> Neg B --> C));
(Γ , (B --> Neg B --> C))]).
2: apply MPRule_I. intros. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists B. exists C.
exists (Neg B --> C). auto. inversion H8. subst.
apply MP with (ps:=[(Γ , ((And B (Neg B)) --> C) --> (B --> Neg B --> C));
(Γ , ((And B (Neg B)) --> C))]).
2: apply MPRule_I. intros. inversion H9. subst.
apply Ax. apply AxRule_I. apply RA9_I. exists B. exists (Neg B). exists C.
auto. inversion H10. subst.
apply MP with (ps:=[(Γ , (Bot --> C) --> (And B (Neg B) --> C));
(Γ , (Bot --> C))]).
2: apply MPRule_I. intros. inversion H11. subst.
apply MP with (ps:=[(Γ , (And B (Neg B) --> Bot) --> (Bot --> C) --> (And B (Neg B) --> C));
(Γ , (And B (Neg B) --> Bot))]).
2: apply MPRule_I. intros. inversion H12. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And B (Neg B)). exists (Bot).
exists (C). auto. inversion H13. subst. apply wContr_Bot. inversion H14. inversion H12. subst.
apply wEFQ. inversion H13. inversion H11. inversion H9. inversion H7. subst.
apply wThm_irrel. inversion H8. inversion H6. inversion H4. inversion H2.
Qed.
Lemma wNeg_Top : forall A B Γ ,
(BIH_rules (Γ , ((wNeg A) --> B))) ->
(BIH_rules (Γ , (Excl (Top) A) --> B)).
Proof.
intros A B Γ D. apply MP with (ps:=[(Γ , (wNeg A --> B) --> (Excl (Top) A --> B));
(Γ , (wNeg A --> B))]). 2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Excl (Top) A --> wNeg A) --> (wNeg A --> B) --> Excl (Top) A --> B);
(Γ , (Excl (Top) A --> wNeg A))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I.
apply RA1_I. exists (Excl (Top) A). exists (wNeg A). exists B. auto.
inversion H1. subst. apply wimp_Id_gen.
inversion H2. inversion H0. subst. assumption. inversion H1.
Qed.
Lemma Top_wNeg : forall A B Γ ,
(BIH_rules (Γ , (Excl (Top) A) --> B)) ->
(BIH_rules (Γ , ((wNeg A) --> B))).
Proof.
intros A B Γ D. apply MP with (ps:=[(Γ , (Excl (Top) A --> B) --> (wNeg A --> B));
(Γ , (Excl (Top) A --> B))]). 2: apply MPRule_I. intros. inversion H. subst.
intros. apply MP with (ps:=[(Γ , (wNeg A --> Excl (Top) A) --> (Excl (Top) A --> B) --> wNeg A --> B);
(Γ , (wNeg A --> Excl (Top) A))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I.
apply RA1_I. exists (wNeg A). exists (Excl (Top) A). exists B. auto.
inversion H1. subst. apply wimp_Id_gen.
inversion H2. inversion H0. subst. assumption. inversion H1.
Qed.
Lemma Top_wNeg_cons : forall A B Γ ,
(BIH_rules (Γ , A --> (Excl (Top) B))) ->
(BIH_rules (Γ , A --> (wNeg B))).
Proof.
intros. apply MP with (ps:=[(Γ , (Excl (Top) B --> wNeg B) --> (A --> wNeg B));
(Γ , (Excl (Top) B --> wNeg B))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ , (A --> Excl (Top) B) --> (Excl (Top) B --> wNeg B) --> (A --> wNeg B));
(Γ , (A --> Excl (Top) B))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I.
apply RA1_I. exists A. exists (Excl (Top) B). exists (wNeg B). auto.
inversion H2. subst. assumption. inversion H3. inversion H1. subst.
apply wimp_Id_gen. inversion H2.
Qed.
Lemma Or_imp_assoc : forall A B C D Γ ,
(BIH_rules (Γ , A --> (Or (Or B C) D))) ->
(BIH_rules (Γ , A --> (Or B (Or C D)))).
Proof.
intros.
apply MP with (ps:=[(Γ , (Or (Or B C) D --> Or B (Or C D)) --> (A --> Or B (Or C D)));
(Γ , (Or (Or B C) D --> Or B (Or C D)))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ , (A --> Or (Or B C) D) --> (Or (Or B C) D --> Or B (Or C D)) --> (A --> Or B (Or C D)));
(Γ , (A --> Or (Or B C) D))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists (Or (Or B C) D).
exists (Or B (Or C D)). auto. inversion H2. subst.
assumption. inversion H3. inversion H1. subst.
apply MP with (ps:=[(Γ , (D --> Or B (Or C D)) --> (Or (Or B C) D --> Or B (Or C D)));
(Γ , (D --> Or B (Or C D)))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , ((Or B C) --> Or B (Or C D)) --> (D --> Or B (Or C D)) --> (Or (Or B C) D --> Or B (Or C D)));
(Γ , ((Or B C) --> Or B (Or C D)))]). 2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists (Or B C).
exists D. exists (Or B (Or C D)). auto. inversion H4. subst.
apply MP with (ps:=[(Γ , (C --> Or B (Or C D)) --> (Or B C --> Or B (Or C D)));
(Γ , C --> Or B (Or C D))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (B --> Or B (Or C D)) --> (C --> Or B (Or C D)) --> (Or B C --> Or B (Or C D)));
(Γ , B --> Or B (Or C D))]). 2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists B. exists C.
exists (Or B (Or C D)). auto. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA2_I. exists B. exists (Or C D). auto.
inversion H8. inversion H6. subst.
apply MP with (ps:=[(Γ , ((Or C D) --> Or B (Or C D)) --> (C --> Or B (Or C D)));
(Γ , (Or C D) --> Or B (Or C D))]). 2: apply MPRule_I. intros. inversion H7. subst.
apply MP with (ps:=[(Γ , (C --> (Or C D)) --> ((Or C D) --> Or B (Or C D)) --> (C --> Or B (Or C D)));
(Γ , (C --> (Or C D)))]). 2: apply MPRule_I. intros. inversion H8. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists C. exists (Or C D).
exists (Or B (Or C D)). auto. inversion H9. subst.
apply Ax. apply AxRule_I. apply RA2_I. exists C. exists D. auto. inversion H10.
inversion H8. subst. apply Ax. apply AxRule_I.
apply RA3_I. exists B. exists (Or C D). auto. inversion H9. inversion H7. inversion H5.
inversion H3. subst.
apply MP with (ps:=[(Γ , ((Or C D) --> Or B (Or C D)) --> (D --> Or B (Or C D)));
(Γ , ((Or C D) --> Or B (Or C D)))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Γ , (D --> (Or C D)) --> ((Or C D) --> Or B (Or C D)) --> (D --> Or B (Or C D)));
(Γ , (D --> (Or C D)))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists D. exists (Or C D).
exists (Or B (Or C D)). auto. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists C. exists D. auto. inversion H7.
inversion H5. subst. apply Ax. apply AxRule_I. apply RA3_I. exists B. exists (Or C D). auto.
inversion H6. inversion H4. inversion H2.
Qed.
Lemma wClaim1 : forall A B Γ ,
(BIH_rules (Γ , (Neg (Excl A B)) --> ((wNeg B) --> (wNeg A)))).
Proof.
intros A B Γ .
pose (BIH_monot (Empty_set _, Neg (Excl A B) --> wNeg B --> wNeg A)). apply b. clear b.
apply MP with (ps:=[(Empty_set _, ((And (Neg (Excl A B)) (wNeg B)) --> wNeg A) --> (Neg (Excl A B) --> wNeg B --> wNeg A));
(Empty_set _, (And (Neg (Excl A B)) (wNeg B)) --> wNeg A)]). 2: apply MPRule_I. intros. inversion H. subst.
apply Ax. apply AxRule_I. apply RA9_I. exists (Neg (Excl A B)).
exists (wNeg B). exists (wNeg A). auto. inversion H0. subst.
apply MP with (ps:=[(Empty_set _, ((Excl (Top) (Or B (Excl A B))) --> wNeg A) --> (And (Neg (Excl A B)) (wNeg B) --> wNeg A));
(Empty_set _, (Excl (Top) (Or B (Excl A B))) --> wNeg A)]). 2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Empty_set _, (And (Neg (Excl A B)) (wNeg B) --> (Excl (Top) (Or B (Excl A B)))) --> ((Excl (Top) (Or B (Excl A B))) --> wNeg A) --> (And (Neg (Excl A B)) (wNeg B) --> wNeg A));
(Empty_set _, (And (Neg (Excl A B)) (wNeg B) --> (Excl (Top) (Or B (Excl A B)))))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And (Neg (Excl A B)) (wNeg B)).
exists (Excl (Top) (Or B (Excl A B))). exists (wNeg A). auto. inversion H3. subst.
apply wOr_Neg. apply Top_wNeg. apply wdual_residuation.
apply Or_imp_assoc. apply wdual_residuation. apply wimp_Id_gen. inversion H4. inversion H2. subst.
apply Top_wNeg_cons. apply wmon_Excl. apply Ax. apply AxRule_I.
apply RA11_I. exists A. exists B. auto. inversion H3. inversion H1.
intro. simpl. intros. inversion H.
Qed.
Lemma wDN_dist_imp : forall A B Γ ,
(BIH_rules (Γ , (Neg (wNeg (A --> B))) --> ((Neg (wNeg A)) --> (Neg (wNeg B))))).
Proof.
intros A B Γ .
apply MP with (ps:=[(Γ , (((wNeg B) --> wNeg A) --> Neg (wNeg A) --> Neg (wNeg B)) --> (Neg (wNeg (A --> B)) --> Neg (wNeg A) --> Neg (wNeg B)));
(Γ , (((wNeg B) --> wNeg A) --> Neg (wNeg A) --> Neg (wNeg B)))]). 2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Neg (wNeg (A --> B)) --> ((wNeg B) --> wNeg A)) --> (((wNeg B) --> wNeg A) --> Neg (wNeg A) --> Neg (wNeg B)) --> (Neg (wNeg (A --> B)) --> Neg (wNeg A) --> Neg (wNeg B)));
(Γ , (Neg (wNeg (A --> B)) --> ((wNeg B) --> wNeg A)))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Neg (wNeg (A --> B))).
exists (wNeg B --> wNeg A). exists (Neg (wNeg A) --> Neg (wNeg B)). auto. inversion H1. subst.
apply MP with (ps:=[(Γ ,((Neg (Excl A B)) --> (wNeg B --> wNeg A)) --> (Neg (wNeg (A --> B)) --> wNeg B --> wNeg A));
(Γ , ((Neg (Excl A B)) --> (wNeg B --> wNeg A)))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ ,(Neg (wNeg (A --> B)) --> (Neg (Excl A B))) --> ((Neg (Excl A B)) --> (wNeg B --> wNeg A)) --> (Neg (wNeg (A --> B)) --> wNeg B --> wNeg A));
(Γ , (Neg (wNeg (A --> B)) --> (Neg (Excl A B))))]). 2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Neg (wNeg (A --> B))).
exists (Neg (Excl A B)). exists (wNeg B --> wNeg A). auto. inversion H4. subst.
apply MP with (ps:=[(Γ , ((Excl A B) --> (wNeg (A --> B))) --> (Neg (wNeg (A --> B)) --> Neg (Excl A B)));
(Γ , (Excl A B) --> (wNeg (A --> B)))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA10_I. exists (Excl A B).
exists (wNeg (A --> B)). auto. inversion H6. subst. apply Ax.
apply AxRule_I. apply RA12_I. exists A. exists B. auto. inversion H7. inversion H5.
inversion H3. subst. apply wClaim1. inversion H4. inversion H2. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA10_I. exists (wNeg B).
exists (wNeg A). auto. inversion H1.
Qed.
Export ListNotations.
Require Import CPP_genT.
Require Import PeanoNat.
Require Import Lia.
Require Import Ensembles.
Require Import CPP_BiInt_GHC.
Require Import CPP_BiInt_logic.
Require Import CPP_BiInt_meta_interactions1.
Theorem BIH_Detachment_Theorem : forall s,
(BIH_rules s) ->
(forall A B Γ , (fst s = Γ ) ->
(snd s = A --> B) ->
BIH_rules (Union _ Γ (Singleton _ (A)), B)).
Proof.
intros s D. induction D.
(* Id *)
- intros A B Γ id1 id2. inversion H. subst. simpl in id2. subst.
simpl. apply MP with (ps:=[(Union _ Γ0 (Singleton _ A), Imp A B);(Union _ Γ0 (Singleton _ A), A)]).
2: apply MPRule_I. intros. inversion H1. subst. apply Id.
apply IdRule_I. apply Union_introl. assumption. inversion H2. subst.
apply Id. apply IdRule_I. apply Union_intror. apply In_singleton. inversion H3.
(* Ax *)
- intros A B Γ id1 id2. inversion H. subst. simpl in id2. subst. simpl.
apply MP with (ps:=[(Union _ Γ0 (Singleton _ A), Imp A B);(Union _ Γ0 (Singleton _ A), A)]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax.
apply AxRule_I. assumption. inversion H2. subst. apply Id. apply IdRule_I.
apply Union_intror. apply In_singleton. inversion H3.
(* MP *)
- intros A B Γ id1 id2. inversion H1. subst. simpl in id2. subst. simpl.
assert (J01: List.In (Γ0, A0 --> A --> B) [(Γ0, A0 --> A --> B); (Γ0, A0)]). apply in_eq.
assert (J1: Γ0 = Γ0). reflexivity.
assert (J2: A0 --> A --> B = A0 --> A --> B). reflexivity.
pose (H0 (Γ0, A0 --> A --> B) J01 A0 (Imp A B) Γ0 J1 J2).
assert (BIH_rules (Γ0, A --> B)).
assert (J3: (forall A1 : BPropF, fst (Union _ Γ0 (Singleton _ A0), A --> B) A1 ->
BIH_rules (Γ0, A1))).
intro. simpl. intro. inversion H2. subst. apply Id.
apply IdRule_I. assumption. subst. inversion H3. subst.
assert (J02: List.In (Γ0, A1) [(Γ0, A1 --> A --> B); (Γ0, A1)]). apply in_cons. apply in_eq.
pose (H (Γ0, A1) J02). assumption.
pose (BIH_comp (Union _ Γ0 (Singleton _ A0), A --> B) b Γ0 J3). simpl in b0. assumption.
apply MP with (ps:=[(Union _ Γ0 (Singleton _ A), (Imp A B));(Union _ Γ0 (Singleton _ A), A)]).
2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Union _ Γ0 (Singleton _ A), Imp A0 (Imp A B));(Union _ Γ0 (Singleton _ A), A0)]).
2: apply MPRule_I. intros. inversion H4. subst.
assert (J4: Included _ (fst (Γ0, A0 --> A --> B)) (Union _ Γ0 (Singleton _ A))).
simpl. intro. intro. apply Union_introl. assumption. pose (H (Γ0, A0 --> A --> B) J01).
pose (BIH_monot (Γ0, A0 --> A --> B) b0 (Union _ Γ0 (Singleton _ A)) J4). assumption.
inversion H5. subst.
assert (J4: Included _ (fst (Γ0, A0 --> A --> B)) (Union _ Γ0 (Singleton _ A))).
simpl. intro. intro. apply Union_introl. assumption.
pose (BIH_monot (Γ0, A0)). apply b0. apply H. apply in_cons. apply in_eq.
auto. inversion H6. inversion H4. subst. apply Id. apply IdRule_I. apply Union_intror.
apply In_singleton. inversion H5.
(* DNw *)
- intros A B Γ id1 id2. inversion H1. subst. simpl in id2. subst. inversion id2. subst. simpl.
assert (J01: List.In (Empty_set (BPropF), A0) [(Empty_set (BPropF), A0)]). apply in_eq.
apply H in J01. remember (Union (BPropF) Γ0 (Singleton (BPropF) (wNeg A0))) as Γ .
apply MP with (ps:=[(Γ , (And (wNeg A0) (Neg (wNeg A0))) --> Bot); (Γ , And (wNeg A0) (Neg (wNeg A0)))]).
2: apply MPRule_I. intros. inversion H2. rewrite <- H3. apply wContr_Bot. inversion H3.
rewrite <- H4.
apply MP with (ps:=[(Γ ,(Top --> (And (wNeg A0) (Neg (wNeg A0)))));(Γ , Top)]).
2: apply MPRule_I. intros. inversion H5. rewrite <- H6.
apply MP with (ps:=[(Γ ,(Top --> (Neg (wNeg A0))) --> (Top --> (And (wNeg A0) (Neg (wNeg A0)))));(Γ , Top --> (Neg (wNeg A0)))]).
2: apply MPRule_I. intros. inversion H7. rewrite <- H8.
apply MP with (ps:=[(Γ ,(Top --> (wNeg A0)) --> (Top --> (Neg (wNeg A0))) --> (Top --> (And (wNeg A0) (Neg (wNeg A0)))));(Γ , Top --> (wNeg A0))]).
2: apply MPRule_I. intros. inversion H9. rewrite <- H10. apply Ax. apply AxRule_I.
apply RA7_I. exists (Top). exists (wNeg A0). exists (Neg (wNeg A0)). auto. inversion H10. 2: inversion H11.
rewrite <- H11.
apply MP with (ps:=[(Γ , wNeg A0 --> Top --> wNeg A0);(Γ , wNeg A0)]). intros. 2: apply MPRule_I.
inversion H12. rewrite <- H13. apply wThm_irrel. inversion H13. 2: inversion H14. rewrite <- H14.
apply Id. apply IdRule_I. subst. apply Union_intror. apply In_singleton.
inversion H8. rewrite <- H9.
apply MP with (ps:=[(Γ , Neg (wNeg A0) --> Top --> Neg (wNeg A0));(Γ , Neg (wNeg A0))]). intros. 2: apply MPRule_I.
inversion H10. rewrite <- H11. apply wThm_irrel. inversion H11. 2: inversion H12. rewrite <- H12.
apply DNw with (ps:=[(Empty_set (BPropF), A0)]) ; auto. apply DNwRule_I. inversion H9.
inversion H6. subst. apply wTop. inversion H7. inversion H4.
Qed.
Theorem BIH_Deduction_Theorem : forall s,
(BIH_rules s) ->
(forall A B Γ , (fst s = Union _ Γ (Singleton _ (A))) ->
(snd s = B) ->
BIH_rules (Γ , A --> B)).
Proof.
intros s D. induction D.
(* Id *)
- intros A B Γ id1 id2. inversion H. subst. simpl in id1. subst. simpl. inversion H0.
+ subst. apply MP with (ps:=[(Γ , A0 --> A --> A0);(Γ , A0)]). 2: apply MPRule_I. intros. inversion H2. subst.
apply wThm_irrel. inversion H3. subst. apply Id. apply IdRule_I. assumption.
inversion H4.
+ subst. inversion H1. subst. apply wimp_Id_gen.
(* Ax *)
- intros A B Γ id1 id2. inversion H. subst. simpl in id1. subst. simpl.
apply MP with (ps:=[(Γ , A0 --> A --> A0);(Γ , A0)]). 2: apply MPRule_I. intros. inversion H1. subst.
apply wThm_irrel. inversion H2. subst.
apply Ax. apply AxRule_I. assumption. inversion H3.
(* MP *)
- intros A B Γ id1 id2. inversion H1. subst. simpl in id1. subst. simpl.
assert (J1: Union _ Γ (Singleton _ A) = Union _ Γ (Singleton _ A)). reflexivity.
assert (J2: A0 --> B0 = A0 --> B0). reflexivity.
assert (J20: List.In (Union (BPropF) Γ (Singleton (BPropF) A), A0 --> B0) [(Union (BPropF) Γ (Singleton (BPropF) A), A0 --> B0); (Union (BPropF) Γ (Singleton (BPropF) A), A0)]).
apply in_eq.
pose (H0 (Union (BPropF) Γ (Singleton (BPropF) A), A0 --> B0) J20
A (Imp A0 B0) Γ J1 J2).
assert (J3: A0 = A0). reflexivity.
apply MP with (ps:=[(Γ , (And A A0 --> B0) --> (A --> B0));(Γ , And A A0 --> B0)]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (A --> And A A0) --> (And A A0 --> B0) --> (A --> B0));(Γ , A --> And A A0)]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (And A A0). exists B0. auto.
inversion H4. subst. 2: inversion H5.
apply MP with (ps:=[(Γ , (A --> A0) --> (A --> And A A0));(Γ , A --> A0)]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (A --> A) --> (A --> A0) --> (A --> And A A0));(Γ , A --> A)]).
2: apply MPRule_I. intros. inversion H6. subst. apply Ax.
apply AxRule_I. apply RA7_I. exists A. exists A. exists A0. auto. inversion H7.
subst. apply wimp_Id_gen. inversion H8. inversion H6. subst. 2: inversion H7.
assert (J30: List.In (Union (BPropF) Γ (Singleton (BPropF) A), A0) [(Union (BPropF) Γ (Singleton (BPropF) A), A0 --> B0); (Union (BPropF) Γ (Singleton (BPropF) A), A0)]).
apply in_cons. apply in_eq. assert (J40: A0 = A0). reflexivity.
pose (H0 (Union (BPropF) Γ (Singleton (BPropF) A), A0) J30
A A0 Γ J1 J40). auto. inversion H3. subst.
apply MP with (ps:=[(Γ , (A --> A0 --> B0) --> (And A A0 --> B0));(Γ , (A --> A0 --> B0))]).
2: apply MPRule_I. intros. inversion H4. subst. apply Ax.
apply AxRule_I. apply RA8_I. exists A. exists A0. exists B0. auto.
inversion H5. subst. assumption. inversion H6. inversion H4.
(* DNw *)
- intros A B Γ id1 id2. inversion H1. subst. simpl in id1. subst. simpl.
assert (J1: BIH_rules (Empty_set _, Neg (wNeg A0))).
apply DNw with (ps:=[(Empty_set _, A0)]). 2: apply DNwRule_I. assumption.
assert (J2: Included _ (fst (Empty_set _, Neg (wNeg A0))) Γ ). intro. intro. inversion H2.
pose (BIH_monot (Empty_set _, Neg (wNeg A0)) J1 Γ J2). simpl in b.
apply MP with (ps:=[(Γ , Neg (wNeg A0) --> A --> Neg (wNeg A0)); (Γ , Neg (wNeg A0))]).
2: apply MPRule_I. intros. inversion H2. subst. apply wThm_irrel.
inversion H3. subst. 2: inversion H4. assumption.
Qed.
Theorem gen_BIH_Detachment_Theorem : forall A B Γ ,
pair_derrec (Γ , Singleton _ (A --> B)) ->
pair_derrec (Union _ Γ (Singleton _ (A)), Singleton _ (B)).
Proof.
intros A B Γ wpair. unfold pair_derrec. exists [B]. repeat split.
apply NoDup_cons. intro. inversion H. apply NoDup_nil. intros. inversion H.
subst. simpl. apply In_singleton. inversion H0. simpl.
apply MP with (ps:=[ (Union _ Γ (Singleton _ A), Imp B (Or B (Bot))); (Union _ Γ (Singleton _ A), B)]).
2: apply MPRule_I. intros. inversion H. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists B. exists (Bot). auto. inversion H0. subst. 2: inversion H1.
destruct wpair. destruct H1. destruct H2. simpl in H3. destruct x.
apply MP with (ps:=[(Union _ Γ (Singleton _ A), Imp (Bot) B);(Union _ Γ (Singleton _ A), (Bot))]).
2: apply MPRule_I. intros. inversion H4. subst. apply wEFQ. inversion H5. subst. 2: inversion H6.
assert (J1: Included _ (fst (Γ , Bot)) (Union _ Γ (Singleton _ A))). intro. intro. apply Union_introl.
assumption.
pose (BIH_monot (Γ , Bot) H3 (Union _ Γ (Singleton _ A)) J1). assumption.
destruct x. simpl in H3. assert (b=A --> B). pose (H2 b). assert (List.In b [b]). apply in_eq.
apply s in H4. inversion H4. reflexivity. subst. apply absorp_Or1 in H3.
assert (J1: Γ = Γ ). reflexivity.
assert (J2: A --> B = A --> B). reflexivity.
pose (BIH_Detachment_Theorem (Γ , A --> B) H3 A B Γ J1 J2). assumption.
exfalso. simpl in H1. inversion H1. apply H6. subst. pose (H2 b).
assert (List.In b (b :: b0 :: x)). apply in_eq. pose (s H4). inversion s0. subst.
pose (H2 b0). assert (List.In b0 (A --> B :: b0 :: x)). apply in_cons. apply in_eq.
pose (s1 H5). inversion s2. subst. apply in_eq.
Qed.
Theorem gen_BIH_Deduction_Theorem : forall A B Γ ,
pair_derrec (Union _ Γ (Singleton _ (A)), Singleton _ (B)) ->
pair_derrec (Γ , Singleton _ (A --> B)).
Proof.
intros A B Γ wpair. unfold pair_derrec. simpl. exists [(A --> B)]. repeat split.
apply NoDup_cons. intro. inversion H. apply NoDup_nil. intros. inversion H.
subst. simpl. apply In_singleton. inversion H0. simpl.
apply MP with (ps:=[(Γ , Imp (A --> B) (Or (A --> B) (Bot))); (Γ , (A --> B))]).
2: apply MPRule_I. intros. inversion H. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists (A --> B). exists (Bot). auto. inversion H0. subst. 2: inversion H1.
destruct wpair. destruct H1. destruct H2. simpl in H3. simpl in H2. destruct x. simpl in H3.
assert (J1: Union _ Γ (Singleton _ A) = Union _ Γ (Singleton _ A)). reflexivity.
assert (J2: Bot = Bot). reflexivity.
pose (BIH_Deduction_Theorem (Union _ Γ (Singleton _ A), Bot) H3 A (Bot) Γ J1 J2).
apply MP with (ps:=[(Γ , (Bot --> B) --> (A --> B));(Γ , Bot --> B)]).
2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Γ , (A --> Bot) --> (Bot --> B) --> (A --> B));(Γ , A --> Bot)]).
2: apply MPRule_I. intros. inversion H5. subst. apply Ax. apply AxRule_I. apply RA1_I. exists A.
exists (Bot). exists B. auto. inversion H6. subst. 2: inversion H7. assumption.
inversion H5. subst. 2: inversion H6. apply wEFQ.
destruct x. simpl in H3. assert (b=B). pose (H2 b). assert (List.In b [b]). apply in_eq.
apply s in H4. inversion H4. reflexivity. subst. apply absorp_Or1 in H3.
assert (J1: Union _ Γ (Singleton _ A) = Union _ Γ (Singleton _ A)). reflexivity.
assert (J2: B = B). reflexivity.
pose (BIH_Deduction_Theorem (Union _ Γ (Singleton _ A), B) H3 A B Γ J1 J2). assumption.
exfalso. simpl in H2. inversion H1. apply H6. subst. pose (H2 b).
assert (List.In b (b :: b0 :: x)). apply in_eq. pose (s H4). inversion s0. subst.
pose (H2 b0). assert (List.In b0 (b :: b0 :: x)). apply in_cons. apply in_eq.
pose (s1 H5). inversion s2. subst. apply in_eq.
Qed.
Theorem BIH_Dual_Detachment_Theorem : forall A B Δ ,
(BIH_rules (Singleton _ (Excl A B), list_disj Δ )) ->
(BIH_rules (Singleton _ (A), Or B (list_disj Δ ))).
Proof.
intros A B Δ D.
assert (J1: Singleton _ (Excl A B) = Union _ (Empty_set _) (Singleton _ (Excl A B))).
apply Extensionality_Ensembles. split. intro. intro. inversion H. subst. apply Union_intror.
apply In_singleton. intro. intro. inversion H. inversion H0. inversion H0. subst. apply In_singleton.
assert (J2: list_disj Δ = list_disj Δ ). reflexivity.
pose (BIH_Deduction_Theorem (Singleton _ (Excl A B), list_disj Δ ) D (Excl A B) (list_disj Δ )
(Empty_set _) J1 J2).
apply wdual_residuation in b.
assert (J3: @Empty_set (BPropF) = @Empty_set _). reflexivity.
assert (J4: A --> Or B (list_disj Δ ) = A --> Or B (list_disj Δ )). reflexivity.
pose (BIH_Detachment_Theorem (Empty_set _, A --> Or B (list_disj Δ )) b A (Or B (list_disj Δ ))
(Empty_set _) J3 J4). assert (Union _ (Empty_set _) (Singleton _ A) = Singleton _ A).
apply Extensionality_Ensembles. split. intro. intro. inversion H. inversion H0.
assumption. intro. intro. apply Union_intror. assumption. rewrite H in b0. assumption.
Qed.
Theorem BIH_Dual_Deduction_Theorem : forall A B Δ ,
(BIH_rules (Singleton _ (A), Or B (list_disj Δ ))) ->
(BIH_rules (Singleton _ (Excl A B), list_disj Δ )).
Proof.
intros A B Δ D.
assert (J1: Singleton _ A = Union _ (Empty_set _) (Singleton _ A)). apply Extensionality_Ensembles.
split. intro. intro. apply Union_intror. assumption. intro. intro. inversion H. inversion H0. assumption.
assert (J2: Or B (list_disj Δ ) = Or B (list_disj Δ )). reflexivity.
pose (BIH_Deduction_Theorem (Singleton _ A, Or B (list_disj Δ )) D A (Or B (list_disj Δ ))
(Empty_set _) J1 J2). apply wdual_residuation in b.
assert (J3: @Empty_set (BPropF) = Empty_set _). reflexivity.
assert (J4: Excl A B --> list_disj Δ = Excl A B --> list_disj Δ ). reflexivity.
pose (BIH_Detachment_Theorem (Empty_set _, Excl A B --> list_disj Δ ) b (Excl A B)
(list_disj Δ ) (Empty_set _) J3 J4).
assert (Union _ (Empty_set _) (Singleton _ (Excl A B)) = Singleton _ (Excl A B)).
apply Extensionality_Ensembles. split. intro. intro. inversion H. inversion H0.
assumption. intro. intro. apply Union_intror. assumption.
rewrite H in b0. assumption.
Qed.
Lemma In_remove : forall (A : BPropF) B (l : list (BPropF)), List.In A (remove eq_dec_form B l) -> List.In A l.
Proof.
intros A B. induction l.
- simpl. auto.
- intro. simpl in H. destruct (eq_dec_form B a).
* subst. apply in_cons. apply IHl. assumption.
* inversion H.
+ subst. apply in_eq.
+ subst. apply in_cons. apply IHl. auto.
Qed.
Lemma InT_remove : forall (A : BPropF) B (l : list (BPropF)), InT A (remove eq_dec_form B l) -> InT A l.
Proof.
intros A B. induction l.
- simpl. auto.
- intro. simpl in H. destruct (eq_dec_form B a).
* subst. apply InT_cons. apply IHl. assumption.
* inversion H.
+ subst. apply InT_eq.
+ subst. apply InT_cons. apply IHl. auto.
Qed.
Lemma NoDup_remove : forall A (l : list (BPropF)), NoDup l -> NoDup (remove eq_dec_form A l).
Proof.
intro A. induction l.
- intro. simpl. apply NoDup_nil.
- intro H. simpl. destruct (eq_dec_form A a).
* subst. apply IHl. inversion H. assumption.
* inversion H. subst. apply NoDup_cons. intro. apply H2. apply In_remove with (B:= A).
assumption. apply IHl. assumption.
Qed.
Lemma remove_disj : forall l B Γ , BIH_rules (Γ , list_disj l --> Or B (list_disj (remove eq_dec_form B l))).
Proof.
induction l.
- intros. simpl. apply Ax. apply AxRule_I. apply RA3_I.
exists B. exists (Bot). auto.
- intros. pose (IHl B Γ ). simpl. destruct (eq_dec_form B a).
* subst. simpl.
apply MP with (ps:=[(Γ , ((list_disj l) --> Or a (list_disj (remove eq_dec_form a l))) --> (Or a (list_disj l) --> Or a (list_disj (remove eq_dec_form a l))));
(Γ , (list_disj l) --> Or a (list_disj (remove eq_dec_form a l)))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (a --> Or a (list_disj (remove eq_dec_form a l))) --> ((list_disj l) --> Or a (list_disj (remove eq_dec_form a l))) --> (Or a (list_disj l) --> Or a (list_disj (remove eq_dec_form a l))));
(Γ , a --> Or a (list_disj (remove eq_dec_form a l)))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA4_I. exists a. exists (list_disj l). exists (Or a (list_disj (remove eq_dec_form a l))).
auto. inversion H1. subst. apply Ax. apply AxRule_I.
apply RA2_I. exists a. exists (list_disj (remove eq_dec_form a l)).
auto. inversion H2. inversion H0. subst. assumption. inversion H1.
* simpl.
apply MP with (ps:=[(Γ , (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (Or a (list_disj l) --> Or B (Or a (list_disj (remove eq_dec_form B l)))));
(Γ , (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Or a (list_disj l) --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (Or a (list_disj l) --> Or B (Or a (list_disj (remove eq_dec_form B l)))));
(Γ , (Or a (list_disj l) --> Or a (Or B (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists (Or a (list_disj l)). exists (Or a (Or B (list_disj (remove eq_dec_form B l)))).
exists (Or B (Or a (list_disj (remove eq_dec_form B l)))). auto. inversion H1. subst.
apply MP with (ps:=[(Γ , (list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (Or a (list_disj l) --> Or a (Or B (list_disj (remove eq_dec_form B l)))));
(Γ , list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l))))]). 2: apply MPRule_I.
intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (a --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (Or a (list_disj l) --> Or a (Or B (list_disj (remove eq_dec_form B l)))));
(Γ , a --> Or a (Or B (list_disj (remove eq_dec_form B l))))]). 2: apply MPRule_I.
intros. inversion H3. subst. apply Ax. apply AxRule_I. apply RA4_I.
exists a. exists (list_disj l). exists (Or a (Or B (list_disj (remove eq_dec_form B l)))).
auto. inversion H4. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists a. exists (Or B (list_disj (remove eq_dec_form B l))). auto. inversion H5.
inversion H3. subst.
apply MP with (ps:=[(Γ , ((Or B (list_disj (remove eq_dec_form B l))) --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l)))));
(Γ , (Or B (list_disj (remove eq_dec_form B l))) --> Or a (Or B (list_disj (remove eq_dec_form B l))))]).
2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Γ , (list_disj l --> (Or B (list_disj (remove eq_dec_form B l)))) --> ((Or B (list_disj (remove eq_dec_form B l))) --> Or a (Or B (list_disj (remove eq_dec_form B l)))) --> (list_disj l --> Or a (Or B (list_disj (remove eq_dec_form B l)))));
(Γ , (list_disj l --> (Or B (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H5. subst. apply Ax. apply AxRule_I. apply RA1_I. exists (list_disj l).
exists (Or B (list_disj (remove eq_dec_form B l))). exists (Or a (Or B (list_disj (remove eq_dec_form B l)))).
auto. inversion H6. subst. assumption. inversion H7. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists a. exists (Or B (list_disj (remove eq_dec_form B l))).
auto. inversion H6. inversion H4. inversion H2. inversion H0. subst.
apply MP with (ps:=[(Γ , ((Or B (list_disj (remove eq_dec_form B l)) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l))))));
(Γ , ((Or B (list_disj (remove eq_dec_form B l)) --> Or B (Or a (list_disj (remove eq_dec_form B l))))))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Γ , (a --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> ((Or B (list_disj (remove eq_dec_form B l)) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (Or a (Or B (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l))))));
(Γ , (a --> Or B (Or a (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I.
apply RA4_I. exists a. exists (Or B (list_disj (remove eq_dec_form B l))).
exists (Or B (Or a (list_disj (remove eq_dec_form B l)))). auto. inversion H3. subst.
apply MP with (ps:=[(Γ , ((Or a (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (a --> Or B (Or a (list_disj (remove eq_dec_form B l)))));
(Γ , (Or a (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l))))]).
2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Γ , (a --> (Or a (list_disj (remove eq_dec_form B l)))) --> ((Or a (list_disj (remove eq_dec_form B l))) --> Or B (Or a (list_disj (remove eq_dec_form B l)))) --> (a --> Or B (Or a (list_disj (remove eq_dec_form B l)))));
(Γ , (a --> (Or a (list_disj (remove eq_dec_form B l)))))]).
2: apply MPRule_I. intros. inversion H5. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists a. exists (Or a (list_disj (remove eq_dec_form B l))).
exists (Or B (Or a (list_disj (remove eq_dec_form B l)))). auto. inversion H6. subst.
apply Ax. apply AxRule_I.
apply RA2_I. exists a. exists (list_disj (remove eq_dec_form B l)).
auto. inversion H7. inversion H5. subst. apply Ax. apply AxRule_I.
apply RA3_I. exists B. exists (Or a (list_disj (remove eq_dec_form B l))).
auto. inversion H6. inversion H4. inversion H2. subst. apply wmonotL_Or.
apply Ax. apply AxRule_I.
apply RA3_I. exists a. exists (list_disj (remove eq_dec_form B l)).
auto. inversion H3. inversion H1.
Qed.
Theorem gen_BIH_Dual_Detachment_Theorem : forall A B Δ ,
pair_derrec (Singleton _ (Excl A B), Δ ) ->
pair_derrec (Singleton _ (A), Union _ (Singleton _ (B)) Δ ).
Proof.
intros A B Δ wpair. destruct wpair. destruct H. destruct H0. simpl in H0. simpl in H1.
exists (B :: (remove eq_dec_form B x)). repeat split.
apply NoDup_cons. apply remove_In. apply NoDup_remove. assumption.
intros. inversion H2. subst. apply Union_introl. apply In_singleton. subst.
apply Union_intror. apply H0. apply In_remove with (B:=B). assumption.
simpl.
pose (BIH_Dual_Detachment_Theorem A B x H1).
apply MP with (ps:=[(Singleton _ A, Imp (Or B (list_disj x)) (Or B (list_disj (remove eq_dec_form B x))));
(Singleton _ A, (Or B (list_disj x)))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Singleton _ A, Imp (Imp (list_disj x) (Or B (list_disj (remove eq_dec_form B x)))) ((Imp (Or B (list_disj x)) (Or B (list_disj (remove eq_dec_form B x))))));
(Singleton _ A, Imp (list_disj x) (Or B (list_disj (remove eq_dec_form B x))))]). 2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Singleton _ A, Imp (Imp (B) (Or B (list_disj (remove eq_dec_form B x)))) (Imp (Imp (list_disj x) (Or B (list_disj (remove eq_dec_form B x)))) ((Imp (Or B (list_disj x)) (Or B (list_disj (remove eq_dec_form B x)))))));
(Singleton _ A, Imp B (Or B (list_disj (remove eq_dec_form B x))))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA4_I.
exists B. exists (list_disj x). exists (Or B (list_disj (remove eq_dec_form B x))).
auto. inversion H5. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists B. exists (list_disj (remove eq_dec_form B x)). auto. inversion H6.
inversion H4. subst. apply remove_disj. inversion H5. inversion H3. subst. assumption.
inversion H4.
Qed.
Theorem gen_BIH_Dual_Deduction_Theorem : forall A B Δ ,
pair_derrec (Singleton _ (A), Union _ (Singleton _ (B)) Δ ) ->
pair_derrec (Singleton _ (Excl A B), Δ ).
Proof.
intros A B Δ wpair. destruct wpair. destruct H. destruct H0. simpl in H0. simpl in H1.
exists (remove eq_dec_form B x). repeat split.
apply NoDup_remove. assumption.
intros. simpl. pose (H0 A0). pose (In_remove _ _ _ H2). apply u in i.
inversion i. exfalso. subst. inversion H3. subst.
pose (remove_In eq_dec_form x A0). apply n. assumption. assumption.
simpl.
pose (BIH_Dual_Deduction_Theorem A B (remove eq_dec_form B x)). apply b.
apply MP with (ps:=[(Singleton _ A, Imp (list_disj x) (Or B (list_disj (remove eq_dec_form B x))));
(Singleton _ A, list_disj x)]). 2: apply MPRule_I. intros. inversion H2. subst. apply remove_disj.
inversion H3. subst. assumption. inversion H4.
Qed.
(* To help for the results about sBIH. *)
Lemma eq_dec_nat : forall (n m : nat), (n = m) + (n <> m).
Proof.
induction n.
- destruct m.
* auto.
* auto.
- intro m. destruct m.
* auto.
* destruct IHn with (m:=m).
+ left. lia.
+ right. lia.
Qed.
Lemma wT_for_DN : forall A n m Γ , (le m n) -> (BIH_rules (Γ , (DN_form n A) --> (DN_form m A))).
Proof.
intro A. induction n.
- intros. assert (m = 0). lia. rewrite H0. simpl. apply wimp_Id_gen.
- intros. destruct (eq_dec_nat m (S n)).
* subst. apply wimp_Id_gen.
* assert (m <= n). lia. pose (IHn m Γ H0).
apply MP with (ps:=[(Γ , (DN_form n A --> DN_form m A) --> (DN_form (S n) A --> DN_form m A));(Γ , (DN_form n A --> DN_form m A))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Γ , (DN_form (S n) A --> DN_form n A) --> (DN_form n A --> DN_form m A) --> (DN_form (S n) A --> DN_form m A));(Γ , (DN_form (S n) A --> DN_form n A))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA1_I. exists (DN_form (S n) A).
exists (DN_form n A). exists (DN_form m A). auto. inversion H3. subst. apply wDN_to_form.
inversion H4. inversion H2. subst. assumption. inversion H3.
Qed.
Lemma wExcl_mon : forall A B C,
(BIH_rules (Empty_set _, A --> B)) ->
(BIH_rules (Empty_set _, (Excl A C) --> (Excl B C))).
Proof.
intros. apply wdual_residuation.
apply MP with (ps:=[(Empty_set _, (B --> Or C (Excl B C)) --> (A --> Or C (Excl B C)));
(Empty_set _, (B --> Or C (Excl B C)))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Empty_set _, (A --> B) --> (B --> Or C (Excl B C)) --> (A --> Or C (Excl B C)));
(Empty_set _, (A --> B))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists B.
exists (Or C (Excl B C)). auto. inversion H2. subst. assumption. inversion H3.
inversion H1. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists B. exists C. auto. inversion H2.
Qed.
Lemma wmon_Excl : forall A B C,
(BIH_rules (Empty_set _, A --> B)) ->
(BIH_rules (Empty_set _, (Excl C B) --> (Excl C A))).
Proof.
intros. apply wdual_residuation.
apply MP with (ps:=[(Empty_set _, (Or A (Excl C A) --> Or B (Excl C A)) --> (C --> Or B (Excl C A)));
(Empty_set _, (Or A (Excl C A) --> Or B (Excl C A)))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Empty_set _, (C --> Or A (Excl C A)) --> (Or A (Excl C A) --> Or B (Excl C A)) --> (C --> Or B (Excl C A)));
(Empty_set _, C --> Or A (Excl C A))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists C. exists (Or A (Excl C A)).
exists (Or B (Excl C A)). auto. inversion H2. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists C. exists A.
auto. inversion H3. inversion H1. subst. 2: inversion H2.
apply MP with (ps:=[(Empty_set _, ((Excl C A) --> Or B (Excl C A)) --> (Or A (Excl C A) --> Or B (Excl C A)));
(Empty_set _, ((Excl C A) --> Or B (Excl C A)))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or B (Excl C A)) --> ((Excl C A) --> Or B (Excl C A)) --> (Or A (Excl C A) --> Or B (Excl C A)));
(Empty_set _, (A --> Or B (Excl C A)))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists A. exists (Excl C A).
exists (Or B (Excl C A)). auto. inversion H4. subst.
apply MP with (ps:=[(Empty_set _, (B --> Or B (Excl C A)) --> (A --> Or B (Excl C A)));
(Empty_set _, (B --> Or B (Excl C A)))]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Empty_set _, (A --> B) --> (B --> Or B (Excl C A)) --> (A --> Or B (Excl C A)));
(Empty_set _, (A --> B))]).
2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists B.
exists (Or B (Excl C A)). auto. inversion H7. subst. assumption.
inversion H8. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA2_I. exists B. exists (Excl C A). auto.
inversion H7. inversion H5. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists B. exists (Excl C A). auto.
inversion H4.
Qed.
Lemma wOr_Neg : forall A B C Γ ,
(BIH_rules (Γ , A --> (Or B C))) ->
(BIH_rules (Γ , (And (Neg B) A) --> C)).
Proof.
intros.
apply MP with (ps:=[(Γ , ((And (Neg B) (Or B C)) --> C) --> (And (Neg B) A --> C));(Γ , And (Neg B) (Or B C) --> C)]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ , ((And (Neg B) A) --> (And (Neg B) (Or B C))) --> ((And (Neg B) (Or B C)) --> C) --> (And (Neg B) A --> C));
(Γ , ((And (Neg B) A) --> (And (Neg B) (Or B C))))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And (Neg B) A). exists (And (Neg B) (Or B C)).
exists C. auto. inversion H2. subst.
apply MP with (ps:=[(Γ , (And (Neg B) A --> (Or B C)) --> (And (Neg B) A --> And (Neg B) (Or B C)));
(Γ , (And (Neg B) A --> (Or B C)))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Γ , (And (Neg B) A --> (Neg B)) --> (And (Neg B) A --> (Or B C)) --> (And (Neg B) A --> And (Neg B) (Or B C)));
(Γ , (And (Neg B) A --> (Neg B)))]).
2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (And (Neg B) A). exists (Neg B).
exists (Or B C). auto. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA5_I. exists (Neg B). exists A. auto.
inversion H6. inversion H4. subst.
apply MP with (ps:=[(Γ , (A --> Or B C) --> (And (Neg B) A --> Or B C));
(Γ , (A --> Or B C))]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (And (Neg B) A --> A) --> (A --> Or B C) --> (And (Neg B) A --> Or B C));
(Γ , (And (Neg B) A --> A))]).
2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And (Neg B) A). exists A.
exists (Or B C). auto. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA6_I. exists (Neg B). exists A. auto.
inversion H8. inversion H6. subst. assumption. inversion H7. inversion H5. inversion H3.
inversion H1. subst.
apply MP with (ps:=[(Γ , (And (Or B C) (Neg B) --> C) --> (And (Neg B) (Or B C) --> C));
(Γ , (And (Or B C) (Neg B) --> C))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (And (Neg B) (Or B C) --> And (Or B C) (Neg B)) --> (And (Or B C) (Neg B) --> C) --> (And (Neg B) (Or B C) --> C));
(Γ , And (Neg B) (Or B C) --> And (Or B C) (Neg B))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And (Neg B) (Or B C)). exists (And (Or B C) (Neg B)).
exists C. auto. inversion H4. subst.
apply MP with (ps:=[(Γ , (And (Neg B) (Or B C) --> (Neg B)) --> (And (Neg B) (Or B C) --> And (Or B C) (Neg B)));
(Γ , (And (Neg B) (Or B C) --> (Neg B)))]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (And (Neg B) (Or B C) --> (Or B C)) --> (And (Neg B) (Or B C) --> (Neg B)) --> (And (Neg B) (Or B C) --> And (Or B C) (Neg B)));
(Γ , (And (Neg B) (Or B C) --> (Or B C)))]).
2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (And (Neg B) (Or B C)). exists (Or B C).
exists (Neg B). auto. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA6_I. exists (Neg B). exists (Or B C).
auto. inversion H8. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA5_I. exists (Neg B). exists (Or B C).
auto. inversion H7. inversion H5. inversion H3. subst.
apply MP with (ps:=[(Γ , ((Or B C) --> (Neg B) --> C) --> (And (Or B C) (Neg B) --> C));
(Γ , ((Or B C) --> (Neg B) --> C))]).
2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA8_I. exists (Or B C). exists (Neg B). exists C.
auto. inversion H5. subst.
apply MP with (ps:=[(Γ , (C --> Neg B --> C) --> (Or B C --> Neg B --> C));
(Γ , (C --> Neg B --> C))]).
2: apply MPRule_I. intros. inversion H6. subst.
apply MP with (ps:=[(Γ , (B --> Neg B --> C) --> (C --> Neg B --> C) --> (Or B C --> Neg B --> C));
(Γ , (B --> Neg B --> C))]).
2: apply MPRule_I. intros. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists B. exists C.
exists (Neg B --> C). auto. inversion H8. subst.
apply MP with (ps:=[(Γ , ((And B (Neg B)) --> C) --> (B --> Neg B --> C));
(Γ , ((And B (Neg B)) --> C))]).
2: apply MPRule_I. intros. inversion H9. subst.
apply Ax. apply AxRule_I. apply RA9_I. exists B. exists (Neg B). exists C.
auto. inversion H10. subst.
apply MP with (ps:=[(Γ , (Bot --> C) --> (And B (Neg B) --> C));
(Γ , (Bot --> C))]).
2: apply MPRule_I. intros. inversion H11. subst.
apply MP with (ps:=[(Γ , (And B (Neg B) --> Bot) --> (Bot --> C) --> (And B (Neg B) --> C));
(Γ , (And B (Neg B) --> Bot))]).
2: apply MPRule_I. intros. inversion H12. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And B (Neg B)). exists (Bot).
exists (C). auto. inversion H13. subst. apply wContr_Bot. inversion H14. inversion H12. subst.
apply wEFQ. inversion H13. inversion H11. inversion H9. inversion H7. subst.
apply wThm_irrel. inversion H8. inversion H6. inversion H4. inversion H2.
Qed.
Lemma wNeg_Top : forall A B Γ ,
(BIH_rules (Γ , ((wNeg A) --> B))) ->
(BIH_rules (Γ , (Excl (Top) A) --> B)).
Proof.
intros A B Γ D. apply MP with (ps:=[(Γ , (wNeg A --> B) --> (Excl (Top) A --> B));
(Γ , (wNeg A --> B))]). 2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Excl (Top) A --> wNeg A) --> (wNeg A --> B) --> Excl (Top) A --> B);
(Γ , (Excl (Top) A --> wNeg A))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I.
apply RA1_I. exists (Excl (Top) A). exists (wNeg A). exists B. auto.
inversion H1. subst. apply wimp_Id_gen.
inversion H2. inversion H0. subst. assumption. inversion H1.
Qed.
Lemma Top_wNeg : forall A B Γ ,
(BIH_rules (Γ , (Excl (Top) A) --> B)) ->
(BIH_rules (Γ , ((wNeg A) --> B))).
Proof.
intros A B Γ D. apply MP with (ps:=[(Γ , (Excl (Top) A --> B) --> (wNeg A --> B));
(Γ , (Excl (Top) A --> B))]). 2: apply MPRule_I. intros. inversion H. subst.
intros. apply MP with (ps:=[(Γ , (wNeg A --> Excl (Top) A) --> (Excl (Top) A --> B) --> wNeg A --> B);
(Γ , (wNeg A --> Excl (Top) A))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I.
apply RA1_I. exists (wNeg A). exists (Excl (Top) A). exists B. auto.
inversion H1. subst. apply wimp_Id_gen.
inversion H2. inversion H0. subst. assumption. inversion H1.
Qed.
Lemma Top_wNeg_cons : forall A B Γ ,
(BIH_rules (Γ , A --> (Excl (Top) B))) ->
(BIH_rules (Γ , A --> (wNeg B))).
Proof.
intros. apply MP with (ps:=[(Γ , (Excl (Top) B --> wNeg B) --> (A --> wNeg B));
(Γ , (Excl (Top) B --> wNeg B))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ , (A --> Excl (Top) B) --> (Excl (Top) B --> wNeg B) --> (A --> wNeg B));
(Γ , (A --> Excl (Top) B))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I.
apply RA1_I. exists A. exists (Excl (Top) B). exists (wNeg B). auto.
inversion H2. subst. assumption. inversion H3. inversion H1. subst.
apply wimp_Id_gen. inversion H2.
Qed.
Lemma Or_imp_assoc : forall A B C D Γ ,
(BIH_rules (Γ , A --> (Or (Or B C) D))) ->
(BIH_rules (Γ , A --> (Or B (Or C D)))).
Proof.
intros.
apply MP with (ps:=[(Γ , (Or (Or B C) D --> Or B (Or C D)) --> (A --> Or B (Or C D)));
(Γ , (Or (Or B C) D --> Or B (Or C D)))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ , (A --> Or (Or B C) D) --> (Or (Or B C) D --> Or B (Or C D)) --> (A --> Or B (Or C D)));
(Γ , (A --> Or (Or B C) D))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists (Or (Or B C) D).
exists (Or B (Or C D)). auto. inversion H2. subst.
assumption. inversion H3. inversion H1. subst.
apply MP with (ps:=[(Γ , (D --> Or B (Or C D)) --> (Or (Or B C) D --> Or B (Or C D)));
(Γ , (D --> Or B (Or C D)))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , ((Or B C) --> Or B (Or C D)) --> (D --> Or B (Or C D)) --> (Or (Or B C) D --> Or B (Or C D)));
(Γ , ((Or B C) --> Or B (Or C D)))]). 2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists (Or B C).
exists D. exists (Or B (Or C D)). auto. inversion H4. subst.
apply MP with (ps:=[(Γ , (C --> Or B (Or C D)) --> (Or B C --> Or B (Or C D)));
(Γ , C --> Or B (Or C D))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (B --> Or B (Or C D)) --> (C --> Or B (Or C D)) --> (Or B C --> Or B (Or C D)));
(Γ , B --> Or B (Or C D))]). 2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists B. exists C.
exists (Or B (Or C D)). auto. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA2_I. exists B. exists (Or C D). auto.
inversion H8. inversion H6. subst.
apply MP with (ps:=[(Γ , ((Or C D) --> Or B (Or C D)) --> (C --> Or B (Or C D)));
(Γ , (Or C D) --> Or B (Or C D))]). 2: apply MPRule_I. intros. inversion H7. subst.
apply MP with (ps:=[(Γ , (C --> (Or C D)) --> ((Or C D) --> Or B (Or C D)) --> (C --> Or B (Or C D)));
(Γ , (C --> (Or C D)))]). 2: apply MPRule_I. intros. inversion H8. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists C. exists (Or C D).
exists (Or B (Or C D)). auto. inversion H9. subst.
apply Ax. apply AxRule_I. apply RA2_I. exists C. exists D. auto. inversion H10.
inversion H8. subst. apply Ax. apply AxRule_I.
apply RA3_I. exists B. exists (Or C D). auto. inversion H9. inversion H7. inversion H5.
inversion H3. subst.
apply MP with (ps:=[(Γ , ((Or C D) --> Or B (Or C D)) --> (D --> Or B (Or C D)));
(Γ , ((Or C D) --> Or B (Or C D)))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Γ , (D --> (Or C D)) --> ((Or C D) --> Or B (Or C D)) --> (D --> Or B (Or C D)));
(Γ , (D --> (Or C D)))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists D. exists (Or C D).
exists (Or B (Or C D)). auto. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists C. exists D. auto. inversion H7.
inversion H5. subst. apply Ax. apply AxRule_I. apply RA3_I. exists B. exists (Or C D). auto.
inversion H6. inversion H4. inversion H2.
Qed.
Lemma wClaim1 : forall A B Γ ,
(BIH_rules (Γ , (Neg (Excl A B)) --> ((wNeg B) --> (wNeg A)))).
Proof.
intros A B Γ .
pose (BIH_monot (Empty_set _, Neg (Excl A B) --> wNeg B --> wNeg A)). apply b. clear b.
apply MP with (ps:=[(Empty_set _, ((And (Neg (Excl A B)) (wNeg B)) --> wNeg A) --> (Neg (Excl A B) --> wNeg B --> wNeg A));
(Empty_set _, (And (Neg (Excl A B)) (wNeg B)) --> wNeg A)]). 2: apply MPRule_I. intros. inversion H. subst.
apply Ax. apply AxRule_I. apply RA9_I. exists (Neg (Excl A B)).
exists (wNeg B). exists (wNeg A). auto. inversion H0. subst.
apply MP with (ps:=[(Empty_set _, ((Excl (Top) (Or B (Excl A B))) --> wNeg A) --> (And (Neg (Excl A B)) (wNeg B) --> wNeg A));
(Empty_set _, (Excl (Top) (Or B (Excl A B))) --> wNeg A)]). 2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Empty_set _, (And (Neg (Excl A B)) (wNeg B) --> (Excl (Top) (Or B (Excl A B)))) --> ((Excl (Top) (Or B (Excl A B))) --> wNeg A) --> (And (Neg (Excl A B)) (wNeg B) --> wNeg A));
(Empty_set _, (And (Neg (Excl A B)) (wNeg B) --> (Excl (Top) (Or B (Excl A B)))))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (And (Neg (Excl A B)) (wNeg B)).
exists (Excl (Top) (Or B (Excl A B))). exists (wNeg A). auto. inversion H3. subst.
apply wOr_Neg. apply Top_wNeg. apply wdual_residuation.
apply Or_imp_assoc. apply wdual_residuation. apply wimp_Id_gen. inversion H4. inversion H2. subst.
apply Top_wNeg_cons. apply wmon_Excl. apply Ax. apply AxRule_I.
apply RA11_I. exists A. exists B. auto. inversion H3. inversion H1.
intro. simpl. intros. inversion H.
Qed.
Lemma wDN_dist_imp : forall A B Γ ,
(BIH_rules (Γ , (Neg (wNeg (A --> B))) --> ((Neg (wNeg A)) --> (Neg (wNeg B))))).
Proof.
intros A B Γ .
apply MP with (ps:=[(Γ , (((wNeg B) --> wNeg A) --> Neg (wNeg A) --> Neg (wNeg B)) --> (Neg (wNeg (A --> B)) --> Neg (wNeg A) --> Neg (wNeg B)));
(Γ , (((wNeg B) --> wNeg A) --> Neg (wNeg A) --> Neg (wNeg B)))]). 2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Neg (wNeg (A --> B)) --> ((wNeg B) --> wNeg A)) --> (((wNeg B) --> wNeg A) --> Neg (wNeg A) --> Neg (wNeg B)) --> (Neg (wNeg (A --> B)) --> Neg (wNeg A) --> Neg (wNeg B)));
(Γ , (Neg (wNeg (A --> B)) --> ((wNeg B) --> wNeg A)))]). 2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Neg (wNeg (A --> B))).
exists (wNeg B --> wNeg A). exists (Neg (wNeg A) --> Neg (wNeg B)). auto. inversion H1. subst.
apply MP with (ps:=[(Γ ,((Neg (Excl A B)) --> (wNeg B --> wNeg A)) --> (Neg (wNeg (A --> B)) --> wNeg B --> wNeg A));
(Γ , ((Neg (Excl A B)) --> (wNeg B --> wNeg A)))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ ,(Neg (wNeg (A --> B)) --> (Neg (Excl A B))) --> ((Neg (Excl A B)) --> (wNeg B --> wNeg A)) --> (Neg (wNeg (A --> B)) --> wNeg B --> wNeg A));
(Γ , (Neg (wNeg (A --> B)) --> (Neg (Excl A B))))]). 2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Neg (wNeg (A --> B))).
exists (Neg (Excl A B)). exists (wNeg B --> wNeg A). auto. inversion H4. subst.
apply MP with (ps:=[(Γ , ((Excl A B) --> (wNeg (A --> B))) --> (Neg (wNeg (A --> B)) --> Neg (Excl A B)));
(Γ , (Excl A B) --> (wNeg (A --> B)))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA10_I. exists (Excl A B).
exists (wNeg (A --> B)). auto. inversion H6. subst. apply Ax.
apply AxRule_I. apply RA12_I. exists A. exists B. auto. inversion H7. inversion H5.
inversion H3. subst. apply wClaim1. inversion H4. inversion H2. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA10_I. exists (wNeg B).
exists (wNeg A). auto. inversion H1.
Qed.