- change in the notation of relatiional relocation and local env.
slicing, to allow more usual notation for functional relocation (not
working yet)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic_2/substitution/ldrop.ma".
+
+(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
+
+definition CP1 ≝ λRR:lenv→relation term. λRS:relation term.
+ ∀L,k. NF … (RR L) RS (⋆k).
+
+definition CP2 ≝ λRR:lenv→relation term. λRS:relation term.
+ ∀L,K,W,i. ⇓[0,i] L ≡ K. 𝕓{Abst} W → NF … (RR L) RS (#i).
+
+definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term.
+ ∀L,V,k. RP L (𝕔{Appl}⋆k.V) → RP L V.
+
+(* requirements for abstract computation properties *)
+record acp (RR:lenv->relation term) (RS:relation term) (RP:lenv→predicate term) : Prop ≝
+{ cp1: CP1 RR RS;
+ cp2: CP2 RR RS;
+ cp3: CP3 RR RP
+}.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic_2/static/aaa.ma".
+include "Basic_2/computation/lsubc.ma".
+
+(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
+
+(* Main propertis ***********************************************************)
+
+axiom aacr_aaa_csubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+ ∀L1,T,A. L1 ⊢ T ÷ A →
+ ∀L2. L2 [RP] ⊑ L1 → {L2, T} [RP] ϵ 〚A〛.
+(*
+#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
+[ #L #k #L2 #HL2
+ lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom
+ @(s2 … HAtom … ◊) // /2 width=2/
+| * #L #K #V #B #i #HLK #_ #IHB #L2 #HL2
+ [
+ | lapply (aacr_acr … H1RP H2RP B) #HB
+ @(s2 … HB … ◊) //
+ @(cp2 … H1RP)
+| #L #V #T #B #A #_ #_ #IHB #IHA #L2 #HL2
+ lapply (aacr_acr … H1RP H2RP A) #HA
+ lapply (aacr_acr … H1RP H2RP B) #HB
+ lapply (s1 … HB) -HB #HB
+ @(s5 … HA … ◊ ◊) // /3 width=1/
+| #L #W #T #B #A #_ #_ #IHB #IHA #L2 #HL2
+ lapply (aacr_acr … H1RP H2RP B) #HB
+ lapply (s1 … HB) -HB #HB
+ @(aacr_abst … H1RP H2RP) /3 width=1/ -HB /4 width=3/
+| /3 width=1/
+| #L #V #T #A #_ #_ #IH1A #IH2A #L2 #HL2
+ lapply (aacr_acr … H1RP H2RP A) #HA
+ lapply (s1 … HA) #H
+ @(s6 … HA … ◊) /2 width=1/ /3 width=1/
+]
+*)
+lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+ ∀L,T,A. L ⊢ T ÷ A → RP L T.
+#RR #RS #RP #H1RP #H2RP #L #T #A #HT
+lapply (aacr_acr … H1RP H2RP A) #HA
+@(s1 … HA) /2 width=4/
+qed.
(**************************************************************************)
include "Basic_2/grammar/aarity.ma".
-include "Basic_2/grammar/lenv.ma".
+include "Basic_2/grammar/term_simple.ma".
+include "Basic_2/substitution/lift_vector.ma".
+include "Basic_2/computation/acp.ma".
-(* ABSTRACT CANDIDATES OF REDUCIBILITY **************************************)
+(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
+
+(* Note: this is Girard's CR1 *)
+definition S1 ≝ λRP,C:lenv→predicate term.
+ ∀L,T. C L T → RP L T.
+
+(* Note: this is Tait's iii, or Girard's CR4 *)
+definition S2 ≝ λRR:lenv→relation term. λRS:relation term. λRP,C:lenv→predicate term.
+ ∀L,Vs. all … (RP L) Vs →
+ ∀T. 𝕊[T] → NF … (RR L) RS T → C L (ⒶVs.T).
+
+(* Note: this is Tait's ii *)
+definition S3 ≝ λRP,C:lenv→predicate term.
+ ∀L,Vs,V,T,W. C L (ⒶVs. 𝕔{Abbr}V. T) → RP L W → C L (ⒶVs. 𝕔{Appl}V. 𝕔{Abst}W. T).
+
+definition S5 ≝ λRP,C:lenv→predicate term.
+ ∀L,V1s,V2s. ⇑[0, 1] V1s ≡ V2s →
+ ∀V,T. C (L. 𝕓{Abbr}V) (ⒶV2s. T) → RP L V → C L (ⒶV1s. 𝕔{Abbr}V. T).
+
+definition S6 ≝ λRP,C:lenv→predicate term.
+ ∀L,Vs,T,W. C L (ⒶVs. T) → RP L W → C L (ⒶVs. 𝕔{Cast}W. T).
+
+definition S7 ≝ λC:lenv→predicate term. ∀L1,L2,T1,T2,d,e.
+ C L1 T1 → ⇓[d, e] L2 ≡ L1 → ⇑[d, e] T1 ≡ T2 → C L2 T2.
+
+(* properties of the abstract candidate of reducibility *)
+record acr (RR:lenv->relation term) (RS:relation term) (RP,C:lenv→predicate term) : Prop ≝
+{ s1: S1 RP C;
+ s2: S2 RR RS RP C;
+ s3: S3 RP C;
+ s5: S5 RP C;
+ s6: S6 RP C;
+ s7: S7 C
+}.
(* the abstract candidate of reducibility associated to an atomic arity *)
-let rec acr (R:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝
+let rec aacr (RP:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝
λT. match A with
-[ AAtom ⇒ R L T
-| APair B A ⇒ ∀V. acr R B L V → acr R A L (𝕔{Appl} V. T)
+[ AAtom ⇒ RP L T
+| APair B A ⇒ ∀V. aacr RP B L V → aacr RP A L (𝕔{Appl} V. T)
].
interpretation
- "candidate of reducibility (abstract)"
- 'InEInt R L T A = (acr R A L T).
+ "candidate of reducibility of an atomic arity (abstract)"
+ 'InEInt RP L T A = (aacr RP A L T).
+
+(* Basic properties *********************************************************)
+
+axiom aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+ ∀A. acr RR RS RP (aacr RP A).
+(*
+#RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
+#B #A #IHB #IHA @mk_acr normalize
+[ #L #T #H
+ lapply (H (⋆0) ?) -H [ @(s2 … IHB … ◊) // /2 width=2/ ] #H
+ @(cp3 … H1RP … 0) @(s1 … IHA) //
+| #L #Vs #HVs #T #H1T #H2T #V #HB
+ lapply (s1 … IHB … HB) #HV
+ @(s2 … IHA … (V :: Vs)) // /2 width=1/
+| #L #Vs #V #T #W #HA #HW #V0 #HB
+ @(s3 … IHA … (V0 :: Vs)) // /2 width=1/
+| #L #V1s #V2s #HV12s #V #T #HA #HV #V1 #HB
+ elim (lift_total V1 0 1) #V2 #HV12
+ @(s5 … IHA … (V1 :: V1s) (V2 :: V2s)) // /2 width=1/
+ @HA @(s7 … IHB … HB … HV12) /2 width=1/
+| #L #Vs #T #W #HA #HW #V0 #HB
+ @(s6 … IHA … (V0 :: Vs)) // /2 width=1/
+| #L1 #L2 #T1 #T2 #d #e #HA #HL21 #HT12 #V2 #HB
+ @(s7 … IHA … HL21) [2: @HA [2:
+]
+qed.
+*)
+lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+ ∀L,W,T,A,B. RP L W →
+ (∀V. {L, V} [RP] ϵ 〚B〛 → {L. 𝕓{Abbr}V, T} [RP] ϵ 〚A〛) →
+ {L, 𝕓{Abst}W. T} [RP] ϵ 〚𝕔B. A〛.
+#RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #V #HB
+lapply (aacr_acr … H1RP H2RP A) #HCA
+lapply (aacr_acr … H1RP H2RP B) #HCB
+lapply (s1 … HCB) -HCB #HCB
+@(s3 … HCA … ◊) // @(s5 … HCA … ◊ ◊) // /2 width=1/
+qed.
(**************************************************************************)
include "Basic_2/reducibility/cpr.ma".
+include "Basic_2/computation/acp.ma".
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
interpretation
"context-sensitive strong normalization (term)"
'SN L T = (csn L T).
+
+(* Basic properties *********************************************************)
+
+axiom csn_acp: acp cpr (eq …) (csn …).
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic_2/computation/acp_aaa.ma".
+include "Basic_2/computation/csn_cr.ma".
+
+(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
+
+(* Main properties **********************************************************)
+
+theorem csn_aaa: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⇓ T.
+#L #T #A #H
+@(acp_aaa … csn_acp csn_acr … H)
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "Basic_2/static/aaa.ma".
-include "Basic_2/computation/csn_cr.ma".
-include "Basic_2/computation/lsubcs.ma".
-
-(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-
-(* Main propertis ***********************************************************)
-
-axiom snc_aarity_csubcs: ∀L1,T,A. L1 ⊢ T ÷ A → ∀L2. L2 ⊑ L1 → {L2, T} ϵ 〚A〛.
-
-lemma snc_aarity: ∀L,T,A. L ⊢ T ÷ A → {L, T} ϵ 〚A〛.
-/2 width=3/ qed.
-
-axiom csn_arity: ∀L,T,A. L ⊢ T ÷ A → L ⊢ ⇓ T.
(* CONTEXT-SENSITIVE STRONGLY NORMALIZING TERMS *****************************)
-(* the candidate of reducibility associated to an atomic arity *)
-definition snc: aarity → lenv → predicate term ≝ acr csn.
+(* Advanced properties ******************************************************)
-interpretation
- "candidate of reducibility (contex-sensitive strong normalization)"
- 'InEInt L T A = (snc A L T).
+axiom csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⇓ T).
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
-inductive lsubc (R:lenv→predicate term) : relation lenv ≝
-| lsubc_atom: lsubc R (⋆) (⋆)
-| lsubc_pair: ∀I,L1,L2,V. lsubc R L1 L2 → lsubc R (L1. 𝕓{I} V) (L2. 𝕓{I} V)
-| lsubc_abbr: ∀L1,L2,V,W,A. R ⊢ {L1, V} ϵ 〚A〛 → R ⊢ {L2, W} ϵ 〚A〛 →
- lsubc R L1 L2 → lsubc R (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
+inductive lsubc (RP:lenv→predicate term): relation lenv ≝
+| lsubc_atom: lsubc RP (⋆) (⋆)
+| lsubc_pair: ∀I,L1,L2,V. lsubc RP L1 L2 → lsubc RP (L1. 𝕓{I} V) (L2. 𝕓{I} V)
+| lsubc_abbr: ∀L1,L2,V,W,A. {L1, V} [RP] ϵ 〚A〛 → {L2, W} [RP] ϵ 〚A〛 →
+ lsubc RP L1 L2 → lsubc RP (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
.
interpretation
"local environment refinement (abstract candidates of reducibility)"
- 'CrSubEq L1 R L2 = (lsubc R L1 L2).
+ 'CrSubEq L1 RP L2 = (lsubc RP L1 L2).
(* Basic properties *********************************************************)
-lemma lsubc_refl: ∀R,L. L [R] ⊑ L.
-#R #L elim L -L // /2 width=1/
+lemma lsubc_refl: ∀RP,L. L [RP] ⊑ L.
+#RP #L elim L -L // /2 width=1/
qed.
(* Basic inversion lemmas ***************************************************)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 "Basic_2/computation/lsubc.ma".
-include "Basic_2/computation/csn.ma".
-
-(* LOCAL ENVIRONMENT REFINEMENT FOR STRONG NORMALIZATION ********************)
-
-definition lsubcs: relation lenv ≝ lsubc csn.
-
-interpretation
- "local environment refinement (strong normalization)"
- 'CrSubEq L1 L2 = (lsubcs L1 L2).
-
-(* Basic properties *********************************************************)
-
-lemma lsubcs_refl: ∀L. L ⊑ L.
-// qed.
-
-(* Basic inversion lemmas ***************************************************)
(* Main properties **********************************************************)
-theorem flift_lift: â\88\80T,d,e. â\86\91[d, e] T â\89¡ â\86\9f[d, e] T.
+theorem flift_lift: â\88\80T,d,e. â\87\91[d, e] T â\89¡ â\86\91[d, e] T.
#T elim T -T
[ * #i #d #e //
elim (lt_or_eq_or_gt i d) #Hid normalize
(* Main inversion properties ************************************************)
-theorem flift_inv_lift: â\88\80d,e,T1,T2. â\86\91[d, e] T1 â\89¡ T2 â\86\92 â\86\9f[d, e] T1 = T2.
+theorem flift_inv_lift: â\88\80d,e,T1,T2. â\87\91[d, e] T1 â\89¡ T2 â\86\92 â\86\91[d, e] T1 = T2.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
[ #i #d #e #Hid >(tri_lt ?????? Hid) //
| #i #d #e #Hid
(* Derived properties *******************************************************)
-lemma flift_join: â\88\80e1,e2,T. â\86\91[e1, e2] â\86\9f[0, e1] T â\89¡ â\86\9f[0, e1 + e2] T.
+lemma flift_join: â\88\80e1,e2,T. â\87\91[e1, e2] â\86\91[0, e1] T â\89¡ â\86\91[0, e1 + e2] T.
#e1 #e2 #T
lapply (flift_lift T 0 (e1+e2)) #H
elim (lift_split … H e1 e1 ? ? ?) -H // #U #H
let rec fsubst W d U on U ≝ match U with
[ TAtom I ⇒ match I with
[ Sort _ ⇒ U
- | LRef i â\87\92 tri â\80¦ i d (#i) (â\86\9f[0, i] W) (#(i-1))
+ | LRef i â\87\92 tri â\80¦ i d (#i) (â\86\91[0, i] W) (#(i-1))
| GRef _ ⇒ U
]
| TPair I V T ⇒ match I with
(* Main properties **********************************************************)
theorem fsubst_delift: ∀K,V,T,L,d.
- â\86\93[0, d] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 L â\8a¢ T [d, 1] â\89¡ â\86¡[d ← V] T.
+ â\87\93[0, d] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 L â\8a¢ T [d, 1] â\89¡ â\86\93[d ← V] T.
#K #V #T elim T -T
[ * #i #L #d #HLK normalize in ⊢ (? ? ? ? ? %); /2 width=3/
elim (lt_or_eq_or_gt i d) #Hid
(* Main inversion properties ************************************************)
-theorem fsubst_inv_delift: â\88\80K,V,T1,L,T2,d. â\86\93[0, d] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92
- L â\8a¢ T1 [d, 1] â\89¡ T2 â\86\92 â\86¡[d ← V] T1 = T2.
+theorem fsubst_inv_delift: â\88\80K,V,T1,L,T2,d. â\87\93[0, d] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92
+ L â\8a¢ T1 [d, 1] â\89¡ T2 â\86\92 â\86\93[d ← V] T1 = T2.
#K #V #T1 elim T1 -T1
[ * #i #L #T2 #d #HLK #H
[ -HLK >(delift_fwd_sort1 … H) -H //
]
]
qed-.
-
\ No newline at end of file
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic_2/grammar/term.ma".
+
+(* TERMS ********************************************************************)
+
+let rec applv Vs T on Vs ≝
+ match Vs with
+ [ nil ⇒ T
+ | cons hd tl ⇒ 𝕔{Appl} hd. (applv tl T)
+ ].
+
+interpretation "application construction (vector)" 'ApplV Vs T = (applv Vs T).
non associative with precedence 90
for @{ 'SFlat $I $T1 $T }.
+notation "hvbox( Ⓐ term 90 T1 . break term 90 T )"
+ non associative with precedence 90
+ for @{ 'ApplV $T1 $T }.
+
notation "hvbox( T . break 𝕓 { I } break term 90 T1 )"
non associative with precedence 89
for @{ 'DBind $T $I $T1 }.
(* Substitution *************************************************************)
-notation "hvbox( â\86\91 [ d , break e ] break T1 â\89¡ break T2 )"
+notation "hvbox( â\87\91 [ d , break e ] break T1 â\89¡ break T2 )"
non associative with precedence 45
for @{ 'RLift $d $e $T1 $T2 }.
-notation "hvbox( ↓ [ e ] break L1 ≡ break L2 )"
- non associative with precedence 45
- for @{ 'RDrop $e $L1 $L2 }.
-
-notation "hvbox( ↓ [ d , break e ] break L1 ≡ break L2 )"
+notation "hvbox( ⇓ [ d , break e ] break L1 ≡ break L2 )"
non associative with precedence 45
- for @{ 'RDrop $d $e $L1 $L2 }.
+ for @{ 'RLDrop $d $e $L1 $L2 }.
notation "hvbox( T1 break [ d , break e ] ≫ break T2 )"
non associative with precedence 45
(* Unfold *******************************************************************)
+notation "hvbox( ⇑ [ e ] break T1 ≡ break T2 )"
+ non associative with precedence 45
+ for @{ 'RLift $e $T1 $T2 }.
+
+notation "hvbox( ⇓ [ e ] break L1 ≡ break L2 )"
+ non associative with precedence 45
+ for @{ 'RLDrop $e $L1 $L2 }.
+
notation "hvbox( T1 break [ d , break e ] ≫* break T2 )"
non associative with precedence 45
for @{ 'PSubstStar $T1 $d $e $T2 }.
non associative with precedence 45
for @{ 'InEInt $L $T $A }.
-notation "hvbox( R ⊢ break { L, break T } ϵ break 〚 A 〛 )"
+notation "hvbox( { L, break T } break [ R ] ϵ break 〚 A 〛 )"
non associative with precedence 45
for @{ 'InEInt $R $L $T $A }.
(* Functional ***************************************************************)
-notation "hvbox( â\86\9f [ d , break e ] break T )"
+notation "hvbox( â\86\91 [ d , break e ] break T )"
non associative with precedence 80
for @{ 'Lift $d $e $T }.
-notation "hvbox( â\86¡ [ d ← break V ] break T )"
+notation "hvbox( â\86\93 [ d ← break V ] break T )"
non associative with precedence 80
for @{ 'Subst $V $d $T }.
(* Advanced properties ******************************************************)
lemma cpr_cdelta: ∀L,K,V1,W1,W2,i.
- â\86\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 â\86\92 K â\8a¢ V1 [0, |L| - i - 1] â\89«* W1 â\86\92
- â\86\91[0, i + 1] W1 â\89¡ W2 â\86\92 L â\8a¢ #i â\87\92 W2.
+ â\87\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 â\86\92 K â\8a¢ V1 [0, |L| - i - 1] â\89«* W1 â\86\92
+ â\87\91[0, i + 1] W1 â\89¡ W2 â\86\92 L â\8a¢ #i â\87\92 W2.
#L #K #V1 #W1 #W2 #i #HLK #HVW1 #HW12
lapply (ldrop_fwd_ldrop2_length … HLK) #Hi
@ex2_1_intro [2: // | skip | @tpss_subst /width=6/ ] (**) (* /3 width=6/ is too slow *)
(* Basic_1: was: pr2_gen_lref *)
lemma cpr_inv_lref1: ∀L,T2,i. L ⊢ #i ⇒ T2 →
T2 = #i ∨
- â\88\83â\88\83K,V1,T1. â\86\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
+ â\88\83â\88\83K,V1,T1. â\87\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
K ⊢ V1 [0, |L| - i - 1] ≫* T1 &
- â\86\91[0, i + 1] T1 â\89¡ T2 &
+ â\87\91[0, i + 1] T1 â\89¡ T2 &
i < |L|.
#L #T2 #i * #X #H
>(tpr_inv_atom1 … H) -H #H
(* Relocation properties ****************************************************)
(* Basic_1: was: pr2_lift *)
-lemma cpr_lift: â\88\80L,K,d,e. â\86\93[d, e] L â\89¡ K â\86\92
- â\88\80T1,U1. â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92
+lemma cpr_lift: â\88\80L,K,d,e. â\87\93[d, e] L â\89¡ K â\86\92
+ â\88\80T1,U1. â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80T2,U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92
K ⊢ T1 ⇒ T2 → L ⊢ U1 ⇒ U2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #T2 #U2 #HTU2 * #T #HT1 #HT2
elim (lift_total T d e) #U #HTU
qed.
(* Basic_1: was: pr2_gen_lift *)
-lemma cpr_inv_lift: â\88\80L,K,d,e. â\86\93[d, e] L â\89¡ K â\86\92
- â\88\80T1,U1. â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. L â\8a¢ U1 â\87\92 U2 â\86\92
- â\88\83â\88\83T2. â\86\91[d, e] T2 â\89¡ U2 & K â\8a¢ T1 â\87\92 T2.
+lemma cpr_inv_lift: â\88\80L,K,d,e. â\87\93[d, e] L â\89¡ K â\86\92
+ â\88\80T1,U1. â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. L â\8a¢ U1 â\87\92 U2 â\86\92
+ â\88\83â\88\83T2. â\87\91[d, e] T2 â\89¡ U2 & K â\8a¢ T1 â\87\92 T2.
#L #K #d #e #HLK #T1 #U1 #HTU1 #U2 * #U #HU1 #HU2
elim (tpr_inv_lift … HU1 … HTU1) -U1 #T #HTU #T1
elim (lt_or_ge (|L|) d) #HLd
(* CONTEXT-FREE PARALLEL REDUCTION ON LOCAL ENVIRONMENTS ********************)
(* Basic_1: was: wcpr0_ldrop *)
-lemma ltpr_ldrop_conf: â\88\80L1,K1,d,e. â\86\93[d, e] L1 â\89¡ K1 â\86\92 â\88\80L2. L1 â\87\92 L2 â\86\92
- â\88\83â\88\83K2. â\86\93[d, e] L2 â\89¡ K2 & K1 â\87\92 K2.
+lemma ltpr_ldrop_conf: â\88\80L1,K1,d,e. â\87\93[d, e] L1 â\89¡ K1 â\86\92 â\88\80L2. L1 â\87\92 L2 â\86\92
+ â\88\83â\88\83K2. â\87\93[d, e] L2 â\89¡ K2 & K1 â\87\92 K2.
#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/
| #K1 #I #V1 #X #H
qed.
(* Basic_1: was: wcpr0_ldrop_back *)
-lemma ltpr_ldrop_trans: â\88\80L1,K1,d,e. â\86\93[d, e] L1 â\89¡ K1 â\86\92 â\88\80K2. K1 â\87\92 K2 â\86\92
- â\88\83â\88\83L2. â\86\93[d, e] L2 â\89¡ K2 & L1 â\87\92 L2.
+lemma ltpr_ldrop_trans: â\88\80L1,K1,d,e. â\87\93[d, e] L1 â\89¡ K1 â\86\92 â\88\80K2. K1 â\87\92 K2 â\86\92
+ â\88\83â\88\83L2. â\87\93[d, e] L2 â\89¡ K2 & L1 â\87\92 L2.
#L1 #K1 #d #e #H elim H -L1 -K1 -d -e
[ #d #e #X #H >(ltpr_inv_atom1 … H) -H /2 width=3/
| #K1 #I #V1 #X #H
tpr V1 V2 → tpr T1 T2 → ⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T →
tpr (𝕓{I} V1. T1) (𝕓{I} V2. T)
| tpr_theta: ∀V,V1,V2,W1,W2,T1,T2.
- tpr V1 V2 â\86\92 â\86\91[0,1] V2 â\89¡ V â\86\92 tpr W1 W2 â\86\92 tpr T1 T2 â\86\92
+ tpr V1 V2 â\86\92 â\87\91[0,1] V2 â\89¡ V â\86\92 tpr W1 W2 â\86\92 tpr T1 T2 â\86\92
tpr (𝕔{Appl} V1. 𝕔{Abbr} W1. T1) (𝕔{Abbr} W2. 𝕔{Appl} V. T2)
-| tpr_zeta : â\88\80V,T,T1,T2. â\86\91[0,1] T1 â\89¡ T â\86\92 tpr T1 T2 â\86\92
+| tpr_zeta : â\88\80V,T,T1,T2. â\87\91[0,1] T1 â\89¡ T â\86\92 tpr T1 T2 â\86\92
tpr (𝕔{Abbr} V. T) T2
| tpr_tau : ∀V,T1,T2. tpr T1 T2 → tpr (𝕔{Cast} V. T1) T2
.
(* Basic properties *********************************************************)
lemma tpr_bind: ∀I,V1,V2,T1,T2. V1 ⇒ V2 → T1 ⇒ T2 →
- 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
+ 𝕓{I} V1. T1 ⇒ 𝕓{I} V2. T2.
/2 width=3/ qed.
(* Basic_1: was by definition: pr0_refl *)
⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
U2 = 𝕓{I} V2. T
) ∨
- â\88\83â\88\83T. â\86\91[0,1] T â\89¡ T1 & T â\87\92 U2 & I = Abbr.
+ â\88\83â\88\83T. â\87\91[0,1] T â\89¡ T1 & T â\87\92 U2 & I = Abbr.
#U1 #U2 * -U1 -U2
[ #J #I #V #T #H destruct
| #I1 #V1 #V2 #T1 #T2 #_ #_ #I #V #T #H destruct
⋆. 𝕓{I} V2 ⊢ T2 [0, 1] ≫ T &
U2 = 𝕓{I} V2. T
) ∨
- â\88\83â\88\83T. â\86\91[0,1] T â\89¡ T1 & T â\87\92 U2 & I = Abbr.
+ â\88\83â\88\83T. â\87\91[0,1] T â\89¡ T1 & T â\87\92 U2 & I = Abbr.
/2 width=3/ qed-.
(* Basic_1: was pr0_gen_abbr *)
⋆. 𝕓{Abbr} V2 ⊢ T2 [0, 1] ≫ T &
U2 = 𝕓{Abbr} V2. T
) ∨
- â\88\83â\88\83T. â\86\91[0,1] T â\89¡ T1 & T â\87\92 U2.
+ â\88\83â\88\83T. â\87\91[0,1] T â\89¡ T1 & T â\87\92 U2.
#V1 #T1 #U2 #H
elim (tpr_inv_bind1 … H) -H * /3 width=7/
qed-.
U0 = 𝕔{Abst} W. T1 &
U2 = 𝕔{Abbr} V2. T2 & I = Appl
| ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
- â\86\91[0,1] V2 â\89¡ V &
+ â\87\91[0,1] V2 â\89¡ V &
U0 = 𝕔{Abbr} W1. T1 &
U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
I = Appl
U0 = 𝕔{Abst} W. T1 &
U2 = 𝕔{Abbr} V2. T2 & I = Appl
| ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
- â\86\91[0,1] V2 â\89¡ V &
+ â\87\91[0,1] V2 â\89¡ V &
U0 = 𝕔{Abbr} W1. T1 &
U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2 &
I = Appl
U0 = 𝕔{Abst} W. T1 &
U2 = 𝕔{Abbr} V2. T2
| ∃∃V2,V,W1,W2,T1,T2. V1 ⇒ V2 & W1 ⇒ W2 & T1 ⇒ T2 &
- â\86\91[0,1] V2 â\89¡ V &
+ â\87\91[0,1] V2 â\89¡ V &
U0 = 𝕔{Abbr} W1. T1 &
U2 = 𝕔{Abbr} W2. 𝕔{Appl} V. T2.
#V1 #U0 #U2 #H
fact tpr_inv_lref2_aux: ∀T1,T2. T1 ⇒ T2 → ∀i. T2 = #i →
∨∨ T1 = #i
- | â\88\83â\88\83V,T,T0. â\86\91[O,1] T0 â\89¡ T & T0 â\87\92 #i &
+ | â\88\83â\88\83V,T,T0. â\87\91[O,1] T0 â\89¡ T & T0 â\87\92 #i &
T1 = 𝕔{Abbr} V. T
| ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
#T1 #T2 * -T1 -T2
lemma tpr_inv_lref2: ∀T1,i. T1 ⇒ #i →
∨∨ T1 = #i
- | â\88\83â\88\83V,T,T0. â\86\91[O,1] T0 â\89¡ T & T0 â\87\92 #i &
+ | â\88\83â\88\83V,T,T0. â\87\91[O,1] T0 â\89¡ T & T0 â\87\92 #i &
T1 = 𝕔{Abbr} V. T
| ∃∃V,T. T ⇒ #i & T1 = 𝕔{Cast} V. T.
/2 width=3/ qed-.
(* Basic_1: was: pr0_lift *)
lemma tpr_lift: ∀T1,T2. T1 ⇒ T2 →
- â\88\80d,e,U1. â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92 U1 â\87\92 U2.
+ â\88\80d,e,U1. â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92 U1 â\87\92 U2.
#T1 #T2 #H elim H -T1 -T2
[ * #i #d #e #U1 #HU1 #U2 #HU2
lapply (lift_mono … HU1 … HU2) -HU1 #H destruct
(* Basic_1: was: pr0_gen_lift *)
lemma tpr_inv_lift: ∀T1,T2. T1 ⇒ T2 →
- â\88\80d,e,U1. â\86\91[d, e] U1 â\89¡ T1 â\86\92
- â\88\83â\88\83U2. â\86\91[d, e] U2 â\89¡ T2 & U1 â\87\92 U2.
+ â\88\80d,e,U1. â\87\91[d, e] U1 â\89¡ T1 â\86\92
+ â\88\83â\88\83U2. â\87\91[d, e] U2 â\89¡ T2 & U1 â\87\92 U2.
#T1 #T2 #H elim H -T1 -T2
[ * #i #d #e #U1 #HU1
[ lapply (lift_inv_sort2 … HU1) -HU1 #H destruct /2 width=3/
∀X1,X2. X0 ⇒ X1 → X0 ⇒ X2 →
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
- V0 â\87\92 V1 â\86\92 V0 â\87\92 V2 â\86\92 â\86\91[O,1] V2 â\89¡ V â\86\92
+ V0 â\87\92 V1 â\86\92 V0 â\87\92 V2 â\86\92 â\87\91[O,1] V2 â\89¡ V â\86\92
W0 ⇒ W2 → U0 ⇒ U2 → 𝕔{Abbr} W0. U0 ⇒ T1 →
∃∃X. 𝕔{Appl} V1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} V. U2 ⇒ X.
#V0 #V1 #T1 #V2 #V #W0 #W2 #U0 #U2 #IH #HV01 #HV02 #HV2 #HW02 #HU02 #H
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
V0 ⇒ V1 → T0 ⇒ T1 → ⋆. 𝕓{Abbr} V1 ⊢ T1 [O,1] ≫ TT1 →
- T2 â\87\92 X2 â\86\92 â\86\91[O, 1] T2 â\89¡ T0 â\86\92
+ T2 â\87\92 X2 â\86\92 â\87\91[O, 1] T2 â\89¡ T0 â\86\92
∃∃X. 𝕓{Abbr} V1. TT1 ⇒ X & X2 ⇒ X.
#X2 #V0 #V1 #T0 #T1 #TT1 #T2 #IH #_ #HT01 #HTT1 #HTX2 #HTT20
elim (tpr_inv_lift … HT01 … HTT20) -HT01 #TT2 #HTT21 #HTT2
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
V0 ⇒ V1 → V0 ⇒ V2 → W0 ⇒ W1 → W0 ⇒ W2 → T0 ⇒ T1 → T0 ⇒ T2 →
- â\86\91[O, 1] V1 â\89¡ VV1 â\86\92 â\86\91[O, 1] V2 â\89¡ VV2 â\86\92
+ â\87\91[O, 1] V1 â\89¡ VV1 â\86\92 â\87\91[O, 1] V2 â\89¡ VV2 â\86\92
∃∃X. 𝕔{Abbr} W1. 𝕔{Appl} VV1. T1 ⇒ X & 𝕔{Abbr} W2. 𝕔{Appl} VV2. T2 ⇒ X.
#VV1 #V0 #V1 #W0 #W1 #T0 #T1 #V2 #VV2 #W2 #T2 #IH #HV01 #HV02 #HW01 #HW02 #HT01 #HT02 #HVV1 #HVV2
elim (IH … HV01 … HV02) -HV01 -HV02 /2 width=1/ #V #HV1 #HV2
∃∃X. X1 ⇒ X & X2 ⇒ X
) →
T0 ⇒ T1 → T2 ⇒ X2 →
- â\86\91[O, 1] T0 â\89¡ TT0 â\86\92 â\86\91[O, 1] T2 â\89¡ TT0 â\86\92
+ â\87\91[O, 1] T0 â\89¡ TT0 â\86\92 â\87\91[O, 1] T2 â\89¡ TT0 â\86\92
∃∃X. T1 ⇒ X & X2 ⇒ X.
#V0 #X2 #TT0 #T0 #T1 #T2 #IH #HT01 #HTX2 #HTT0 #HTT20
lapply (lift_inj … HTT0 … HTT20) -HTT0 #H destruct
inductive aaa: lenv → term → predicate aarity ≝
| aaa_sort: ∀L,k. aaa L (⋆k) 𝕒
-| aaa_lref: â\88\80I,L,K,V,B,i. â\86\93[0, i] L â\89¡ K. ð\9d\95\93{I} V â\86\92 aaa K V B â\86\92 aaa L (#i) B
+| aaa_lref: â\88\80I,L,K,V,B,i. â\87\93[0, i] L â\89¡ K. ð\9d\95\93{I} V â\86\92 aaa K V B â\86\92 aaa L (#i) B
| aaa_abbr: ∀L,V,T,B,A.
aaa L V B → aaa (L. 𝕓{Abbr} V) T A → aaa L (𝕔{Abbr} V. T) A
| aaa_abst: ∀L,V,T,B,A.
- aaa L V B → aaa (L. 𝕓{Abst} V) T A → aaa L (𝕔{Abbr} V. T) (𝕔 B. A)
+ aaa L V B → aaa (L. 𝕓{Abst} V) T A → aaa L (𝕔{Abst} V. T) (𝕔 B. A)
| aaa_appl: ∀L,V,T,B,A. aaa L V B → aaa L T (𝕔 B. A) → aaa L (𝕔{Appl} V. T) A
| aaa_cast: ∀L,V,T,A. aaa L V A → aaa L T A → aaa L (𝕔{Cast} V. T) A
.
(* GLOBAL ENVIRONMENT SLICING ***********************************************)
inductive gdrop (e:nat) (G1:lenv) : predicate lenv ≝
-| gdrop_lt: â\88\80G2. e < |G1| â\86\92 â\86\93[0, |G1| - (e + 1)] G1 â\89¡ G2 â\86\92 gdrop e G1 G2
+| gdrop_lt: â\88\80G2. e < |G1| â\86\92 â\87\93[0, |G1| - (e + 1)] G1 â\89¡ G2 â\86\92 gdrop e G1 G2
| gdrop_ge: |G1| ≤ e → gdrop e G1 (⋆)
.
-interpretation "global slicing" 'RDrop e G1 G2 = (gdrop e G1 G2).
+interpretation "global slicing" 'RGDrop e G1 G2 = (gdrop e G1 G2).
(* basic inversion lemmas ***************************************************)
-
-fact gdrop_inv_atom2_aux: â\88\80G1,G2,e. â\86\93[e] G1 â\89¡ G2 â\86\92 G2 = â\8b\86 â\86\92 |G1| â\89¤ e.
+(*
+fact gdrop_inv_atom2_aux: â\88\80G1,G2,e. â\87\93[e] G1 â\89¡ G2 â\86\92 G2 = â\8b\86 â\86\92 |G1| â\89¤ e.
#G1 #G2 #e * -G2 //
#G2 #He #HG12 #H destruct
lapply (ldrop_fwd_O1_length … HG12) -HG12
>(commutative_plus e) normalize #H destruct
qed.
-lemma gdrop_inv_atom2: â\88\80G1,e. â\86\93[e] G1 â\89¡ â\8b\86 â\86\92 |G1| â\89¤ e.
+lemma gdrop_inv_atom2: â\88\80G1,e. â\87\93[e] G1 â\89¡ â\8b\86 â\86\92 |G1| â\89¤ e.
/2 width=3/ qed-.
-lemma gdrop_inv_ge: â\88\80G1,G2,e. â\86\93[e] G1 â\89¡ G2 â\86\92 |G1| â\89¤ e â\86\92 G2 = â\8b\86.
+lemma gdrop_inv_ge: â\88\80G1,G2,e. â\87\93[e] G1 â\89¡ G2 â\86\92 |G1| â\89¤ e â\86\92 G2 = â\8b\86.
#G1 #G2 #e * // #G2 #H1 #_ #H2
lapply (lt_to_le_to_lt … H1 H2) -H1 -H2 #He
elim (lt_refl_false … He)
qed-.
+*)
(* Basic_1: includes: ldrop_skip_bind *)
inductive ldrop: nat → nat → relation lenv ≝
-| ldrop_atom: ∀d,e. ldrop d e (⋆) (⋆)
-| ldrop_pair: ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
+| ldrop_atom : ∀d,e. ldrop d e (⋆) (⋆)
+| ldrop_pair : ∀L,I,V. ldrop 0 0 (L. 𝕓{I} V) (L. 𝕓{I} V)
| ldrop_ldrop: ∀L1,L2,I,V,e. ldrop 0 e L1 L2 → ldrop 0 (e + 1) (L1. 𝕓{I} V) L2
-| ldrop_skip: ∀L1,L2,I,V1,V2,d,e.
- ldrop d e L1 L2 â\86\92 â\86\91[d,e] V2 â\89¡ V1 â\86\92
- ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
+| ldrop_skip : ∀L1,L2,I,V1,V2,d,e.
+ ldrop d e L1 L2 â\86\92 â\87\91[d,e] V2 â\89¡ V1 â\86\92
+ ldrop (d + 1) e (L1. 𝕓{I} V1) (L2. 𝕓{I} V2)
.
-interpretation "local slicing" 'RDrop d e L1 L2 = (ldrop d e L1 L2).
+interpretation "local slicing" 'RLDrop d e L1 L2 = (ldrop d e L1 L2).
(* Basic inversion lemmas ***************************************************)
-fact ldrop_inv_refl_aux: â\88\80d,e,L1,L2. â\86\93[d, e] L1 â\89¡ L2 â\86\92 d = 0 â\86\92 e = 0 â\86\92 L1 = L2.
+fact ldrop_inv_refl_aux: â\88\80d,e,L1,L2. â\87\93[d, e] L1 â\89¡ L2 â\86\92 d = 0 â\86\92 e = 0 â\86\92 L1 = L2.
#d #e #L1 #L2 * -d -e -L1 -L2
[ //
| //
qed.
(* Basic_1: was: ldrop_gen_refl *)
-lemma ldrop_inv_refl: â\88\80L1,L2. â\86\93[0, 0] L1 â\89¡ L2 â\86\92 L1 = L2.
+lemma ldrop_inv_refl: â\88\80L1,L2. â\87\93[0, 0] L1 â\89¡ L2 â\86\92 L1 = L2.
/2 width=5/ qed-.
-fact ldrop_inv_atom1_aux: â\88\80d,e,L1,L2. â\86\93[d, e] L1 â\89¡ L2 â\86\92 L1 = â\8b\86 â\86\92
+fact ldrop_inv_atom1_aux: â\88\80d,e,L1,L2. â\87\93[d, e] L1 â\89¡ L2 â\86\92 L1 = â\8b\86 â\86\92
L2 = ⋆.
#d #e #L1 #L2 * -d -e -L1 -L2
[ //
qed.
(* Basic_1: was: ldrop_gen_sort *)
-lemma ldrop_inv_atom1: â\88\80d,e,L2. â\86\93[d, e] â\8b\86 â\89¡ L2 â\86\92 L2 = â\8b\86.
+lemma ldrop_inv_atom1: â\88\80d,e,L2. â\87\93[d, e] â\8b\86 â\89¡ L2 â\86\92 L2 = â\8b\86.
/2 width=5/ qed-.
-fact ldrop_inv_O1_aux: â\88\80d,e,L1,L2. â\86\93[d, e] L1 â\89¡ L2 â\86\92 d = 0 â\86\92
+fact ldrop_inv_O1_aux: â\88\80d,e,L1,L2. â\87\93[d, e] L1 â\89¡ L2 â\86\92 d = 0 â\86\92
∀K,I,V. L1 = K. 𝕓{I} V →
(e = 0 ∧ L2 = K. 𝕓{I} V) ∨
- (0 < e â\88§ â\86\93[d, e - 1] K â\89¡ L2).
+ (0 < e â\88§ â\87\93[d, e - 1] K â\89¡ L2).
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #K #I #V #H destruct
| #L #I #V #_ #K #J #W #HX destruct /3 width=1/
]
qed.
-lemma ldrop_inv_O1: â\88\80e,K,I,V,L2. â\86\93[0, e] K. ð\9d\95\93{I} V â\89¡ L2 â\86\92
+lemma ldrop_inv_O1: â\88\80e,K,I,V,L2. â\87\93[0, e] K. ð\9d\95\93{I} V â\89¡ L2 â\86\92
(e = 0 ∧ L2 = K. 𝕓{I} V) ∨
- (0 < e â\88§ â\86\93[0, e - 1] K â\89¡ L2).
+ (0 < e â\88§ â\87\93[0, e - 1] K â\89¡ L2).
/2 width=3/ qed-.
(* Basic_1: was: ldrop_gen_ldrop *)
lemma ldrop_inv_ldrop1: ∀e,K,I,V,L2.
- â\86\93[0, e] K. ð\9d\95\93{I} V â\89¡ L2 â\86\92 0 < e â\86\92 â\86\93[0, e - 1] K â\89¡ L2.
+ â\87\93[0, e] K. ð\9d\95\93{I} V â\89¡ L2 â\86\92 0 < e â\86\92 â\87\93[0, e - 1] K â\89¡ L2.
#e #K #I #V #L2 #H #He
elim (ldrop_inv_O1 … H) -H * // #H destruct
elim (lt_refl_false … He)
qed-.
-fact ldrop_inv_skip1_aux: â\88\80d,e,L1,L2. â\86\93[d, e] L1 â\89¡ L2 â\86\92 0 < d â\86\92
+fact ldrop_inv_skip1_aux: â\88\80d,e,L1,L2. â\87\93[d, e] L1 â\89¡ L2 â\86\92 0 < d â\86\92
∀I,K1,V1. L1 = K1. 𝕓{I} V1 →
- â\88\83â\88\83K2,V2. â\86\93[d - 1, e] K1 â\89¡ K2 &
- â\86\91[d - 1, e] V2 â\89¡ V1 &
+ â\88\83â\88\83K2,V2. â\87\93[d - 1, e] K1 â\89¡ K2 &
+ â\87\91[d - 1, e] V2 â\89¡ V1 &
L2 = K2. 𝕓{I} V2.
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #I #K #V #H destruct
qed.
(* Basic_1: was: ldrop_gen_skip_l *)
-lemma ldrop_inv_skip1: â\88\80d,e,I,K1,V1,L2. â\86\93[d, e] K1. ð\9d\95\93{I} V1 â\89¡ L2 â\86\92 0 < d â\86\92
- â\88\83â\88\83K2,V2. â\86\93[d - 1, e] K1 â\89¡ K2 &
- â\86\91[d - 1, e] V2 â\89¡ V1 &
+lemma ldrop_inv_skip1: â\88\80d,e,I,K1,V1,L2. â\87\93[d, e] K1. ð\9d\95\93{I} V1 â\89¡ L2 â\86\92 0 < d â\86\92
+ â\88\83â\88\83K2,V2. â\87\93[d - 1, e] K1 â\89¡ K2 &
+ â\87\91[d - 1, e] V2 â\89¡ V1 &
L2 = K2. 𝕓{I} V2.
/2 width=3/ qed-.
-fact ldrop_inv_skip2_aux: â\88\80d,e,L1,L2. â\86\93[d, e] L1 â\89¡ L2 â\86\92 0 < d â\86\92
+fact ldrop_inv_skip2_aux: â\88\80d,e,L1,L2. â\87\93[d, e] L1 â\89¡ L2 â\86\92 0 < d â\86\92
∀I,K2,V2. L2 = K2. 𝕓{I} V2 →
- â\88\83â\88\83K1,V1. â\86\93[d - 1, e] K1 â\89¡ K2 &
- â\86\91[d - 1, e] V2 â\89¡ V1 &
+ â\88\83â\88\83K1,V1. â\87\93[d - 1, e] K1 â\89¡ K2 &
+ â\87\91[d - 1, e] V2 â\89¡ V1 &
L1 = K1. 𝕓{I} V1.
#d #e #L1 #L2 * -d -e -L1 -L2
[ #d #e #_ #I #K #V #H destruct
qed.
(* Basic_1: was: ldrop_gen_skip_r *)
-lemma ldrop_inv_skip2: â\88\80d,e,I,L1,K2,V2. â\86\93[d, e] L1 â\89¡ K2. ð\9d\95\93{I} V2 â\86\92 0 < d â\86\92
- â\88\83â\88\83K1,V1. â\86\93[d - 1, e] K1 â\89¡ K2 & â\86\91[d - 1, e] V2 â\89¡ V1 &
+lemma ldrop_inv_skip2: â\88\80d,e,I,L1,K2,V2. â\87\93[d, e] L1 â\89¡ K2. ð\9d\95\93{I} V2 â\86\92 0 < d â\86\92
+ â\88\83â\88\83K1,V1. â\87\93[d - 1, e] K1 â\89¡ K2 & â\87\91[d - 1, e] V2 â\89¡ V1 &
L1 = K1. 𝕓{I} V1.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
(* Basic_1: was by definition: ldrop_refl *)
-lemma ldrop_refl: â\88\80L. â\86\93[0, 0] L â\89¡ L.
+lemma ldrop_refl: â\88\80L. â\87\93[0, 0] L â\89¡ L.
#L elim L -L //
qed.
lemma ldrop_ldrop_lt: ∀L1,L2,I,V,e.
- â\86\93[0, e - 1] L1 â\89¡ L2 â\86\92 0 < e â\86\92 â\86\93[0, e] L1. ð\9d\95\93{I} V â\89¡ L2.
+ â\87\93[0, e - 1] L1 â\89¡ L2 â\86\92 0 < e â\86\92 â\87\93[0, e] L1. ð\9d\95\93{I} V â\89¡ L2.
#L1 #L2 #I #V #e #HL12 #He >(plus_minus_m_m e 1) // /2 width=1/
qed.
lemma ldrop_lsubs_ldrop1_abbr: ∀L1,L2,d,e. L1 [d, e] ≼ L2 →
- â\88\80K1,V,i. â\86\93[0, i] L1 â\89¡ K1. ð\9d\95\93{Abbr} V â\86\92
+ â\88\80K1,V,i. â\87\93[0, i] L1 â\89¡ K1. ð\9d\95\93{Abbr} V â\86\92
d ≤ i → i < d + e →
∃∃K2. K1 [0, d + e - i - 1] ≼ K2 &
- â\86\93[0, i] L2 â\89¡ K2. ð\9d\95\93{Abbr} V.
+ â\87\93[0, i] L2 â\89¡ K2. ð\9d\95\93{Abbr} V.
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e
[ #d #e #K1 #V #i #H
lapply (ldrop_inv_atom1 … H) -H #H destruct
(* Basic forvard lemmas *****************************************************)
(* Basic_1: was: ldrop_S *)
-lemma ldrop_fwd_ldrop2: â\88\80L1,I2,K2,V2,e. â\86\93[O, e] L1 â\89¡ K2. ð\9d\95\93{I2} V2 â\86\92
- â\86\93[O, e + 1] L1 â\89¡ K2.
+lemma ldrop_fwd_ldrop2: â\88\80L1,I2,K2,V2,e. â\87\93[O, e] L1 â\89¡ K2. ð\9d\95\93{I2} V2 â\86\92
+ â\87\93[O, e + 1] L1 â\89¡ K2.
#L1 elim L1 -L1
[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
]
qed-.
-lemma ldrop_fwd_lw: â\88\80L1,L2,d,e. â\86\93[d, e] L1 â\89¡ L2 â\86\92 #[L2] â\89¤ #[L1].
+lemma ldrop_fwd_lw: â\88\80L1,L2,d,e. â\87\93[d, e] L1 â\89¡ L2 â\86\92 #[L2] â\89¤ #[L1].
#L1 #L2 #d #e #H elim H -L1 -L2 -d -e // normalize
[ /2 width=3/
| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12
qed-.
lemma ldrop_fwd_ldrop2_length: ∀L1,I2,K2,V2,e.
- â\86\93[0, e] L1 â\89¡ K2. ð\9d\95\93{I2} V2 â\86\92 e < |L1|.
+ â\87\93[0, e] L1 â\89¡ K2. ð\9d\95\93{I2} V2 â\86\92 e < |L1|.
#L1 elim L1 -L1
[ #I2 #K2 #V2 #e #H lapply (ldrop_inv_atom1 … H) -H #H destruct
| #K1 #I1 #V1 #IHL1 #I2 #K2 #V2 #e #H
]
qed-.
-lemma ldrop_fwd_O1_length: â\88\80L1,L2,e. â\86\93[0, e] L1 â\89¡ L2 â\86\92 |L2| = |L1| - e.
+lemma ldrop_fwd_O1_length: â\88\80L1,L2,e. â\87\93[0, e] L1 â\89¡ L2 â\86\92 |L2| = |L1| - e.
#L1 elim L1 -L1
[ #L2 #e #H >(ldrop_inv_atom1 … H) -H //
| #K1 #I1 #V1 #IHL1 #L2 #e #H
(* Main properties **********************************************************)
(* Basic_1: was: ldrop_mono *)
-theorem ldrop_mono: â\88\80d,e,L,L1. â\86\93[d, e] L â\89¡ L1 â\86\92
- â\88\80L2. â\86\93[d, e] L â\89¡ L2 â\86\92 L1 = L2.
+theorem ldrop_mono: â\88\80d,e,L,L1. â\87\93[d, e] L â\89¡ L1 â\86\92
+ â\88\80L2. â\87\93[d, e] L â\89¡ L2 â\86\92 L1 = L2.
#d #e #L #L1 #H elim H -d -e -L -L1
[ #d #e #L2 #H
>(ldrop_inv_atom1 … H) -L2 //
qed-.
(* Basic_1: was: ldrop_conf_ge *)
-theorem ldrop_conf_ge: â\88\80d1,e1,L,L1. â\86\93[d1, e1] L â\89¡ L1 â\86\92
- â\88\80e2,L2. â\86\93[0, e2] L â\89¡ L2 â\86\92 d1 + e1 â\89¤ e2 â\86\92
- â\86\93[0, e2 - e1] L1 â\89¡ L2.
+theorem ldrop_conf_ge: â\88\80d1,e1,L,L1. â\87\93[d1, e1] L â\89¡ L1 â\86\92
+ â\88\80e2,L2. â\87\93[0, e2] L â\89¡ L2 â\86\92 d1 + e1 â\89¤ e2 â\86\92
+ â\87\93[0, e2 - e1] L1 â\89¡ L2.
#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1
[ #d #e #e2 #L2 #H
>(ldrop_inv_atom1 … H) -L2 //
qed.
(* Basic_1: was: ldrop_conf_lt *)
-theorem ldrop_conf_lt: â\88\80d1,e1,L,L1. â\86\93[d1, e1] L â\89¡ L1 â\86\92
- â\88\80e2,K2,I,V2. â\86\93[0, e2] L â\89¡ K2. ð\9d\95\93{I} V2 â\86\92
+theorem ldrop_conf_lt: â\88\80d1,e1,L,L1. â\87\93[d1, e1] L â\89¡ L1 â\86\92
+ â\88\80e2,K2,I,V2. â\87\93[0, e2] L â\89¡ K2. ð\9d\95\93{I} V2 â\86\92
e2 < d1 → let d ≝ d1 - e2 - 1 in
- â\88\83â\88\83K1,V1. â\86\93[0, e2] L1 â\89¡ K1. ð\9d\95\93{I} V1 &
- â\86\93[d, e1] K2 â\89¡ K1 & â\86\91[d, e1] V1 â\89¡ V2.
+ â\88\83â\88\83K1,V1. â\87\93[0, e2] L1 â\89¡ K1. ð\9d\95\93{I} V1 &
+ â\87\93[d, e1] K2 â\89¡ K1 & â\87\91[d, e1] V1 â\89¡ V2.
#d1 #e1 #L #L1 #H elim H -d1 -e1 -L -L1
[ #d #e #e2 #K2 #I #V2 #H
lapply (ldrop_inv_atom1 … H) -H #H destruct
qed.
(* Basic_1: was: ldrop_trans_le *)
-theorem ldrop_trans_le: â\88\80d1,e1,L1,L. â\86\93[d1, e1] L1 â\89¡ L â\86\92
- â\88\80e2,L2. â\86\93[0, e2] L â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
- â\88\83â\88\83L0. â\86\93[0, e2] L1 â\89¡ L0 & â\86\93[d1 - e2, e1] L0 â\89¡ L2.
+theorem ldrop_trans_le: â\88\80d1,e1,L1,L. â\87\93[d1, e1] L1 â\89¡ L â\86\92
+ â\88\80e2,L2. â\87\93[0, e2] L â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
+ â\88\83â\88\83L0. â\87\93[0, e2] L1 â\89¡ L0 & â\87\93[d1 - e2, e1] L0 â\89¡ L2.
#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L
[ #d #e #e2 #L2 #H
>(ldrop_inv_atom1 … H) -L2 /2 width=3/
qed.
(* Basic_1: was: ldrop_trans_ge *)
-theorem ldrop_trans_ge: â\88\80d1,e1,L1,L. â\86\93[d1, e1] L1 â\89¡ L â\86\92
- â\88\80e2,L2. â\86\93[0, e2] L â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 â\86\93[0, e1 + e2] L1 â\89¡ L2.
+theorem ldrop_trans_ge: â\88\80d1,e1,L1,L. â\87\93[d1, e1] L1 â\89¡ L â\86\92
+ â\88\80e2,L2. â\87\93[0, e2] L â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 â\87\93[0, e1 + e2] L1 â\89¡ L2.
#d1 #e1 #L1 #L #H elim H -d1 -e1 -L1 -L
[ #d #e #e2 #L2 #H
>(ldrop_inv_atom1 … H) -H -L2 //
qed.
theorem ldrop_trans_ge_comm: ∀d1,e1,e2,L1,L2,L.
- â\86\93[d1, e1] L1 â\89¡ L â\86\92 â\86\93[0, e2] L â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92
- â\86\93[0, e2 + e1] L1 â\89¡ L2.
+ â\87\93[d1, e1] L1 â\89¡ L â\86\92 â\87\93[0, e2] L â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92
+ â\87\93[0, e2 + e1] L1 â\89¡ L2.
#e1 #e1 #e2 >commutative_plus /2 width=5/
qed.
(* Basic_1: was: ldrop_conf_rev *)
-axiom ldrop_div: â\88\80e1,L1,L. â\86\93[0, e1] L1 â\89¡ L â\86\92 â\88\80e2,L2. â\86\93[0, e2] L2 â\89¡ L â\86\92
- â\88\83â\88\83L0. â\86\93[0, e1] L0 â\89¡ L2 & â\86\93[e1, e2] L0 â\89¡ L1.
+axiom ldrop_div: â\88\80e1,L1,L. â\87\93[0, e1] L1 â\89¡ L â\86\92 â\88\80e2,L2. â\87\93[0, e2] L2 â\89¡ L â\86\92
+ â\88\83â\88\83L0. â\87\93[0, e1] L0 â\89¡ L2 & â\87\93[e1, e2] L0 â\89¡ L1.
(* Basic inversion lemmas ***************************************************)
-fact lift_inv_refl_O2_aux: â\88\80d,e,T1,T2. â\86\91[d, e] T1 â\89¡ T2 â\86\92 e = 0 â\86\92 T1 = T2.
+fact lift_inv_refl_O2_aux: â\88\80d,e,T1,T2. â\87\91[d, e] T1 â\89¡ T2 â\86\92 e = 0 â\86\92 T1 = T2.
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 // /3 width=1/
qed.
-lemma lift_inv_refl_O2: â\88\80d,T1,T2. â\86\91[d, 0] T1 â\89¡ T2 â\86\92 T1 = T2.
+lemma lift_inv_refl_O2: â\88\80d,T1,T2. â\87\91[d, 0] T1 â\89¡ T2 â\86\92 T1 = T2.
/2 width=4/ qed-.
-fact lift_inv_sort1_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80k. T1 = â\8b\86k â\86\92 T2 = â\8b\86k.
+fact lift_inv_sort1_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80k. T1 = â\8b\86k â\86\92 T2 = â\8b\86k.
#d #e #T1 #T2 * -d -e -T1 -T2 //
[ #i #d #e #_ #k #H destruct
| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
]
qed.
-lemma lift_inv_sort1: â\88\80d,e,T2,k. â\86\91[d,e] â\8b\86k â\89¡ T2 â\86\92 T2 = â\8b\86k.
+lemma lift_inv_sort1: â\88\80d,e,T2,k. â\87\91[d,e] â\8b\86k â\89¡ T2 â\86\92 T2 = â\8b\86k.
/2 width=5/ qed-.
-fact lift_inv_lref1_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80i. T1 = #i â\86\92
+fact lift_inv_lref1_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80i. T1 = #i â\86\92
(i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #i #H destruct
]
qed.
-lemma lift_inv_lref1: â\88\80d,e,T2,i. â\86\91[d,e] #i â\89¡ T2 â\86\92
+lemma lift_inv_lref1: â\88\80d,e,T2,i. â\87\91[d,e] #i â\89¡ T2 â\86\92
(i < d ∧ T2 = #i) ∨ (d ≤ i ∧ T2 = #(i + e)).
/2 width=3/ qed-.
-lemma lift_inv_lref1_lt: â\88\80d,e,T2,i. â\86\91[d,e] #i â\89¡ T2 â\86\92 i < d â\86\92 T2 = #i.
+lemma lift_inv_lref1_lt: â\88\80d,e,T2,i. â\87\91[d,e] #i â\89¡ T2 â\86\92 i < d â\86\92 T2 = #i.
#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd
elim (lt_refl_false … Hdd)
qed-.
-lemma lift_inv_lref1_ge: â\88\80d,e,T2,i. â\86\91[d,e] #i â\89¡ T2 â\86\92 d â\89¤ i â\86\92 T2 = #(i + e).
+lemma lift_inv_lref1_ge: â\88\80d,e,T2,i. â\87\91[d,e] #i â\89¡ T2 â\86\92 d â\89¤ i â\86\92 T2 = #(i + e).
#d #e #T2 #i #H elim (lift_inv_lref1 … H) -H * //
#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd
elim (lt_refl_false … Hdd)
qed-.
-fact lift_inv_gref1_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80p. T1 = §p â\86\92 T2 = §p.
+fact lift_inv_gref1_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80p. T1 = §p â\86\92 T2 = §p.
#d #e #T1 #T2 * -d -e -T1 -T2 //
[ #i #d #e #_ #k #H destruct
| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
]
qed.
-lemma lift_inv_gref1: â\88\80d,e,T2,p. â\86\91[d,e] §p â\89¡ T2 â\86\92 T2 = §p.
+lemma lift_inv_gref1: â\88\80d,e,T2,p. â\87\91[d,e] §p â\89¡ T2 â\86\92 T2 = §p.
/2 width=5/ qed-.
-fact lift_inv_bind1_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92
+fact lift_inv_bind1_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92
∀I,V1,U1. T1 = 𝕓{I} V1.U1 →
- â\88\83â\88\83V2,U2. â\86\91[d,e] V1 â\89¡ V2 & â\86\91[d+1,e] U1 â\89¡ U2 &
+ â\88\83â\88\83V2,U2. â\87\91[d,e] V1 â\89¡ V2 & â\87\91[d+1,e] U1 â\89¡ U2 &
T2 = 𝕓{I} V2. U2.
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V1 #U1 #H destruct
]
qed.
-lemma lift_inv_bind1: â\88\80d,e,T2,I,V1,U1. â\86\91[d,e] ð\9d\95\93{I} V1. U1 â\89¡ T2 â\86\92
- â\88\83â\88\83V2,U2. â\86\91[d,e] V1 â\89¡ V2 & â\86\91[d+1,e] U1 â\89¡ U2 &
+lemma lift_inv_bind1: â\88\80d,e,T2,I,V1,U1. â\87\91[d,e] ð\9d\95\93{I} V1. U1 â\89¡ T2 â\86\92
+ â\88\83â\88\83V2,U2. â\87\91[d,e] V1 â\89¡ V2 & â\87\91[d+1,e] U1 â\89¡ U2 &
T2 = 𝕓{I} V2. U2.
/2 width=3/ qed-.
-fact lift_inv_flat1_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92
+fact lift_inv_flat1_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92
∀I,V1,U1. T1 = 𝕗{I} V1.U1 →
- â\88\83â\88\83V2,U2. â\86\91[d,e] V1 â\89¡ V2 & â\86\91[d,e] U1 â\89¡ U2 &
+ â\88\83â\88\83V2,U2. â\87\91[d,e] V1 â\89¡ V2 & â\87\91[d,e] U1 â\89¡ U2 &
T2 = 𝕗{I} V2. U2.
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V1 #U1 #H destruct
]
qed.
-lemma lift_inv_flat1: â\88\80d,e,T2,I,V1,U1. â\86\91[d,e] ð\9d\95\97{I} V1. U1 â\89¡ T2 â\86\92
- â\88\83â\88\83V2,U2. â\86\91[d,e] V1 â\89¡ V2 & â\86\91[d,e] U1 â\89¡ U2 &
+lemma lift_inv_flat1: â\88\80d,e,T2,I,V1,U1. â\87\91[d,e] ð\9d\95\97{I} V1. U1 â\89¡ T2 â\86\92
+ â\88\83â\88\83V2,U2. â\87\91[d,e] V1 â\89¡ V2 & â\87\91[d,e] U1 â\89¡ U2 &
T2 = 𝕗{I} V2. U2.
/2 width=3/ qed-.
-fact lift_inv_sort2_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80k. T2 = â\8b\86k â\86\92 T1 = â\8b\86k.
+fact lift_inv_sort2_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80k. T2 = â\8b\86k â\86\92 T1 = â\8b\86k.
#d #e #T1 #T2 * -d -e -T1 -T2 //
[ #i #d #e #_ #k #H destruct
| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
qed.
(* Basic_1: was: lift_gen_sort *)
-lemma lift_inv_sort2: â\88\80d,e,T1,k. â\86\91[d,e] T1 â\89¡ â\8b\86k â\86\92 T1 = â\8b\86k.
+lemma lift_inv_sort2: â\88\80d,e,T1,k. â\87\91[d,e] T1 â\89¡ â\8b\86k â\86\92 T1 = â\8b\86k.
/2 width=5/ qed-.
-fact lift_inv_lref2_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80i. T2 = #i â\86\92
+fact lift_inv_lref2_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80i. T2 = #i â\86\92
(i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #i #H destruct
qed.
(* Basic_1: was: lift_gen_lref *)
-lemma lift_inv_lref2: â\88\80d,e,T1,i. â\86\91[d,e] T1 â\89¡ #i â\86\92
+lemma lift_inv_lref2: â\88\80d,e,T1,i. â\87\91[d,e] T1 â\89¡ #i â\86\92
(i < d ∧ T1 = #i) ∨ (d + e ≤ i ∧ T1 = #(i - e)).
/2 width=3/ qed-.
(* Basic_1: was: lift_gen_lref_lt *)
-lemma lift_inv_lref2_lt: â\88\80d,e,T1,i. â\86\91[d,e] T1 â\89¡ #i â\86\92 i < d â\86\92 T1 = #i.
+lemma lift_inv_lref2_lt: â\88\80d,e,T1,i. â\87\91[d,e] T1 â\89¡ #i â\86\92 i < d â\86\92 T1 = #i.
#d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * //
#Hdi #_ #Hid lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd
elim (lt_inv_plus_l … Hdd) -Hdd #Hdd
qed-.
(* Basic_1: was: lift_gen_lref_false *)
-lemma lift_inv_lref2_be: â\88\80d,e,T1,i. â\86\91[d,e] T1 â\89¡ #i â\86\92
+lemma lift_inv_lref2_be: â\88\80d,e,T1,i. â\87\91[d,e] T1 â\89¡ #i â\86\92
d ≤ i → i < d + e → False.
#d #e #T1 #i #H elim (lift_inv_lref2 … H) -H *
[ #H1 #_ #H2 #_ | #H2 #_ #_ #H1 ]
qed-.
(* Basic_1: was: lift_gen_lref_ge *)
-lemma lift_inv_lref2_ge: â\88\80d,e,T1,i. â\86\91[d,e] T1 â\89¡ #i â\86\92 d + e â\89¤ i â\86\92 T1 = #(i - e).
+lemma lift_inv_lref2_ge: â\88\80d,e,T1,i. â\87\91[d,e] T1 â\89¡ #i â\86\92 d + e â\89¤ i â\86\92 T1 = #(i - e).
#d #e #T1 #i #H elim (lift_inv_lref2 … H) -H * //
#Hid #_ #Hdi lapply (le_to_lt_to_lt … Hdi Hid) -Hdi -Hid #Hdd
elim (lt_inv_plus_l … Hdd) -Hdd #Hdd
elim (lt_refl_false … Hdd)
qed-.
-fact lift_inv_gref2_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80p. T2 = §p â\86\92 T1 = §p.
+fact lift_inv_gref2_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92 â\88\80p. T2 = §p â\86\92 T1 = §p.
#d #e #T1 #T2 * -d -e -T1 -T2 //
[ #i #d #e #_ #k #H destruct
| #I #V1 #V2 #T1 #T2 #d #e #_ #_ #k #H destruct
]
qed.
-lemma lift_inv_gref2: â\88\80d,e,T1,p. â\86\91[d,e] T1 â\89¡ §p â\86\92 T1 = §p.
+lemma lift_inv_gref2: â\88\80d,e,T1,p. â\87\91[d,e] T1 â\89¡ §p â\86\92 T1 = §p.
/2 width=5/ qed-.
-fact lift_inv_bind2_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92
+fact lift_inv_bind2_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92
∀I,V2,U2. T2 = 𝕓{I} V2.U2 →
- â\88\83â\88\83V1,U1. â\86\91[d,e] V1 â\89¡ V2 & â\86\91[d+1,e] U1 â\89¡ U2 &
+ â\88\83â\88\83V1,U1. â\87\91[d,e] V1 â\89¡ V2 & â\87\91[d+1,e] U1 â\89¡ U2 &
T1 = 𝕓{I} V1. U1.
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V2 #U2 #H destruct
qed.
(* Basic_1: was: lift_gen_bind *)
-lemma lift_inv_bind2: â\88\80d,e,T1,I,V2,U2. â\86\91[d,e] T1 â\89¡ ð\9d\95\93{I} V2. U2 â\86\92
- â\88\83â\88\83V1,U1. â\86\91[d,e] V1 â\89¡ V2 & â\86\91[d+1,e] U1 â\89¡ U2 &
+lemma lift_inv_bind2: â\88\80d,e,T1,I,V2,U2. â\87\91[d,e] T1 â\89¡ ð\9d\95\93{I} V2. U2 â\86\92
+ â\88\83â\88\83V1,U1. â\87\91[d,e] V1 â\89¡ V2 & â\87\91[d+1,e] U1 â\89¡ U2 &
T1 = 𝕓{I} V1. U1.
/2 width=3/ qed-.
-fact lift_inv_flat2_aux: â\88\80d,e,T1,T2. â\86\91[d,e] T1 â\89¡ T2 â\86\92
+fact lift_inv_flat2_aux: â\88\80d,e,T1,T2. â\87\91[d,e] T1 â\89¡ T2 â\86\92
∀I,V2,U2. T2 = 𝕗{I} V2.U2 →
- â\88\83â\88\83V1,U1. â\86\91[d,e] V1 â\89¡ V2 & â\86\91[d,e] U1 â\89¡ U2 &
+ â\88\83â\88\83V1,U1. â\87\91[d,e] V1 â\89¡ V2 & â\87\91[d,e] U1 â\89¡ U2 &
T1 = 𝕗{I} V1. U1.
#d #e #T1 #T2 * -d -e -T1 -T2
[ #k #d #e #I #V2 #U2 #H destruct
qed.
(* Basic_1: was: lift_gen_flat *)
-lemma lift_inv_flat2: â\88\80d,e,T1,I,V2,U2. â\86\91[d,e] T1 â\89¡ ð\9d\95\97{I} V2. U2 â\86\92
- â\88\83â\88\83V1,U1. â\86\91[d,e] V1 â\89¡ V2 & â\86\91[d,e] U1 â\89¡ U2 &
+lemma lift_inv_flat2: â\88\80d,e,T1,I,V2,U2. â\87\91[d,e] T1 â\89¡ ð\9d\95\97{I} V2. U2 â\86\92
+ â\88\83â\88\83V1,U1. â\87\91[d,e] V1 â\89¡ V2 & â\87\91[d,e] U1 â\89¡ U2 &
T1 = 𝕗{I} V1. U1.
/2 width=3/ qed-.
-lemma lift_inv_pair_xy_x: â\88\80d,e,I,V,T. â\86\91[d, e] ð\9d\95\94{I} V. T â\89¡ V â\86\92 False.
+lemma lift_inv_pair_xy_x: â\88\80d,e,I,V,T. â\87\91[d, e] ð\9d\95\94{I} V. T â\89¡ V â\86\92 False.
#d #e #J #V elim V -V
[ * #i #T #H
[ lapply (lift_inv_sort2 … H) -H #H destruct
]
qed-.
-lemma lift_inv_pair_xy_y: â\88\80I,T,V,d,e. â\86\91[d, e] ð\9d\95\94{I} V. T â\89¡ T â\86\92 False.
+lemma lift_inv_pair_xy_y: â\88\80I,T,V,d,e. â\87\91[d, e] ð\9d\95\94{I} V. T â\89¡ T â\86\92 False.
#J #T elim T -T
[ * #i #V #d #e #H
[ lapply (lift_inv_sort2 … H) -H #H destruct
(* Basic forward lemmas *****************************************************)
-lemma tw_lift: â\88\80d,e,T1,T2. â\86\91[d, e] T1 â\89¡ T2 â\86\92 #[T1] = #[T2].
+lemma tw_lift: â\88\80d,e,T1,T2. â\87\91[d, e] T1 â\89¡ T2 â\86\92 #[T1] = #[T2].
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
(* Basic properties *********************************************************)
(* Basic_1: was: lift_lref_gt *)
-lemma lift_lref_ge_minus: â\88\80d,e,i. d + e â\89¤ i â\86\92 â\86\91[d, e] #(i - e) â\89¡ #i.
+lemma lift_lref_ge_minus: â\88\80d,e,i. d + e â\89¤ i â\86\92 â\87\91[d, e] #(i - e) â\89¡ #i.
#d #e #i #H >(plus_minus_m_m i e) in ⊢ (? ? ? ? %); /2 width=2/ /3 width=2/
qed.
-lemma lift_lref_ge_minus_eq: â\88\80d,e,i,j. d + e â\89¤ i â\86\92 j = i - e â\86\92 â\86\91[d, e] #j â\89¡ #i.
+lemma lift_lref_ge_minus_eq: â\88\80d,e,i,j. d + e â\89¤ i â\86\92 j = i - e â\86\92 â\87\91[d, e] #j â\89¡ #i.
/2 width=1/ qed-.
(* Basic_1: was: lift_r *)
-lemma lift_refl: â\88\80T,d. â\86\91[d, 0] T â\89¡ T.
+lemma lift_refl: â\88\80T,d. â\87\91[d, 0] T â\89¡ T.
#T elim T -T
[ * #i // #d elim (lt_or_ge i d) /2 width=1/
| * /2 width=1/
]
qed.
-lemma lift_total: â\88\80T1,d,e. â\88\83T2. â\86\91[d,e] T1 â\89¡ T2.
+lemma lift_total: â\88\80T1,d,e. â\88\83T2. â\87\91[d,e] T1 â\89¡ T2.
#T1 elim T1 -T1
[ * #i /2 width=2/ #d #e elim (lt_or_ge i d) /3 width=2/
| * #I #V1 #T1 #IHV1 #IHT1 #d #e
qed.
(* Basic_1: was: lift_free (right to left) *)
-lemma lift_split: â\88\80d1,e2,T1,T2. â\86\91[d1, e2] T1 â\89¡ T2 â\86\92
+lemma lift_split: â\88\80d1,e2,T1,T2. â\87\91[d1, e2] T1 â\89¡ T2 â\86\92
∀d2,e1. d1 ≤ d2 → d2 ≤ d1 + e1 → e1 ≤ e2 →
- â\88\83â\88\83T. â\86\91[d1, e1] T1 â\89¡ T & â\86\91[d2, e2 - e1] T â\89¡ T2.
+ â\88\83â\88\83T. â\87\91[d1, e1] T1 â\89¡ T & â\87\91[d2, e2 - e1] T â\89¡ T2.
#d1 #e2 #T1 #T2 #H elim H -d1 -e2 -T1 -T2
[ /3 width=3/
| #i #d1 #e2 #Hid1 #d2 #e1 #Hd12 #_ #_
qed.
(* Basic_1: was only: dnf_dec2 dnf_dec *)
-lemma is_lift_dec: â\88\80T2,d,e. Decidable (â\88\83T1. â\86\91[d,e] T1 â\89¡ T2).
+lemma is_lift_dec: â\88\80T2,d,e. Decidable (â\88\83T1. â\87\91[d,e] T1 â\89¡ T2).
#T1 elim T1 -T1
[ * [1,3: /3 width=2/ ] #i #d #e
elim (lt_dec i d) #Hid
(* Main properies ***********************************************************)
(* Basic_1: was: lift_inj *)
-theorem lift_inj: â\88\80d,e,T1,U. â\86\91[d,e] T1 â\89¡ U â\86\92 â\88\80T2. â\86\91[d,e] T2 â\89¡ U â\86\92 T1 = T2.
+theorem lift_inj: â\88\80d,e,T1,U. â\87\91[d,e] T1 â\89¡ U â\86\92 â\88\80T2. â\87\91[d,e] T2 â\89¡ U â\86\92 T1 = T2.
#d #e #T1 #U #H elim H -d -e -T1 -U
[ #k #d #e #X #HX
lapply (lift_inv_sort2 … HX) -HX //
qed-.
(* Basic_1: was: lift_gen_lift *)
-theorem lift_div_le: â\88\80d1,e1,T1,T. â\86\91[d1, e1] T1 â\89¡ T â\86\92
- â\88\80d2,e2,T2. â\86\91[d2 + e1, e2] T2 â\89¡ T â\86\92
+theorem lift_div_le: â\88\80d1,e1,T1,T. â\87\91[d1, e1] T1 â\89¡ T â\86\92
+ â\88\80d2,e2,T2. â\87\91[d2 + e1, e2] T2 â\89¡ T â\86\92
d1 ≤ d2 →
- â\88\83â\88\83T0. â\86\91[d1, e1] T0 â\89¡ T2 & â\86\91[d2, e2] T0 â\89¡ T1.
+ â\88\83â\88\83T0. â\87\91[d1, e1] T0 â\89¡ T2 & â\87\91[d2, e2] T0 â\89¡ T1.
#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T
[ #k #d1 #e1 #d2 #e2 #T2 #Hk #Hd12
lapply (lift_inv_sort2 … Hk) -Hk #Hk destruct /3 width=3/
qed.
(* Note: apparently this was missing in Basic_1 *)
-theorem lift_div_be: â\88\80d1,e1,T1,T. â\86\91[d1, e1] T1 â\89¡ T â\86\92
- â\88\80e,e2,T2. â\86\91[d1 + e, e2] T2 â\89¡ T â\86\92
+theorem lift_div_be: â\88\80d1,e1,T1,T. â\87\91[d1, e1] T1 â\89¡ T â\86\92
+ â\88\80e,e2,T2. â\87\91[d1 + e, e2] T2 â\89¡ T â\86\92
e ≤ e1 → e1 ≤ e + e2 →
- â\88\83â\88\83T0. â\86\91[d1, e] T0 â\89¡ T2 & â\86\91[d1, e + e2 - e1] T0 â\89¡ T1.
+ â\88\83â\88\83T0. â\87\91[d1, e] T0 â\89¡ T2 & â\87\91[d1, e + e2 - e1] T0 â\89¡ T1.
#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T
[ #k #d1 #e1 #e #e2 #T2 #H >(lift_inv_sort2 … H) -H /2 width=3/
| #i #d1 #e1 #Hid1 #e #e2 #T2 #H #He1 #He1e2
]
qed.
-theorem lift_mono: â\88\80d,e,T,U1. â\86\91[d,e] T â\89¡ U1 â\86\92 â\88\80U2. â\86\91[d,e] T â\89¡ U2 â\86\92 U1 = U2.
+theorem lift_mono: â\88\80d,e,T,U1. â\87\91[d,e] T â\89¡ U1 â\86\92 â\88\80U2. â\87\91[d,e] T â\89¡ U2 â\86\92 U1 = U2.
#d #e #T #U1 #H elim H -d -e -T -U1
[ #k #d #e #X #HX
lapply (lift_inv_sort1 … HX) -HX //
qed-.
(* Basic_1: was: lift_free (left to right) *)
-theorem lift_trans_be: â\88\80d1,e1,T1,T. â\86\91[d1, e1] T1 â\89¡ T â\86\92
- â\88\80d2,e2,T2. â\86\91[d2, e2] T â\89¡ T2 â\86\92
- d1 â\89¤ d2 â\86\92 d2 â\89¤ d1 + e1 â\86\92 â\86\91[d1, e1 + e2] T1 â\89¡ T2.
+theorem lift_trans_be: â\88\80d1,e1,T1,T. â\87\91[d1, e1] T1 â\89¡ T â\86\92
+ â\88\80d2,e2,T2. â\87\91[d2, e2] T â\89¡ T2 â\86\92
+ d1 â\89¤ d2 â\86\92 d2 â\89¤ d1 + e1 â\86\92 â\87\91[d1, e1 + e2] T1 â\89¡ T2.
#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T
[ #k #d1 #e1 #d2 #e2 #T2 #HT2 #_ #_
>(lift_inv_sort1 … HT2) -HT2 //
qed.
(* Basic_1: was: lift_d (right to left) *)
-theorem lift_trans_le: â\88\80d1,e1,T1,T. â\86\91[d1, e1] T1 â\89¡ T â\86\92
- â\88\80d2,e2,T2. â\86\91[d2, e2] T â\89¡ T2 â\86\92 d2 â\89¤ d1 â\86\92
- â\88\83â\88\83T0. â\86\91[d2, e2] T1 â\89¡ T0 & â\86\91[d1 + e2, e1] T0 â\89¡ T2.
+theorem lift_trans_le: â\88\80d1,e1,T1,T. â\87\91[d1, e1] T1 â\89¡ T â\86\92
+ â\88\80d2,e2,T2. â\87\91[d2, e2] T â\89¡ T2 â\86\92 d2 â\89¤ d1 â\86\92
+ â\88\83â\88\83T0. â\87\91[d2, e2] T1 â\89¡ T0 & â\87\91[d1 + e2, e1] T0 â\89¡ T2.
#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T
[ #k #d1 #e1 #d2 #e2 #X #HX #_
>(lift_inv_sort1 … HX) -HX /2 width=3/
qed.
(* Basic_1: was: lift_d (left to right) *)
-theorem lift_trans_ge: â\88\80d1,e1,T1,T. â\86\91[d1, e1] T1 â\89¡ T â\86\92
- â\88\80d2,e2,T2. â\86\91[d2, e2] T â\89¡ T2 â\86\92 d1 + e1 â\89¤ d2 â\86\92
- â\88\83â\88\83T0. â\86\91[d2 - e1, e2] T1 â\89¡ T0 & â\86\91[d1, e1] T0 â\89¡ T2.
+theorem lift_trans_ge: â\88\80d1,e1,T1,T. â\87\91[d1, e1] T1 â\89¡ T â\86\92
+ â\88\80d2,e2,T2. â\87\91[d2, e2] T â\89¡ T2 â\86\92 d1 + e1 â\89¤ d2 â\86\92
+ â\88\83â\88\83T0. â\87\91[d2 - e1, e2] T1 â\89¡ T0 & â\87\91[d1, e1] T0 â\89¡ T2.
#d1 #e1 #T1 #T #H elim H -d1 -e1 -T1 -T
[ #k #d1 #e1 #d2 #e2 #X #HX #_
>(lift_inv_sort1 … HX) -HX /2 width=3/
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 "Basic_2/grammar/term_vector.ma".
+include "Basic_2/substitution/lift.ma".
+
+(* RELOCATION ***************************************************************)
+
+inductive liftv (d,e:nat) : relation (list term) ≝
+| liftv_nil : liftv d e ◊ ◊
+| liftv_cons: ∀T1s,T2s,T1,T2.
+ ⇑[d, e] T1 ≡ T2 → liftv d e T1s T2s →
+ liftv d e (T1 :: T1s) (T2 :: T2s)
+.
+
+interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s).
+
(* PARALLEL SUBSTITUTION ON LOCAL ENVIRONMENTS ******************************)
lemma ltps_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92
- d1 + e1 â\89¤ e2 â\86\92 â\86\93[0, e2] L1 â\89¡ L2.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92
+ d1 + e1 â\89¤ e2 â\86\92 â\87\93[0, e2] L1 â\89¡ L2.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
| //
qed.
lemma ltps_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92
- d1 + e1 â\89¤ e2 â\86\92 â\86\93[0, e2] L1 â\89¡ L2.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92
+ d1 + e1 â\89¤ e2 â\86\92 â\87\93[0, e2] L1 â\89¡ L2.
#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H //
| //
qed.
lemma ltps_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
- â\88\83â\88\83L. L2 [0, d1 + e1 - e2] â\89« L & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
+ â\88\83â\88\83L. L2 [0, d1 + e1 - e2] â\89« L & â\87\93[0, e2] L1 â\89¡ L.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
qed.
lemma ltps_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
- â\88\83â\88\83L. L [0, d1 + e1 - e2] â\89« L2 & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
+ â\88\83â\88\83L. L [0, d1 + e1 - e2] â\89« L2 & â\87\93[0, e2] L1 â\89¡ L.
#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
| normalize #L #I #V #L2 #e2 #HL2 #_ #He2
qed.
lemma ltps_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫ L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
- â\88\83â\88\83L. L2 [d1 - e2, e1] â\89« L & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
+ â\88\83â\88\83L. L2 [d1 - e2, e1] â\89« L & â\87\93[0, e2] L1 â\89¡ L.
#L0 #L1 #d1 #e1 #H elim H -L0 -L1 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
| /2 width=3/
qed.
lemma ltps_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫ L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
- â\88\83â\88\83L. L [d1 - e2, e1] â\89« L2 & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
+ â\88\83â\88\83L. L [d1 - e2, e1] â\89« L2 & â\87\93[0, e2] L1 â\89¡ L.
#L1 #L0 #d1 #e1 #H elim H -L1 -L0 -d1 -e1
[ #d1 #e1 #L2 #e2 #H >(ldrop_inv_atom1 … H) -H /2 width=3/
| /2 width=3/
inductive tps: nat → nat → lenv → relation term ≝
| tps_atom : ∀L,I,d,e. tps d e L (𝕒{I}) (𝕒{I})
| tps_subst: ∀L,K,V,W,i,d,e. d ≤ i → i < d + e →
- â\86\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 â\86\91[0, i + 1] V â\89¡ W â\86\92 tps d e L (#i) W
+ â\87\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 â\87\91[0, i + 1] V â\89¡ W â\86\92 tps d e L (#i) W
| tps_bind : ∀L,I,V1,V2,T1,T2,d,e.
tps d e L V1 V2 → tps (d + 1) e (L. 𝕓{I} V2) T1 T2 →
tps d e L (𝕓{I} V1. T1) (𝕓{I} V2. T2)
qed.
(* Basic_1: was: subst1_ex *)
-lemma tps_full: â\88\80K,V,T1,L,d. â\86\93[0, d] L â\89¡ (K. ð\9d\95\93{Abbr} V) â\86\92
- â\88\83â\88\83T2,T. L â\8a¢ T1 [d, 1] â\89« T2 & â\86\91[d, 1] T â\89¡ T2.
+lemma tps_full: â\88\80K,V,T1,L,d. â\87\93[0, d] L â\89¡ (K. ð\9d\95\93{Abbr} V) â\86\92
+ â\88\83â\88\83T2,T. L â\8a¢ T1 [d, 1] â\89« T2 & â\87\91[d, 1] T â\89¡ T2.
#K #V #T1 elim T1 -T1
[ * #i #L #d #HLK /2 width=4/
elim (lt_or_eq_or_gt i d) #Hid /3 width=4/
fact tps_inv_atom1_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → ∀I. T1 = 𝕒{I} →
T2 = 𝕒{I} ∨
∃∃K,V,i. d ≤ i & i < d + e &
- â\86\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V &
- â\86\91[O, i + 1] V â\89¡ T2 &
+ â\87\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V &
+ â\87\91[O, i + 1] V â\89¡ T2 &
I = LRef i.
#L #T1 #T2 #d #e * -L -T1 -T2 -d -e
[ #L #I #d #e #J #H destruct /2 width=1/
lemma tps_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫ T2 →
T2 = 𝕒{I} ∨
∃∃K,V,i. d ≤ i & i < d + e &
- â\86\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V &
- â\86\91[O, i + 1] V â\89¡ T2 &
+ â\87\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V &
+ â\87\91[O, i + 1] V â\89¡ T2 &
I = LRef i.
/2 width=3/ qed-.
lemma tps_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫ T2 →
T2 = #i ∨
∃∃K,V. d ≤ i & i < d + e &
- â\86\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V &
- â\86\91[O, i + 1] V â\89¡ T2.
+ â\87\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V &
+ â\87\91[O, i + 1] V â\89¡ T2.
#L #T2 #i #d #e #H
elim (tps_inv_atom1 … H) -H /2 width=1/
* #K #V #j #Hdj #Hjde #HLK #HVT2 #H destruct /3 width=4/
(* Advanced inversion lemmas ************************************************)
fact tps_inv_refl_SO2_aux: ∀L,T1,T2,d,e. L ⊢ T1 [d, e] ≫ T2 → e = 1 →
- â\88\80K,V. â\86\93[0, d] L â\89¡ K. ð\9d\95\93{Abst} V â\86\92 T1 = T2.
+ â\88\80K,V. â\87\93[0, d] L â\89¡ K. ð\9d\95\93{Abst} V â\86\92 T1 = T2.
#L #T1 #T2 #d #e #H elim H -L -T1 -T2 -d -e
[ //
| #L #K0 #V0 #W #i #d #e #Hdi #Hide #HLK0 #_ #H destruct
qed.
lemma tps_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫ T2 →
- â\88\80K,V. â\86\93[0, d] L â\89¡ K. ð\9d\95\93{Abst} V â\86\92 T1 = T2.
+ â\88\80K,V. â\87\93[0, d] L â\89¡ K. ð\9d\95\93{Abst} V â\86\92 T1 = T2.
/2 width=8/ qed-.
(* Relocation properties ****************************************************)
(* Basic_1: was: subst1_lift_lt *)
lemma tps_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
- â\88\80L,U1,U2,d,e. â\86\93[d, e] L â\89¡ K â\86\92
- â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\86\91[d, e] T2 â\89¡ U2 â\86\92
+ â\88\80L,U1,U2,d,e. â\87\93[d, e] L â\89¡ K â\86\92
+ â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\87\91[d, e] T2 â\89¡ U2 â\86\92
dt + et ≤ d →
L ⊢ U1 [dt, et] ≫ U2.
#K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et
qed.
lemma tps_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
- â\88\80L,U1,U2,d,e. â\86\93[d, e] L â\89¡ K â\86\92
- â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\86\91[d, e] T2 â\89¡ U2 â\86\92
+ â\88\80L,U1,U2,d,e. â\87\93[d, e] L â\89¡ K â\86\92
+ â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\87\91[d, e] T2 â\89¡ U2 â\86\92
dt ≤ d → d ≤ dt + et →
L ⊢ U1 [dt, et + e] ≫ U2.
#K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et
(* Basic_1: was: subst1_lift_ge *)
lemma tps_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫ T2 →
- â\88\80L,U1,U2,d,e. â\86\93[d, e] L â\89¡ K â\86\92
- â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\86\91[d, e] T2 â\89¡ U2 â\86\92
+ â\88\80L,U1,U2,d,e. â\87\93[d, e] L â\89¡ K â\86\92
+ â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\87\91[d, e] T2 â\89¡ U2 â\86\92
d ≤ dt →
L ⊢ U1 [dt + e, et] ≫ U2.
#K #T1 #T2 #dt #et #H elim H -K -T1 -T2 -dt -et
(* Basic_1: was: subst1_gen_lift_lt *)
lemma tps_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
dt + et ≤ d →
- â\88\83â\88\83T2. K â\8a¢ T1 [dt, et] â\89« T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [dt, et] â\89« T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et
[ #L * #i #dt #et #K #d #e #_ #T1 #H #_
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
qed.
lemma tps_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
dt ≤ d → d + e ≤ dt + et →
- â\88\83â\88\83T2. K â\8a¢ T1 [dt, et - e] â\89« T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [dt, et - e] â\89« T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et
[ #L * #i #dt #et #K #d #e #_ #T1 #H #_
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
(* Basic_1: was: subst1_gen_lift_ge *)
lemma tps_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
d + e ≤ dt →
- â\88\83â\88\83T2. K â\8a¢ T1 [dt - e, et] â\89« T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [dt - e, et] â\89« T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #H elim H -L -U1 -U2 -dt -et
[ #L * #i #dt #et #K #d #e #_ #T1 #H #_
[ lapply (lift_inv_sort2 … H) -H #H destruct /2 width=3/
(* Basic_1: was: subst1_gen_lift_eq *)
lemma tps_inv_lift1_eq: ∀L,U1,U2,d,e.
- L â\8a¢ U1 [d, e] â\89« U2 â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92 U1 = U2.
+ L â\8a¢ U1 [d, e] â\89« U2 â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92 U1 = U2.
#L #U1 #U2 #d #e #H elim H -L -U1 -U2 -d -e
[ //
| #L #K #V #W #i #d #e #Hdi #Hide #_ #_ #T1 #H
(EX u1 | t1 = (lift (minus (plus d h) (S i)) (S i) u1)).
*)
lemma tps_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
- â\88\83â\88\83T2. K â\8a¢ T1 [d, dt + et - (d + e)] â\89« T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [d, dt + et - (d + e)] â\89« T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (tps_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
lapply (tps_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
qed.
lemma tps_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫ U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
dt ≤ d → dt + et ≤ d + e →
- â\88\83â\88\83T2. K â\8a¢ T1 [dt, d - dt] â\89« T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [dt, d - dt] â\89« T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde
lapply (tps_weak … HU12 dt (d + e - dt) ? ?) -HU12 // /2 width=3/ -Hdetde #HU12
elim (tps_inv_lift1_be … HU12 … HLK … HTU1 ? ?) -U1 -L // /2 width=3/
(* DELIFT ON TERMS **********************************************************)
definition delift: nat → nat → lenv → relation term ≝
- λd,e,L,T1,T2. â\88\83â\88\83T. L â\8a¢ T1 [d, e] â\89«* T & â\86\91[d, e] T2 â\89¡ T.
+ λd,e,L,T1,T2. â\88\83â\88\83T. L â\8a¢ T1 [d, e] â\89«* T & â\87\91[d, e] T2 â\89¡ T.
interpretation "delift (term)"
'TSubst L T1 d e T2 = (delift d e L T1 T2).
lemma delift_fwd_lref1_be: ∀L,U2,d,e,i. L ⊢ #i [d, e] ≡ U2 →
d ≤ i → i < d + e →
- â\88\83â\88\83K,V1,V2. â\86\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
+ â\88\83â\88\83K,V1,V2. â\87\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
K ⊢ V1 [0, d + e - i - 1] ≡ V2 &
- â\86\91[0, d] V2 â\89¡ U2.
+ â\87\91[0, d] V2 â\89¡ U2.
#L #U2 #d #e #i * #U #HU #HU2 #Hdi #Hide
elim (tpss_inv_lref1 … HU) -HU
[ #H destruct elim (lift_inv_lref2_be … HU2 ? ?) //
(* PARTIAL UNFOLD ON LOCAL ENVIRONMENTS *************************************)
lemma ltpss_ldrop_conf_ge: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92
- d1 + e1 â\89¤ e2 â\86\92 â\86\93[0, e2] L1 â\89¡ L2.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92
+ d1 + e1 â\89¤ e2 â\86\92 â\87\93[0, e2] L1 â\89¡ L2.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1 // /3 width=6/
qed.
lemma ltpss_ldrop_trans_ge: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92
- d1 + e1 â\89¤ e2 â\86\92 â\86\93[0, e2] L1 â\89¡ L2.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92
+ d1 + e1 â\89¤ e2 â\86\92 â\87\93[0, e2] L1 â\89¡ L2.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0 // /3 width=6/
qed.
lemma ltpss_ldrop_conf_be: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
- â\88\83â\88\83L. L2 [0, d1 + e1 - e2] â\89«* L & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
+ â\88\83â\88\83L. L2 [0, d1 + e1 - e2] â\89«* L & â\87\93[0, e2] L1 â\89¡ L.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
[ /2 width=3/
| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
qed.
lemma ltpss_ldrop_trans_be: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
- â\88\83â\88\83L. L [0, d1 + e1 - e2] â\89«* L2 & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 d1 â\89¤ e2 â\86\92 e2 â\89¤ d1 + e1 â\86\92
+ â\88\83â\88\83L. L [0, d1 + e1 - e2] â\89«* L2 & â\87\93[0, e2] L1 â\89¡ L.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
[ /2 width=3/
| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #Hd1e2 #He2de1
qed.
lemma ltpss_ldrop_conf_le: ∀L0,L1,d1,e1. L0 [d1, e1] ≫* L1 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
- â\88\83â\88\83L. L2 [d1 - e2, e1] â\89«* L & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
+ â\88\83â\88\83L. L2 [d1 - e2, e1] â\89«* L & â\87\93[0, e2] L1 â\89¡ L.
#L0 #L1 #d1 #e1 #H @(ltpss_ind … H) -L1
[ /2 width=3/
| #L #L1 #_ #HL1 #IHL #L2 #e2 #HL02 #He2d1
qed.
lemma ltpss_ldrop_trans_le: ∀L1,L0,d1,e1. L1 [d1, e1] ≫* L0 →
- â\88\80L2,e2. â\86\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
- â\88\83â\88\83L. L [d1 - e2, e1] â\89«* L2 & â\86\93[0, e2] L1 â\89¡ L.
+ â\88\80L2,e2. â\87\93[0, e2] L0 â\89¡ L2 â\86\92 e2 â\89¤ d1 â\86\92
+ â\88\83â\88\83L. L [d1 - e2, e1] â\89«* L2 & â\87\93[0, e2] L1 â\89¡ L.
#L1 #L0 #d1 #e1 #H @(ltpss_ind … H) -L0
[ /2 width=3/
| #L #L0 #_ #HL0 #IHL #L2 #e2 #HL02 #He2d1
lemma tpss_subst: ∀L,K,V,U1,i,d,e.
d ≤ i → i < d + e →
- â\86\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 K â\8a¢ V [0, d + e - i - 1] â\89«* U1 â\86\92
- â\88\80U2. â\86\91[0, i + 1] U1 â\89¡ U2 â\86\92 L â\8a¢ #i [d, e] â\89«* U2.
+ â\87\93[0, i] L â\89¡ K. ð\9d\95\93{Abbr} V â\86\92 K â\8a¢ V [0, d + e - i - 1] â\89«* U1 â\86\92
+ â\88\80U2. â\87\91[0, i + 1] U1 â\89¡ U2 â\86\92 L â\8a¢ #i [d, e] â\89«* U2.
#L #K #V #U1 #i #d #e #Hdi #Hide #HLK #H @(tpss_ind … H) -U1
[ /3 width=4/
| #U #U1 #_ #HU1 #IHU #U2 #HU12
lemma tpss_inv_atom1: ∀L,T2,I,d,e. L ⊢ 𝕒{I} [d, e] ≫* T2 →
T2 = 𝕒{I} ∨
∃∃K,V1,V2,i. d ≤ i & i < d + e &
- â\86\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
+ â\87\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
- â\86\91[O, i + 1] V2 â\89¡ T2 &
+ â\87\91[O, i + 1] V2 â\89¡ T2 &
I = LRef i.
#L #T2 #I #d #e #H @(tpss_ind … H) -T2
[ /2 width=1/
lemma tpss_inv_lref1: ∀L,T2,i,d,e. L ⊢ #i [d, e] ≫* T2 →
T2 = #i ∨
∃∃K,V1,V2. d ≤ i & i < d + e &
- â\86\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
+ â\87\93[O, i] L â\89¡ K. ð\9d\95\93{Abbr} V1 &
K ⊢ V1 [0, d + e - i - 1] ≫* V2 &
- â\86\91[O, i + 1] V2 â\89¡ T2.
+ â\87\91[O, i + 1] V2 â\89¡ T2.
#L #T2 #i #d #e #H
elim (tpss_inv_atom1 … H) -H /2 width=1/
* #K #V1 #V2 #j #Hdj #Hjde #HLK #HV12 #HVT2 #H destruct /3 width=6/
qed-.
lemma tpss_inv_refl_SO2: ∀L,T1,T2,d. L ⊢ T1 [d, 1] ≫* T2 →
- â\88\80K,V. â\86\93[0, d] L â\89¡ K. ð\9d\95\93{Abst} V â\86\92 T1 = T2.
+ â\88\80K,V. â\87\93[0, d] L â\89¡ K. ð\9d\95\93{Abst} V â\86\92 T1 = T2.
#L #T1 #T2 #d #H #K #V #HLK @(tpss_ind … H) -T2 //
#T #T2 #_ #HT2 #IHT <(tps_inv_refl_SO2 … HT2 … HLK) //
qed-.
(* Relocation properties ****************************************************)
lemma tpss_lift_le: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
- â\88\80L,U1,d,e. dt + et â\89¤ d â\86\92 â\86\93[d, e] L â\89¡ K â\86\92
- â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92
+ â\88\80L,U1,d,e. dt + et â\89¤ d â\86\92 â\87\93[d, e] L â\89¡ K â\86\92
+ â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92
L ⊢ U1 [dt, et] ≫* U2.
#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdetd #HLK #HTU1 @(tpss_ind … H) -T2
[ #U2 #H >(lift_mono … HTU1 … H) -H //
lemma tpss_lift_be: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
∀L,U1,d,e. dt ≤ d → d ≤ dt + et →
- â\86\93[d, e] L â\89¡ K â\86\92 â\86\91[d, e] T1 â\89¡ U1 â\86\92
- â\88\80U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92 L â\8a¢ U1 [dt, et + e] â\89«* U2.
+ â\87\93[d, e] L â\89¡ K â\86\92 â\87\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92 L â\8a¢ U1 [dt, et + e] â\89«* U2.
#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hdtd #Hddet #HLK #HTU1 @(tpss_ind … H) -T2
[ #U2 #H >(lift_mono … HTU1 … H) -H //
| -HTU1 #T #T2 #_ #HT2 #IHT #U2 #HTU2
qed.
lemma tpss_lift_ge: ∀K,T1,T2,dt,et. K ⊢ T1 [dt, et] ≫* T2 →
- â\88\80L,U1,d,e. d â\89¤ dt â\86\92 â\86\93[d, e] L â\89¡ K â\86\92
- â\86\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\86\91[d, e] T2 â\89¡ U2 â\86\92
+ â\88\80L,U1,d,e. d â\89¤ dt â\86\92 â\87\93[d, e] L â\89¡ K â\86\92
+ â\87\91[d, e] T1 â\89¡ U1 â\86\92 â\88\80U2. â\87\91[d, e] T2 â\89¡ U2 â\86\92
L ⊢ U1 [dt + e, et] ≫* U2.
#K #T1 #T2 #dt #et #H #L #U1 #d #e #Hddt #HLK #HTU1 @(tpss_ind … H) -T2
[ #U2 #H >(lift_mono … HTU1 … H) -H //
qed.
lemma tpss_inv_lift1_le: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
dt + et ≤ d →
- â\88\83â\88\83T2. K â\8a¢ T1 [dt, et] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [dt, et] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdetd @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
qed.
lemma tpss_inv_lift1_be: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
dt ≤ d → d + e ≤ dt + et →
- â\88\83â\88\83T2. K â\8a¢ T1 [dt, et - e] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [dt, et - e] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdedet @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
qed.
lemma tpss_inv_lift1_ge: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
d + e ≤ dt →
- â\88\83â\88\83T2. K â\8a¢ T1 [dt - e, et] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [dt - e, et] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdedt @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
qed.
lemma tpss_inv_lift1_eq: ∀L,U1,U2,d,e.
- L â\8a¢ U1 [d, e] â\89«* U2 â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92 U1 = U2.
+ L â\8a¢ U1 [d, e] â\89«* U2 â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92 U1 = U2.
#L #U1 #U2 #d #e #H #T1 #HTU1 @(tpss_ind … H) -U2 //
#U #U2 #_ #HU2 #IHU destruct
<(tps_inv_lift1_eq … HU2 … HTU1) -HU2 -HTU1 //
qed.
lemma tpss_inv_lift1_be_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
dt ≤ d → dt + et ≤ d + e →
- â\88\83â\88\83T2. K â\8a¢ T1 [dt, d - dt] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [dt, d - dt] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #H #K #d #e #HLK #T1 #HTU1 #Hdtd #Hdetde @(tpss_ind … H) -U2
[ /2 width=3/
| -HTU1 #U #U2 #_ #HU2 * #T #HT1 #HTU
qed.
lemma tpss_inv_lift1_up: ∀L,U1,U2,dt,et. L ⊢ U1 [dt, et] ≫* U2 →
- â\88\80K,d,e. â\86\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\86\91[d, e] T1 â\89¡ U1 â\86\92
+ â\88\80K,d,e. â\87\93[d, e] L â\89¡ K â\86\92 â\88\80T1. â\87\91[d, e] T1 â\89¡ U1 â\86\92
d ≤ dt → dt ≤ d + e → d + e ≤ dt + et →
- â\88\83â\88\83T2. K â\8a¢ T1 [d, dt + et - (d + e)] â\89«* T2 & â\86\91[d, e] T2 â\89¡ U2.
+ â\88\83â\88\83T2. K â\8a¢ T1 [d, dt + et - (d + e)] â\89«* T2 & â\87\91[d, e] T2 â\89¡ U2.
#L #U1 #U2 #dt #et #HU12 #K #d #e #HLK #T1 #HTU1 #Hddt #Hdtde #Hdedet
elim (tpss_split_up … HU12 (d + e) ? ?) -HU12 // -Hdedet #U #HU1 #HU2
lapply (tpss_weak … HU1 d e ? ?) -HU1 // [ >commutative_plus /2 width=1/ ] -Hddt -Hdtde #HU1
interpretation "cons (list)" 'Cons hd tl = (cons ? hd tl).
-let rec append A (l1: list A) l2 on l1 ≝
- match l1 with
- [ nil ⇒ l2
- | cons hd tl ⇒ hd :: append A tl l2
+let rec all A (R:predicate A) (l:list A) on l ≝
+ match l with
+ [ nil ⇒ True
+ | cons hd tl ⇒ R hd ∧ all A R tl
].
-
-interpretation "append (list)" 'Append l1 l2 = (append ? l1 l2).
(* Lists ********************************************************************)
+notation "hvbox( ◊ )"
+ non associative with precedence 90
+ for @{'Nil}.
+
notation "hvbox( hd break :: tl )"
right associative with precedence 47
for @{'Cons $hd $tl}.
projects / helm.git / commitdiff