CPPsiteProjPackage.CPP_BiInt_meta_interactions1
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.
Lemma wThm_irrel : forall A B Γ , BIH_rules (Γ , A --> (B --> A)).
Proof.
intros A B Γ .
apply MP with (ps:=[(Γ ,(And A B --> A) --> (A --> (B --> A)));(Γ , (And A B --> A))]).
2: apply MPRule_I. intros. inversion H. subst.
apply Ax. apply AxRule_I. apply RA9_I. exists A. exists B. exists A. auto.
inversion H0. subst. apply Ax. apply AxRule_I. apply RA5_I. exists A. exists B. auto. inversion H1.
Qed.
Lemma wimp_Id_gen : forall A Γ , BIH_rules (Γ , A --> A).
Proof.
intros A Γ .
apply MP with (ps:=[(Γ , (And A A --> A) --> (A --> A)); (Γ , (And A A --> A))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , ((And (And A A --> A) A) --> A) --> (And A A --> A) --> (A --> A)); (Γ , (And (And A A --> A) A) --> A)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I. apply RA9_I.
exists (And A A --> A). exists A. exists A. auto. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA6_I.
exists (And A A --> A). exists A. auto. inversion H2. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA5_I. exists A. exists A. auto. inversion H1.
Qed.
Lemma comm_And_obj : forall A B Γ ,
(BIH_rules (Γ , And A B --> And B A)).
Proof.
intros A B Γ .
apply MP with (ps:=[(Γ , (And A B --> A) --> (And A B --> And B A));(Γ , (And A B --> A))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (And A B --> B) --> (And A B --> A) --> (And A B --> And B A));(Γ , (And A B --> B))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (And A B). exists B. exists A.
auto. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA6_I. exists A. exists B. auto. inversion H2.
inversion H0. subst. apply Ax. apply AxRule_I. apply RA5_I. exists A. exists B. auto.
inversion H1.
Qed.
Lemma wContr_Bot : forall A Γ , BIH_rules (Γ , And A (Neg A) --> (Bot)).
Proof.
intros A Γ .
apply MP with (ps:=[(Γ , (And (Neg A) A --> Bot) --> (And A (Neg A) --> Bot));(Γ , And (Neg A) A --> Bot)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (And A (Neg A) --> And (Neg A) A) --> (And (Neg A) A --> Bot) --> (And A (Neg A) --> Bot));(Γ , And A (Neg A) --> And (Neg A) A)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (And A (Neg A)). exists (And (Neg A) A). exists (Bot). auto. inversion H1.
subst. apply comm_And_obj. inversion H2. inversion H0. subst.
apply MP with (ps:=[(Γ , ((Neg A) --> A --> Bot) --> (And (Neg A) A --> Bot));(Γ , ((Neg A) --> A --> Bot))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax.
apply AxRule_I. apply RA8_I. exists (Neg A). exists A. exists (Bot). auto. inversion H2.
subst. apply wimp_Id_gen. inversion H3. inversion H1.
Qed.
Lemma wmonotR_Or : forall A B Γ ,
(BIH_rules (Γ , A --> B)) ->
(forall C, BIH_rules (Γ , (Or A C) --> (Or B C))).
Proof.
intros A B Γ D C.
apply MP with (ps:=[(Γ , (C --> Or B C) --> (Or A C --> Or B C));(Γ ,(C --> Or B C))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (A --> Or B C) --> (C --> Or B C) --> (Or A C --> Or B C));(Γ ,(A --> Or B C))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists A. exists C.
exists (Or B C). auto. inversion H1. subst.
apply MP with (ps:=[(Γ , (B --> Or B C) --> (A --> Or B C));(Γ ,((B --> Or B C)))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (A --> B) --> (B --> Or B C) --> (A --> Or B C));(Γ ,(A --> B))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists B. exists (Or B C). auto.
inversion H4. subst. assumption. inversion H5. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists B. exists C.
auto. inversion H4. inversion H2. inversion H0. subst. apply Ax. apply AxRule_I. apply RA3_I.
exists B. exists C. auto. inversion H1.
Qed.
Lemma wmonotL_Or : forall A B Γ,
(BIH_rules (Γ, A --> B)) ->
(forall C, BIH_rules (Γ, (Or C A) --> (Or C B))).
Proof.
intros A B Γ D C.
apply MP with (ps:=[(Γ , (A --> Or C B) --> ((Or C A) --> (Or C B)));(Γ ,(A --> Or C B))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (C --> Or C B) --> (A --> Or C B) --> ((Or C A) --> (Or C B)));(Γ ,(C --> Or C B))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I. apply RA4_I. exists C. exists A.
exists (Or C B). auto. inversion H1. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists C. exists B.
auto. inversion H2. inversion H0. subst.
apply MP with (ps:=[(Γ , (B --> Or C B) --> (A --> Or C B));(Γ ,((B --> Or C B)))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Γ , (A --> B) --> (B --> Or C B) --> (A --> Or C B));(Γ ,(A --> B))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists B. exists (Or C B). auto. inversion H3. subst.
assumption. inversion H4. inversion H2. subst. apply Ax.
apply AxRule_I. apply RA3_I. exists C. exists B.
auto. inversion H3. inversion H1.
Qed.
Lemma comm_Or_obj : forall A B Γ , (BIH_rules (Γ , Or A B --> Or B A)).
Proof.
intros A B Γ .
apply MP with (ps:=[(Γ , (B --> Or B A) --> (Or A B --> Or B A));(Γ , (B --> Or B A))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (A --> Or B A) --> (B --> Or B A) --> (Or A B --> Or B A));(Γ , (A --> Or B A))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists A. exists B. exists (Or B A).
auto. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists B. exists A. auto.
inversion H2. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA2_I. exists B. exists A. auto.
inversion H1.
Qed.
Lemma comm_Or : forall A B Γ , (BIH_rules (Γ , Or A B)) -> (BIH_rules (Γ , Or B A)).
Proof.
intros A B Γ D.
apply MP with (ps:=[(Γ , Or A B --> Or B A);(Γ , Or A B)]).
2: apply MPRule_I. intros. inversion H. subst. apply comm_Or_obj.
inversion H0. subst. assumption. inversion H1.
Qed.
Lemma wmonot_Or2 : forall A B Γ , (BIH_rules (Γ , A --> B)) ->
(forall C, BIH_rules (Γ , (Or A C) --> (Or C B))).
Proof.
intros A B Γ D C.
apply MP with (ps:=[(Γ , (C --> Or C B) --> (Or A C --> Or C B));(Γ , C --> Or C B)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (A --> Or C B) --> (C --> Or C B) --> (Or A C --> Or C B));(Γ , A --> Or C B)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax.
apply AxRule_I. apply RA4_I. exists A. exists C. exists (Or C B). auto.
inversion H1. subst.
apply MP with (ps:=[(Γ , (B --> Or C B) --> (A --> Or C B));(Γ , B --> Or C B)]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (A --> B) --> (B --> Or C B) --> (A --> Or C B));(Γ , A --> B)]).
2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists B. exists (Or C B).
auto. inversion H4. subst. assumption. inversion H5. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists C. exists B. auto. inversion H4.
inversion H2. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA2_I. exists C. exists B. auto. inversion H1.
Qed.
Theorem wdual_residuation0 : forall A B C,
(BIH_rules (Empty_set _, (Excl A B) --> C) ->
BIH_rules (Empty_set _, A --> (Or B C))).
Proof.
intros A B C D. pose (@wmonot_Or2 (Excl A B) C (Empty_set _) D B).
apply MP with (ps:=[(Empty_set _, (Or (Excl A B) B --> Or B C) --> (A --> Or B C));(Empty_set _,Or (Excl A B) B --> Or B C)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or (Excl A B) B) --> (Or (Excl A B) B --> Or B C) --> (A --> Or B C));(Empty_set _,(A --> Or (Excl A B) B))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists (Or (Excl A B) B). exists (Or B C). auto.
inversion H1. subst.
apply MP with (ps:=[(Empty_set _, (Or B (Excl A B) --> Or (Excl A B) B) --> (A --> Or (Excl A B) B));(Empty_set _,(Or B (Excl A B) --> Or (Excl A B) B))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or B (Excl A B)) --> (Or B (Excl A B) --> Or (Excl A B) B) --> (A --> Or (Excl A B) B));(Empty_set _,(A --> Or B (Excl A B)))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (Or B (Excl A B)). exists (Or (Excl A B) B).
auto. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists A. exists B. auto. inversion H5.
inversion H3. subst. apply comm_Or_obj. inversion H4. inversion H2. inversion H0.
subst. assumption. inversion H1.
Qed.
Lemma wDN_to_form : forall A Γ , (BIH_rules (Γ , Neg (wNeg A)--> A)).
Proof.
intros A Γ .
apply MP with (ps:=[(Γ , (Top) --> Neg (wNeg A) --> A);(Γ , Top)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , ((And (Top) (Neg (wNeg A))) --> A) --> ((Top) --> (Neg (wNeg A)) --> A));(Γ , ((And (Top) (Neg (wNeg A))) --> A))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA9_I. exists (Top). exists (Neg (wNeg A)). exists A. auto.
inversion H1. subst.
apply MP with (ps:=[(Γ , ((And (Neg (wNeg A)) (Top))--> A) --> (And (Top) (Neg (wNeg A)) --> A));(Γ , (And (Neg (wNeg A)) (Top))--> A)]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , ((And (Top) (Neg (wNeg A))) --> (And (Neg (wNeg A)) (Top))) --> ((And (Neg (wNeg A)) (Top))--> A) --> (And (Top) (Neg (wNeg A)) --> A));
(Γ , ((And (Top) (Neg (wNeg A))) --> (And (Neg (wNeg A)) (Top))))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (And (Top) (Neg (wNeg A))). exists (And (Neg (wNeg A)) (Top)).
exists A. auto. inversion H4. subst.
apply MP with (ps:=[(Γ , (And (Top) (Neg (wNeg A)) --> (Top)) --> And (Top) (Neg (wNeg A)) --> And (Neg (wNeg A)) (Top));
(Γ , And (Top) (Neg (wNeg A)) --> (Top))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (And (Top) (Neg (wNeg A)) --> (Neg (wNeg A))) --> (And (Top) (Neg (wNeg A)) --> (Top)) --> And (Top) (Neg (wNeg A)) --> And (Neg (wNeg A)) (Top));
(Γ , And (Top) (Neg (wNeg A)) --> (Neg (wNeg A)))]). 2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (And (Top) (Neg (wNeg A))).
exists (Neg (wNeg A)). exists (Top). auto. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA6_I. exists (Top).
exists (Neg (wNeg A)). auto. inversion H8. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA5_I. exists (Top).
exists (Neg (wNeg A)). auto. inversion H7. inversion H5. inversion H3. subst.
apply MP with (ps:=[(Γ , ((Neg (wNeg A)) --> (Top) --> A) --> And (Neg (wNeg A)) (Top) --> A);
(Γ , ((Neg (wNeg A)) --> (Top) --> A))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA8_I. exists (Neg (wNeg A)).
exists (Top). exists A. auto. inversion H5. subst.
apply MP with (ps:=[(Γ , (((wNeg A) --> (Bot)) --> Top --> A) --> (Neg (wNeg A) --> Top --> A));
(Γ , (((wNeg A) --> (Bot)) --> Top --> A))]). 2: apply MPRule_I. intros. inversion H6. subst.
apply MP with (ps:=[(Γ , (Neg (wNeg A) --> ((wNeg A) --> (Bot))) --> (((wNeg A) --> (Bot)) --> Top --> A) --> (Neg (wNeg A) --> Top --> A));
(Γ , Neg (wNeg A) --> ((wNeg A) --> (Bot)))]). 2: apply MPRule_I. intros. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Neg (wNeg A)).
exists (wNeg A --> Bot). exists (Top --> A). auto. inversion H8. subst.
apply wimp_Id_gen. inversion H9.
inversion H7. subst.
apply MP with (ps:=[(Γ , (((Excl (Top) A) --> Bot) --> Top --> A) --> (wNeg A --> Bot) --> Top --> A);(Γ , ((Excl (Top) A) --> Bot) --> Top --> A)]).
2: apply MPRule_I. intros. inversion H8. subst.
apply MP with (ps:=[(Γ , ((wNeg A --> Bot) --> ((Excl (Top) A) --> Bot)) --> (((Excl (Top) A) --> Bot) --> Top --> A) --> (wNeg A --> Bot) --> Top --> A);
(Γ , (wNeg A --> Bot) --> ((Excl (Top) A) --> Bot))]).
2: apply MPRule_I. intros. inversion H9. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists (wNeg A --> Bot). exists (Excl (Top) A --> Bot).
exists (Top --> A). auto. inversion H10. subst.
apply MP with (ps:=[(Γ , (Excl (Top) A --> (wNeg A)) --> ((wNeg A --> Bot) --> Excl (Top) A --> Bot));(Γ , (Excl (Top) A --> (wNeg A)))]).
2: apply MPRule_I. intros. inversion H11. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Excl (Top) A). exists (wNeg A). exists (Bot). auto. inversion H12. subst.
apply wimp_Id_gen.
inversion H13. inversion H11. inversion H9. subst.
apply MP with (ps:=[(Γ , (Neg (Excl (Top) A) --> Top --> A) --> ((Excl (Top) A --> Bot) --> Top --> A));(Γ , (Neg (Excl (Top) A) --> Top --> A))]).
2: apply MPRule_I. intros. inversion H10. subst.
apply MP with (ps:=[(Γ , ((Excl (Top) A --> Bot) --> Neg (Excl (Top) A)) --> (Neg (Excl (Top) A) --> Top --> A) --> ((Excl (Top) A --> Bot) --> Top --> A));
(Γ , (Excl (Top) A --> Bot) --> Neg (Excl (Top) A))]).
2: apply MPRule_I. intros. inversion H11. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists (Excl (Top) A --> Bot). exists (Neg (Excl (Top) A)).
exists (Top --> A). auto. inversion H12. subst.
apply wimp_Id_gen.
inversion H13. inversion H11. subst. apply Ax. apply AxRule_I.
apply RA14_I. exists (Top). exists A. auto. inversion H12. inversion H10.
inversion H8. inversion H6. inversion H4. inversion H2. inversion H0. subst.
apply MP with (ps:=[(Γ , Imp (Imp A A) (Top));(Γ , Imp A A)]).
2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA15_I. exists (A --> A). auto. inversion H2.
subst. apply wimp_Id_gen. inversion H3. inversion H1.
Qed.
Lemma wEFQ : forall A Γ , BIH_rules (Γ , (Bot) --> A).
Proof.
intros A Γ .
apply MP with (ps:=[(Γ , ((Neg (wNeg A)) --> A) --> (Bot --> A));(Γ , (Neg (wNeg A)) --> A)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Bot --> (Neg (wNeg A))) --> ((Neg (wNeg A)) --> A) --> (Bot --> A));(Γ , (Bot) --> (Neg (wNeg A)))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Bot). exists (Neg (wNeg A)). exists A. auto.
inversion H1. subst.
apply MP with (ps:=[(Γ , (Neg (Top) --> Neg (wNeg A)) --> (Bot --> Neg (wNeg A)));
(Γ , Neg (Top) --> Neg (wNeg A))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (Bot --> Neg (Top)) --> (Neg (Top) --> Neg (wNeg A)) --> (Bot --> Neg (wNeg A)));
(Γ , Bot --> Neg (Top))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Bot). exists (Neg (Top)). exists (Neg (wNeg A)). auto.
inversion H4. subst.
apply MP with (ps:=[(Γ , (((Top) --> (Bot)) --> Neg (Top)) --> (Bot --> Neg (Top)));
(Γ , ((Top) --> (Bot)) --> Neg (Top))]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (Bot --> ((Top) --> (Bot))) --> (((Top) --> (Bot)) --> Neg (Top)) --> (Bot --> Neg (Top)));
(Γ , Bot --> ((Top) --> (Bot)))]).
2: apply MPRule_I. intros. inversion H6. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Bot). exists ((Top) --> (Bot)). exists (Neg (Top)). auto.
inversion H7. subst. apply wThm_irrel. inversion H8. inversion H6. subst.
apply wimp_Id_gen. inversion H7. inversion H5. inversion H3. subst.
apply MP with (ps:=[(Γ , ((wNeg A) --> (Top)) --> (Neg (Top) --> Neg (wNeg A)));
(Γ , ((wNeg A) --> (Top)))]).
2: apply MPRule_I. intros. inversion H4. subst. apply Ax. apply AxRule_I.
apply RA10_I. exists (wNeg A). exists (Top). auto. inversion H5. subst.
apply MP with (ps:=[(Γ , (Top) --> (wNeg A --> Top));(Γ , Top)]).
2: apply MPRule_I. intros. inversion H6. subst. apply wThm_irrel.
inversion H7. subst.
apply MP with (ps:=[(Γ , (A --> A) --> Top);(Γ , A --> A)]).
2: apply MPRule_I. intros. inversion H8. subst. apply Ax. apply AxRule_I.
apply RA15_I. exists (A --> A). auto. inversion H9. subst. apply wimp_Id_gen.
inversion H10. inversion H8. inversion H6. inversion H4. inversion H2.
inversion H0. subst. apply wDN_to_form. inversion H1.
Qed.
Lemma absorp_Or1 : forall A Γ ,
(BIH_rules (Γ , Or A (Bot))) ->
(BIH_rules (Γ , A)).
Proof.
intros A Γ D.
apply MP with (ps:=[(Γ , Imp (Or A (Bot)) A);(Γ , Or A (Bot))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Bot --> A) --> (Or A (Bot) --> A));(Γ , (Bot --> A))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ , (A --> A) --> (Bot --> A) --> (Or A (Bot) --> A));(Γ , A --> A)]).
2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists A. exists (Bot).
exists A. auto. inversion H2. subst. apply wimp_Id_gen. inversion H3.
inversion H1. subst. apply wEFQ. inversion H2. inversion H0. subst.
assumption. inversion H1.
Qed.
Theorem wdual_residuation : forall A B C,
(BIH_rules (Empty_set _, (Excl A B) --> C) ->
BIH_rules (Empty_set _, A --> (Or B C))) *
(BIH_rules (Empty_set _, A --> (Or B C)) ->
BIH_rules (Empty_set _, (Excl A B) --> C)).
Proof.
intros A B C. split.
- intro D. pose (@wmonot_Or2 (Excl A B) C (Empty_set _) D B).
apply MP with (ps:=[(Empty_set _, (Or (Excl A B) B --> Or B C) --> (A --> Or B C));(Empty_set _,Or (Excl A B) B --> Or B C)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or (Excl A B) B) --> (Or (Excl A B) B --> Or B C) --> (A --> Or B C));(Empty_set _,(A --> Or (Excl A B) B))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (Or (Excl A B) B). exists (Or B C). auto.
inversion H1. subst.
apply MP with (ps:=[(Empty_set _, (Or B (Excl A B) --> Or (Excl A B) B) --> (A --> Or (Excl A B) B));(Empty_set _,(Or B (Excl A B) --> Or (Excl A B) B))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or B (Excl A B)) --> (Or B (Excl A B) --> Or (Excl A B) B) --> (A --> Or (Excl A B) B));(Empty_set _,(A --> Or B (Excl A B)))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (Or B (Excl A B)). exists (Or (Excl A B) B).
auto. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists A. exists B. auto. inversion H5. inversion H3. subst. apply comm_Or_obj.
inversion H4. inversion H2. inversion H0. subst. assumption. inversion H1.
- intro D. apply MP with (ps:=[(Empty_set _, ((Or C (Excl A (Or B C))) --> C) --> (Excl A B --> C));(Empty_set _, (Or C (Excl A (Or B C))) --> C)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Empty_set _, (Excl A B --> (Or C (Excl A (Or B C)))) --> ((Or C (Excl A (Or B C))) --> C) --> (Excl A B --> C));(Empty_set _, Excl A B --> (Or C (Excl A (Or B C))))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists (Excl A B). exists (Or C (Excl A (Or B C))). exists C. auto. inversion H1. subst.
apply MP with (ps:=[(Empty_set _, ((Or C (Excl (Excl A B) C)) --> Or C (Excl A (Or B C))) --> (Excl A B --> Or C (Excl A (Or B C))));(Empty_set _, ((Or C (Excl (Excl A B) C)) --> Or C (Excl A (Or B C))))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (Excl A B --> (Or C (Excl (Excl A B) C)))--> ((Or C (Excl (Excl A B) C)) --> Or C (Excl A (Or B C))) --> (Excl A B --> Or C (Excl A (Or B C))));
(Empty_set _, (Excl A B --> (Or C (Excl (Excl A B) C))))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Excl A B). exists (Or C (Excl (Excl A B) C)).
exists (Or C (Excl A (Or B C))). auto. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists (Excl A B). exists C. auto. inversion H5.
inversion H3. subst. apply wmonotL_Or.
apply Ax. apply AxRule_I. apply RA13_I.
exists A. exists B. exists C. auto. inversion H4. inversion H2. inversion H0. subst. 2: inversion H1.
apply MP with (ps:=[(Empty_set _, (Or C (Bot) --> C) --> (Or C (Excl A (Or B C)) --> C));
(Empty_set _, (Or C (Bot) --> C))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Empty_set _, (Or C (Excl A (Or B C)) --> Or C (Bot)) --> (Or C (Bot) --> C) --> (Or C (Excl A (Or B C)) --> C));
(Empty_set _, (Or C (Excl A (Or B C)) --> Or C (Bot)))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Or C (Excl A (Or B C))).
exists (Or C (Bot)). exists C. auto. inversion H3. subst. apply wmonotL_Or.
apply MP with (ps:=[(Empty_set _, ((And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))) --> Bot) --> (Excl A (Or B C) --> Bot));
(Empty_set _, ((And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))) --> Bot))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Empty_set _, (Excl A (Or B C) --> (And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C))))) --> ((And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))) --> Bot) --> (Excl A (Or B C) --> Bot));
(Empty_set _, (Excl A (Or B C) --> (And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C))))))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Excl A (Or B C)).
exists (And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))). exists (Bot). auto. inversion H6. subst.
apply MP with (ps:=[(Empty_set _, (Excl A (Or B C) --> (Neg (wNeg (A --> Or B C)))) --> (Excl A (Or B C) --> And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))));
(Empty_set _, (Excl A (Or B C) --> (Neg (wNeg (A --> Or B C)))))]). 2: apply MPRule_I. intros. inversion H7. subst.
apply MP with (ps:=[(Empty_set _, (Excl A (Or B C) --> (wNeg (A --> Or B C))) --> (Excl A (Or B C) --> (Neg (wNeg (A --> Or B C)))) --> (Excl A (Or B C) --> And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))));
(Empty_set _, (Excl A (Or B C) --> (wNeg (A --> Or B C))))]). 2: apply MPRule_I. intros. inversion H8. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (Excl A (Or B C)).
exists (wNeg (A --> Or B C)). exists (Neg (wNeg (A --> Or B C))). auto. inversion H9.
subst. apply Ax. apply AxRule_I. apply RA12_I. exists A. exists (Or B C).
auto. inversion H10. inversion H8. subst.
apply MP with (ps:=[(Empty_set _, (Neg (wNeg (A --> Or B C))) --> (Excl A (Or B C) --> Neg (wNeg (A --> Or B C))));
(Empty_set _, (Neg (wNeg (A --> Or B C))))]). 2: apply MPRule_I. intros. inversion H9. subst.
apply wThm_irrel. inversion H10. subst. apply DNw with (ps:=[(Empty_set _, A --> Or B C)]).
2: apply DNwRule_I. intros. inversion H11. subst. assumption. inversion H12. inversion H11.
inversion H9. inversion H7. inversion H5. subst. apply wContr_Bot. inversion H6.
inversion H4. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (Bot --> C) --> (Or C (Bot) --> C));(Empty_set _, (Bot --> C))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Empty_set _, (C --> C) --> (Bot --> C) --> (Or C (Bot) --> C));(Empty_set _, (C --> C))]).
2: apply MPRule_I. intros. inversion H4. subst. apply Ax.
apply AxRule_I. apply RA4_I. exists C. exists (Bot). exists C. auto.
inversion H5. subst. apply wimp_Id_gen. inversion H6. inversion H4. subst.
apply wEFQ. inversion H5. inversion H3.
Qed.
Lemma wAThm_irrel : forall A B Γ , BIH_rules (Γ , (Excl A B) --> A).
Proof.
intros A B Γ . pose (BIH_monot (Empty_set _, Excl A B --> A)). apply b.
apply wdual_residuation. apply Ax. apply AxRule_I.
apply RA3_I. exists B. exists A. auto. intro. intros. simpl in H.
inversion H.
Qed.
Theorem wdual_residuation_gen : forall A B C,
(pair_derrec (Empty_set _, Singleton _ ((Excl A B) --> C)) ->
pair_derrec (Empty_set _, Singleton _ (A --> (Or B C)))) *
(pair_derrec (Empty_set _, Singleton _ (A --> (Or B C))) ->
pair_derrec (Empty_set _, Singleton _ ((Excl A B) --> C))).
Proof.
intros A B C. split.
- intro. exists [(A --> Or B C)]. repeat split.
* apply NoDup_cons. intro. inversion H0. apply NoDup_nil.
* intros. inversion H. subst. simpl. inversion H0. subst. apply In_singleton. inversion H2.
* destruct H. destruct H. pose (wdual_residuation A B C). destruct p. simpl.
simpl in b. simpl in b0. simpl in H0. destruct H0. destruct x.
+ simpl in H1. apply MP with (ps:=[(Empty_set _, Bot --> Or (A --> Or B C) (Bot));(Empty_set _, Bot)]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax.
apply AxRule_I. apply RA3_I. exists (A --> Or B C). exists (Bot). auto.
inversion H3. subst. assumption. inversion H4.
+ assert (x=nil). inversion H. subst. assert (b1 = (Excl A B --> C)). pose (H0 b1).
assert (List.In b1 (b1 :: x)). apply in_eq. apply s in H2. inversion H2. reflexivity.
subst. destruct x. reflexivity. exfalso. apply H4. pose (H0 b1).
assert (List.In b1 (Excl A B --> C :: b1 :: x)). apply in_cons. apply in_eq.
apply s in H2. inversion H2. subst. apply in_eq. subst. simpl in H1. assert (b1= Excl A B --> C).
pose (H0 b1). assert (List.In b1 [b1]). apply in_eq. apply s in H2. inversion H2. auto.
subst. apply absorp_Or1 in H1. apply b in H1.
apply MP with (ps:=[(Empty_set _, (A --> Or B C) --> (Or (A --> Or B C) (Bot)));(Empty_set _, (A --> Or B C))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists (A --> Or B C). exists (Bot). auto. inversion H3. subst. assumption.
inversion H4.
- intro. exists [(Excl A B --> C)]. repeat split.
* apply NoDup_cons. intro. inversion H0. apply NoDup_nil.
* intros. inversion H0. subst. simpl. inversion H0. subst. apply In_singleton. inversion H1. inversion H1.
* destruct H. destruct H. pose (wdual_residuation A B C). destruct p. clear b. simpl.
simpl in H0. simpl in b0. destruct H0. destruct x.
+ simpl in H1. apply MP with (ps:=[(Empty_set _, Bot --> Or (Excl A B --> C) (Bot));(Empty_set _, Bot)]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax.
apply AxRule_I. apply RA3_I. exists (Excl A B --> C). exists (Bot). auto.
inversion H3. subst. assumption. inversion H4.
+ assert (x=nil). inversion H. subst. assert (b = (A --> Or B C)). pose (H0 b).
assert (List.In b (b :: x)). apply in_eq. apply s in H2. inversion H2. reflexivity.
subst. destruct x. reflexivity. exfalso. apply H4. pose (H0 b).
assert (List.In b (A --> Or B C :: b :: x)). apply in_cons. apply in_eq.
apply s in H2. inversion H2. subst. apply in_eq. subst. simpl in H1. assert (b= A --> Or B C).
pose (H0 b). assert (List.In b [b]). apply in_eq. apply s in H2. inversion H2. auto.
subst. apply absorp_Or1 in H1. apply b0 in H1.
apply MP with (ps:=[(Empty_set _, (Excl A B --> C) --> (Or (Excl A B --> C) (Bot)));(Empty_set _, (Excl A B --> C))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists (Excl A B --> C). exists (Bot). auto. inversion H3. subst. assumption.
inversion H4.
Qed.
Lemma wTop : forall Γ , BIH_rules (Γ , Top).
Proof.
intros. apply MP with (ps:=[(Γ , Imp (Imp (Top) (Top)) (Top));(Γ , (Imp (Top) (Top)))]).
2: apply MPRule_I. intros. inversion H. subst. apply Ax. apply AxRule_I.
apply RA15_I. exists (Top --> Top). auto. inversion H0. subst. apply wimp_Id_gen.
inversion H1.
Qed.
Lemma wBiLEM : forall A Γ , BIH_rules (Γ , Or A (wNeg A)).
Proof.
intros. pose (BIH_monot (Empty_set _, Or A (wNeg A))). apply b.
apply MP with (ps:=[(Empty_set _, (Or A (Excl (Top) A)) --> (Or A (wNeg A)));(Empty_set _, (Or A (Excl (Top) A)))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Empty_set _, ((Excl (Top) A) --> (Or A (wNeg A))) --> ((Or A (Excl (Top) A)) --> (Or A (wNeg A))));(Empty_set _, ((Excl (Top) A) --> (Or A (wNeg A))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Empty_set _, (A --> (Or A (wNeg A))) --> ((Excl (Top) A) --> (Or A (wNeg A))) --> ((Or A (Excl (Top) A)) --> (Or A (wNeg A))));(Empty_set _, (A --> (Or A (wNeg A))))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA4_I.
exists A. exists (Excl (Top) A). exists (Or A (wNeg A)). auto. inversion H2.
subst. apply Ax. apply AxRule_I. apply RA2_I. exists A. exists (wNeg A). auto.
inversion H3. inversion H1. subst.
apply MP with (ps:=[(Empty_set _, ((wNeg A) --> Or A (wNeg A)) --> (Excl (Top) A --> Or A (wNeg A)));(Empty_set _, ((wNeg A) --> Or A (wNeg A)))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (Excl (Top) A --> (wNeg A)) --> ((wNeg A) --> Or A (wNeg A)) --> (Excl (Top) A --> Or A (wNeg A)));(Empty_set _, (Excl (Top) A --> (wNeg A)))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Excl (Top) A). exists (wNeg A). exists (Or A (wNeg A)).
auto. inversion H4. 2: inversion H5. subst. apply wimp_Id_gen.
inversion H3. subst. apply Ax. apply AxRule_I. apply RA3_I. exists A.
exists (wNeg A). auto. inversion H4. inversion H2. inversion H0. subst. 2: inversion H1.
apply MP with (ps:=[(Empty_set _, Imp (Top) (Or A (Excl (Top) A)));(Empty_set _, Top)]). 2: apply MPRule_I.
intros. inversion H1. subst. apply wdual_residuation. apply wimp_Id_gen. inversion H2.
2: inversion H3. subst. apply wTop. intro. intros. inversion H.
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.
Lemma wThm_irrel : forall A B Γ , BIH_rules (Γ , A --> (B --> A)).
Proof.
intros A B Γ .
apply MP with (ps:=[(Γ ,(And A B --> A) --> (A --> (B --> A)));(Γ , (And A B --> A))]).
2: apply MPRule_I. intros. inversion H. subst.
apply Ax. apply AxRule_I. apply RA9_I. exists A. exists B. exists A. auto.
inversion H0. subst. apply Ax. apply AxRule_I. apply RA5_I. exists A. exists B. auto. inversion H1.
Qed.
Lemma wimp_Id_gen : forall A Γ , BIH_rules (Γ , A --> A).
Proof.
intros A Γ .
apply MP with (ps:=[(Γ , (And A A --> A) --> (A --> A)); (Γ , (And A A --> A))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , ((And (And A A --> A) A) --> A) --> (And A A --> A) --> (A --> A)); (Γ , (And (And A A --> A) A) --> A)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I. apply RA9_I.
exists (And A A --> A). exists A. exists A. auto. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA6_I.
exists (And A A --> A). exists A. auto. inversion H2. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA5_I. exists A. exists A. auto. inversion H1.
Qed.
Lemma comm_And_obj : forall A B Γ ,
(BIH_rules (Γ , And A B --> And B A)).
Proof.
intros A B Γ .
apply MP with (ps:=[(Γ , (And A B --> A) --> (And A B --> And B A));(Γ , (And A B --> A))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (And A B --> B) --> (And A B --> A) --> (And A B --> And B A));(Γ , (And A B --> B))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (And A B). exists B. exists A.
auto. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA6_I. exists A. exists B. auto. inversion H2.
inversion H0. subst. apply Ax. apply AxRule_I. apply RA5_I. exists A. exists B. auto.
inversion H1.
Qed.
Lemma wContr_Bot : forall A Γ , BIH_rules (Γ , And A (Neg A) --> (Bot)).
Proof.
intros A Γ .
apply MP with (ps:=[(Γ , (And (Neg A) A --> Bot) --> (And A (Neg A) --> Bot));(Γ , And (Neg A) A --> Bot)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (And A (Neg A) --> And (Neg A) A) --> (And (Neg A) A --> Bot) --> (And A (Neg A) --> Bot));(Γ , And A (Neg A) --> And (Neg A) A)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (And A (Neg A)). exists (And (Neg A) A). exists (Bot). auto. inversion H1.
subst. apply comm_And_obj. inversion H2. inversion H0. subst.
apply MP with (ps:=[(Γ , ((Neg A) --> A --> Bot) --> (And (Neg A) A --> Bot));(Γ , ((Neg A) --> A --> Bot))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax.
apply AxRule_I. apply RA8_I. exists (Neg A). exists A. exists (Bot). auto. inversion H2.
subst. apply wimp_Id_gen. inversion H3. inversion H1.
Qed.
Lemma wmonotR_Or : forall A B Γ ,
(BIH_rules (Γ , A --> B)) ->
(forall C, BIH_rules (Γ , (Or A C) --> (Or B C))).
Proof.
intros A B Γ D C.
apply MP with (ps:=[(Γ , (C --> Or B C) --> (Or A C --> Or B C));(Γ ,(C --> Or B C))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (A --> Or B C) --> (C --> Or B C) --> (Or A C --> Or B C));(Γ ,(A --> Or B C))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists A. exists C.
exists (Or B C). auto. inversion H1. subst.
apply MP with (ps:=[(Γ , (B --> Or B C) --> (A --> Or B C));(Γ ,((B --> Or B C)))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (A --> B) --> (B --> Or B C) --> (A --> Or B C));(Γ ,(A --> B))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists B. exists (Or B C). auto.
inversion H4. subst. assumption. inversion H5. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists B. exists C.
auto. inversion H4. inversion H2. inversion H0. subst. apply Ax. apply AxRule_I. apply RA3_I.
exists B. exists C. auto. inversion H1.
Qed.
Lemma wmonotL_Or : forall A B Γ,
(BIH_rules (Γ, A --> B)) ->
(forall C, BIH_rules (Γ, (Or C A) --> (Or C B))).
Proof.
intros A B Γ D C.
apply MP with (ps:=[(Γ , (A --> Or C B) --> ((Or C A) --> (Or C B)));(Γ ,(A --> Or C B))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (C --> Or C B) --> (A --> Or C B) --> ((Or C A) --> (Or C B)));(Γ ,(C --> Or C B))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I. apply RA4_I. exists C. exists A.
exists (Or C B). auto. inversion H1. subst. apply Ax.
apply AxRule_I. apply RA2_I. exists C. exists B.
auto. inversion H2. inversion H0. subst.
apply MP with (ps:=[(Γ , (B --> Or C B) --> (A --> Or C B));(Γ ,((B --> Or C B)))]).
2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Γ , (A --> B) --> (B --> Or C B) --> (A --> Or C B));(Γ ,(A --> B))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists B. exists (Or C B). auto. inversion H3. subst.
assumption. inversion H4. inversion H2. subst. apply Ax.
apply AxRule_I. apply RA3_I. exists C. exists B.
auto. inversion H3. inversion H1.
Qed.
Lemma comm_Or_obj : forall A B Γ , (BIH_rules (Γ , Or A B --> Or B A)).
Proof.
intros A B Γ .
apply MP with (ps:=[(Γ , (B --> Or B A) --> (Or A B --> Or B A));(Γ , (B --> Or B A))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (A --> Or B A) --> (B --> Or B A) --> (Or A B --> Or B A));(Γ , (A --> Or B A))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists A. exists B. exists (Or B A).
auto. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists B. exists A. auto.
inversion H2. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA2_I. exists B. exists A. auto.
inversion H1.
Qed.
Lemma comm_Or : forall A B Γ , (BIH_rules (Γ , Or A B)) -> (BIH_rules (Γ , Or B A)).
Proof.
intros A B Γ D.
apply MP with (ps:=[(Γ , Or A B --> Or B A);(Γ , Or A B)]).
2: apply MPRule_I. intros. inversion H. subst. apply comm_Or_obj.
inversion H0. subst. assumption. inversion H1.
Qed.
Lemma wmonot_Or2 : forall A B Γ , (BIH_rules (Γ , A --> B)) ->
(forall C, BIH_rules (Γ , (Or A C) --> (Or C B))).
Proof.
intros A B Γ D C.
apply MP with (ps:=[(Γ , (C --> Or C B) --> (Or A C --> Or C B));(Γ , C --> Or C B)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (A --> Or C B) --> (C --> Or C B) --> (Or A C --> Or C B));(Γ , A --> Or C B)]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax.
apply AxRule_I. apply RA4_I. exists A. exists C. exists (Or C B). auto.
inversion H1. subst.
apply MP with (ps:=[(Γ , (B --> Or C B) --> (A --> Or C B));(Γ , B --> Or C B)]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (A --> B) --> (B --> Or C B) --> (A --> Or C B));(Γ , A --> B)]).
2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists B. exists (Or C B).
auto. inversion H4. subst. assumption. inversion H5. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA3_I. exists C. exists B. auto. inversion H4.
inversion H2. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA2_I. exists C. exists B. auto. inversion H1.
Qed.
Theorem wdual_residuation0 : forall A B C,
(BIH_rules (Empty_set _, (Excl A B) --> C) ->
BIH_rules (Empty_set _, A --> (Or B C))).
Proof.
intros A B C D. pose (@wmonot_Or2 (Excl A B) C (Empty_set _) D B).
apply MP with (ps:=[(Empty_set _, (Or (Excl A B) B --> Or B C) --> (A --> Or B C));(Empty_set _,Or (Excl A B) B --> Or B C)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or (Excl A B) B) --> (Or (Excl A B) B --> Or B C) --> (A --> Or B C));(Empty_set _,(A --> Or (Excl A B) B))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists A. exists (Or (Excl A B) B). exists (Or B C). auto.
inversion H1. subst.
apply MP with (ps:=[(Empty_set _, (Or B (Excl A B) --> Or (Excl A B) B) --> (A --> Or (Excl A B) B));(Empty_set _,(Or B (Excl A B) --> Or (Excl A B) B))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or B (Excl A B)) --> (Or B (Excl A B) --> Or (Excl A B) B) --> (A --> Or (Excl A B) B));(Empty_set _,(A --> Or B (Excl A B)))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (Or B (Excl A B)). exists (Or (Excl A B) B).
auto. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists A. exists B. auto. inversion H5.
inversion H3. subst. apply comm_Or_obj. inversion H4. inversion H2. inversion H0.
subst. assumption. inversion H1.
Qed.
Lemma wDN_to_form : forall A Γ , (BIH_rules (Γ , Neg (wNeg A)--> A)).
Proof.
intros A Γ .
apply MP with (ps:=[(Γ , (Top) --> Neg (wNeg A) --> A);(Γ , Top)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , ((And (Top) (Neg (wNeg A))) --> A) --> ((Top) --> (Neg (wNeg A)) --> A));(Γ , ((And (Top) (Neg (wNeg A))) --> A))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA9_I. exists (Top). exists (Neg (wNeg A)). exists A. auto.
inversion H1. subst.
apply MP with (ps:=[(Γ , ((And (Neg (wNeg A)) (Top))--> A) --> (And (Top) (Neg (wNeg A)) --> A));(Γ , (And (Neg (wNeg A)) (Top))--> A)]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , ((And (Top) (Neg (wNeg A))) --> (And (Neg (wNeg A)) (Top))) --> ((And (Neg (wNeg A)) (Top))--> A) --> (And (Top) (Neg (wNeg A)) --> A));
(Γ , ((And (Top) (Neg (wNeg A))) --> (And (Neg (wNeg A)) (Top))))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (And (Top) (Neg (wNeg A))). exists (And (Neg (wNeg A)) (Top)).
exists A. auto. inversion H4. subst.
apply MP with (ps:=[(Γ , (And (Top) (Neg (wNeg A)) --> (Top)) --> And (Top) (Neg (wNeg A)) --> And (Neg (wNeg A)) (Top));
(Γ , And (Top) (Neg (wNeg A)) --> (Top))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (And (Top) (Neg (wNeg A)) --> (Neg (wNeg A))) --> (And (Top) (Neg (wNeg A)) --> (Top)) --> And (Top) (Neg (wNeg A)) --> And (Neg (wNeg A)) (Top));
(Γ , And (Top) (Neg (wNeg A)) --> (Neg (wNeg A)))]). 2: apply MPRule_I. intros. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (And (Top) (Neg (wNeg A))).
exists (Neg (wNeg A)). exists (Top). auto. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA6_I. exists (Top).
exists (Neg (wNeg A)). auto. inversion H8. inversion H6. subst.
apply Ax. apply AxRule_I. apply RA5_I. exists (Top).
exists (Neg (wNeg A)). auto. inversion H7. inversion H5. inversion H3. subst.
apply MP with (ps:=[(Γ , ((Neg (wNeg A)) --> (Top) --> A) --> And (Neg (wNeg A)) (Top) --> A);
(Γ , ((Neg (wNeg A)) --> (Top) --> A))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA8_I. exists (Neg (wNeg A)).
exists (Top). exists A. auto. inversion H5. subst.
apply MP with (ps:=[(Γ , (((wNeg A) --> (Bot)) --> Top --> A) --> (Neg (wNeg A) --> Top --> A));
(Γ , (((wNeg A) --> (Bot)) --> Top --> A))]). 2: apply MPRule_I. intros. inversion H6. subst.
apply MP with (ps:=[(Γ , (Neg (wNeg A) --> ((wNeg A) --> (Bot))) --> (((wNeg A) --> (Bot)) --> Top --> A) --> (Neg (wNeg A) --> Top --> A));
(Γ , Neg (wNeg A) --> ((wNeg A) --> (Bot)))]). 2: apply MPRule_I. intros. inversion H7. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Neg (wNeg A)).
exists (wNeg A --> Bot). exists (Top --> A). auto. inversion H8. subst.
apply wimp_Id_gen. inversion H9.
inversion H7. subst.
apply MP with (ps:=[(Γ , (((Excl (Top) A) --> Bot) --> Top --> A) --> (wNeg A --> Bot) --> Top --> A);(Γ , ((Excl (Top) A) --> Bot) --> Top --> A)]).
2: apply MPRule_I. intros. inversion H8. subst.
apply MP with (ps:=[(Γ , ((wNeg A --> Bot) --> ((Excl (Top) A) --> Bot)) --> (((Excl (Top) A) --> Bot) --> Top --> A) --> (wNeg A --> Bot) --> Top --> A);
(Γ , (wNeg A --> Bot) --> ((Excl (Top) A) --> Bot))]).
2: apply MPRule_I. intros. inversion H9. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists (wNeg A --> Bot). exists (Excl (Top) A --> Bot).
exists (Top --> A). auto. inversion H10. subst.
apply MP with (ps:=[(Γ , (Excl (Top) A --> (wNeg A)) --> ((wNeg A --> Bot) --> Excl (Top) A --> Bot));(Γ , (Excl (Top) A --> (wNeg A)))]).
2: apply MPRule_I. intros. inversion H11. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Excl (Top) A). exists (wNeg A). exists (Bot). auto. inversion H12. subst.
apply wimp_Id_gen.
inversion H13. inversion H11. inversion H9. subst.
apply MP with (ps:=[(Γ , (Neg (Excl (Top) A) --> Top --> A) --> ((Excl (Top) A --> Bot) --> Top --> A));(Γ , (Neg (Excl (Top) A) --> Top --> A))]).
2: apply MPRule_I. intros. inversion H10. subst.
apply MP with (ps:=[(Γ , ((Excl (Top) A --> Bot) --> Neg (Excl (Top) A)) --> (Neg (Excl (Top) A) --> Top --> A) --> ((Excl (Top) A --> Bot) --> Top --> A));
(Γ , (Excl (Top) A --> Bot) --> Neg (Excl (Top) A))]).
2: apply MPRule_I. intros. inversion H11. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists (Excl (Top) A --> Bot). exists (Neg (Excl (Top) A)).
exists (Top --> A). auto. inversion H12. subst.
apply wimp_Id_gen.
inversion H13. inversion H11. subst. apply Ax. apply AxRule_I.
apply RA14_I. exists (Top). exists A. auto. inversion H12. inversion H10.
inversion H8. inversion H6. inversion H4. inversion H2. inversion H0. subst.
apply MP with (ps:=[(Γ , Imp (Imp A A) (Top));(Γ , Imp A A)]).
2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA15_I. exists (A --> A). auto. inversion H2.
subst. apply wimp_Id_gen. inversion H3. inversion H1.
Qed.
Lemma wEFQ : forall A Γ , BIH_rules (Γ , (Bot) --> A).
Proof.
intros A Γ .
apply MP with (ps:=[(Γ , ((Neg (wNeg A)) --> A) --> (Bot --> A));(Γ , (Neg (wNeg A)) --> A)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Bot --> (Neg (wNeg A))) --> ((Neg (wNeg A)) --> A) --> (Bot --> A));(Γ , (Bot) --> (Neg (wNeg A)))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Bot). exists (Neg (wNeg A)). exists A. auto.
inversion H1. subst.
apply MP with (ps:=[(Γ , (Neg (Top) --> Neg (wNeg A)) --> (Bot --> Neg (wNeg A)));
(Γ , Neg (Top) --> Neg (wNeg A))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Γ , (Bot --> Neg (Top)) --> (Neg (Top) --> Neg (wNeg A)) --> (Bot --> Neg (wNeg A)));
(Γ , Bot --> Neg (Top))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Bot). exists (Neg (Top)). exists (Neg (wNeg A)). auto.
inversion H4. subst.
apply MP with (ps:=[(Γ , (((Top) --> (Bot)) --> Neg (Top)) --> (Bot --> Neg (Top)));
(Γ , ((Top) --> (Bot)) --> Neg (Top))]).
2: apply MPRule_I. intros. inversion H5. subst.
apply MP with (ps:=[(Γ , (Bot --> ((Top) --> (Bot))) --> (((Top) --> (Bot)) --> Neg (Top)) --> (Bot --> Neg (Top)));
(Γ , Bot --> ((Top) --> (Bot)))]).
2: apply MPRule_I. intros. inversion H6. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Bot). exists ((Top) --> (Bot)). exists (Neg (Top)). auto.
inversion H7. subst. apply wThm_irrel. inversion H8. inversion H6. subst.
apply wimp_Id_gen. inversion H7. inversion H5. inversion H3. subst.
apply MP with (ps:=[(Γ , ((wNeg A) --> (Top)) --> (Neg (Top) --> Neg (wNeg A)));
(Γ , ((wNeg A) --> (Top)))]).
2: apply MPRule_I. intros. inversion H4. subst. apply Ax. apply AxRule_I.
apply RA10_I. exists (wNeg A). exists (Top). auto. inversion H5. subst.
apply MP with (ps:=[(Γ , (Top) --> (wNeg A --> Top));(Γ , Top)]).
2: apply MPRule_I. intros. inversion H6. subst. apply wThm_irrel.
inversion H7. subst.
apply MP with (ps:=[(Γ , (A --> A) --> Top);(Γ , A --> A)]).
2: apply MPRule_I. intros. inversion H8. subst. apply Ax. apply AxRule_I.
apply RA15_I. exists (A --> A). auto. inversion H9. subst. apply wimp_Id_gen.
inversion H10. inversion H8. inversion H6. inversion H4. inversion H2.
inversion H0. subst. apply wDN_to_form. inversion H1.
Qed.
Lemma absorp_Or1 : forall A Γ ,
(BIH_rules (Γ , Or A (Bot))) ->
(BIH_rules (Γ , A)).
Proof.
intros A Γ D.
apply MP with (ps:=[(Γ , Imp (Or A (Bot)) A);(Γ , Or A (Bot))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Γ , (Bot --> A) --> (Or A (Bot) --> A));(Γ , (Bot --> A))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Γ , (A --> A) --> (Bot --> A) --> (Or A (Bot) --> A));(Γ , A --> A)]).
2: apply MPRule_I. intros. inversion H1. subst.
apply Ax. apply AxRule_I. apply RA4_I. exists A. exists (Bot).
exists A. auto. inversion H2. subst. apply wimp_Id_gen. inversion H3.
inversion H1. subst. apply wEFQ. inversion H2. inversion H0. subst.
assumption. inversion H1.
Qed.
Theorem wdual_residuation : forall A B C,
(BIH_rules (Empty_set _, (Excl A B) --> C) ->
BIH_rules (Empty_set _, A --> (Or B C))) *
(BIH_rules (Empty_set _, A --> (Or B C)) ->
BIH_rules (Empty_set _, (Excl A B) --> C)).
Proof.
intros A B C. split.
- intro D. pose (@wmonot_Or2 (Excl A B) C (Empty_set _) D B).
apply MP with (ps:=[(Empty_set _, (Or (Excl A B) B --> Or B C) --> (A --> Or B C));(Empty_set _,Or (Excl A B) B --> Or B C)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or (Excl A B) B) --> (Or (Excl A B) B --> Or B C) --> (A --> Or B C));(Empty_set _,(A --> Or (Excl A B) B))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (Or (Excl A B) B). exists (Or B C). auto.
inversion H1. subst.
apply MP with (ps:=[(Empty_set _, (Or B (Excl A B) --> Or (Excl A B) B) --> (A --> Or (Excl A B) B));(Empty_set _,(Or B (Excl A B) --> Or (Excl A B) B))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (A --> Or B (Excl A B)) --> (Or B (Excl A B) --> Or (Excl A B) B) --> (A --> Or (Excl A B) B));(Empty_set _,(A --> Or B (Excl A B)))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax.
apply AxRule_I. apply RA1_I. exists A. exists (Or B (Excl A B)). exists (Or (Excl A B) B).
auto. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists A. exists B. auto. inversion H5. inversion H3. subst. apply comm_Or_obj.
inversion H4. inversion H2. inversion H0. subst. assumption. inversion H1.
- intro D. apply MP with (ps:=[(Empty_set _, ((Or C (Excl A (Or B C))) --> C) --> (Excl A B --> C));(Empty_set _, (Or C (Excl A (Or B C))) --> C)]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Empty_set _, (Excl A B --> (Or C (Excl A (Or B C)))) --> ((Or C (Excl A (Or B C))) --> C) --> (Excl A B --> C));(Empty_set _, Excl A B --> (Or C (Excl A (Or B C))))]).
2: apply MPRule_I. intros. inversion H0. subst. apply Ax. apply AxRule_I. apply RA1_I.
exists (Excl A B). exists (Or C (Excl A (Or B C))). exists C. auto. inversion H1. subst.
apply MP with (ps:=[(Empty_set _, ((Or C (Excl (Excl A B) C)) --> Or C (Excl A (Or B C))) --> (Excl A B --> Or C (Excl A (Or B C))));(Empty_set _, ((Or C (Excl (Excl A B) C)) --> Or C (Excl A (Or B C))))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (Excl A B --> (Or C (Excl (Excl A B) C)))--> ((Or C (Excl (Excl A B) C)) --> Or C (Excl A (Or B C))) --> (Excl A B --> Or C (Excl A (Or B C))));
(Empty_set _, (Excl A B --> (Or C (Excl (Excl A B) C))))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Excl A B). exists (Or C (Excl (Excl A B) C)).
exists (Or C (Excl A (Or B C))). auto. inversion H4. subst.
apply Ax. apply AxRule_I. apply RA11_I. exists (Excl A B). exists C. auto. inversion H5.
inversion H3. subst. apply wmonotL_Or.
apply Ax. apply AxRule_I. apply RA13_I.
exists A. exists B. exists C. auto. inversion H4. inversion H2. inversion H0. subst. 2: inversion H1.
apply MP with (ps:=[(Empty_set _, (Or C (Bot) --> C) --> (Or C (Excl A (Or B C)) --> C));
(Empty_set _, (Or C (Bot) --> C))]). 2: apply MPRule_I. intros. inversion H1. subst.
apply MP with (ps:=[(Empty_set _, (Or C (Excl A (Or B C)) --> Or C (Bot)) --> (Or C (Bot) --> C) --> (Or C (Excl A (Or B C)) --> C));
(Empty_set _, (Or C (Excl A (Or B C)) --> Or C (Bot)))]). 2: apply MPRule_I. intros. inversion H2. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Or C (Excl A (Or B C))).
exists (Or C (Bot)). exists C. auto. inversion H3. subst. apply wmonotL_Or.
apply MP with (ps:=[(Empty_set _, ((And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))) --> Bot) --> (Excl A (Or B C) --> Bot));
(Empty_set _, ((And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))) --> Bot))]). 2: apply MPRule_I. intros. inversion H4. subst.
apply MP with (ps:=[(Empty_set _, (Excl A (Or B C) --> (And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C))))) --> ((And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))) --> Bot) --> (Excl A (Or B C) --> Bot));
(Empty_set _, (Excl A (Or B C) --> (And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C))))))]). 2: apply MPRule_I. intros. inversion H5. subst.
apply Ax. apply AxRule_I. apply RA1_I. exists (Excl A (Or B C)).
exists (And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))). exists (Bot). auto. inversion H6. subst.
apply MP with (ps:=[(Empty_set _, (Excl A (Or B C) --> (Neg (wNeg (A --> Or B C)))) --> (Excl A (Or B C) --> And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))));
(Empty_set _, (Excl A (Or B C) --> (Neg (wNeg (A --> Or B C)))))]). 2: apply MPRule_I. intros. inversion H7. subst.
apply MP with (ps:=[(Empty_set _, (Excl A (Or B C) --> (wNeg (A --> Or B C))) --> (Excl A (Or B C) --> (Neg (wNeg (A --> Or B C)))) --> (Excl A (Or B C) --> And (wNeg (A --> Or B C)) (Neg (wNeg (A --> Or B C)))));
(Empty_set _, (Excl A (Or B C) --> (wNeg (A --> Or B C))))]). 2: apply MPRule_I. intros. inversion H8. subst.
apply Ax. apply AxRule_I. apply RA7_I. exists (Excl A (Or B C)).
exists (wNeg (A --> Or B C)). exists (Neg (wNeg (A --> Or B C))). auto. inversion H9.
subst. apply Ax. apply AxRule_I. apply RA12_I. exists A. exists (Or B C).
auto. inversion H10. inversion H8. subst.
apply MP with (ps:=[(Empty_set _, (Neg (wNeg (A --> Or B C))) --> (Excl A (Or B C) --> Neg (wNeg (A --> Or B C))));
(Empty_set _, (Neg (wNeg (A --> Or B C))))]). 2: apply MPRule_I. intros. inversion H9. subst.
apply wThm_irrel. inversion H10. subst. apply DNw with (ps:=[(Empty_set _, A --> Or B C)]).
2: apply DNwRule_I. intros. inversion H11. subst. assumption. inversion H12. inversion H11.
inversion H9. inversion H7. inversion H5. subst. apply wContr_Bot. inversion H6.
inversion H4. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (Bot --> C) --> (Or C (Bot) --> C));(Empty_set _, (Bot --> C))]).
2: apply MPRule_I. intros. inversion H3. subst.
apply MP with (ps:=[(Empty_set _, (C --> C) --> (Bot --> C) --> (Or C (Bot) --> C));(Empty_set _, (C --> C))]).
2: apply MPRule_I. intros. inversion H4. subst. apply Ax.
apply AxRule_I. apply RA4_I. exists C. exists (Bot). exists C. auto.
inversion H5. subst. apply wimp_Id_gen. inversion H6. inversion H4. subst.
apply wEFQ. inversion H5. inversion H3.
Qed.
Lemma wAThm_irrel : forall A B Γ , BIH_rules (Γ , (Excl A B) --> A).
Proof.
intros A B Γ . pose (BIH_monot (Empty_set _, Excl A B --> A)). apply b.
apply wdual_residuation. apply Ax. apply AxRule_I.
apply RA3_I. exists B. exists A. auto. intro. intros. simpl in H.
inversion H.
Qed.
Theorem wdual_residuation_gen : forall A B C,
(pair_derrec (Empty_set _, Singleton _ ((Excl A B) --> C)) ->
pair_derrec (Empty_set _, Singleton _ (A --> (Or B C)))) *
(pair_derrec (Empty_set _, Singleton _ (A --> (Or B C))) ->
pair_derrec (Empty_set _, Singleton _ ((Excl A B) --> C))).
Proof.
intros A B C. split.
- intro. exists [(A --> Or B C)]. repeat split.
* apply NoDup_cons. intro. inversion H0. apply NoDup_nil.
* intros. inversion H. subst. simpl. inversion H0. subst. apply In_singleton. inversion H2.
* destruct H. destruct H. pose (wdual_residuation A B C). destruct p. simpl.
simpl in b. simpl in b0. simpl in H0. destruct H0. destruct x.
+ simpl in H1. apply MP with (ps:=[(Empty_set _, Bot --> Or (A --> Or B C) (Bot));(Empty_set _, Bot)]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax.
apply AxRule_I. apply RA3_I. exists (A --> Or B C). exists (Bot). auto.
inversion H3. subst. assumption. inversion H4.
+ assert (x=nil). inversion H. subst. assert (b1 = (Excl A B --> C)). pose (H0 b1).
assert (List.In b1 (b1 :: x)). apply in_eq. apply s in H2. inversion H2. reflexivity.
subst. destruct x. reflexivity. exfalso. apply H4. pose (H0 b1).
assert (List.In b1 (Excl A B --> C :: b1 :: x)). apply in_cons. apply in_eq.
apply s in H2. inversion H2. subst. apply in_eq. subst. simpl in H1. assert (b1= Excl A B --> C).
pose (H0 b1). assert (List.In b1 [b1]). apply in_eq. apply s in H2. inversion H2. auto.
subst. apply absorp_Or1 in H1. apply b in H1.
apply MP with (ps:=[(Empty_set _, (A --> Or B C) --> (Or (A --> Or B C) (Bot)));(Empty_set _, (A --> Or B C))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists (A --> Or B C). exists (Bot). auto. inversion H3. subst. assumption.
inversion H4.
- intro. exists [(Excl A B --> C)]. repeat split.
* apply NoDup_cons. intro. inversion H0. apply NoDup_nil.
* intros. inversion H0. subst. simpl. inversion H0. subst. apply In_singleton. inversion H1. inversion H1.
* destruct H. destruct H. pose (wdual_residuation A B C). destruct p. clear b. simpl.
simpl in H0. simpl in b0. destruct H0. destruct x.
+ simpl in H1. apply MP with (ps:=[(Empty_set _, Bot --> Or (Excl A B --> C) (Bot));(Empty_set _, Bot)]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax.
apply AxRule_I. apply RA3_I. exists (Excl A B --> C). exists (Bot). auto.
inversion H3. subst. assumption. inversion H4.
+ assert (x=nil). inversion H. subst. assert (b = (A --> Or B C)). pose (H0 b).
assert (List.In b (b :: x)). apply in_eq. apply s in H2. inversion H2. reflexivity.
subst. destruct x. reflexivity. exfalso. apply H4. pose (H0 b).
assert (List.In b (A --> Or B C :: b :: x)). apply in_cons. apply in_eq.
apply s in H2. inversion H2. subst. apply in_eq. subst. simpl in H1. assert (b= A --> Or B C).
pose (H0 b). assert (List.In b [b]). apply in_eq. apply s in H2. inversion H2. auto.
subst. apply absorp_Or1 in H1. apply b0 in H1.
apply MP with (ps:=[(Empty_set _, (Excl A B --> C) --> (Or (Excl A B --> C) (Bot)));(Empty_set _, (Excl A B --> C))]).
2: apply MPRule_I. intros. inversion H2. subst. apply Ax. apply AxRule_I. apply RA2_I.
exists (Excl A B --> C). exists (Bot). auto. inversion H3. subst. assumption.
inversion H4.
Qed.
Lemma wTop : forall Γ , BIH_rules (Γ , Top).
Proof.
intros. apply MP with (ps:=[(Γ , Imp (Imp (Top) (Top)) (Top));(Γ , (Imp (Top) (Top)))]).
2: apply MPRule_I. intros. inversion H. subst. apply Ax. apply AxRule_I.
apply RA15_I. exists (Top --> Top). auto. inversion H0. subst. apply wimp_Id_gen.
inversion H1.
Qed.
Lemma wBiLEM : forall A Γ , BIH_rules (Γ , Or A (wNeg A)).
Proof.
intros. pose (BIH_monot (Empty_set _, Or A (wNeg A))). apply b.
apply MP with (ps:=[(Empty_set _, (Or A (Excl (Top) A)) --> (Or A (wNeg A)));(Empty_set _, (Or A (Excl (Top) A)))]).
2: apply MPRule_I. intros. inversion H. subst.
apply MP with (ps:=[(Empty_set _, ((Excl (Top) A) --> (Or A (wNeg A))) --> ((Or A (Excl (Top) A)) --> (Or A (wNeg A))));(Empty_set _, ((Excl (Top) A) --> (Or A (wNeg A))))]).
2: apply MPRule_I. intros. inversion H0. subst.
apply MP with (ps:=[(Empty_set _, (A --> (Or A (wNeg A))) --> ((Excl (Top) A) --> (Or A (wNeg A))) --> ((Or A (Excl (Top) A)) --> (Or A (wNeg A))));(Empty_set _, (A --> (Or A (wNeg A))))]).
2: apply MPRule_I. intros. inversion H1. subst. apply Ax. apply AxRule_I. apply RA4_I.
exists A. exists (Excl (Top) A). exists (Or A (wNeg A)). auto. inversion H2.
subst. apply Ax. apply AxRule_I. apply RA2_I. exists A. exists (wNeg A). auto.
inversion H3. inversion H1. subst.
apply MP with (ps:=[(Empty_set _, ((wNeg A) --> Or A (wNeg A)) --> (Excl (Top) A --> Or A (wNeg A)));(Empty_set _, ((wNeg A) --> Or A (wNeg A)))]).
2: apply MPRule_I. intros. inversion H2. subst.
apply MP with (ps:=[(Empty_set _, (Excl (Top) A --> (wNeg A)) --> ((wNeg A) --> Or A (wNeg A)) --> (Excl (Top) A --> Or A (wNeg A)));(Empty_set _, (Excl (Top) A --> (wNeg A)))]).
2: apply MPRule_I. intros. inversion H3. subst. apply Ax. apply AxRule_I.
apply RA1_I. exists (Excl (Top) A). exists (wNeg A). exists (Or A (wNeg A)).
auto. inversion H4. 2: inversion H5. subst. apply wimp_Id_gen.
inversion H3. subst. apply Ax. apply AxRule_I. apply RA3_I. exists A.
exists (wNeg A). auto. inversion H4. inversion H2. inversion H0. subst. 2: inversion H1.
apply MP with (ps:=[(Empty_set _, Imp (Top) (Or A (Excl (Top) A)));(Empty_set _, Top)]). 2: apply MPRule_I.
intros. inversion H1. subst. apply wdual_residuation. apply wimp_Id_gen. inversion H2.
2: inversion H3. subst. apply wTop. intro. intros. inversion H.
Qed.