From efd683d260c9daefaf9e2c9a437d2aa00e965d89 Mon Sep 17 00:00:00 2001 From: Wilmer Ricciotti Date: Fri, 29 May 2009 15:08:59 +0000 Subject: [PATCH] POPLmark part 1a using the de Bruijn encoding. --- .../matita/contribs/POPLmark/Fsub/defndb.ma | 465 ++++++++++++++++++ .../matita/contribs/POPLmark/Fsub/part1adb.ma | 173 +++++++ 2 files changed, 638 insertions(+) create mode 100644 helm/software/matita/contribs/POPLmark/Fsub/defndb.ma create mode 100644 helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma diff --git a/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma b/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma new file mode 100644 index 000000000..4a61bcb2f --- /dev/null +++ b/helm/software/matita/contribs/POPLmark/Fsub/defndb.ma @@ -0,0 +1,465 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Fsub/util.ma". +include "nat/le_arith.ma". +include "nat/lt_arith.ma". + +(*** representation of Fsub types ***) +inductive Typ : Set ≝ + | TVar : nat → Typ (* type var *) + | Top : Typ (* maximum type *) + | Arrow : Typ → Typ → Typ (* functions *) + | Forall : Typ → Typ → Typ. (* universal type *) + +(* representation of bounds *) + +record bound : Set ≝ { + istype : bool; (* is subtyping bound? *) + btype : Typ (* type to which the name is bound *) + }. + +(*** Type Well-Formedness judgement ***) + +inductive WFType : list bound → Typ → Prop ≝ + | WFT_TVar : ∀G,n,T.n < length ? G → (nth ? G (mk_bound true Top) n = mk_bound true T) → + WFType G (TVar n) + | WFT_Top : ∀G.WFType G Top + | WFT_Arrow : ∀G,T,U.WFType G T → WFType G U → WFType G (Arrow T U) + | WFT_Forall : ∀G,T,U.WFType G T → WFType (mk_bound true T::G) U → + WFType G (Forall T U). + +(*** Environment Well-Formedness judgement ***) + +inductive WFEnv : list bound → Prop ≝ + | WFE_Empty : WFEnv (nil ?) + | WFE_cons : ∀B,T,G.WFEnv G → WFType G T → WFEnv (mk_bound B T :: G). + +let rec lift T h k on T ≝ +match T with +[ TVar n ⇒ TVar (match (leb k n) with [true ⇒ n + h | false ⇒ n]) +| Top ⇒ Top +| Arrow U V ⇒ Arrow (lift U h k) (lift V h k) +| Forall U V ⇒ Forall (lift U h k) (lift V h (S k))]. + +(*** Subtyping judgement ***) +inductive JSubtype : list bound → Typ → Typ → Prop ≝ + | SA_Top : ∀G,T.WFEnv G → WFType G T → JSubtype G T Top + | SA_Refl_TVar : ∀G,n.WFEnv G → WFType G (TVar n) → JSubtype G (TVar n) (TVar n) + | SA_Trans_TVar : ∀G,n,T,U.n < length ? G → + nth ? G (mk_bound true Top) n = mk_bound true U → + JSubtype G (lift U (S n) O) T → JSubtype G (TVar n) T + | SA_Arrow : ∀G,S1,S2,T1,T2. JSubtype G T1 S1 → JSubtype G S2 T2 → + JSubtype G (Arrow S1 S2) (Arrow T1 T2) + | SA_All : ∀G,S1,S2,T1,T2. + JSubtype G T1 S1 → JSubtype (mk_bound true T1 :: G) S2 T2 → + JSubtype G (Forall S1 S2) (Forall T1 T2). + +notation "hvbox(e ⊢ break ta ⊴ break tb)" + non associative with precedence 30 for @{ 'subjudg $e $ta $tb }. +interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb). + +notation > "hvbox(\Forall S.T)" + non associative with precedence 60 for @{ 'forall $S $T}. +notation < "hvbox('All' \sub S. break T)" + non associative with precedence 60 for @{ 'forall $S $T}. +interpretation "universal type" 'forall S T = (Forall S T). + +notation "#x" with precedence 79 for @{'tvar $x}. +interpretation "bound tvar" 'tvar x = (TVar x). + +notation "⊤" with precedence 90 for @{'toptype}. +interpretation "toptype" 'toptype = Top. + +notation "hvbox(s break ⇛ t)" + right associative with precedence 55 for @{ 'arrow $s $t }. +interpretation "arrow type" 'arrow S T = (Arrow S T). + +notation "hvbox(⊴ T)" + non associative with precedence 60 for @{ 'subtypebound $T }. +interpretation "subtyping bound" 'subtypebound T = (mk_bound true T). + +(****** PROOFS ********) + +(*** theorems about lists ***) + +let rec flift f k on k ≝ match k with +[ O ⇒ f +| S p ⇒ flift (λn.match n with [ O ⇒ O | S m ⇒ S (f m) ]) p ]. + +let rec perm T f ≝ match T with +[ TVar m ⇒ TVar (f m) +| Top ⇒ Top +| Arrow U V ⇒ Arrow (perm U f) (perm V f) +| Forall U V ⇒ Forall (perm U f) (perm V (flift f 1))]. + +definition blift : bound → nat → bound ≝ +λB,n.match B with [ mk_bound b t ⇒ mk_bound b (lift t n O) ]. + +definition bperm : bound → (nat→nat) → bound ≝ +λB,f.match B with [ mk_bound b t ⇒ mk_bound b (perm t f) ]. + +definition incl : list bound → list bound → (nat → nat) → Prop ≝ +λG,H,f.injective ?? f → ∀n.n < length ? G → + bperm (blift (nth ? G (mk_bound true Top) n) (S n)) f = + blift (nth ? H (mk_bound true Top) (f n)) (S (f n)). + +lemma lift_lift : ∀T,n,m,k.lift (lift T n k) m k = lift T (n+m) k. +intros 3;elim T;simplify; +[apply (leb_elim k n1);intros;simplify; + [apply leb_elim;intros;simplify; + [apply eq_f;rewrite < assoc_plus;reflexivity + |elim H1;autobatch] + |rewrite > lt_to_leb_false + [simplify;reflexivity + |autobatch]] +|*:autobatch] +qed. + +lemma lift_O : ∀T,k.lift T O k = T. +intro;elim T;simplify +[cases (leb k n);simplify;autobatch paramodulation +|*:autobatch] +qed. + +lemma flift_flift : ∀h,k,f.flift (flift f h) k = flift f (h+k). +intros 2;elim h;simplify +[reflexivity +|rewrite > H;reflexivity] +qed. + +lemma eq_f_g_to_eq_fx_gx : ∀A,B:Type.∀f,g:A → B.∀x.f = g → f x = g x. +intros;rewrite > H;reflexivity; +qed. + +lemma flift_S : ∀n,m,f.flift f (S n) (S m) = S (flift f n m). +intros 2;elim n +[reflexivity +|cut (flift f (S (S n1)) (S m) = flift (flift f (S n1)) 1 (S m)) + [rewrite > Hcut;simplify;reflexivity + |change in match (S (S n1)) with (1 + (S n1));rewrite > sym_plus; + apply eq_f_g_to_eq_fx_gx;symmetry;apply flift_flift]] +qed. + +lemma le_flift : ∀k,n.k ≤ n → ∀f.k ≤ flift f k n. +intro;elim k +[autobatch +|cut (∃p.n1 = S p) + [elim Hcut;rewrite > H2;rewrite > flift_S;apply le_S_S;apply H; + rewrite > H2 in H1;autobatch + |elim H1 + [exists[apply n] + reflexivity + |elim H3;exists[apply (S a)] + apply eq_f;assumption]]] +qed. + +lemma le_flift2 : ∀k,n.n < k → ∀f.flift f k n = n. +intro;elim k +[elim (not_le_Sn_O ? H) +|generalize in match H1;cases n1;intros + [cut (flift f (S n) O = flift (flift f n) 1 O) + [rewrite > Hcut;reflexivity + |apply eq_f_g_to_eq_fx_gx;autobatch paramodulation] + |rewrite > flift_S;apply eq_f;apply H;autobatch]] +qed. + +lemma lift_perm : ∀T,n,f,k.perm (lift T (S n) k) (flift f (S k)) = lift (perm (lift T n k) (flift f k)) 1 k. +intros 2;elim T;simplify; +[apply (leb_elim k n1);simplify;intros + [apply eq_f;change in ⊢ (??(?%??)?) with (flift f 1); + cut (flift (flift f 1) k (n1+S n) = flift (flift f k) 1 (n1+S n)) + [rewrite > Hcut;rewrite < plus_n_Sm;simplify; + apply (leb_elim k (flift f k (n1+n)));simplify;intros + [rewrite > sym_plus in ⊢ (???%);simplify;reflexivity + |elim H1;elim k in H + [autobatch + |apply le_flift;autobatch]] + |apply eq_f_g_to_eq_fx_gx;autobatch paramodulation] + |apply eq_f;change in ⊢ (??(?%??)?) with (flift f 1); + rewrite > le_flift2 [|autobatch] + apply (leb_elim k (flift f k n1));simplify;intro + [rewrite > le_flift2 in H1 [|autobatch] + elim (H H1) + |symmetry;apply le_flift2;autobatch]] +|reflexivity +|apply eq_f2;change in ⊢ (? ? (? ? (? % ?)) ?) with (flift f 1); + rewrite > flift_flift;simplify in ⊢ (? ? (? ? (? ? %)) ?);autobatch +|apply eq_f2 + [change in ⊢ (? ? (? ? (? % ?)) ?) with (flift f 1); + rewrite > flift_flift;simplify in ⊢ (? ? (? ? (? ? %)) ?);autobatch + |change in ⊢ (??(??%)?) with (flift (flift (flift f 1) k) 1); + rewrite > flift_flift in ⊢ (??%?); + rewrite > sym_plus in ⊢ (? ? (? ? (? ? %)) ?); + rewrite > flift_flift; + simplify in ⊢ (? ? (? ? (? ? %)) ?); + rewrite > H1;do 2 apply eq_f_g_to_eq_fx_gx; + apply eq_f;apply eq_f; + change in ⊢ (???%) with (flift (flift f k) 1); + rewrite > flift_flift;rewrite > sym_plus;reflexivity]] +qed. + +lemma blift_bperm : ∀B,n,f.bperm (blift B (S n)) (flift f 1) = blift (bperm (blift B n) f) 1. +intros;cases B;simplify;apply eq_f; +change in ⊢ (? ? ? (? (? ? %) ? ?)) with (flift f O); +apply lift_perm; +qed. + +definition lifter : nat → nat → nat → nat ≝ + λn,k,m.match (leb k m) with + [ true ⇒ m+n + | false ⇒ m ]. + +lemma extensional_perm : ∀T.∀f,g.(∀x.f x = g x) → perm T f = perm T g. +intro;elim T +[4:whd in ⊢ (??%%);cut (∀x.flift f 1 x = flift g 1 x) + [autobatch + |intro;simplify;cases x + [reflexivity + |simplify;rewrite > H2;reflexivity]] +|*:simplify;autobatch] +qed. + +lemma flift_lifter : ∀p,n,m,k.flift (lifter n k) p m = lifter n (k+p) m. +intro;elim p +[simplify;autobatch paramodulation +|change in ⊢ (? ? (? ? % ?) ?) with (1+n); + rewrite < plus_n_Sm;whd in ⊢ (???%); + transitivity (flift (flift (lifter n1 k) n) 1 m) + [apply eq_f_g_to_eq_fx_gx;rewrite > sym_plus;autobatch + |unfold lifter;simplify; + change in ⊢ (? ? match ? return ? with [_⇒?|_⇒λ_:?.? (? % ? ?)] ?) with (lifter n1 k); + cases m + [simplify;reflexivity + |simplify;rewrite > H;unfold lifter;cases (leb (k+n) n2);reflexivity]]] +qed. + +lemma lift_perm2 : ∀T,n,k.lift T n k = perm T (lifter n k). +intros 2;elim T;simplify +[1,2,3:autobatch +|rewrite < H;change in ⊢ (???(??(??%))) with (flift (lifter n k) 1); + rewrite > H1; + rewrite > (extensional_perm ? (lifter n (S k)) (flift (lifter n k) 1)) + [reflexivity + |intro;symmetry;autobatch]] +qed. + +lemma incl_cons : ∀G,H,f,T.injective ?? f → incl G H f → + incl (⊴ T::G) (⊴ perm T f :: H) (flift f 1). +intros;unfold;intros 2; +elim n; +[simplify;change in ⊢ (? ? (? ? (? ? %)) ?) with (flift f 1); + rewrite > lift_perm;rewrite > lift_O;reflexivity +|simplify in H5;lapply (le_S_S_to_le ?? H5);clear H5; + simplify in ⊢ (? ? ? (? % ?)); + simplify in ⊢ (? ? (? (? % ?) ?) ?); + unfold in H2;rewrite > (blift_bperm ? ? f); + rewrite > (H2 ?? Hletin); + [cases (nth bound H (mk_bound true Top) (f n1)); + simplify;rewrite > lift_lift;rewrite > sym_plus; + reflexivity + |assumption]] +qed. + +lemma injective_flift : ∀f,n.injective ?? f → injective ?? (flift f n). +intros;elim n +[simplify;assumption +|change in ⊢ (? ? ? (? ? %)) with (1+n1);rewrite > sym_plus; + rewrite < flift_flift;unfold;intros 2; + cases (decidable_eq_nat x 0) + [rewrite > le_flift2 + [cases (decidable_eq_nat y 0) + [intro;autobatch paramodulation + |elim y in H3 + [elim H3;reflexivity + |simplify in H5;destruct]] + |rewrite > H2;autobatch] + |generalize in match H2;cases x + [intros;elim H3;reflexivity + |intro;cases y;simplify;intros;destruct; + rewrite > (H1 ?? Hcut);reflexivity]]] +qed. + +lemma injective_lifter : ∀n,k.injective ?? (lifter n k). +intros;unfold;intros;unfold lifter in H; +apply (leb_elim k x);intros; +[rewrite > (le_to_leb_true ?? H1) in H;apply (leb_elim k y);intros; + [rewrite > (le_to_leb_true ?? H2) in H;simplify in H; + autobatch + |lapply (not_le_to_lt ?? H2) as H3;rewrite > (lt_to_leb_false ?? H3) in H; + simplify in H;rewrite < H in H2;elim H2;autobatch] +|lapply (not_le_to_lt ?? H1) as H2;rewrite > (lt_to_leb_false ?? H2) in H; + apply (leb_elim k y);intros + [rewrite > (le_to_leb_true ?? H3) in H;simplify in H;rewrite > H in H1; + elim H1;autobatch + |lapply (not_le_to_lt ?? H3) as H4;rewrite > (lt_to_leb_false ?? H4) in H; + simplify in H;assumption]] +qed. + +lemma incl_append : ∀G,H. incl G (H@G) (lifter (length ? H) O). +intros;unfold;intros; +cut (nth ? G (⊴ ⊤) n = nth ? (H@G) (⊴ ⊤) (lifter (length ? H) O n)) +[rewrite < Hcut;cases (nth bound G (⊴ ⊤) n);simplify; + rewrite < lift_perm2;rewrite > lift_lift;reflexivity +|elim H + [simplify;rewrite < plus_n_O;reflexivity + |simplify;rewrite < plus_n_Sm;apply H3]] +qed. + +lemma flift_id : ∀m,n.flift (λx.x) m n = n. +intro;elim m +[reflexivity +|change in ⊢ (??(??%?)?) with (1+n);rewrite > sym_plus; + transitivity (flift (flift (λx.x) n) 1 n1) + [apply eq_f_g_to_eq_fx_gx;autobatch + |simplify;generalize in match H;cases n1;intro + [reflexivity + |simplify;apply eq_f;apply H1]]] +qed. + +lemma perm_id : ∀T,n.T = perm T (flift (λx.x) n). +intro;elim T; +[1:simplify;rewrite > flift_id;reflexivity +|4:whd in ⊢ (???%);rewrite > flift_flift;rewrite < H1;rewrite < H;reflexivity +|*:simplify;autobatch] +qed. + +lemma perm_compose : ∀T,f,g.perm (perm T f) g = perm T (λx.g (f x)). +intro;elim T +[reflexivity +|reflexivity +|simplify;autobatch +|simplify;rewrite > H; + change in ⊢ (? ? (? ? (? (? ? %) ?)) ?) with (flift f 1); + change in ⊢ (? ? (? ? (? ? %)) ?) with (flift g 1); + rewrite > H1; + change in ⊢ (? ? ? (? ? (? ? %))) with (flift (λx.g (f x)) 1); + rewrite > (extensional_perm ? (λx.flift g 1 (flift f 1 x)) (flift (λx.g (f x)) 1)); + [reflexivity + |intros;cases x;simplify;reflexivity]] +qed. + +lemma WFT_env_incl : ∀G,T.WFType G T → ∀H,f.injective nat nat f → incl G H f → + (∀n. n < length ? G → f n < length ? H) → + WFType H (perm T f). +intros 3;elim H +[simplify;unfold in H5;lapply (H5 H4 n H1); + cut (∃T.nth ? H3 (mk_bound true Top) (f n) = mk_bound true T) + [elim Hcut;apply WFT_TVar + [apply a + |*:autobatch] + |rewrite > H2 in Hletin;simplify in Hletin; + elim (nth bound H3 (mk_bound true Top) (f n)) in Hletin;elim b in H7 + [exists[apply t1] + reflexivity + |simplify in H7;destruct]] +|2:simplify;autobatch +|simplify;autobatch width=4 size=9 +|simplify;apply WFT_Forall + [autobatch + |apply H4 + [change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption + |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption + |intro;cases n;simplify;intros;autobatch depth=4]]] +qed. + +lemma WFT_env_incl2: ∀G,T.WFType G T → ∀H.length ? G = length ? H → +(∀n,U.n < length ? G → nth ? G (mk_bound true Top) n = mk_bound true U → + ∃V.nth ? H (mk_bound true Top) n = mk_bound true V) → + WFType H T. +intros 3;elim H +[elim (H5 n t) + [apply WFT_TVar + [2:applyS H1 + |3:apply H6] + |assumption + |assumption] +|autobatch +|apply WFT_Arrow;autobatch +|apply WFT_Forall;try autobatch; + apply H4; + [simplify;autobatch + |intros;elim n in H8 H9 + [exists[apply t] + reflexivity + |elim (H7 n1 U ? H10) + [exists[apply a] + assumption + |apply le_S_S_to_le;apply H9]]]] +qed. + +lemma WFT_extends : ∀G,H,U,P,T.WFType (G@(mk_bound true U::H)) T → WFType (G@(mk_bound true P::H)) T. +intros;apply (WFT_env_incl2 ?? H1) +[elim G;simplify + [reflexivity + |rewrite > H2;reflexivity] +|intros 3;elim (decidable_eq_nat n (length ? G)) + [exists [apply P] + elim G in n H3 + [simplify in H4;destruct;reflexivity + |simplify;simplify in H5;rewrite > H5;simplify;apply H3;reflexivity] + |exists [apply U1] + elim G in n H3 H4 0 + [simplify;intro;elim n1 + [elim H3;reflexivity + |simplify in H5;simplify;assumption] + |simplify;intros 4;elim n1 + [simplify in H5;simplify;assumption + |simplify;apply H3 + [intro;elim H5;autobatch + |apply H6]]]]] +qed. + +lemma WFE_extends : ∀G,H,U,P.WFType H P → WFEnv (G@(mk_bound true U::H)) → WFEnv (G@(mk_bound true P::H)). +intros;cut (WFType H U) +[generalize in match H2;elim G 0;simplify;intros + [inversion H3;intros;destruct;autobatch + |generalize in match H4;cases a;intros;apply WFE_cons + [inversion H4;intros;destruct;autobatch + |inversion H5;intros;destruct;autobatch]] +|elim G in H2 0;simplify;intros; + [inversion H2;intros;destruct;assumption + |apply H2;inversion H3;simplify;intros;destruct;assumption]] +qed. + +(*** lemmata relating subtyping and well-formedness ***) + +lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → WFEnv G. +intros;elim H;assumption. +qed. + +lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → WFType G T ∧ WFType G U. +intros;elim H + [1,2:autobatch + |elim H4;split;autobatch + |decompose;autobatch size=7 + |decompose;split + [apply WFT_Forall; + [assumption + |apply (WFT_env_incl2 ?? H2) [reflexivity] + simplify;intros 3;elim n + [exists[apply t] + reflexivity + |exists[apply U1] + assumption]] + |autobatch]] +qed. + +lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → WFType G T. +intros;elim (JS_to_WFT ? ? ? H);assumption; +qed. + +lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → WFType G U. +intros;elim (JS_to_WFT ? ? ? H);assumption; +qed. diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma new file mode 100644 index 000000000..3b0b677b7 --- /dev/null +++ b/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma @@ -0,0 +1,173 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "Fsub/defndb.ma". +include "nat/lt_arith.ma". +include "nat/le_arith.ma". + +(*** Lemma A.1 (Reflexivity) ***) +theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴ T. +intros 3;elim H;autobatch depth=4 size=7; +qed. + +(* + * A slightly more general variant to lemma A.2.2, where weakening isn't + * defined as concatenation of any two disjoint environments, but as + * set inclusion. + *) + +lemma JS_weakening : ∀G,T,U.G ⊢ T ⊴ U → ∀H.WFEnv H → + ∀f. injective nat nat f → + (∀n:ℕ.n H2 in Hletin1;simplify in Hletin1; + cut (∃t.nth bound H5 (mk_bound true Top) (f n) = mk_bound true t) + [elim Hcut;rewrite > H10 in Hletin1;simplify in Hletin1;destruct; + rewrite > Hcut1 in Hletin;apply (SA_Trans_TVar ?????? Hletin);autobatch + |elim (nth bound H5 (mk_bound true Top) (f n)) in Hletin1; + elim b in H10;simplify in H10;destruct;exists [apply t2] + reflexivity] + |*:assumption] + |simplify;apply SA_Arrow;autobatch width=4 + |simplify;apply (SA_All ? ? ? ? ? (H2 ? H6 ?? H8 H9)) + [assumption + |apply H4 + [apply WFE_cons + [assumption + |lapply (H2 ? H6 ? H7);autobatch] + |change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption + |intro;cases n;simplify;intros;autobatch depth=4 + |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption]]] +qed. + +inverter JS_indinv for JSubtype (%?%). + +theorem narrowing:∀G,G1,U,P,M,N. + G1 ⊢ P ⊴ U → + (∀G2,S,T. + G2@G1 ⊢ S ⊴ lift U (length ? G2) O → + G2@G1 ⊢ lift U (length ? G2) O ⊴ T \to + G2@G1 ⊢ S ⊴ T) → + G ⊢ M ⊴ N → + ∀l.G=l@(mk_bound true U::G1) → l@(mk_bound true P::G1) ⊢ M ⊴ N. +intros 9;elim H2;destruct;try autobatch depth=4 size=7; +elim (decidable_eq_nat n (length ? l1)) +[apply (SA_Trans_TVar ??? P); + [elim l1 in n H7 + [rewrite > H7;simplify;autobatch + |rewrite > H8;simplify;apply le_S_S;apply H7;reflexivity] + |elim l1 in n H4 H7 + [rewrite > H7;reflexivity + |rewrite > H8;simplify;apply H4 + [rewrite > H8 in H7;apply H7 + |reflexivity]] + |cut (U = t1) + [change in ⊢ (? (? ? ? %) ? ?) with ([mk_bound true P]@G1); + cut (S n = length ? (l1@[mk_bound true P])) + [rewrite > Hcut1;rewrite < associative_append;apply H1;rewrite < Hcut1; + rewrite > Hcut;rewrite > associative_append; + [do 2 rewrite > lift_perm2;rewrite < Hcut; + apply (JS_weakening ??? H) + [simplify;autobatch + |autobatch + |intros;simplify;change in ⊢ (??(??%)) with (l1@[⊴P]@G1); + rewrite < associative_append; + rewrite > length_append;rewrite < Hcut1;rewrite < sym_plus; + autobatch + |applyS incl_append] + |apply H6;reflexivity] + |elim l1 in n H7 + [simplify;rewrite > H7;reflexivity + |simplify;rewrite > H8;rewrite < H7 + [simplify;apply refl_eq + |skip + |reflexivity]]] + |elim l1 in n H7 H4;destruct; + [simplify in H4;destruct;reflexivity + |simplify in H7;apply H4 + [2:apply H7 + |skip + |reflexivity]]]] +|apply (SA_Trans_TVar ??? t1) + [cut (length ? (l1@⊴ P :: G1) = length ? (l1@⊴U::G1)) + [rewrite > Hcut;assumption + |elim l1;simplify;autobatch] + |rewrite < H4;elim l1 in n H7 0 + [simplify;intro;cases n1;intros + [elim H7;reflexivity + |reflexivity] + |simplify;intros 4;elim n1 + [simplify;reflexivity + |simplify;apply H7;intro;elim H9;autobatch]] + |apply H6;reflexivity]] +qed. + +lemma JS_trans_prova: ∀T,G1.WFType G1 T → +∀G,R,U,f.injective ?? f → length ? G1 ≤ length ? G → G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U. +intros 3;elim H;clear H; try autobatch; + [simplify in H5;simplify in H6;elim H5 using JS_indinv;destruct;autobatch + |simplify in H4;inversion H4; intros; destruct; assumption + |simplify in H7;elim H7 using JS_indinv;intros;destruct; + [autobatch + |simplify in H8;inversion H8;intros;destruct; + [apply SA_Top;autobatch; + |apply SA_Arrow + [apply (H2 ?????? H12 H);assumption + |apply (H4 ?????? H10 H14);assumption]]] + |simplify in H7;elim H7 using JS_indinv;intros;destruct; + [autobatch + |simplify in H8;inversion H8;intros;destruct; + [apply SA_Top;autobatch + |apply SA_All + [apply (H2 ?????? H12 H);assumption + |apply H4 + [3:simplify;apply le_S_S;assumption + |4:apply (narrowing (mk_bound true (perm t f)::G) G ???? H12 ? H10 []) + [intros;rewrite > lift_perm2 in H16;rewrite > lift_perm2 in H17; + rewrite > perm_compose in H16; rewrite > perm_compose in H17; + apply H2 + [3:apply (trans_le ??? H6);rewrite > length_append;autobatch + |4:apply H16 + |5:apply H17 + |2:apply injective_compose;autobatch] + |reflexivity] + |5:assumption + |2:change in ⊢ (???%) with (flift f 1);autobatch]]]]] +qed. + +theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V. +intros 4;rewrite > (perm_id ? 0) in ⊢ (???% → ??%? → ?); +intros;apply (JS_trans_prova ????????? H H1) +[apply G +|rewrite < perm_id in H;autobatch +|simplify;intros;assumption +|apply le_n] +qed. + +theorem JS_narrow : ∀G1,G2,P,Q,T,U. + (G2 @ (mk_bound true Q :: G1)) ⊢ T ⊴ U → G1 ⊢ P ⊴ Q → + (G2 @ (mk_bound true P :: G1)) ⊢ T ⊴ U. +intros; apply (narrowing ? ? ? ? ? ? H1 ? H) [|autobatch] +intros;autobatch; +qed. -- 2.39.2