K.KS.KS_ctr
Require Import List.
Export ListNotations.
Require Import Lia.
Require Import PeanoNat Arith.
Require Import KS_calc.
Require Import KS_inv_ImpR_ImpL.
(* Next are the definitions for contraction of one formula on the left, and
on the right. Note that while the leftmost occurrence of the formula is kept,
if we have exchange for our calculus it amounts to the same to keep the rightmost
formula. *)
Inductive ctr_L (fml : MPropF) : relationT Seq :=
| ctr_LI Γ0 Γ1 Γ2 Δ : ctr_L fml
(Γ0 ++ fml :: Γ1 ++ fml :: Γ2, Δ) (Γ0 ++ fml :: Γ1 ++ Γ2, Δ).
Inductive ctr_R (fml : MPropF) : relationT Seq :=
| ctr_RI Γ Δ0 Δ1 Δ2 : ctr_R fml
(Γ, Δ0 ++ fml :: Δ1 ++ fml :: Δ2) (Γ, Δ0 ++ fml :: Δ1 ++ Δ2).
(* The following lemmas make sure that if a rule is applied on a sequent s with
premises ps, then the same rule is applicable on a sequent sc which is a contracted
version of s, with some premises psc that are such that they are either the same premises
(in case the contracted formula was weakened) or contracted versions of ps. *)
Lemma ImpR_app_ctr_L : forall s sc A ps,
(@ctr_L A s sc) ->
(ImpRRule [ps] s) ->
(existsT2 psc, (ImpRRule [psc] sc) * (@ctr_L A ps psc)).
Proof.
intros s sc A ps ctr RA. inversion RA. inversion ctr. subst.
inversion H. subst. apply app2_find_hole in H1. destruct H1. destruct s.
- destruct s.
+ destruct p. subst. exists (Γ2 ++ A0 :: A :: Γ3 ++ Γ4, Δ0 ++ B :: Δ1).
split. apply ImpRRule_I.
assert (E1: Γ2 ++ A0 :: A :: Γ3 ++ A :: Γ4 = (Γ2 ++ [A0]) ++ A :: Γ3 ++ A :: Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: Γ2 ++ A0 :: A :: Γ3 ++ Γ4 = (Γ2 ++ [A0]) ++ A :: Γ3 ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
+ destruct p. subst. destruct x.
* simpl in e0. subst. repeat rewrite app_nil_r.
exists (Γ2 ++ A0 :: A :: Γ3 ++ Γ4, Δ0 ++ B :: Δ1). split. apply ImpRRule_I.
assert (E1: Γ2 ++ A0 :: A :: Γ3 ++ A :: Γ4 = (Γ2 ++ [A0]) ++ A :: Γ3 ++ A :: Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: Γ2 ++ A0 :: A :: Γ3 ++ Γ4 = (Γ2 ++ [A0]) ++ A :: Γ3 ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
* inversion e0. subst. apply app2_find_hole in H2. destruct H2. destruct s.
{ destruct s.
- destruct p. subst. exists ((Γ2 ++ m :: Γ3) ++ A0 :: Γ4, Δ0 ++ B :: Δ1).
split.
assert (E: Γ2 ++ m :: Γ3 ++ Γ4 = (Γ2 ++ m :: Γ3) ++ Γ4).
rewrite <- app_assoc. reflexivity. rewrite E. apply ImpRRule_I.
assert (E1: (Γ2 ++ m :: Γ3) ++ A0 :: m :: Γ4 = Γ2 ++ m :: (Γ3 ++ [A0]) ++ m :: Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Γ2 ++ m :: Γ3) ++ A0 :: Γ4 = Γ2 ++ m :: (Γ3 ++ [A0]) ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
- destruct p. subst. destruct x0.
+ simpl in e1. subst. repeat rewrite app_nil_r.
exists ((Γ2 ++ m :: Γ3) ++ A0 :: Γ4, Δ0 ++ B :: Δ1). split.
assert (E: Γ2 ++ m :: Γ3 ++ Γ4 = (Γ2 ++ m :: Γ3) ++ Γ4).
rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpRRule_I.
assert (E1: (Γ2 ++ m :: Γ3) ++ A0 :: m :: Γ4 = Γ2 ++ m :: (Γ3 ++ [A0]) ++ m :: Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Γ2 ++ m :: Γ3) ++ A0 :: Γ4 = Γ2 ++ m :: (Γ3 ++ [A0]) ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
+ inversion e1. subst.
exists ((Γ2 ++ m0 :: Γ3 ++ x0) ++ A0 :: Γ1, Δ0 ++ B :: Δ1). split.
assert (E: Γ2 ++ m0 :: Γ3 ++ x0 ++ Γ1 = (Γ2 ++ m0 :: Γ3 ++ x0) ++ Γ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpRRule_I.
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_LI. }
{ destruct p. subst. exists ((Γ2 ++ m :: x) ++ A0 :: x0 ++ Γ4,Δ0 ++ B :: Δ1).
split. assert (E: Γ2 ++ m :: (x ++ x0) ++ Γ4 = (Γ2 ++ m :: x) ++ x0 ++ Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite E. apply ImpRRule_I.
assert (E1: (Γ2 ++ m :: x) ++ A0 :: x0 ++ m :: Γ4 = Γ2 ++ m :: (x ++ A0 :: x0) ++ m :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Γ2 ++ m :: x) ++ A0 :: x0 ++ Γ4 = Γ2 ++ m :: (x ++ A0 :: x0) ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI. }
- destruct p. subst. exists (Γ0 ++ A0 :: x ++ A :: Γ3 ++ Γ4, Δ0 ++ B :: Δ1).
split. rewrite <- app_assoc. apply ImpRRule_I.
assert (E1: Γ0 ++ A0 :: x ++ A :: Γ3 ++ A :: Γ4 = (Γ0 ++ A0 :: x) ++ A :: Γ3 ++ A :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: Γ0 ++ A0 :: x ++ A :: Γ3 ++ Γ4 = (Γ0 ++ A0 :: x) ++ A :: Γ3 ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
Qed.
Lemma ImpL_app_ctr_L : forall s sc A ps1 ps2,
(@ctr_L A s sc) ->
(ImpLRule [ps1;ps2] s) ->
((existsT2 psc1 psc2, (ImpLRule [psc1;psc2] sc) *
(@ctr_L A ps1 psc1) *
(@ctr_L A ps2 psc2))
+
(existsT2 B C invps11 invps12 invps21 invps22 invpsc11 invpsc22,
(A = Imp B C) *
(ImpLRule [invps11;invps12] ps1) *
(ImpLRule [invps21;invps22] ps2) *
(@ctr_R B invps11 invpsc11) *
(@ctr_L C invps22 invpsc22) *
(ImpLRule [invpsc11;invpsc22] sc))).
Proof.
intros s sc A ps1 ps2 ctr RA. inversion RA. inversion ctr. subst. inversion H.
subst. apply app2_find_hole in H1. destruct H1. repeat destruct s ; destruct p ; subst.
- inversion e0. subst. right. exists A0. exists B.
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ Γ3 ++ B :: Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ Δ1). repeat split.
assert (Γ2 ++ Γ3 ++ Γ4 = (Γ2 ++ Γ3) ++ Γ4). rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ2 ++ Γ3 ++ B :: Γ4 = (Γ2 ++ Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Γ2 ++ Γ3 ++ A0 --> B :: Γ4 = (Γ2 ++ Γ3) ++ A0 --> B :: Γ4). rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Γ2 ++ B :: Γ3 ++ Γ4 = (Γ2 ++ B :: Γ3) ++ Γ4). rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ2 ++ B :: Γ3 ++ B :: Γ4 = (Γ2 ++ B :: Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Γ2 ++ B :: Γ3 ++ A0 --> B :: Γ4 = (Γ2 ++ B :: Γ3) ++ A0 --> B :: Γ4). rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI.
- destruct x.
* simpl in e0. inversion e0. subst. right. exists A0. exists B.
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ Γ3 ++ B :: Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ Δ1). repeat split.
assert (Γ2 ++ Γ3 ++ Γ4 = (Γ2 ++ Γ3) ++ Γ4). repeat rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ2 ++ Γ3 ++ B :: Γ4 = (Γ2 ++ Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert ((Γ2 ++ []) ++ Γ3 ++ A0 --> B :: Γ4 = (Γ2 ++ Γ3) ++ A0 --> B :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Γ2 ++ B :: Γ3 ++ Γ4 = (Γ2 ++ B :: Γ3) ++ Γ4). rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ2 ++ B :: Γ3 ++ B :: Γ4 = (Γ2 ++ B :: Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert ((Γ2 ++ []) ++ B :: Γ3 ++ A0 --> B :: Γ4 = (Γ2 ++ B :: Γ3) ++ A0 --> B :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI.
* inversion e0. subst. apply app2_find_hole in H2. destruct H2. repeat destruct s ; destruct p ; subst.
+ inversion e1. subst. right. exists A0. exists B.
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ Γ3 ++ B :: Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ Δ1). repeat split.
repeat rewrite <- app_assoc. apply ImpLRule_I. repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI.
+ destruct x0.
{ simpl in e1. inversion e1. subst. right. exists A0. exists B.
exists (Γ2 ++ Γ3 ++ Γ1, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ1, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ Γ3 ++ B :: Γ1, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ B :: Γ1, Δ0 ++ Δ1).
exists (Γ2 ++ Γ3 ++ Γ1, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ1, Δ0 ++ Δ1). repeat split.
repeat rewrite <- app_assoc. simpl. rewrite app_nil_r. apply ImpLRule_I. repeat rewrite <- app_assoc.
rewrite app_nil_r. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI. }
{ inversion e1. subst. left. exists (Γ2 ++ m0 :: Γ3 ++ x0 ++ Γ1, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ m0 :: Γ3 ++ x0 ++ B :: Γ1, Δ0 ++ Δ1). repeat split.
assert (Γ2 ++ m0 :: Γ3 ++ x0 ++ Γ1 = (Γ2 ++ m0 :: Γ3 ++ x0) ++ Γ1). repeat rewrite <- app_assoc.
simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ3 ++ x0 ++ A0 --> B :: Γ1 = (Γ2 ++ m0 :: Γ3 ++ x0) ++ A0 --> B :: Γ1). repeat rewrite <- app_assoc.
simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ3 ++ x0 ++ B :: Γ1 = (Γ2 ++ m0 :: Γ3 ++ x0) ++ B :: Γ1). repeat rewrite <- app_assoc.
simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_LI.
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_LI. }
+ destruct x0.
{ simpl in e1. inversion e1. subst. right. exists A0. exists B.
exists (Γ2 ++ x ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ B :: x ++ Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ x ++ B :: Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: x ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ2 ++ x ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: x ++ Γ4, Δ0 ++ Δ1). repeat split.
repeat rewrite <- app_assoc. apply ImpLRule_I. repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI. rewrite <- app_assoc. simpl. apply ImpLRule_I. }
{ inversion e1. subst. left. exists (Γ2 ++ m :: x ++ x0 ++ Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ m :: x ++ B :: x0 ++ Γ4, Δ0 ++ Δ1). repeat split.
assert (Γ2 ++ m :: x ++ x0 ++ Γ4 = (Γ2 ++ m :: x) ++ x0 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m :: x ++ B :: x0 ++ Γ4 = (Γ2 ++ m :: x) ++ B :: x0 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m :: (x ++ A0 --> B :: x0) ++ Γ4 = (Γ2 ++ m :: x) ++ A0 --> B :: x0 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ m :: x) ++ x0 ++ m :: Γ4 = Γ2 ++ m :: (x ++ x0) ++ m :: Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m :: x ++ x0 ++ Γ4 = Γ2 ++ m :: (x ++ x0) ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_LI.
assert ((Γ2 ++ m :: x) ++ B :: x0 ++ m :: Γ4 = Γ2 ++ m :: (x ++ B :: x0) ++ m :: Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m :: x ++ B :: x0 ++ Γ4 = Γ2 ++ m :: (x ++ B :: x0) ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_LI. }
- destruct x.
+ simpl in e0. inversion e0. subst. right. exists A0. exists B.
exists (Γ0 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ0 ++ Γ3 ++ B :: Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ0 ++ B :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ0 ++ B :: Γ3 ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ0 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ0 ++ B :: Γ3 ++ Γ4, Δ0 ++ Δ1) . repeat split.
assert (Γ0 ++ Γ3 ++ Γ4 = (Γ0 ++ Γ3) ++ Γ4). repeat rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ0 ++ Γ3 ++ B :: Γ4 = (Γ0 ++ Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Γ0 ++ Γ3 ++ A0 --> B :: Γ4 = (Γ0 ++ Γ3) ++ A0 --> B :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Γ0 ++ B :: Γ3 ++ Γ4 = (Γ0 ++ B :: Γ3) ++ Γ4). rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ0 ++ B :: Γ3 ++ B :: Γ4 = (Γ0 ++ B :: Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Γ0 ++ B :: Γ3 ++ A0 --> B :: Γ4 = (Γ0 ++ B :: Γ3) ++ A0 --> B :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI. repeat rewrite <- app_assoc. simpl. apply ImpLRule_I.
+ inversion e0. subst. left. exists (Γ0 ++ x ++ A :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ0 ++ B :: x ++ A :: Γ3 ++ Γ4, Δ0 ++ Δ1). repeat split. repeat rewrite <- app_assoc.
apply ImpLRule_I.
assert (Γ0 ++ x ++ A :: Γ3 ++ A :: Γ4 = (Γ0 ++ x) ++ A :: Γ3 ++ A :: Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ A :: Γ3 ++ Γ4 = (Γ0 ++ x) ++ A :: Γ3 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_LI.
assert (Γ0 ++ B :: x ++ A :: Γ3 ++ A :: Γ4 = (Γ0 ++ B :: x) ++ A :: Γ3 ++ A :: Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ A :: Γ3 ++ Γ4 = (Γ0 ++ B :: x) ++ A :: Γ3 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_LI.
Qed.
Lemma KR_app_ctr_L : forall s sc A ps,
(@ctr_L A s sc) ->
(KRRule [ps] s) ->
((KRRule [ps] sc) +
(existsT2 psc, (KRRule [psc] sc) * (@ctr_L (unBox_formula A) ps psc))).
Proof.
intros s sc A ps ctr RA. inversion RA. inversion ctr. rewrite <- H1 in H2.
inversion H2. subst. apply univ_gen_ext_elem_deep with (l3:=Γ1) (l4:=Γ2 ++ A :: Γ3) (a:=A) in X.
destruct X. 3: reflexivity.
- destruct p. apply univ_gen_ext_elem_deep with (l3:=Γ1 ++ Γ2) (l4:=Γ3) (a:=A) in u. destruct u. destruct p.
3: rewrite <- app_assoc. 3: reflexivity.
* left. apply KRRule_I.
assumption.
apply univ_gen_ext_add_elem_deep. rewrite app_assoc. assumption. assumption.
* exfalso. apply f. repeat destruct s. repeat destruct p. subst. apply is_box_is_in_boxed_list with (A:=A) in H0 .
unfold is_boxedT. destruct H0. exists x1. auto. apply in_or_app. right. apply in_eq.
- repeat destruct s. repeat destruct p. apply univ_gen_ext_elem_deep with (l3:=Γ2) (l4:=Γ3) (a:=A) in u0.
destruct u0. 3: reflexivity.
* destruct p. exfalso. subst. apply is_box_is_in_boxed_list with (A:=A) in H0. apply f. unfold is_boxedT.
destruct H0. exists x1. auto. apply in_or_app. right. apply in_eq.
* repeat destruct s. repeat destruct p. right. subst.
exists (unboxed_list (x ++ A :: x1 ++ x2), [A0]). split.
{ apply KRRule_I.
intro. intros. apply H0. apply in_app_or in H. destruct H. apply in_or_app. left. assumption.
inversion H. subst. apply in_or_app. right. apply in_eq. apply in_app_or in H1. destruct H1.
apply in_or_app. right. apply in_cons. apply in_or_app. left. assumption.
apply in_or_app. right. apply in_cons. apply in_or_app. right. apply in_cons.
assumption.
apply univ_gen_ext_combine. assumption. apply univ_gen_ext_cons. apply univ_gen_ext_combine.
assumption. assumption. }
{ repeat rewrite cons_single. repeat rewrite unbox_app_distrib. simpl. apply ctr_LI. }
Qed.
Lemma ImpR_app_ctr_R : forall s sc A ps,
(@ctr_R A s sc) ->
(ImpRRule [ps] s) ->
((existsT2 psc, (ImpRRule [psc] sc) * (@ctr_R A ps psc))
+
(existsT2 B C invps invpsc0 invpsc, (A = Imp B C) * (ImpRRule [invps] ps) * (ImpRRule [invpsc] sc) *
(@ctr_L B invps invpsc0) * (@ctr_R C invpsc0 invpsc))).
Proof.
intros s sc A ps ctr RA. inversion RA. inversion ctr. subst.
inversion H. subst. apply app2_find_hole in H2. destruct H2. repeat destruct s ; destruct p ; subst.
- inversion e0. right. exists A0. exists B. exists (Γ0 ++ A0 :: A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ Δ4).
repeat split. assert (Δ2 ++ B :: Δ3 ++ B :: Δ4 = (Δ2 ++ B :: Δ3) ++ B :: Δ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Δ2 ++ B :: Δ3 ++ A0 --> B :: Δ4 = (Δ2 ++ B :: Δ3) ++ A0 --> B :: Δ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI.
- destruct x.
* simpl in e0. inversion e0. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, (Δ2 ++ []) ++ B :: Δ3 ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, (Δ2 ++ []) ++ B :: Δ3 ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, (Δ2 ++ []) ++ B :: Δ3 ++ Δ4).
repeat split. assert ((Δ2 ++ []) ++ B :: Δ3 ++ B :: Δ4 = (Δ2 ++ B :: Δ3) ++ B :: Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. assert ((Δ2 ++ []) ++ B :: Δ3 ++ A0 --> B :: Δ4 = (Δ2 ++ B :: Δ3) ++ A0 --> B :: Δ4).
rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpRRule_I. repeat rewrite <- app_assoc. simpl. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI.
* inversion e0. subst. apply app2_find_hole in H2. destruct H2. repeat destruct s ; destruct p ; subst.
+ inversion e1. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ Δ4). repeat split.
repeat rewrite <- app_assoc. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI.
+ destruct x0.
{ simpl in e1. inversion e1. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ1). exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ1).
exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ Δ1). repeat split.
repeat rewrite <- app_assoc. simpl. rewrite app_nil_r. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI. }
{ inversion e1. subst. left. exists (Γ0 ++ A0 :: Γ1, Δ2 ++ m0 :: Δ3 ++ x0 ++ B :: Δ1).
repeat split. assert (Δ2 ++ m0 :: Δ3 ++ x0 ++ B :: Δ1 = (Δ2 ++ m0 :: Δ3 ++ x0) ++ B :: Δ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ m0 :: Δ3 ++ x0 ++ A0 --> B :: Δ1 = (Δ2 ++ m0 :: Δ3 ++ x0) ++ A0 --> B :: Δ1). repeat rewrite <- app_assoc.
simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpRRule_I.
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_RI. }
+ destruct x0.
{ simpl in e1. inversion e1. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, Δ2 ++ B :: x ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: x ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: x ++ Δ4). repeat split.
repeat rewrite <- app_assoc. apply ImpRRule_I. repeat rewrite <- app_assoc. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI. }
{ inversion e1. subst. left. exists (Γ0 ++ A0 :: Γ1, Δ2 ++ m :: x ++ B :: x0 ++ Δ4).
repeat split.
assert (Δ2 ++ m :: x ++ B :: x0 ++ Δ4 = (Δ2 ++ m :: x) ++ B :: x0 ++ Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ m :: (x ++ A0 --> B :: x0) ++ Δ4 = (Δ2 ++ m :: x) ++ A0 --> B :: x0 ++ Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpRRule_I.
assert ((Δ2 ++ m :: x) ++ B :: x0 ++ m :: Δ4 = Δ2 ++ m :: (x ++ B :: x0) ++ m :: Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ m :: x ++ B :: x0 ++ Δ4 = Δ2 ++ m :: (x ++ B :: x0) ++ Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_RI. }
- destruct x.
+ simpl in e0. inversion e0. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, Δ0 ++ B :: Δ3 ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, Δ0 ++ B :: Δ3 ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, Δ0 ++ B :: Δ3 ++ Δ4). repeat split.
assert (Δ0 ++ B :: Δ3 ++ A0 --> B :: Δ4 = (Δ0 ++ B :: Δ3) ++ A0 --> B :: Δ4). repeat rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Δ0 ++ B :: Δ3 ++ B :: Δ4 = (Δ0 ++ B :: Δ3) ++ B :: Δ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply ImpRRule_I. repeat rewrite <- app_assoc. simpl. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI.
+ inversion e0. subst. left. exists (Γ0 ++ A0 :: Γ1, Δ0 ++ B :: x ++ A :: Δ3 ++ Δ4).
repeat split. repeat rewrite <- app_assoc. apply ImpRRule_I.
assert (Δ0 ++ B :: x ++ A :: Δ3 ++ A :: Δ4 = (Δ0 ++ B :: x) ++ A :: Δ3 ++ A :: Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ B :: x ++ A :: Δ3 ++ Δ4 = (Δ0 ++ B :: x) ++ A :: Δ3 ++ Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_RI.
Qed.
Lemma ImpL_app_ctr_R : forall s sc A ps1 ps2,
(@ctr_R A s sc) ->
(ImpLRule [ps1;ps2] s) ->
(existsT2 psc1 psc2, (ImpLRule [psc1;psc2] sc) * (@ctr_R A ps1 psc1) * (@ctr_R A ps2 psc2)).
Proof.
intros s sc A ps1 ps2 ctr RA. inversion RA. inversion ctr. subst.
inversion H. subst. apply app2_find_hole in H2. destruct H2. destruct s.
- destruct s.
+ destruct p. subst. exists (Γ0 ++ Γ1, Δ2 ++ A0 :: A :: Δ3 ++ Δ4). exists (Γ0 ++ B :: Γ1, Δ2 ++ A :: Δ3 ++ Δ4).
split. split.
apply ImpLRule_I.
assert (E1: Δ2 ++ A0 :: A :: Δ3 ++ A :: Δ4 = (Δ2 ++ [A0]) ++ A :: Δ3 ++ A :: Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E1.
assert (E2: Δ2 ++ A0 :: A :: Δ3 ++ Δ4 = (Δ2 ++ [A0]) ++ A :: Δ3 ++ Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E2. apply ctr_RI.
apply ctr_RI.
+ destruct p. destruct x.
* rewrite app_nil_r in e. rewrite app_nil_l in e0. subst.
exists (Γ0 ++ Γ1, Δ2 ++ A0 :: A :: Δ3 ++ Δ4). exists (Γ0 ++ B :: Γ1, Δ2 ++ A :: Δ3 ++ Δ4).
split. split.
apply ImpLRule_I.
assert (E1: Δ2 ++ A0 :: A :: Δ3 ++ A :: Δ4 = (Δ2 ++ [A0]) ++ A :: Δ3 ++ A :: Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E1.
assert (E2: Δ2 ++ A0 :: A :: Δ3 ++ Δ4 = (Δ2 ++ [A0]) ++ A :: Δ3 ++ Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E2. apply ctr_RI.
apply ctr_RI.
* inversion e0. subst. apply app2_find_hole in H2. destruct H2. destruct s.
{ destruct s.
- destruct p. subst. exists (Γ0 ++ Γ1, (Δ2 ++ m :: Δ3) ++ A0 :: Δ4).
exists (Γ0 ++ B :: Γ1, (Δ2 ++ m :: Δ3) ++ Δ4). split. split.
assert (E: Δ2 ++ m :: Δ3 ++ Δ4 = (Δ2 ++ m :: Δ3) ++ Δ4).
rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpLRule_I.
assert (E1: (Δ2 ++ m :: Δ3) ++ A0 :: m :: Δ4 = Δ2 ++ m :: (Δ3 ++ [A0]) ++ m :: Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E1.
assert (E2: (Δ2 ++ m :: Δ3) ++ A0 :: Δ4 = Δ2 ++ m :: (Δ3 ++ [A0]) ++ Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E2. apply ctr_RI.
rewrite <- app_assoc. simpl. apply ctr_RI.
- destruct p. subst. destruct x0.
+ rewrite app_nil_l in e1. rewrite app_nil_r in e0. subst.
exists (Γ0 ++ Γ1,(Δ2 ++ m :: Δ3) ++ A0 :: Δ4). exists (Γ0 ++ B :: Γ1, (Δ2 ++ m :: Δ3) ++ Δ4).
split. split.
assert (E: Δ2 ++ m :: Δ3 ++ Δ4 = (Δ2 ++ m :: Δ3) ++ Δ4).
rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpLRule_I.
assert (E1: (Δ2 ++ m :: Δ3 ++ []) ++ A0 :: m :: Δ4 = Δ2 ++ m :: (Δ3 ++ [A0]) ++ m :: Δ4).
rewrite app_nil_r. repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E1.
assert (E2: (Δ2 ++ m :: Δ3) ++ A0 :: Δ4 = Δ2 ++ m :: (Δ3 ++ [A0]) ++ Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E2. apply ctr_RI.
rewrite <- app_assoc. simpl. apply ctr_RI.
+ inversion e1. subst. exists (Γ0 ++ Γ1,(Δ2 ++ m0 :: Δ3 ++ x0) ++ A0 :: Δ1).
exists (Γ0 ++ B :: Γ1,(Δ2 ++ m0 :: Δ3 ++ x0) ++ Δ1). split. split.
assert (E: Δ2 ++ m0 :: Δ3 ++ x0 ++ Δ1 = (Δ2 ++ m0 :: Δ3 ++ x0) ++ Δ1).
rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpLRule_I.
assert (E1: (Δ2 ++ m0 :: Δ3 ++ m0 :: x0) ++ A0 :: Δ1 = Δ2 ++ m0 :: Δ3 ++ m0 :: x0 ++ A0 :: Δ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Δ2 ++ m0 :: Δ3 ++ x0) ++ A0 :: Δ1 = Δ2 ++ m0 :: Δ3 ++ x0 ++ A0 :: Δ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E2. apply ctr_RI.
rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_RI. }
{ destruct p. subst. exists (Γ0 ++ Γ1,(Δ2 ++ m :: x) ++ A0 :: x0 ++ Δ4).
exists (Γ0 ++ B :: Γ1, (Δ2 ++ m :: x) ++ x0 ++ Δ4). split. split.
assert (E: Δ2 ++ m :: (x ++ x0) ++ Δ4 = (Δ2 ++ m :: x) ++ x0 ++ Δ4).
rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpLRule_I.
assert (E1: (Δ2 ++ m :: x) ++ A0 :: x0 ++ m :: Δ4 = Δ2 ++ m :: (x ++ A0 :: x0) ++ m :: Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Δ2 ++ m :: x) ++ A0 :: x0 ++ Δ4 = Δ2 ++ m :: (x ++ A0 :: x0) ++ Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E2. apply ctr_RI.
assert (E1: (Δ2 ++ m :: x) ++ x0 ++ Δ4 = Δ2 ++ m :: (x ++ x0) ++ Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E1. apply ctr_RI. }
- destruct p. subst. exists (Γ0 ++ Γ1, Δ0 ++ A0 :: x ++ A :: Δ3 ++ Δ4).
exists (Γ0 ++ B :: Γ1, Δ0 ++ x ++ A :: Δ3 ++ Δ4). split. split.
rewrite <- app_assoc. apply ImpLRule_I.
assert (E1: Δ0 ++ A0 :: x ++ A :: Δ3 ++ A :: Δ4 = (Δ0 ++ A0 :: x) ++ A :: Δ3 ++ A :: Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: Δ0 ++ A0 :: x ++ A :: Δ3 ++ Δ4 = (Δ0 ++ A0 :: x) ++ A :: Δ3 ++ Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E2. apply ctr_RI.
rewrite app_assoc. apply ctr_RI.
Qed.
Lemma KR_app_ctr_R : forall s sc A ps,
(@ctr_R A s sc) -> (KRRule [ps] s) -> (KRRule [ps] sc).
Proof.
intros s sc A ps ctr RA. inversion RA. inversion ctr. rewrite <- H1 in H2.
inversion H2. apply app2_find_hole in H6. destruct H6. destruct s0.
+ destruct s0.
* destruct p. inversion e0. apply KRRule_I. assumption. assumption.
* destruct p. subst. destruct x.
{ rewrite app_nil_l in e0. inversion e0. subst. apply KRRule_I.
assumption. assumption. }
{ inversion e0. subst. apply app2_find_hole in H3. destruct H3. destruct s.
- destruct s.
+ destruct p. inversion e1. apply KRRule_I. assumption. assumption.
+ destruct p. subst. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst. apply KRRule_I. assumption.
assumption.
* inversion e1. subst. assert (E: Δ2 ++ m0 :: Δ3 ++ x0 ++ Box A0 :: Δ1 = (Δ2 ++ m0 :: Δ3 ++ x0) ++ Box A0 :: Δ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E. apply KRRule_I. assumption.
assumption.
- destruct p. subst. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst. apply KRRule_I. assumption. assumption.
* inversion e1. subst. assert (E: Δ2 ++ m :: (x ++ Box A0 :: x0) ++ Δ4 = (Δ2 ++ m :: x) ++ Box A0 :: x0 ++ Δ4).
repeat rewrite <- app_assoc. reflexivity. rewrite E. apply KRRule_I. assumption. assumption. }
+ destruct p. subst. destruct x.
* rewrite app_nil_l in e0. rewrite app_nil_r. inversion e0. subst. apply KRRule_I. assumption. assumption.
* inversion e0. rewrite <- app_assoc. simpl. apply KRRule_I. assumption. assumption.
Qed.
(* Now we can prove that contraction rules are height-preserving admissible. *)
Theorem KS_hpadm_ctr_LR0 : forall (k : nat) s
(D0 : KS_prv s),
k = (derrec_height D0) ->
(forall sc A, (((@ctr_L A s sc) + (@ctr_R A s sc)) ->
existsT2 (D1 : KS_prv sc),
derrec_height D1 <= k)).
Proof.
induction k as [n IH] using (well_founded_induction_type lt_wf).
intros s D0. remember D0 as D0'. destruct D0.
(* D0 ip a leaf *)
- intros hei sc A ctr. inversion f.
(* D0 is ends with an application of rule *)
- intros hei sc A ctr. destruct ctr as [ctr | ctr].
{ inversion ctr. assert (DersNil: dersrec KS_rules (fun _ : Seq => False) []).
apply dersrec_nil. inversion k.
(* IdP *)
* inversion H1. rewrite <- H in H5. inversion H5.
apply app2_find_hole in H7. destruct H7. destruct s.
+ destruct s.
{ destruct p. inversion e0. subst. pose (IdPRule_I P Γ3 (Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ3 ++ # P :: Γ1 ++ Γ2, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl. repeat rewrite dersrec_height_nil.
left. reflexivity. reflexivity. }
{ destruct p. destruct x.
- rewrite app_nil_l in e0. inversion e0.
subst. pose (IdPRule_I P (Γ3 ++ []) (Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) ((Γ3 ++ []) ++ # P :: Γ1 ++ Γ2,Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- inversion e0. subst.
pose (IdPRule_I P Γ3 (x ++ A :: Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
assert (E: Γ3 ++ # P :: x ++ A :: Γ1 ++ Γ2 = (Γ3 ++ # P :: x) ++ A :: Γ1 ++ Γ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in i. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) ((Γ3 ++ # P :: x) ++ A :: Γ1 ++ Γ2,Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
+ destruct p. destruct x.
{ rewrite app_nil_l in e0. inversion e0. subst.
pose (IdPRule_I P Γ0 (Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1 ++ Γ2, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
{ inversion e0. subst. apply app2_find_hole in H9. destruct H9. destruct s.
- destruct s.
+ destruct p. inversion e1. subst.
pose (IdPRule_I P Γ0 (Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1 ++ Γ2, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ destruct p. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst.
pose (IdPRule_I P Γ0 (Γ1 ++ Γ4) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1 ++ Γ4, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
* inversion e1. subst.
pose (IdPRule_I P (Γ0 ++ m0 :: Γ1 ++ x0) Γ4 Δ0 Δ1). apply IdP in i. simpl in i.
repeat rewrite <- app_assoc in i. simpl in i. repeat rewrite <- app_assoc in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ m0 :: Γ1 ++ x0 ++ # P :: Γ4,Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- destruct p. destruct x0.
+ rewrite app_nil_l in e1. inversion e1. subst.
pose (IdPRule_I P Γ0 ((x ++ []) ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: (x ++ []) ++ Γ2, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ inversion e1. subst.
pose (IdPRule_I P (Γ0 ++ m :: x) (x0 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
assert (E: (Γ0 ++ m :: x) ++ # P :: x0 ++ Γ2 = Γ0 ++ m :: (x ++ # P :: x0) ++ Γ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in i. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ m :: (x ++ # P :: x0) ++ Γ2,Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
(* BotL *)
* inversion H1. rewrite <- H in H5. inversion H5.
apply app2_find_hole in H7. destruct H7. destruct s.
+ destruct s.
{ destruct p. inversion e0. subst. pose (BotLRule_I Γ3 (Γ1 ++ Γ2) Δ). apply BotL in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ3 ++ Bot :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl. repeat rewrite dersrec_height_nil.
left. reflexivity. reflexivity. }
{ destruct p. destruct x.
- rewrite app_nil_l in e0. inversion e0.
subst. pose (BotLRule_I (Γ3 ++ []) (Γ1 ++ Γ2) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) ((Γ3 ++ []) ++ Bot :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- inversion e0. subst.
pose (BotLRule_I Γ3 (x ++ A :: Γ1 ++ Γ2) Δ). apply BotL in b. simpl in b.
assert (E: Γ3 ++ Bot :: x ++ A :: Γ1 ++ Γ2 = (Γ3 ++ Bot :: x) ++ A :: Γ1 ++ Γ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in b. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) ((Γ3 ++ Bot :: x) ++ A :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
+ destruct p. destruct x.
{ rewrite app_nil_l in e0. inversion e0. subst.
pose (BotLRule_I Γ0 (Γ1 ++ Γ2) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
{ inversion e0. subst. apply app2_find_hole in H9. destruct H9. destruct s.
- destruct s.
+ destruct p. inversion e1. subst.
pose (BotLRule_I Γ0 (Γ1 ++ Γ2) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ destruct p. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst.
pose (BotLRule_I Γ0 (Γ1 ++ Γ4) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: Γ1 ++ Γ4, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
* inversion e1. subst.
pose (BotLRule_I (Γ0 ++ m0 :: Γ1 ++ x0) Γ4 Δ). apply BotL in b. simpl in b.
repeat rewrite <- app_assoc in b. simpl in b. repeat rewrite <- app_assoc in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ m0 :: Γ1 ++ x0 ++ Bot :: Γ4, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- destruct p. destruct x0.
+ rewrite app_nil_l in e1. inversion e1. subst.
pose (BotLRule_I Γ0 ((x ++ []) ++ Γ2) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: (x ++ []) ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ inversion e1. subst.
pose (BotLRule_I (Γ0 ++ m :: x) (x0 ++ Γ2) Δ). apply BotL in b. simpl in b.
assert (E: (Γ0 ++ m :: x) ++ Bot :: x0 ++ Γ2 = Γ0 ++ m :: (x ++ Bot :: x0) ++ Γ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in b. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ m :: (x ++ Bot :: x0) ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
(* ImpR *)
* inversion H1. subst. inversion H5. subst. pose (ImpR_app_ctr_L _ _ _ _ ctr H1). destruct s. destruct p.
apply ImpR in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x]) (Γ0 ++ A :: Γ1 ++ Γ2, Δ0 ++ A0 --> B :: Δ1) i). subst. simpl.
remember [(Γ3 ++ A0 :: Γ4, Δ0 ++ B :: Δ1)] as ps'. destruct d. inversion Heqps'.
inversion Heqps'. subst. simpl. rewrite dersrec_height_nil. simpl in IH.
rewrite dersrec_height_nil in IH. rewrite Nat.max_0_r. rewrite Nat.max_0_r in IH.
assert (E: derrec_height d < S (derrec_height d)). auto.
assert (E1: derrec_height d = derrec_height d). auto.
assert ((ctr_L A (Γ3 ++ A0 :: Γ4, Δ0 ++ B :: Δ1) x) + (ctr_R A (Γ3 ++ A0 :: Γ4, Δ0 ++ B :: Δ1) x)).
left. auto.
pose (IH (derrec_height d) E (Γ3 ++ A0 :: Γ4, Δ0 ++ B :: Δ1) d E1 x A H).
destruct s.
pose (dlCons x0 d1). pose (d0 d2). exists d3. simpl. rewrite dersrec_height_nil.
rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. assumption. reflexivity. reflexivity. reflexivity.
(* ImpL *)
* inversion H1. subst. inversion H5. subst. pose (ImpL_app_ctr_L _ _ _ _ _ ctr H1). destruct s.
{ repeat destruct s. repeat destruct p. apply ImpL in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x;x0]) (Γ0 ++ A :: Γ1 ++ Γ2, Δ0 ++ Δ1) i). subst. simpl.
remember [(Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1);(Γ3 ++ B :: Γ4, Δ0 ++ Δ1)] as ps'. destruct d.
inversion Heqps'. inversion Heqps'. subst.
remember [(Γ3 ++ B :: Γ4, Δ0 ++ Δ1)] as ps''. destruct d1. inversion Heqps''.
inversion Heqps''. simpl. subst. rewrite dersrec_height_nil. simpl in IH.
rewrite dersrec_height_nil in IH. rewrite Nat.max_0_r. rewrite Nat.max_0_r in IH.
assert (E1: derrec_height d < S (Init.Nat.max (derrec_height d)(derrec_height d1))).
apply Nat.lt_succ_r. apply Nat.le_max_l.
assert (E2: derrec_height d = derrec_height d). auto.
assert ((ctr_L A (Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1) x) + (ctr_R A (Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1) x)).
auto.
pose (IH (derrec_height d) E1 (Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1) d E2 x A H).
destruct s.
assert (E3: derrec_height d1 < S (Init.Nat.max (derrec_height d)(derrec_height d1))).
apply Nat.lt_succ_r. apply Nat.le_max_r.
assert (E4: derrec_height d1 = derrec_height d1). auto.
assert ((ctr_L A (Γ3 ++ B :: Γ4, Δ0 ++ Δ1) x0) + (ctr_R A (Γ3 ++ B :: Γ4, Δ0 ++ Δ1) x0)).
auto.
pose (IH (derrec_height d1) E3 (Γ3 ++ B :: Γ4, Δ0 ++ Δ1) d1 E4 x0 A H2).
destruct s.
pose (dlCons x1 (dlCons x2 d2)). pose (d0 d3). exists d4. simpl. rewrite dersrec_height_nil.
rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. apply Nat.max_le_compat.
assumption. assumption. reflexivity. reflexivity. reflexivity. }
{ simpl. repeat destruct s. repeat destruct p. subst. apply ImpL in i.
assert (J30: dersrec_height d = dersrec_height d). reflexivity.
pose (@dersrec_derrec2_height (dersrec_height d) _ _ _ _ _ d J30). repeat destruct s.
assert (J1: derrec_height x7 = derrec_height x7). reflexivity.
pose (ImpR_ImpL_hpinv _ _ _ J1). destruct p. clear s. pose (s0 _ _ i1). repeat destruct s.
clear s0. destruct p. simpl in IH.
assert (J2: derrec_height x9 < S (dersrec_height d)). lia.
assert (J3: derrec_height x9 = derrec_height x9). reflexivity.
assert (J4: (ctr_L x x1 x5) + (ctr_R x x1 x5)). auto.
pose (IH _ J2 _ _ J3 _ _ J4). destruct s.
assert (J5: derrec_height x8 = derrec_height x8). reflexivity.
pose (ImpR_ImpL_hpinv _ _ _ J5). destruct p. clear s. pose (s0 _ _ i0). repeat destruct s.
clear s0. destruct p.
assert (J6: derrec_height x13 < S (dersrec_height d)). lia.
assert (J7: derrec_height x13 = derrec_height x13). reflexivity.
assert (J8: (ctr_L x0 x4 x6) + (ctr_R x0 x4 x6)). auto.
pose (IH _ J6 _ _ J7 _ _ J8). destruct s. pose (dlCons x14 DersNil). pose (dlCons x11 d0).
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x5;x6]) (Γ0 ++ x --> x0 :: Γ1 ++ Γ2, Δ0 ++ Δ1) i d1). exists d2. simpl.
rewrite dersrec_height_nil. lia. reflexivity. }
(* KR *)
* inversion X. rewrite <- H4 in X. pose (KR_app_ctr_L _ _ _ _ ctr X). destruct s.
{ apply KR in k0. pose (derI (rules:=KS_rules)
(prems:=fun _ : Seq => False) (ps:=[(unboxed_list BΓ, [A0])])
sc k0). subst. pose (d0 d). exists d1. simpl. reflexivity. }
{ repeat destruct s. repeat destruct p. apply KR in k0.
remember [(unboxed_list BΓ, [A0])] as ps'. destruct d. subst. inversion H4.
rewrite Heqps' in H4. inversion H4. subst. simpl. simpl in IH.
assert (E1: derrec_height d < S (Init.Nat.max (derrec_height d) (dersrec_height d0))).
rewrite dersrec_height_nil. rewrite Nat.max_0_r. apply Nat.lt_succ_r. left. reflexivity.
assert (E2: derrec_height d = derrec_height d). auto.
assert ((ctr_L (unBox_formula A) (unboxed_list BΓ, [A0]) x) +
(ctr_R (unBox_formula A) (unboxed_list BΓ, [A0]) x)). auto.
pose (IH (derrec_height d) E1 ((unboxed_list BΓ, [A0])) d E2 x (unBox_formula A) H).
destruct s.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x]) (Γ0 ++ A :: Γ1 ++ Γ2, Δ) k0). subst. simpl.
pose (dlCons x0 d0). pose (d1 d2). exists d3. simpl. rewrite dersrec_height_nil.
repeat rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. lia. auto. }}
{ inversion ctr. assert (DersNil: dersrec KS_rules (fun _ : Seq => False) []).
apply dersrec_nil. inversion k.
(* IdP *)
* inversion H1. rewrite <- H in H5. inversion H5.
apply app2_find_hole in H8. destruct H8. destruct s.
+ destruct s.
{ destruct p. inversion e0. subst. pose (IdPRule_I P Γ0 Γ1 Δ3 (Δ1 ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ3 ++ # P :: Δ1 ++ Δ2) i DersNil). exists d0. simpl. repeat rewrite dersrec_height_nil.
left. reflexivity. reflexivity. }
{ destruct p. destruct x.
- rewrite app_nil_l in e0. inversion e0.
subst. pose (IdPRule_I P Γ0 Γ1 (Δ3 ++ []) (Δ1 ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, (Δ3 ++ []) ++ # P :: Δ1 ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- inversion e0. subst.
pose (IdPRule_I P Γ0 Γ1 Δ3 (x ++ A :: Δ1 ++ Δ2)). apply IdP in i. simpl in i.
assert (E: Δ3 ++ # P :: x ++ A :: Δ1 ++ Δ2 = (Δ3 ++ # P :: x) ++ A :: Δ1 ++ Δ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in i. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, (Δ3 ++ # P :: x) ++ A :: Δ1 ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
+ destruct p. destruct x.
{ rewrite app_nil_l in e0. inversion e0. subst.
pose (IdPRule_I P Γ0 Γ1 Δ0 (Δ1 ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ # P :: Δ1 ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
{ inversion e0. subst. apply app2_find_hole in H9. destruct H9. destruct s.
- destruct s.
+ destruct p. inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 Δ0 (Δ1 ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ # P :: Δ1 ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ destruct p. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 Δ0 (Δ1 ++ Δ4)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ # P :: Δ1 ++ Δ4) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
* inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 (Δ0 ++ m0 :: Δ1 ++ x0) Δ4). apply IdP in i. simpl in i.
repeat rewrite <- app_assoc in i. simpl in i. repeat rewrite <- app_assoc in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ m0 :: Δ1 ++ x0 ++ # P :: Δ4) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- destruct p. destruct x0.
+ rewrite app_nil_l in e1. inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 Δ0 ((x ++ []) ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ # P :: (x ++ []) ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 (Δ0 ++ m :: x) (x0 ++ Δ2)). apply IdP in i. simpl in i.
assert (E: (Δ0 ++ m :: x) ++ # P :: x0 ++ Δ2 = Δ0 ++ m :: (x ++ # P :: x0) ++ Δ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in i. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ m :: (x ++ # P :: x0) ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
(* BotL *)
* inversion H1. rewrite <- H in H5. inversion H5.
pose (BotLRule_I Γ0 Γ1 (Δ0 ++ A :: Δ1 ++ Δ2)). apply BotL in b.
pose (derI (rules:=KS_rules)
(prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: Γ1, Δ0 ++ A :: Δ1 ++ Δ2) b DersNil). subst. exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
(* ImpR *)
* inversion H1. subst. inversion H5. subst. pose (ImpR_app_ctr_R _ _ _ _ ctr H1). destruct s.
{ destruct s. destruct p. apply ImpR in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x]) (Γ0 ++ Γ1, Δ0 ++ A :: Δ1 ++ Δ2) i). subst. simpl.
remember [(Γ0 ++ A0 :: Γ1, Δ3 ++ B :: Δ4)] as ps'. destruct d. inversion Heqps'.
inversion Heqps'. subst. simpl. rewrite dersrec_height_nil. simpl in IH.
rewrite dersrec_height_nil in IH. rewrite Nat.max_0_r. rewrite Nat.max_0_r in IH.
assert (E: derrec_height d < S (derrec_height d)). auto.
assert (E1: derrec_height d = derrec_height d). auto.
assert ((ctr_L A (Γ0 ++ A0 :: Γ1, Δ3 ++ B :: Δ4) x) + (ctr_R A (Γ0 ++ A0 :: Γ1, Δ3 ++ B :: Δ4) x)).
auto.
pose (IH (derrec_height d) E (Γ0 ++ A0 :: Γ1, Δ3 ++ B :: Δ4) d E1 x A H).
destruct s.
pose (dlCons x0 d1). pose (d0 d2). exists d3. simpl. rewrite dersrec_height_nil.
rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. assumption. reflexivity. reflexivity. reflexivity. }
{ repeat destruct s. repeat destruct p. subst. apply ImpR in i.
assert (J30: dersrec_height d = dersrec_height d). reflexivity.
pose (dersrec_derrec_height d J30). destruct s.
assert (J1: derrec_height x4 = derrec_height x4). reflexivity.
pose (ImpR_ImpL_hpinv _ _ _ J1). destruct p. clear s0. pose (s _ i0). repeat destruct s0.
clear s. simpl in IH.
assert (J2: derrec_height x5 < S (dersrec_height d)). lia.
assert (J3: derrec_height x5 = derrec_height x5). reflexivity.
assert (J4: (ctr_L x x1 x2) + (ctr_R x x1 x2)). auto.
pose (IH _ J2 _ _ J3 _ _ J4). destruct s.
assert (J5: derrec_height x6 = derrec_height x6). reflexivity.
assert (J6: derrec_height x6 < S (dersrec_height d)). lia.
assert (J8: (ctr_L x0 x2 x3) + (ctr_R x0 x2 x3)). auto.
pose (IH _ J6 _ _ J5 _ _ J8). destruct s. pose (dlCons x7 DersNil).
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x3]) (Γ0 ++ Γ1, Δ0 ++ x --> x0 :: Δ1 ++ Δ2) i d0). simpl. exists d1. simpl. rewrite dersrec_height_nil.
lia. reflexivity. }
(* ImpL *)
* inversion H1. subst. inversion H5. subst. pose (ImpL_app_ctr_R _ _ _ _ _ ctr H1). destruct s.
repeat destruct s. repeat destruct p. apply ImpL in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x;x0]) (Γ0 ++ A0 --> B :: Γ1, Δ0 ++ A :: Δ1 ++ Δ2) i). subst. simpl.
remember [(Γ0 ++ Γ1, Δ3 ++ A0 :: Δ4);(Γ0 ++ B :: Γ1, Δ3 ++ Δ4)] as ps'. destruct d.
inversion Heqps'. inversion Heqps'. subst.
remember [(Γ0 ++ B :: Γ1, Δ3 ++ Δ4)] as ps''. destruct d1. inversion Heqps''.
inversion Heqps''. simpl. subst. rewrite dersrec_height_nil. simpl in IH.
rewrite dersrec_height_nil in IH. rewrite Nat.max_0_r. rewrite Nat.max_0_r in IH.
assert (E1: derrec_height d < S (Init.Nat.max (derrec_height d)(derrec_height d1))).
apply Nat.lt_succ_r. apply Nat.le_max_l.
assert (E2: derrec_height d = derrec_height d). auto.
assert ((ctr_L A (Γ0 ++ Γ1, Δ3 ++ A0 :: Δ4) x) + (ctr_R A (Γ0 ++ Γ1, Δ3 ++ A0 :: Δ4) x)).
auto.
pose (IH (derrec_height d) E1 (Γ0 ++ Γ1, Δ3 ++ A0 :: Δ4) d E2 x A H).
destruct s.
assert (E3: derrec_height d1 < S (Init.Nat.max (derrec_height d)(derrec_height d1))).
apply Nat.lt_succ_r. apply Nat.le_max_r.
assert (E4: derrec_height d1 = derrec_height d1). auto.
assert ((ctr_L A (Γ0 ++ B :: Γ1, Δ3 ++ Δ4) x0) + (ctr_R A (Γ0 ++ B :: Γ1, Δ3 ++ Δ4) x0)).
auto.
pose (IH (derrec_height d1) E3 (Γ0 ++ B :: Γ1, Δ3 ++ Δ4) d1 E4 x0 A H0).
destruct s.
pose (dlCons x1 (dlCons x2 d2)). pose (d0 d3). exists d4. simpl. rewrite dersrec_height_nil.
rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. apply Nat.max_le_compat.
assumption. assumption. reflexivity. reflexivity. reflexivity.
(* KR *)
* inversion X. rewrite <- H4 in X. pose (KR_app_ctr_R _ _ _ _ ctr X).
apply KR in k0.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[(unboxed_list BΓ, [A0])]) sc k0). subst. simpl. pose (d0 d). exists d1.
simpl. rewrite <- Nat.succ_le_mono. left. }
Qed.
Theorem KS_hpadm_ctr_LR : forall s (D0 : KS_prv s),
(forall sc A, ((ctr_L A s sc) + (ctr_R A s sc)) ->
existsT2 (D1 : KS_prv sc),
derrec_height D1 <= derrec_height D0).
Proof.
intros.
assert (J0: derrec_height D0 = derrec_height D0). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) _ D0 J0 _ _ H).
auto.
Qed.
Theorem KS_hpadm_ctr_L : forall (k : nat) s
(D0 : KS_prv s),
k = (derrec_height D0) ->
(forall sc A, ((@ctr_L A s sc) ->
existsT2 (D1 : KS_prv sc),
derrec_height D1 <= k)).
Proof.
intros. intros. assert (H1: derrec_height D0 = derrec_height D0). reflexivity.
assert (H3 : (ctr_L A s sc) + (ctr_R A s sc)). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) s
D0 H1 sc A H3). destruct s0. exists x. lia.
Qed.
Theorem KS_hpadm_ctr_R : forall (k : nat) s
(D0 : KS_prv s),
k = (derrec_height D0) ->
(forall sc A, ((@ctr_R A s sc) ->
existsT2 (D1 : KS_prv sc),
derrec_height D1 <= k)).
Proof.
intros. intros. assert (H1: derrec_height D0 = derrec_height D0). reflexivity.
assert (H3 : (ctr_L A s sc) + (ctr_R A s sc)). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) s
D0 H1 sc A H3). destruct s0. exists x. lia.
Qed.
(* We can now prove that contraction of lists is also admissible. *)
Theorem KS_hpadm_list_ctr_L : forall Γ1 (k : nat) Γ0 Γ2 Γ3 Δ
(D0 : KS_prv (Γ0 ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3,Δ)),
k = (derrec_height D0) ->
existsT2 (D1 : KS_prv (Γ0 ++ Γ1 ++ Γ2 ++ Γ3,Δ)),
derrec_height D1 <= k.
Proof.
induction Γ1.
- intros. exists D0. rewrite H. auto.
- intros. assert (H0: derrec_height D0 = derrec_height D0). reflexivity.
assert (H1 : ctr_L a (Γ0 ++ (a :: Γ1) ++ Γ2 ++ (a :: Γ1) ++ Γ3, Δ) ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3, Δ)).
simpl. assert (Γ0 ++ a :: Γ1 ++ Γ2 ++ a :: Γ1 ++ Γ3 = Γ0 ++ a :: (Γ1 ++ Γ2) ++ a :: (Γ1 ++ Γ3)).
repeat rewrite <- app_assoc. reflexivity. rewrite H1.
assert ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3 = Γ0 ++ a :: (Γ1 ++ Γ2) ++ Γ1 ++ Γ3). repeat rewrite <- app_assoc.
reflexivity. rewrite H2. apply ctr_LI.
assert ((ctr_L a (Γ0 ++ (a :: Γ1) ++ Γ2 ++ (a :: Γ1) ++ Γ3, Δ) ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3, Δ)) +
(ctr_R a (Γ0 ++ (a :: Γ1) ++ Γ2 ++ (a :: Γ1) ++ Γ3, Δ) ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3, Δ))). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) (Γ0 ++ (a :: Γ1) ++ Γ2 ++ (a :: Γ1) ++ Γ3, Δ)
D0 H0 ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3, Δ) a H2). destruct s.
assert (H3: derrec_height x = derrec_height x). reflexivity.
pose (IHΓ1 (derrec_height x) (Γ0 ++ [a]) Γ2 Γ3 Δ x H3). destruct s.
assert (Γ0 ++ (a :: Γ1) ++ Γ2 ++ Γ3 = (Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ3). repeat rewrite <- app_assoc. auto.
rewrite H4. exists x0. lia.
Qed.
Theorem KS_hpadm_list_ctr_R : forall Δ1 (k : nat) Γ Δ0 Δ2 Δ3
(D0 : KS_prv (Γ,Δ0 ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3)),
k = (derrec_height D0) ->
existsT2 (D1 : KS_prv (Γ,Δ0 ++ Δ1 ++ Δ2 ++ Δ3)),
derrec_height D1 <= k.
Proof.
induction Δ1.
- intros. exists D0. rewrite H. auto.
- intros. assert (H0: derrec_height D0 = derrec_height D0). reflexivity.
assert (H1 : ctr_R a (Γ, Δ0 ++ (a :: Δ1) ++ Δ2 ++ (a :: Δ1) ++ Δ3) (Γ, (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3)).
simpl. assert (Δ0 ++ a :: Δ1 ++ Δ2 ++ a :: Δ1 ++ Δ3 = Δ0 ++ a :: (Δ1 ++ Δ2) ++ a :: (Δ1 ++ Δ3)).
repeat rewrite <- app_assoc. reflexivity. rewrite H1.
assert ((Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3 = Δ0 ++ a :: (Δ1 ++ Δ2) ++ Δ1 ++ Δ3). repeat rewrite <- app_assoc.
reflexivity. rewrite H2. apply ctr_RI.
assert ((ctr_L a (Γ, Δ0 ++ (a :: Δ1) ++ Δ2 ++ (a :: Δ1) ++ Δ3) (Γ, (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3)) +
(ctr_R a (Γ, Δ0 ++ (a :: Δ1) ++ Δ2 ++ (a :: Δ1) ++ Δ3) (Γ, (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3))). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) (Γ, Δ0 ++ (a :: Δ1) ++ Δ2 ++ (a :: Δ1) ++ Δ3)
D0 H0 (Γ, (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3) a H2). destruct s.
assert (H3: derrec_height x = derrec_height x). reflexivity.
pose (IHΔ1 (derrec_height x) Γ (Δ0 ++ [a]) Δ2 Δ3 x H3). destruct s.
assert (Δ0 ++ (a :: Δ1) ++ Δ2 ++ Δ3 = (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ3). repeat rewrite <- app_assoc. auto.
rewrite H4. exists x0. lia.
Qed.
Export ListNotations.
Require Import Lia.
Require Import PeanoNat Arith.
Require Import KS_calc.
Require Import KS_inv_ImpR_ImpL.
(* Next are the definitions for contraction of one formula on the left, and
on the right. Note that while the leftmost occurrence of the formula is kept,
if we have exchange for our calculus it amounts to the same to keep the rightmost
formula. *)
Inductive ctr_L (fml : MPropF) : relationT Seq :=
| ctr_LI Γ0 Γ1 Γ2 Δ : ctr_L fml
(Γ0 ++ fml :: Γ1 ++ fml :: Γ2, Δ) (Γ0 ++ fml :: Γ1 ++ Γ2, Δ).
Inductive ctr_R (fml : MPropF) : relationT Seq :=
| ctr_RI Γ Δ0 Δ1 Δ2 : ctr_R fml
(Γ, Δ0 ++ fml :: Δ1 ++ fml :: Δ2) (Γ, Δ0 ++ fml :: Δ1 ++ Δ2).
(* The following lemmas make sure that if a rule is applied on a sequent s with
premises ps, then the same rule is applicable on a sequent sc which is a contracted
version of s, with some premises psc that are such that they are either the same premises
(in case the contracted formula was weakened) or contracted versions of ps. *)
Lemma ImpR_app_ctr_L : forall s sc A ps,
(@ctr_L A s sc) ->
(ImpRRule [ps] s) ->
(existsT2 psc, (ImpRRule [psc] sc) * (@ctr_L A ps psc)).
Proof.
intros s sc A ps ctr RA. inversion RA. inversion ctr. subst.
inversion H. subst. apply app2_find_hole in H1. destruct H1. destruct s.
- destruct s.
+ destruct p. subst. exists (Γ2 ++ A0 :: A :: Γ3 ++ Γ4, Δ0 ++ B :: Δ1).
split. apply ImpRRule_I.
assert (E1: Γ2 ++ A0 :: A :: Γ3 ++ A :: Γ4 = (Γ2 ++ [A0]) ++ A :: Γ3 ++ A :: Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: Γ2 ++ A0 :: A :: Γ3 ++ Γ4 = (Γ2 ++ [A0]) ++ A :: Γ3 ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
+ destruct p. subst. destruct x.
* simpl in e0. subst. repeat rewrite app_nil_r.
exists (Γ2 ++ A0 :: A :: Γ3 ++ Γ4, Δ0 ++ B :: Δ1). split. apply ImpRRule_I.
assert (E1: Γ2 ++ A0 :: A :: Γ3 ++ A :: Γ4 = (Γ2 ++ [A0]) ++ A :: Γ3 ++ A :: Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: Γ2 ++ A0 :: A :: Γ3 ++ Γ4 = (Γ2 ++ [A0]) ++ A :: Γ3 ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
* inversion e0. subst. apply app2_find_hole in H2. destruct H2. destruct s.
{ destruct s.
- destruct p. subst. exists ((Γ2 ++ m :: Γ3) ++ A0 :: Γ4, Δ0 ++ B :: Δ1).
split.
assert (E: Γ2 ++ m :: Γ3 ++ Γ4 = (Γ2 ++ m :: Γ3) ++ Γ4).
rewrite <- app_assoc. reflexivity. rewrite E. apply ImpRRule_I.
assert (E1: (Γ2 ++ m :: Γ3) ++ A0 :: m :: Γ4 = Γ2 ++ m :: (Γ3 ++ [A0]) ++ m :: Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Γ2 ++ m :: Γ3) ++ A0 :: Γ4 = Γ2 ++ m :: (Γ3 ++ [A0]) ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
- destruct p. subst. destruct x0.
+ simpl in e1. subst. repeat rewrite app_nil_r.
exists ((Γ2 ++ m :: Γ3) ++ A0 :: Γ4, Δ0 ++ B :: Δ1). split.
assert (E: Γ2 ++ m :: Γ3 ++ Γ4 = (Γ2 ++ m :: Γ3) ++ Γ4).
rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpRRule_I.
assert (E1: (Γ2 ++ m :: Γ3) ++ A0 :: m :: Γ4 = Γ2 ++ m :: (Γ3 ++ [A0]) ++ m :: Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Γ2 ++ m :: Γ3) ++ A0 :: Γ4 = Γ2 ++ m :: (Γ3 ++ [A0]) ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
+ inversion e1. subst.
exists ((Γ2 ++ m0 :: Γ3 ++ x0) ++ A0 :: Γ1, Δ0 ++ B :: Δ1). split.
assert (E: Γ2 ++ m0 :: Γ3 ++ x0 ++ Γ1 = (Γ2 ++ m0 :: Γ3 ++ x0) ++ Γ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpRRule_I.
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_LI. }
{ destruct p. subst. exists ((Γ2 ++ m :: x) ++ A0 :: x0 ++ Γ4,Δ0 ++ B :: Δ1).
split. assert (E: Γ2 ++ m :: (x ++ x0) ++ Γ4 = (Γ2 ++ m :: x) ++ x0 ++ Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite E. apply ImpRRule_I.
assert (E1: (Γ2 ++ m :: x) ++ A0 :: x0 ++ m :: Γ4 = Γ2 ++ m :: (x ++ A0 :: x0) ++ m :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Γ2 ++ m :: x) ++ A0 :: x0 ++ Γ4 = Γ2 ++ m :: (x ++ A0 :: x0) ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI. }
- destruct p. subst. exists (Γ0 ++ A0 :: x ++ A :: Γ3 ++ Γ4, Δ0 ++ B :: Δ1).
split. rewrite <- app_assoc. apply ImpRRule_I.
assert (E1: Γ0 ++ A0 :: x ++ A :: Γ3 ++ A :: Γ4 = (Γ0 ++ A0 :: x) ++ A :: Γ3 ++ A :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: Γ0 ++ A0 :: x ++ A :: Γ3 ++ Γ4 = (Γ0 ++ A0 :: x) ++ A :: Γ3 ++ Γ4).
repeat rewrite cons_single. repeat rewrite <- app_assoc. reflexivity. rewrite E2.
apply ctr_LI.
Qed.
Lemma ImpL_app_ctr_L : forall s sc A ps1 ps2,
(@ctr_L A s sc) ->
(ImpLRule [ps1;ps2] s) ->
((existsT2 psc1 psc2, (ImpLRule [psc1;psc2] sc) *
(@ctr_L A ps1 psc1) *
(@ctr_L A ps2 psc2))
+
(existsT2 B C invps11 invps12 invps21 invps22 invpsc11 invpsc22,
(A = Imp B C) *
(ImpLRule [invps11;invps12] ps1) *
(ImpLRule [invps21;invps22] ps2) *
(@ctr_R B invps11 invpsc11) *
(@ctr_L C invps22 invpsc22) *
(ImpLRule [invpsc11;invpsc22] sc))).
Proof.
intros s sc A ps1 ps2 ctr RA. inversion RA. inversion ctr. subst. inversion H.
subst. apply app2_find_hole in H1. destruct H1. repeat destruct s ; destruct p ; subst.
- inversion e0. subst. right. exists A0. exists B.
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ Γ3 ++ B :: Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ Δ1). repeat split.
assert (Γ2 ++ Γ3 ++ Γ4 = (Γ2 ++ Γ3) ++ Γ4). rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ2 ++ Γ3 ++ B :: Γ4 = (Γ2 ++ Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Γ2 ++ Γ3 ++ A0 --> B :: Γ4 = (Γ2 ++ Γ3) ++ A0 --> B :: Γ4). rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Γ2 ++ B :: Γ3 ++ Γ4 = (Γ2 ++ B :: Γ3) ++ Γ4). rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ2 ++ B :: Γ3 ++ B :: Γ4 = (Γ2 ++ B :: Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Γ2 ++ B :: Γ3 ++ A0 --> B :: Γ4 = (Γ2 ++ B :: Γ3) ++ A0 --> B :: Γ4). rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI.
- destruct x.
* simpl in e0. inversion e0. subst. right. exists A0. exists B.
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ Γ3 ++ B :: Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ Δ1). repeat split.
assert (Γ2 ++ Γ3 ++ Γ4 = (Γ2 ++ Γ3) ++ Γ4). repeat rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ2 ++ Γ3 ++ B :: Γ4 = (Γ2 ++ Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert ((Γ2 ++ []) ++ Γ3 ++ A0 --> B :: Γ4 = (Γ2 ++ Γ3) ++ A0 --> B :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Γ2 ++ B :: Γ3 ++ Γ4 = (Γ2 ++ B :: Γ3) ++ Γ4). rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ2 ++ B :: Γ3 ++ B :: Γ4 = (Γ2 ++ B :: Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert ((Γ2 ++ []) ++ B :: Γ3 ++ A0 --> B :: Γ4 = (Γ2 ++ B :: Γ3) ++ A0 --> B :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI.
* inversion e0. subst. apply app2_find_hole in H2. destruct H2. repeat destruct s ; destruct p ; subst.
+ inversion e1. subst. right. exists A0. exists B.
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ Γ3 ++ B :: Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ2 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ4, Δ0 ++ Δ1). repeat split.
repeat rewrite <- app_assoc. apply ImpLRule_I. repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI.
+ destruct x0.
{ simpl in e1. inversion e1. subst. right. exists A0. exists B.
exists (Γ2 ++ Γ3 ++ Γ1, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ1, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ Γ3 ++ B :: Γ1, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ B :: Γ1, Δ0 ++ Δ1).
exists (Γ2 ++ Γ3 ++ Γ1, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: Γ3 ++ Γ1, Δ0 ++ Δ1). repeat split.
repeat rewrite <- app_assoc. simpl. rewrite app_nil_r. apply ImpLRule_I. repeat rewrite <- app_assoc.
rewrite app_nil_r. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI. }
{ inversion e1. subst. left. exists (Γ2 ++ m0 :: Γ3 ++ x0 ++ Γ1, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ m0 :: Γ3 ++ x0 ++ B :: Γ1, Δ0 ++ Δ1). repeat split.
assert (Γ2 ++ m0 :: Γ3 ++ x0 ++ Γ1 = (Γ2 ++ m0 :: Γ3 ++ x0) ++ Γ1). repeat rewrite <- app_assoc.
simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ3 ++ x0 ++ A0 --> B :: Γ1 = (Γ2 ++ m0 :: Γ3 ++ x0) ++ A0 --> B :: Γ1). repeat rewrite <- app_assoc.
simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m0 :: Γ3 ++ x0 ++ B :: Γ1 = (Γ2 ++ m0 :: Γ3 ++ x0) ++ B :: Γ1). repeat rewrite <- app_assoc.
simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_LI.
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_LI. }
+ destruct x0.
{ simpl in e1. inversion e1. subst. right. exists A0. exists B.
exists (Γ2 ++ x ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ2 ++ B :: x ++ Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ x ++ B :: Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: x ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ2 ++ x ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ2 ++ B :: x ++ Γ4, Δ0 ++ Δ1). repeat split.
repeat rewrite <- app_assoc. apply ImpLRule_I. repeat rewrite <- app_assoc. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI. rewrite <- app_assoc. simpl. apply ImpLRule_I. }
{ inversion e1. subst. left. exists (Γ2 ++ m :: x ++ x0 ++ Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ2 ++ m :: x ++ B :: x0 ++ Γ4, Δ0 ++ Δ1). repeat split.
assert (Γ2 ++ m :: x ++ x0 ++ Γ4 = (Γ2 ++ m :: x) ++ x0 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m :: x ++ B :: x0 ++ Γ4 = (Γ2 ++ m :: x) ++ B :: x0 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m :: (x ++ A0 --> B :: x0) ++ Γ4 = (Γ2 ++ m :: x) ++ A0 --> B :: x0 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert ((Γ2 ++ m :: x) ++ x0 ++ m :: Γ4 = Γ2 ++ m :: (x ++ x0) ++ m :: Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m :: x ++ x0 ++ Γ4 = Γ2 ++ m :: (x ++ x0) ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_LI.
assert ((Γ2 ++ m :: x) ++ B :: x0 ++ m :: Γ4 = Γ2 ++ m :: (x ++ B :: x0) ++ m :: Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ2 ++ m :: x ++ B :: x0 ++ Γ4 = Γ2 ++ m :: (x ++ B :: x0) ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_LI. }
- destruct x.
+ simpl in e0. inversion e0. subst. right. exists A0. exists B.
exists (Γ0 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: A0 :: Δ1). exists (Γ0 ++ Γ3 ++ B :: Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ0 ++ B :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ0 ++ B :: Γ3 ++ B :: Γ4, Δ0 ++ Δ1).
exists (Γ0 ++ Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1). exists (Γ0 ++ B :: Γ3 ++ Γ4, Δ0 ++ Δ1) . repeat split.
assert (Γ0 ++ Γ3 ++ Γ4 = (Γ0 ++ Γ3) ++ Γ4). repeat rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ0 ++ Γ3 ++ B :: Γ4 = (Γ0 ++ Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Γ0 ++ Γ3 ++ A0 --> B :: Γ4 = (Γ0 ++ Γ3) ++ A0 --> B :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Γ0 ++ B :: Γ3 ++ Γ4 = (Γ0 ++ B :: Γ3) ++ Γ4). rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Γ0 ++ B :: Γ3 ++ B :: Γ4 = (Γ0 ++ B :: Γ3) ++ B :: Γ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Γ0 ++ B :: Γ3 ++ A0 --> B :: Γ4 = (Γ0 ++ B :: Γ3) ++ A0 --> B :: Γ4).
repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpLRule_I.
assert (Δ0 ++ A0 :: A0 :: Δ1 = Δ0 ++ A0 :: [] ++ A0 :: Δ1). reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ A0 :: Δ1 = Δ0 ++ A0 :: [] ++ Δ1). reflexivity. rewrite H0. clear H0.
apply ctr_RI. repeat rewrite <- app_assoc. simpl. apply ImpLRule_I.
+ inversion e0. subst. left. exists (Γ0 ++ x ++ A :: Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1).
exists (Γ0 ++ B :: x ++ A :: Γ3 ++ Γ4, Δ0 ++ Δ1). repeat split. repeat rewrite <- app_assoc.
apply ImpLRule_I.
assert (Γ0 ++ x ++ A :: Γ3 ++ A :: Γ4 = (Γ0 ++ x) ++ A :: Γ3 ++ A :: Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ x ++ A :: Γ3 ++ Γ4 = (Γ0 ++ x) ++ A :: Γ3 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_LI.
assert (Γ0 ++ B :: x ++ A :: Γ3 ++ A :: Γ4 = (Γ0 ++ B :: x) ++ A :: Γ3 ++ A :: Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ B :: x ++ A :: Γ3 ++ Γ4 = (Γ0 ++ B :: x) ++ A :: Γ3 ++ Γ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_LI.
Qed.
Lemma KR_app_ctr_L : forall s sc A ps,
(@ctr_L A s sc) ->
(KRRule [ps] s) ->
((KRRule [ps] sc) +
(existsT2 psc, (KRRule [psc] sc) * (@ctr_L (unBox_formula A) ps psc))).
Proof.
intros s sc A ps ctr RA. inversion RA. inversion ctr. rewrite <- H1 in H2.
inversion H2. subst. apply univ_gen_ext_elem_deep with (l3:=Γ1) (l4:=Γ2 ++ A :: Γ3) (a:=A) in X.
destruct X. 3: reflexivity.
- destruct p. apply univ_gen_ext_elem_deep with (l3:=Γ1 ++ Γ2) (l4:=Γ3) (a:=A) in u. destruct u. destruct p.
3: rewrite <- app_assoc. 3: reflexivity.
* left. apply KRRule_I.
assumption.
apply univ_gen_ext_add_elem_deep. rewrite app_assoc. assumption. assumption.
* exfalso. apply f. repeat destruct s. repeat destruct p. subst. apply is_box_is_in_boxed_list with (A:=A) in H0 .
unfold is_boxedT. destruct H0. exists x1. auto. apply in_or_app. right. apply in_eq.
- repeat destruct s. repeat destruct p. apply univ_gen_ext_elem_deep with (l3:=Γ2) (l4:=Γ3) (a:=A) in u0.
destruct u0. 3: reflexivity.
* destruct p. exfalso. subst. apply is_box_is_in_boxed_list with (A:=A) in H0. apply f. unfold is_boxedT.
destruct H0. exists x1. auto. apply in_or_app. right. apply in_eq.
* repeat destruct s. repeat destruct p. right. subst.
exists (unboxed_list (x ++ A :: x1 ++ x2), [A0]). split.
{ apply KRRule_I.
intro. intros. apply H0. apply in_app_or in H. destruct H. apply in_or_app. left. assumption.
inversion H. subst. apply in_or_app. right. apply in_eq. apply in_app_or in H1. destruct H1.
apply in_or_app. right. apply in_cons. apply in_or_app. left. assumption.
apply in_or_app. right. apply in_cons. apply in_or_app. right. apply in_cons.
assumption.
apply univ_gen_ext_combine. assumption. apply univ_gen_ext_cons. apply univ_gen_ext_combine.
assumption. assumption. }
{ repeat rewrite cons_single. repeat rewrite unbox_app_distrib. simpl. apply ctr_LI. }
Qed.
Lemma ImpR_app_ctr_R : forall s sc A ps,
(@ctr_R A s sc) ->
(ImpRRule [ps] s) ->
((existsT2 psc, (ImpRRule [psc] sc) * (@ctr_R A ps psc))
+
(existsT2 B C invps invpsc0 invpsc, (A = Imp B C) * (ImpRRule [invps] ps) * (ImpRRule [invpsc] sc) *
(@ctr_L B invps invpsc0) * (@ctr_R C invpsc0 invpsc))).
Proof.
intros s sc A ps ctr RA. inversion RA. inversion ctr. subst.
inversion H. subst. apply app2_find_hole in H2. destruct H2. repeat destruct s ; destruct p ; subst.
- inversion e0. right. exists A0. exists B. exists (Γ0 ++ A0 :: A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ Δ4).
repeat split. assert (Δ2 ++ B :: Δ3 ++ B :: Δ4 = (Δ2 ++ B :: Δ3) ++ B :: Δ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. assert (Δ2 ++ B :: Δ3 ++ A0 --> B :: Δ4 = (Δ2 ++ B :: Δ3) ++ A0 --> B :: Δ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI.
- destruct x.
* simpl in e0. inversion e0. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, (Δ2 ++ []) ++ B :: Δ3 ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, (Δ2 ++ []) ++ B :: Δ3 ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, (Δ2 ++ []) ++ B :: Δ3 ++ Δ4).
repeat split. assert ((Δ2 ++ []) ++ B :: Δ3 ++ B :: Δ4 = (Δ2 ++ B :: Δ3) ++ B :: Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. assert ((Δ2 ++ []) ++ B :: Δ3 ++ A0 --> B :: Δ4 = (Δ2 ++ B :: Δ3) ++ A0 --> B :: Δ4).
rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
apply ImpRRule_I. repeat rewrite <- app_assoc. simpl. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI.
* inversion e0. subst. apply app2_find_hole in H2. destruct H2. repeat destruct s ; destruct p ; subst.
+ inversion e1. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ Δ4). repeat split.
repeat rewrite <- app_assoc. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI.
+ destruct x0.
{ simpl in e1. inversion e1. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ1). exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ B :: Δ1).
exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: Δ3 ++ Δ1). repeat split.
repeat rewrite <- app_assoc. simpl. rewrite app_nil_r. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI. }
{ inversion e1. subst. left. exists (Γ0 ++ A0 :: Γ1, Δ2 ++ m0 :: Δ3 ++ x0 ++ B :: Δ1).
repeat split. assert (Δ2 ++ m0 :: Δ3 ++ x0 ++ B :: Δ1 = (Δ2 ++ m0 :: Δ3 ++ x0) ++ B :: Δ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ m0 :: Δ3 ++ x0 ++ A0 --> B :: Δ1 = (Δ2 ++ m0 :: Δ3 ++ x0) ++ A0 --> B :: Δ1). repeat rewrite <- app_assoc.
simpl. repeat rewrite <- app_assoc. reflexivity. rewrite H0. clear H0. apply ImpRRule_I.
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_RI. }
+ destruct x0.
{ simpl in e1. inversion e1. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, Δ2 ++ B :: x ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: x ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, Δ2 ++ B :: x ++ Δ4). repeat split.
repeat rewrite <- app_assoc. apply ImpRRule_I. repeat rewrite <- app_assoc. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI. }
{ inversion e1. subst. left. exists (Γ0 ++ A0 :: Γ1, Δ2 ++ m :: x ++ B :: x0 ++ Δ4).
repeat split.
assert (Δ2 ++ m :: x ++ B :: x0 ++ Δ4 = (Δ2 ++ m :: x) ++ B :: x0 ++ Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ m :: (x ++ A0 --> B :: x0) ++ Δ4 = (Δ2 ++ m :: x) ++ A0 --> B :: x0 ++ Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ImpRRule_I.
assert ((Δ2 ++ m :: x) ++ B :: x0 ++ m :: Δ4 = Δ2 ++ m :: (x ++ B :: x0) ++ m :: Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Δ2 ++ m :: x ++ B :: x0 ++ Δ4 = Δ2 ++ m :: (x ++ B :: x0) ++ Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_RI. }
- destruct x.
+ simpl in e0. inversion e0. subst. right. exists A0. exists B.
exists (Γ0 ++ A0 :: A0 :: Γ1, Δ0 ++ B :: Δ3 ++ B :: Δ4). exists (Γ0 ++ A0 :: Γ1, Δ0 ++ B :: Δ3 ++ B :: Δ4).
exists (Γ0 ++ A0 :: Γ1, Δ0 ++ B :: Δ3 ++ Δ4). repeat split.
assert (Δ0 ++ B :: Δ3 ++ A0 --> B :: Δ4 = (Δ0 ++ B :: Δ3) ++ A0 --> B :: Δ4). repeat rewrite <- app_assoc. reflexivity. rewrite H0.
clear H0. assert (Δ0 ++ B :: Δ3 ++ B :: Δ4 = (Δ0 ++ B :: Δ3) ++ B :: Δ4). rewrite <- app_assoc. reflexivity.
rewrite H0. clear H0. apply ImpRRule_I. repeat rewrite <- app_assoc. simpl. apply ImpRRule_I.
assert (Γ0 ++ A0 :: A0 :: Γ1 = Γ0 ++ A0 :: [] ++ A0 :: Γ1). reflexivity. rewrite H0. clear H0.
assert (Γ0 ++ A0 :: Γ1 = Γ0 ++ A0 :: [] ++ Γ1). reflexivity. rewrite H0. clear H0.
apply ctr_LI.
+ inversion e0. subst. left. exists (Γ0 ++ A0 :: Γ1, Δ0 ++ B :: x ++ A :: Δ3 ++ Δ4).
repeat split. repeat rewrite <- app_assoc. apply ImpRRule_I.
assert (Δ0 ++ B :: x ++ A :: Δ3 ++ A :: Δ4 = (Δ0 ++ B :: x) ++ A :: Δ3 ++ A :: Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0.
assert (Δ0 ++ B :: x ++ A :: Δ3 ++ Δ4 = (Δ0 ++ B :: x) ++ A :: Δ3 ++ Δ4). repeat rewrite <- app_assoc.
reflexivity. rewrite H0. clear H0. apply ctr_RI.
Qed.
Lemma ImpL_app_ctr_R : forall s sc A ps1 ps2,
(@ctr_R A s sc) ->
(ImpLRule [ps1;ps2] s) ->
(existsT2 psc1 psc2, (ImpLRule [psc1;psc2] sc) * (@ctr_R A ps1 psc1) * (@ctr_R A ps2 psc2)).
Proof.
intros s sc A ps1 ps2 ctr RA. inversion RA. inversion ctr. subst.
inversion H. subst. apply app2_find_hole in H2. destruct H2. destruct s.
- destruct s.
+ destruct p. subst. exists (Γ0 ++ Γ1, Δ2 ++ A0 :: A :: Δ3 ++ Δ4). exists (Γ0 ++ B :: Γ1, Δ2 ++ A :: Δ3 ++ Δ4).
split. split.
apply ImpLRule_I.
assert (E1: Δ2 ++ A0 :: A :: Δ3 ++ A :: Δ4 = (Δ2 ++ [A0]) ++ A :: Δ3 ++ A :: Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E1.
assert (E2: Δ2 ++ A0 :: A :: Δ3 ++ Δ4 = (Δ2 ++ [A0]) ++ A :: Δ3 ++ Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E2. apply ctr_RI.
apply ctr_RI.
+ destruct p. destruct x.
* rewrite app_nil_r in e. rewrite app_nil_l in e0. subst.
exists (Γ0 ++ Γ1, Δ2 ++ A0 :: A :: Δ3 ++ Δ4). exists (Γ0 ++ B :: Γ1, Δ2 ++ A :: Δ3 ++ Δ4).
split. split.
apply ImpLRule_I.
assert (E1: Δ2 ++ A0 :: A :: Δ3 ++ A :: Δ4 = (Δ2 ++ [A0]) ++ A :: Δ3 ++ A :: Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E1.
assert (E2: Δ2 ++ A0 :: A :: Δ3 ++ Δ4 = (Δ2 ++ [A0]) ++ A :: Δ3 ++ Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E2. apply ctr_RI.
apply ctr_RI.
* inversion e0. subst. apply app2_find_hole in H2. destruct H2. destruct s.
{ destruct s.
- destruct p. subst. exists (Γ0 ++ Γ1, (Δ2 ++ m :: Δ3) ++ A0 :: Δ4).
exists (Γ0 ++ B :: Γ1, (Δ2 ++ m :: Δ3) ++ Δ4). split. split.
assert (E: Δ2 ++ m :: Δ3 ++ Δ4 = (Δ2 ++ m :: Δ3) ++ Δ4).
rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpLRule_I.
assert (E1: (Δ2 ++ m :: Δ3) ++ A0 :: m :: Δ4 = Δ2 ++ m :: (Δ3 ++ [A0]) ++ m :: Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E1.
assert (E2: (Δ2 ++ m :: Δ3) ++ A0 :: Δ4 = Δ2 ++ m :: (Δ3 ++ [A0]) ++ Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E2. apply ctr_RI.
rewrite <- app_assoc. simpl. apply ctr_RI.
- destruct p. subst. destruct x0.
+ rewrite app_nil_l in e1. rewrite app_nil_r in e0. subst.
exists (Γ0 ++ Γ1,(Δ2 ++ m :: Δ3) ++ A0 :: Δ4). exists (Γ0 ++ B :: Γ1, (Δ2 ++ m :: Δ3) ++ Δ4).
split. split.
assert (E: Δ2 ++ m :: Δ3 ++ Δ4 = (Δ2 ++ m :: Δ3) ++ Δ4).
rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpLRule_I.
assert (E1: (Δ2 ++ m :: Δ3 ++ []) ++ A0 :: m :: Δ4 = Δ2 ++ m :: (Δ3 ++ [A0]) ++ m :: Δ4).
rewrite app_nil_r. repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E1.
assert (E2: (Δ2 ++ m :: Δ3) ++ A0 :: Δ4 = Δ2 ++ m :: (Δ3 ++ [A0]) ++ Δ4).
repeat rewrite <- app_assoc. rewrite cons_single. reflexivity. rewrite E2. apply ctr_RI.
rewrite <- app_assoc. simpl. apply ctr_RI.
+ inversion e1. subst. exists (Γ0 ++ Γ1,(Δ2 ++ m0 :: Δ3 ++ x0) ++ A0 :: Δ1).
exists (Γ0 ++ B :: Γ1,(Δ2 ++ m0 :: Δ3 ++ x0) ++ Δ1). split. split.
assert (E: Δ2 ++ m0 :: Δ3 ++ x0 ++ Δ1 = (Δ2 ++ m0 :: Δ3 ++ x0) ++ Δ1).
rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpLRule_I.
assert (E1: (Δ2 ++ m0 :: Δ3 ++ m0 :: x0) ++ A0 :: Δ1 = Δ2 ++ m0 :: Δ3 ++ m0 :: x0 ++ A0 :: Δ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Δ2 ++ m0 :: Δ3 ++ x0) ++ A0 :: Δ1 = Δ2 ++ m0 :: Δ3 ++ x0 ++ A0 :: Δ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E2. apply ctr_RI.
rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. apply ctr_RI. }
{ destruct p. subst. exists (Γ0 ++ Γ1,(Δ2 ++ m :: x) ++ A0 :: x0 ++ Δ4).
exists (Γ0 ++ B :: Γ1, (Δ2 ++ m :: x) ++ x0 ++ Δ4). split. split.
assert (E: Δ2 ++ m :: (x ++ x0) ++ Δ4 = (Δ2 ++ m :: x) ++ x0 ++ Δ4).
rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E.
apply ImpLRule_I.
assert (E1: (Δ2 ++ m :: x) ++ A0 :: x0 ++ m :: Δ4 = Δ2 ++ m :: (x ++ A0 :: x0) ++ m :: Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: (Δ2 ++ m :: x) ++ A0 :: x0 ++ Δ4 = Δ2 ++ m :: (x ++ A0 :: x0) ++ Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E2. apply ctr_RI.
assert (E1: (Δ2 ++ m :: x) ++ x0 ++ Δ4 = Δ2 ++ m :: (x ++ x0) ++ Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E1. apply ctr_RI. }
- destruct p. subst. exists (Γ0 ++ Γ1, Δ0 ++ A0 :: x ++ A :: Δ3 ++ Δ4).
exists (Γ0 ++ B :: Γ1, Δ0 ++ x ++ A :: Δ3 ++ Δ4). split. split.
rewrite <- app_assoc. apply ImpLRule_I.
assert (E1: Δ0 ++ A0 :: x ++ A :: Δ3 ++ A :: Δ4 = (Δ0 ++ A0 :: x) ++ A :: Δ3 ++ A :: Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E1.
assert (E2: Δ0 ++ A0 :: x ++ A :: Δ3 ++ Δ4 = (Δ0 ++ A0 :: x) ++ A :: Δ3 ++ Δ4).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E2. apply ctr_RI.
rewrite app_assoc. apply ctr_RI.
Qed.
Lemma KR_app_ctr_R : forall s sc A ps,
(@ctr_R A s sc) -> (KRRule [ps] s) -> (KRRule [ps] sc).
Proof.
intros s sc A ps ctr RA. inversion RA. inversion ctr. rewrite <- H1 in H2.
inversion H2. apply app2_find_hole in H6. destruct H6. destruct s0.
+ destruct s0.
* destruct p. inversion e0. apply KRRule_I. assumption. assumption.
* destruct p. subst. destruct x.
{ rewrite app_nil_l in e0. inversion e0. subst. apply KRRule_I.
assumption. assumption. }
{ inversion e0. subst. apply app2_find_hole in H3. destruct H3. destruct s.
- destruct s.
+ destruct p. inversion e1. apply KRRule_I. assumption. assumption.
+ destruct p. subst. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst. apply KRRule_I. assumption.
assumption.
* inversion e1. subst. assert (E: Δ2 ++ m0 :: Δ3 ++ x0 ++ Box A0 :: Δ1 = (Δ2 ++ m0 :: Δ3 ++ x0) ++ Box A0 :: Δ1).
repeat rewrite <- app_assoc. simpl. repeat rewrite <- app_assoc. reflexivity. rewrite E. apply KRRule_I. assumption.
assumption.
- destruct p. subst. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst. apply KRRule_I. assumption. assumption.
* inversion e1. subst. assert (E: Δ2 ++ m :: (x ++ Box A0 :: x0) ++ Δ4 = (Δ2 ++ m :: x) ++ Box A0 :: x0 ++ Δ4).
repeat rewrite <- app_assoc. reflexivity. rewrite E. apply KRRule_I. assumption. assumption. }
+ destruct p. subst. destruct x.
* rewrite app_nil_l in e0. rewrite app_nil_r. inversion e0. subst. apply KRRule_I. assumption. assumption.
* inversion e0. rewrite <- app_assoc. simpl. apply KRRule_I. assumption. assumption.
Qed.
(* Now we can prove that contraction rules are height-preserving admissible. *)
Theorem KS_hpadm_ctr_LR0 : forall (k : nat) s
(D0 : KS_prv s),
k = (derrec_height D0) ->
(forall sc A, (((@ctr_L A s sc) + (@ctr_R A s sc)) ->
existsT2 (D1 : KS_prv sc),
derrec_height D1 <= k)).
Proof.
induction k as [n IH] using (well_founded_induction_type lt_wf).
intros s D0. remember D0 as D0'. destruct D0.
(* D0 ip a leaf *)
- intros hei sc A ctr. inversion f.
(* D0 is ends with an application of rule *)
- intros hei sc A ctr. destruct ctr as [ctr | ctr].
{ inversion ctr. assert (DersNil: dersrec KS_rules (fun _ : Seq => False) []).
apply dersrec_nil. inversion k.
(* IdP *)
* inversion H1. rewrite <- H in H5. inversion H5.
apply app2_find_hole in H7. destruct H7. destruct s.
+ destruct s.
{ destruct p. inversion e0. subst. pose (IdPRule_I P Γ3 (Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ3 ++ # P :: Γ1 ++ Γ2, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl. repeat rewrite dersrec_height_nil.
left. reflexivity. reflexivity. }
{ destruct p. destruct x.
- rewrite app_nil_l in e0. inversion e0.
subst. pose (IdPRule_I P (Γ3 ++ []) (Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) ((Γ3 ++ []) ++ # P :: Γ1 ++ Γ2,Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- inversion e0. subst.
pose (IdPRule_I P Γ3 (x ++ A :: Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
assert (E: Γ3 ++ # P :: x ++ A :: Γ1 ++ Γ2 = (Γ3 ++ # P :: x) ++ A :: Γ1 ++ Γ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in i. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) ((Γ3 ++ # P :: x) ++ A :: Γ1 ++ Γ2,Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
+ destruct p. destruct x.
{ rewrite app_nil_l in e0. inversion e0. subst.
pose (IdPRule_I P Γ0 (Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1 ++ Γ2, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
{ inversion e0. subst. apply app2_find_hole in H9. destruct H9. destruct s.
- destruct s.
+ destruct p. inversion e1. subst.
pose (IdPRule_I P Γ0 (Γ1 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1 ++ Γ2, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ destruct p. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst.
pose (IdPRule_I P Γ0 (Γ1 ++ Γ4) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1 ++ Γ4, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
* inversion e1. subst.
pose (IdPRule_I P (Γ0 ++ m0 :: Γ1 ++ x0) Γ4 Δ0 Δ1). apply IdP in i. simpl in i.
repeat rewrite <- app_assoc in i. simpl in i. repeat rewrite <- app_assoc in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ m0 :: Γ1 ++ x0 ++ # P :: Γ4,Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- destruct p. destruct x0.
+ rewrite app_nil_l in e1. inversion e1. subst.
pose (IdPRule_I P Γ0 ((x ++ []) ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: (x ++ []) ++ Γ2, Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ inversion e1. subst.
pose (IdPRule_I P (Γ0 ++ m :: x) (x0 ++ Γ2) Δ0 Δ1). apply IdP in i. simpl in i.
assert (E: (Γ0 ++ m :: x) ++ # P :: x0 ++ Γ2 = Γ0 ++ m :: (x ++ # P :: x0) ++ Γ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in i. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ m :: (x ++ # P :: x0) ++ Γ2,Δ0 ++ # P :: Δ1) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
(* BotL *)
* inversion H1. rewrite <- H in H5. inversion H5.
apply app2_find_hole in H7. destruct H7. destruct s.
+ destruct s.
{ destruct p. inversion e0. subst. pose (BotLRule_I Γ3 (Γ1 ++ Γ2) Δ). apply BotL in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ3 ++ Bot :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl. repeat rewrite dersrec_height_nil.
left. reflexivity. reflexivity. }
{ destruct p. destruct x.
- rewrite app_nil_l in e0. inversion e0.
subst. pose (BotLRule_I (Γ3 ++ []) (Γ1 ++ Γ2) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) ((Γ3 ++ []) ++ Bot :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- inversion e0. subst.
pose (BotLRule_I Γ3 (x ++ A :: Γ1 ++ Γ2) Δ). apply BotL in b. simpl in b.
assert (E: Γ3 ++ Bot :: x ++ A :: Γ1 ++ Γ2 = (Γ3 ++ Bot :: x) ++ A :: Γ1 ++ Γ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in b. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) ((Γ3 ++ Bot :: x) ++ A :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
+ destruct p. destruct x.
{ rewrite app_nil_l in e0. inversion e0. subst.
pose (BotLRule_I Γ0 (Γ1 ++ Γ2) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
{ inversion e0. subst. apply app2_find_hole in H9. destruct H9. destruct s.
- destruct s.
+ destruct p. inversion e1. subst.
pose (BotLRule_I Γ0 (Γ1 ++ Γ2) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: Γ1 ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ destruct p. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst.
pose (BotLRule_I Γ0 (Γ1 ++ Γ4) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: Γ1 ++ Γ4, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
* inversion e1. subst.
pose (BotLRule_I (Γ0 ++ m0 :: Γ1 ++ x0) Γ4 Δ). apply BotL in b. simpl in b.
repeat rewrite <- app_assoc in b. simpl in b. repeat rewrite <- app_assoc in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ m0 :: Γ1 ++ x0 ++ Bot :: Γ4, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- destruct p. destruct x0.
+ rewrite app_nil_l in e1. inversion e1. subst.
pose (BotLRule_I Γ0 ((x ++ []) ++ Γ2) Δ). apply BotL in b. simpl in b.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: (x ++ []) ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ inversion e1. subst.
pose (BotLRule_I (Γ0 ++ m :: x) (x0 ++ Γ2) Δ). apply BotL in b. simpl in b.
assert (E: (Γ0 ++ m :: x) ++ Bot :: x0 ++ Γ2 = Γ0 ++ m :: (x ++ Bot :: x0) ++ Γ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in b. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ m :: (x ++ Bot :: x0) ++ Γ2, Δ) b DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
(* ImpR *)
* inversion H1. subst. inversion H5. subst. pose (ImpR_app_ctr_L _ _ _ _ ctr H1). destruct s. destruct p.
apply ImpR in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x]) (Γ0 ++ A :: Γ1 ++ Γ2, Δ0 ++ A0 --> B :: Δ1) i). subst. simpl.
remember [(Γ3 ++ A0 :: Γ4, Δ0 ++ B :: Δ1)] as ps'. destruct d. inversion Heqps'.
inversion Heqps'. subst. simpl. rewrite dersrec_height_nil. simpl in IH.
rewrite dersrec_height_nil in IH. rewrite Nat.max_0_r. rewrite Nat.max_0_r in IH.
assert (E: derrec_height d < S (derrec_height d)). auto.
assert (E1: derrec_height d = derrec_height d). auto.
assert ((ctr_L A (Γ3 ++ A0 :: Γ4, Δ0 ++ B :: Δ1) x) + (ctr_R A (Γ3 ++ A0 :: Γ4, Δ0 ++ B :: Δ1) x)).
left. auto.
pose (IH (derrec_height d) E (Γ3 ++ A0 :: Γ4, Δ0 ++ B :: Δ1) d E1 x A H).
destruct s.
pose (dlCons x0 d1). pose (d0 d2). exists d3. simpl. rewrite dersrec_height_nil.
rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. assumption. reflexivity. reflexivity. reflexivity.
(* ImpL *)
* inversion H1. subst. inversion H5. subst. pose (ImpL_app_ctr_L _ _ _ _ _ ctr H1). destruct s.
{ repeat destruct s. repeat destruct p. apply ImpL in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x;x0]) (Γ0 ++ A :: Γ1 ++ Γ2, Δ0 ++ Δ1) i). subst. simpl.
remember [(Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1);(Γ3 ++ B :: Γ4, Δ0 ++ Δ1)] as ps'. destruct d.
inversion Heqps'. inversion Heqps'. subst.
remember [(Γ3 ++ B :: Γ4, Δ0 ++ Δ1)] as ps''. destruct d1. inversion Heqps''.
inversion Heqps''. simpl. subst. rewrite dersrec_height_nil. simpl in IH.
rewrite dersrec_height_nil in IH. rewrite Nat.max_0_r. rewrite Nat.max_0_r in IH.
assert (E1: derrec_height d < S (Init.Nat.max (derrec_height d)(derrec_height d1))).
apply Nat.lt_succ_r. apply Nat.le_max_l.
assert (E2: derrec_height d = derrec_height d). auto.
assert ((ctr_L A (Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1) x) + (ctr_R A (Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1) x)).
auto.
pose (IH (derrec_height d) E1 (Γ3 ++ Γ4, Δ0 ++ A0 :: Δ1) d E2 x A H).
destruct s.
assert (E3: derrec_height d1 < S (Init.Nat.max (derrec_height d)(derrec_height d1))).
apply Nat.lt_succ_r. apply Nat.le_max_r.
assert (E4: derrec_height d1 = derrec_height d1). auto.
assert ((ctr_L A (Γ3 ++ B :: Γ4, Δ0 ++ Δ1) x0) + (ctr_R A (Γ3 ++ B :: Γ4, Δ0 ++ Δ1) x0)).
auto.
pose (IH (derrec_height d1) E3 (Γ3 ++ B :: Γ4, Δ0 ++ Δ1) d1 E4 x0 A H2).
destruct s.
pose (dlCons x1 (dlCons x2 d2)). pose (d0 d3). exists d4. simpl. rewrite dersrec_height_nil.
rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. apply Nat.max_le_compat.
assumption. assumption. reflexivity. reflexivity. reflexivity. }
{ simpl. repeat destruct s. repeat destruct p. subst. apply ImpL in i.
assert (J30: dersrec_height d = dersrec_height d). reflexivity.
pose (@dersrec_derrec2_height (dersrec_height d) _ _ _ _ _ d J30). repeat destruct s.
assert (J1: derrec_height x7 = derrec_height x7). reflexivity.
pose (ImpR_ImpL_hpinv _ _ _ J1). destruct p. clear s. pose (s0 _ _ i1). repeat destruct s.
clear s0. destruct p. simpl in IH.
assert (J2: derrec_height x9 < S (dersrec_height d)). lia.
assert (J3: derrec_height x9 = derrec_height x9). reflexivity.
assert (J4: (ctr_L x x1 x5) + (ctr_R x x1 x5)). auto.
pose (IH _ J2 _ _ J3 _ _ J4). destruct s.
assert (J5: derrec_height x8 = derrec_height x8). reflexivity.
pose (ImpR_ImpL_hpinv _ _ _ J5). destruct p. clear s. pose (s0 _ _ i0). repeat destruct s.
clear s0. destruct p.
assert (J6: derrec_height x13 < S (dersrec_height d)). lia.
assert (J7: derrec_height x13 = derrec_height x13). reflexivity.
assert (J8: (ctr_L x0 x4 x6) + (ctr_R x0 x4 x6)). auto.
pose (IH _ J6 _ _ J7 _ _ J8). destruct s. pose (dlCons x14 DersNil). pose (dlCons x11 d0).
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x5;x6]) (Γ0 ++ x --> x0 :: Γ1 ++ Γ2, Δ0 ++ Δ1) i d1). exists d2. simpl.
rewrite dersrec_height_nil. lia. reflexivity. }
(* KR *)
* inversion X. rewrite <- H4 in X. pose (KR_app_ctr_L _ _ _ _ ctr X). destruct s.
{ apply KR in k0. pose (derI (rules:=KS_rules)
(prems:=fun _ : Seq => False) (ps:=[(unboxed_list BΓ, [A0])])
sc k0). subst. pose (d0 d). exists d1. simpl. reflexivity. }
{ repeat destruct s. repeat destruct p. apply KR in k0.
remember [(unboxed_list BΓ, [A0])] as ps'. destruct d. subst. inversion H4.
rewrite Heqps' in H4. inversion H4. subst. simpl. simpl in IH.
assert (E1: derrec_height d < S (Init.Nat.max (derrec_height d) (dersrec_height d0))).
rewrite dersrec_height_nil. rewrite Nat.max_0_r. apply Nat.lt_succ_r. left. reflexivity.
assert (E2: derrec_height d = derrec_height d). auto.
assert ((ctr_L (unBox_formula A) (unboxed_list BΓ, [A0]) x) +
(ctr_R (unBox_formula A) (unboxed_list BΓ, [A0]) x)). auto.
pose (IH (derrec_height d) E1 ((unboxed_list BΓ, [A0])) d E2 x (unBox_formula A) H).
destruct s.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x]) (Γ0 ++ A :: Γ1 ++ Γ2, Δ) k0). subst. simpl.
pose (dlCons x0 d0). pose (d1 d2). exists d3. simpl. rewrite dersrec_height_nil.
repeat rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. lia. auto. }}
{ inversion ctr. assert (DersNil: dersrec KS_rules (fun _ : Seq => False) []).
apply dersrec_nil. inversion k.
(* IdP *)
* inversion H1. rewrite <- H in H5. inversion H5.
apply app2_find_hole in H8. destruct H8. destruct s.
+ destruct s.
{ destruct p. inversion e0. subst. pose (IdPRule_I P Γ0 Γ1 Δ3 (Δ1 ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ3 ++ # P :: Δ1 ++ Δ2) i DersNil). exists d0. simpl. repeat rewrite dersrec_height_nil.
left. reflexivity. reflexivity. }
{ destruct p. destruct x.
- rewrite app_nil_l in e0. inversion e0.
subst. pose (IdPRule_I P Γ0 Γ1 (Δ3 ++ []) (Δ1 ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, (Δ3 ++ []) ++ # P :: Δ1 ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- inversion e0. subst.
pose (IdPRule_I P Γ0 Γ1 Δ3 (x ++ A :: Δ1 ++ Δ2)). apply IdP in i. simpl in i.
assert (E: Δ3 ++ # P :: x ++ A :: Δ1 ++ Δ2 = (Δ3 ++ # P :: x) ++ A :: Δ1 ++ Δ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in i. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, (Δ3 ++ # P :: x) ++ A :: Δ1 ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
+ destruct p. destruct x.
{ rewrite app_nil_l in e0. inversion e0. subst.
pose (IdPRule_I P Γ0 Γ1 Δ0 (Δ1 ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ # P :: Δ1 ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
{ inversion e0. subst. apply app2_find_hole in H9. destruct H9. destruct s.
- destruct s.
+ destruct p. inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 Δ0 (Δ1 ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ # P :: Δ1 ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ destruct p. destruct x0.
* rewrite app_nil_l in e1. inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 Δ0 (Δ1 ++ Δ4)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ # P :: Δ1 ++ Δ4) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
* inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 (Δ0 ++ m0 :: Δ1 ++ x0) Δ4). apply IdP in i. simpl in i.
repeat rewrite <- app_assoc in i. simpl in i. repeat rewrite <- app_assoc in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ m0 :: Δ1 ++ x0 ++ # P :: Δ4) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
- destruct p. destruct x0.
+ rewrite app_nil_l in e1. inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 Δ0 ((x ++ []) ++ Δ2)). apply IdP in i. simpl in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ # P :: (x ++ []) ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
+ inversion e1. subst.
pose (IdPRule_I P Γ0 Γ1 (Δ0 ++ m :: x) (x0 ++ Δ2)). apply IdP in i. simpl in i.
assert (E: (Δ0 ++ m :: x) ++ # P :: x0 ++ Δ2 = Δ0 ++ m :: (x ++ # P :: x0) ++ Δ2). repeat rewrite <- app_assoc. reflexivity.
rewrite E in i. clear E.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ # P :: Γ1, Δ0 ++ m :: (x ++ # P :: x0) ++ Δ2) i DersNil). exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity. }
(* BotL *)
* inversion H1. rewrite <- H in H5. inversion H5.
pose (BotLRule_I Γ0 Γ1 (Δ0 ++ A :: Δ1 ++ Δ2)). apply BotL in b.
pose (derI (rules:=KS_rules)
(prems:=fun _ : Seq => False)
(ps:=[]) (Γ0 ++ Bot :: Γ1, Δ0 ++ A :: Δ1 ++ Δ2) b DersNil). subst. exists d0. simpl.
repeat rewrite dersrec_height_nil. left. reflexivity. reflexivity.
(* ImpR *)
* inversion H1. subst. inversion H5. subst. pose (ImpR_app_ctr_R _ _ _ _ ctr H1). destruct s.
{ destruct s. destruct p. apply ImpR in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x]) (Γ0 ++ Γ1, Δ0 ++ A :: Δ1 ++ Δ2) i). subst. simpl.
remember [(Γ0 ++ A0 :: Γ1, Δ3 ++ B :: Δ4)] as ps'. destruct d. inversion Heqps'.
inversion Heqps'. subst. simpl. rewrite dersrec_height_nil. simpl in IH.
rewrite dersrec_height_nil in IH. rewrite Nat.max_0_r. rewrite Nat.max_0_r in IH.
assert (E: derrec_height d < S (derrec_height d)). auto.
assert (E1: derrec_height d = derrec_height d). auto.
assert ((ctr_L A (Γ0 ++ A0 :: Γ1, Δ3 ++ B :: Δ4) x) + (ctr_R A (Γ0 ++ A0 :: Γ1, Δ3 ++ B :: Δ4) x)).
auto.
pose (IH (derrec_height d) E (Γ0 ++ A0 :: Γ1, Δ3 ++ B :: Δ4) d E1 x A H).
destruct s.
pose (dlCons x0 d1). pose (d0 d2). exists d3. simpl. rewrite dersrec_height_nil.
rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. assumption. reflexivity. reflexivity. reflexivity. }
{ repeat destruct s. repeat destruct p. subst. apply ImpR in i.
assert (J30: dersrec_height d = dersrec_height d). reflexivity.
pose (dersrec_derrec_height d J30). destruct s.
assert (J1: derrec_height x4 = derrec_height x4). reflexivity.
pose (ImpR_ImpL_hpinv _ _ _ J1). destruct p. clear s0. pose (s _ i0). repeat destruct s0.
clear s. simpl in IH.
assert (J2: derrec_height x5 < S (dersrec_height d)). lia.
assert (J3: derrec_height x5 = derrec_height x5). reflexivity.
assert (J4: (ctr_L x x1 x2) + (ctr_R x x1 x2)). auto.
pose (IH _ J2 _ _ J3 _ _ J4). destruct s.
assert (J5: derrec_height x6 = derrec_height x6). reflexivity.
assert (J6: derrec_height x6 < S (dersrec_height d)). lia.
assert (J8: (ctr_L x0 x2 x3) + (ctr_R x0 x2 x3)). auto.
pose (IH _ J6 _ _ J5 _ _ J8). destruct s. pose (dlCons x7 DersNil).
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x3]) (Γ0 ++ Γ1, Δ0 ++ x --> x0 :: Δ1 ++ Δ2) i d0). simpl. exists d1. simpl. rewrite dersrec_height_nil.
lia. reflexivity. }
(* ImpL *)
* inversion H1. subst. inversion H5. subst. pose (ImpL_app_ctr_R _ _ _ _ _ ctr H1). destruct s.
repeat destruct s. repeat destruct p. apply ImpL in i.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[x;x0]) (Γ0 ++ A0 --> B :: Γ1, Δ0 ++ A :: Δ1 ++ Δ2) i). subst. simpl.
remember [(Γ0 ++ Γ1, Δ3 ++ A0 :: Δ4);(Γ0 ++ B :: Γ1, Δ3 ++ Δ4)] as ps'. destruct d.
inversion Heqps'. inversion Heqps'. subst.
remember [(Γ0 ++ B :: Γ1, Δ3 ++ Δ4)] as ps''. destruct d1. inversion Heqps''.
inversion Heqps''. simpl. subst. rewrite dersrec_height_nil. simpl in IH.
rewrite dersrec_height_nil in IH. rewrite Nat.max_0_r. rewrite Nat.max_0_r in IH.
assert (E1: derrec_height d < S (Init.Nat.max (derrec_height d)(derrec_height d1))).
apply Nat.lt_succ_r. apply Nat.le_max_l.
assert (E2: derrec_height d = derrec_height d). auto.
assert ((ctr_L A (Γ0 ++ Γ1, Δ3 ++ A0 :: Δ4) x) + (ctr_R A (Γ0 ++ Γ1, Δ3 ++ A0 :: Δ4) x)).
auto.
pose (IH (derrec_height d) E1 (Γ0 ++ Γ1, Δ3 ++ A0 :: Δ4) d E2 x A H).
destruct s.
assert (E3: derrec_height d1 < S (Init.Nat.max (derrec_height d)(derrec_height d1))).
apply Nat.lt_succ_r. apply Nat.le_max_r.
assert (E4: derrec_height d1 = derrec_height d1). auto.
assert ((ctr_L A (Γ0 ++ B :: Γ1, Δ3 ++ Δ4) x0) + (ctr_R A (Γ0 ++ B :: Γ1, Δ3 ++ Δ4) x0)).
auto.
pose (IH (derrec_height d1) E3 (Γ0 ++ B :: Γ1, Δ3 ++ Δ4) d1 E4 x0 A H0).
destruct s.
pose (dlCons x1 (dlCons x2 d2)). pose (d0 d3). exists d4. simpl. rewrite dersrec_height_nil.
rewrite Nat.max_0_r. rewrite <- Nat.succ_le_mono. apply Nat.max_le_compat.
assumption. assumption. reflexivity. reflexivity. reflexivity.
(* KR *)
* inversion X. rewrite <- H4 in X. pose (KR_app_ctr_R _ _ _ _ ctr X).
apply KR in k0.
pose (derI (rules:=KS_rules) (prems:=fun _ : Seq => False)
(ps:=[(unboxed_list BΓ, [A0])]) sc k0). subst. simpl. pose (d0 d). exists d1.
simpl. rewrite <- Nat.succ_le_mono. left. }
Qed.
Theorem KS_hpadm_ctr_LR : forall s (D0 : KS_prv s),
(forall sc A, ((ctr_L A s sc) + (ctr_R A s sc)) ->
existsT2 (D1 : KS_prv sc),
derrec_height D1 <= derrec_height D0).
Proof.
intros.
assert (J0: derrec_height D0 = derrec_height D0). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) _ D0 J0 _ _ H).
auto.
Qed.
Theorem KS_hpadm_ctr_L : forall (k : nat) s
(D0 : KS_prv s),
k = (derrec_height D0) ->
(forall sc A, ((@ctr_L A s sc) ->
existsT2 (D1 : KS_prv sc),
derrec_height D1 <= k)).
Proof.
intros. intros. assert (H1: derrec_height D0 = derrec_height D0). reflexivity.
assert (H3 : (ctr_L A s sc) + (ctr_R A s sc)). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) s
D0 H1 sc A H3). destruct s0. exists x. lia.
Qed.
Theorem KS_hpadm_ctr_R : forall (k : nat) s
(D0 : KS_prv s),
k = (derrec_height D0) ->
(forall sc A, ((@ctr_R A s sc) ->
existsT2 (D1 : KS_prv sc),
derrec_height D1 <= k)).
Proof.
intros. intros. assert (H1: derrec_height D0 = derrec_height D0). reflexivity.
assert (H3 : (ctr_L A s sc) + (ctr_R A s sc)). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) s
D0 H1 sc A H3). destruct s0. exists x. lia.
Qed.
(* We can now prove that contraction of lists is also admissible. *)
Theorem KS_hpadm_list_ctr_L : forall Γ1 (k : nat) Γ0 Γ2 Γ3 Δ
(D0 : KS_prv (Γ0 ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3,Δ)),
k = (derrec_height D0) ->
existsT2 (D1 : KS_prv (Γ0 ++ Γ1 ++ Γ2 ++ Γ3,Δ)),
derrec_height D1 <= k.
Proof.
induction Γ1.
- intros. exists D0. rewrite H. auto.
- intros. assert (H0: derrec_height D0 = derrec_height D0). reflexivity.
assert (H1 : ctr_L a (Γ0 ++ (a :: Γ1) ++ Γ2 ++ (a :: Γ1) ++ Γ3, Δ) ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3, Δ)).
simpl. assert (Γ0 ++ a :: Γ1 ++ Γ2 ++ a :: Γ1 ++ Γ3 = Γ0 ++ a :: (Γ1 ++ Γ2) ++ a :: (Γ1 ++ Γ3)).
repeat rewrite <- app_assoc. reflexivity. rewrite H1.
assert ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3 = Γ0 ++ a :: (Γ1 ++ Γ2) ++ Γ1 ++ Γ3). repeat rewrite <- app_assoc.
reflexivity. rewrite H2. apply ctr_LI.
assert ((ctr_L a (Γ0 ++ (a :: Γ1) ++ Γ2 ++ (a :: Γ1) ++ Γ3, Δ) ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3, Δ)) +
(ctr_R a (Γ0 ++ (a :: Γ1) ++ Γ2 ++ (a :: Γ1) ++ Γ3, Δ) ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3, Δ))). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) (Γ0 ++ (a :: Γ1) ++ Γ2 ++ (a :: Γ1) ++ Γ3, Δ)
D0 H0 ((Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ1 ++ Γ3, Δ) a H2). destruct s.
assert (H3: derrec_height x = derrec_height x). reflexivity.
pose (IHΓ1 (derrec_height x) (Γ0 ++ [a]) Γ2 Γ3 Δ x H3). destruct s.
assert (Γ0 ++ (a :: Γ1) ++ Γ2 ++ Γ3 = (Γ0 ++ [a]) ++ Γ1 ++ Γ2 ++ Γ3). repeat rewrite <- app_assoc. auto.
rewrite H4. exists x0. lia.
Qed.
Theorem KS_hpadm_list_ctr_R : forall Δ1 (k : nat) Γ Δ0 Δ2 Δ3
(D0 : KS_prv (Γ,Δ0 ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3)),
k = (derrec_height D0) ->
existsT2 (D1 : KS_prv (Γ,Δ0 ++ Δ1 ++ Δ2 ++ Δ3)),
derrec_height D1 <= k.
Proof.
induction Δ1.
- intros. exists D0. rewrite H. auto.
- intros. assert (H0: derrec_height D0 = derrec_height D0). reflexivity.
assert (H1 : ctr_R a (Γ, Δ0 ++ (a :: Δ1) ++ Δ2 ++ (a :: Δ1) ++ Δ3) (Γ, (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3)).
simpl. assert (Δ0 ++ a :: Δ1 ++ Δ2 ++ a :: Δ1 ++ Δ3 = Δ0 ++ a :: (Δ1 ++ Δ2) ++ a :: (Δ1 ++ Δ3)).
repeat rewrite <- app_assoc. reflexivity. rewrite H1.
assert ((Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3 = Δ0 ++ a :: (Δ1 ++ Δ2) ++ Δ1 ++ Δ3). repeat rewrite <- app_assoc.
reflexivity. rewrite H2. apply ctr_RI.
assert ((ctr_L a (Γ, Δ0 ++ (a :: Δ1) ++ Δ2 ++ (a :: Δ1) ++ Δ3) (Γ, (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3)) +
(ctr_R a (Γ, Δ0 ++ (a :: Δ1) ++ Δ2 ++ (a :: Δ1) ++ Δ3) (Γ, (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3))). auto.
pose (@KS_hpadm_ctr_LR0 (derrec_height D0) (Γ, Δ0 ++ (a :: Δ1) ++ Δ2 ++ (a :: Δ1) ++ Δ3)
D0 H0 (Γ, (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ1 ++ Δ3) a H2). destruct s.
assert (H3: derrec_height x = derrec_height x). reflexivity.
pose (IHΔ1 (derrec_height x) Γ (Δ0 ++ [a]) Δ2 Δ3 x H3). destruct s.
assert (Δ0 ++ (a :: Δ1) ++ Δ2 ++ Δ3 = (Δ0 ++ [a]) ++ Δ1 ++ Δ2 ++ Δ3). repeat rewrite <- app_assoc. auto.
rewrite H4. exists x0. lia.
Qed.