(* *)
(**************************************************************************)
+include "Basic_2/unfold/gr2_gr2.ma".
include "Basic_2/unfold/lifts_lifts.ma".
include "Basic_2/unfold/ldrops_ldrops.ma".
include "Basic_2/static/aaa.ma".
>(lifts_inv_sort1 … H) -H
lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom
@(s2 … HAtom … ◊) // /2 width=2/
-| * #L #K #V #B #i #HLK #_ #IHB #L0 #des #HL0 #X #H #L2 #HL20
- elim (lifts_inv_lref1 … H) -H #i0 #Hi0 #H destruct
- elim (ldrops_ldrop_trans … HL0 … HLK) -L #L #des1 #i1 #HL0 #HLK #Hi1 #Hdes1
-
- elim (lsubc_ldrop_trans … HL20 … HL0) -L0 #L0 #HL20 #HL0
- [
- | lapply (aacr_acr … H1RP H2RP B) #HB
- @(s2 … HB … ◊) //
- @(cp2 … H1RP)
+| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L0 #des #HL01 #X #H #L2 #HL20
+ lapply (aacr_acr … H1RP H2RP B) #HB
+ elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
+ lapply (ldrop_fwd_ldrop2 … HLK1) #HK1b
+ elim (ldrops_ldrop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1
+ >(at_mono … Hi1 … Hi0) -i1
+ elim (ldrops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct
+ elim (lsubc_ldrop_trans … HL20 … HL0) -HL0 #X #HLK2 #H
+ elim (lift_total V0 0 (i0 +1)) #V #HV0
+ elim (lsubc_inv_pair2 … H) -H *
+ [ #K2 #HK20 #H destruct
+ generalize in match HLK2; generalize in match I; -HLK2 -I * #HLK2
+ [ @(s4 … HB … ◊ … HV0 HLK2)
+ @(IHB … HL20) [2: /2 width=6/ | skip ]
+ | skip
+ ]
+(⇧*[des0]V1≡V0) → (⇧[O,i0+1]V0≡V) → (@[i]des≡i0) → (des+1▭i+1≡des0+1) →
+⇧*[{O,i+1}::des]V1≡V)
+
+ Theorem lift1_free: (hds:?; i:?; t:?)
+ (lift1 hds (lift (S i) (0) t)) =
+ (lift (S (trans hds i)) (0) (lift1 (ptrans hds i) t)).
+
+
+
+
+ | @(s2 … HB … ◊) // /2 width=3/
+ ]
+ | #K2 #V2 #A2 #HV2 #HV0 #HK20 #H1 #H2 destruct
]
-
| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (aacr_acr … H1RP H2RP A) #HA
| #L3 #V3 #T3 #des3 #HL32 #HT03 #HB
elim (lifts_total des3 W0) #W2 #HW02
elim (ldrops_lsubc_trans … HL32 … HL02) -L2 #L2 #HL32 #HL20
- @(IHA (L2. 𝕓{Abst} W2) … (ss des @ ss des3))
+ @(IHA (L2. 𝕓{Abst} W2) … (des + 1 @ des3 + 1))
/2 width=3/ /3 width=5/ /4 width=6/
]
| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
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 S4 ≝ λRP,C:lenv→predicate term. ∀L,K,Vs,V1,V2,i.
+ C L (ⒶVs. V2) → ⇧[0, i + 1] V1 ≡ V2 →
+ ⇩[0, i] L ≡ K. 𝕓{Abbr} V1 → C L (Ⓐ Vs. #i).
+
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).
{ s1: S1 RP C;
s2: S2 RR RS RP C;
s3: S3 RP C;
+ s4: S4 RP C;
s5: S5 RP C;
s6: S6 RP C;
s7: S7 C
@conj /2 width=1/ /2 width=6 by rp_lifts/
qed.
-lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+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
| /3 width=7/
]
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 → (
∀L0,V0,T0,des. ⇩*[des] L0 ≡ L → ⇧*[des + 1] T ≡ T0 →
"local environment refinement (abstract candidates of reducibility)"
'CrSubEq L1 RP L2 = (lsubc RP L1 L2).
+(* Basic inversion lemmas ***************************************************)
+
+fact lsubc_inv_pair2_aux: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀I,K2,W. L2 = K2. 𝕓{I} W →
+ (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+ ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & ⦃K2, W⦄ [RP] ϵ 〚A〛 &
+ K1 [RP] ⊑ K2 & L1 = K1. 𝕓{Abbr} V &
+ I = Abst.
+#RP #L1 #L2 * -L1 -L2
+[ #I #K2 #W #H destruct
+| #J #L1 #L2 #V #HL12 #I #K2 #W #H destruct /3 width=3/
+| #L1 #L2 #V1 #W2 #A #H #HV1 #HW2 #I #K2 #W #H destruct /3 width=7/
+]
+qed.
+
+lemma lsubc_inv_pair2: ∀RP,I,L1,K2,W. L1 [RP] ⊑ K2. 𝕓{I} W →
+ (∃∃K1. K1 [RP] ⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+ ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & ⦃K2, W⦄ [RP] ϵ 〚A〛 &
+ K1 [RP] ⊑ K2 & L1 = K1. 𝕓{Abbr} V &
+ I = Abst.
+/2 width=3/ qed-.
+
(* Basic properties *********************************************************)
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/unfold/gr2.ma".
+
+(* GENERIC RELOCATION WITH PAIRS ********************************************)
+
+(* Main properties **********************************************************)
+
+axiom at_mono: ∀des,i,i1. @[i] des ≡ i1 → ∀i2. @[i] des ≡ i2 → i1 = i2.
interpretation "generic local environment slicing"
'RDropStar des T1 T2 = (ldrops des T1 T2).
+(* Basic inversion lemmas ***************************************************)
+
+fact ldrops_inv_nil_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → des = ⟠ → L1 = L2.
+#L1 #L2 #des * -L1 -L2 -des //
+#L1 #L #L2 #d #e #des #_ #_ #H destruct
+qed.
+
+lemma ldrops_inv_nil: ∀L1,L2. ⇩*[⟠] L1 ≡ L2 → L1 = L2.
+/2 width=3/ qed-.
+
+fact ldrops_inv_cons_aux: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 →
+ ∀d,e,tl. des = {d, e} :: tl →
+ ∃∃L. ⇩*[tl] L1 ≡ L & ⇩[d, e] L ≡ L2.
+#L1 #L2 #des * -L1 -L2 -des
+[ #L #d #e #tl #H destruct
+| #L1 #L #L2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
+ /2 width=3/
+qed.
+
+lemma ldrops_inv_cons: ∀L1,L2,d,e,des. ⇩*[{d, e} :: des] L1 ≡ L2 →
+ ∃∃L. ⇩*[des] L1 ≡ L & ⇩[d, e] L ≡ L2.
+/2 width=3/ qed-.
+
+lemma ldrops_inv_skip2: ∀I,des,i,des2. des ▭ i ≡ des2 →
+ ∀L1,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 →
+ ∃∃K1,V1,des1. des + 1 ▭ i + 1 ≡ des1 + 1 &
+ ⇩*[des1] K1 ≡ K2 &
+ ⇧*[des1] V2 ≡ V1 &
+ L1 = K1. 𝕓{I} V1.
+#I #des #i #des2 #H elim H -des -i -des2
+[ #i #L1 #K2 #V2 #H
+ >(ldrops_inv_nil … H) -L1 /2 width=7/
+| #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H
+ elim (ldrops_inv_cons … H) -H #L #HL1 #H
+ elim (ldrop_inv_skip2 … H ?) -H /2 width=1/ #K #V >minus_plus #HK2 #HV2 #H destruct
+ elim (IHdes2 … HL1) -IHdes2 -HL1 #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct
+ @(ex4_3_intro … K1 V1 … ) // [3,4: /2 width=7/ | skip ]
+ normalize >plus_minus // @minuss_lt // /2 width=1/ (**) (* explicit constructors, /3 width=1/ is a bit slow *)
+| #des #des2 #d #e #i #Hid #_ #IHdes2 #L1 #K2 #V2 #H
+ elim (IHdes2 … H) -IHdes2 -H #K1 #V1 #des1 #Hdes1 #HK1 #HV1 #X destruct
+ /4 width=7/
+]
+qed-.
+
(* Basic properties *********************************************************)
lemma ldrops_skip: ∀L1,L2,des. ⇩*[des] L1 ≡ L2 → ∀V1,V2. ⇧*[des] V2 ≡ V1 →
(* Basic_1: removed theorems 1: drop1_getl_trans
*)
-(*
-lemma ldrops_inv_skip2: ∀des2,L1,I,K2,V2. ⇩*[des2] L1 ≡ K2. 𝕓{I} V2 →
- ∀des,i. des ▭ i ≡ des2 →
- ∃∃K1,V1,des1. des ▭ (i + 1) ≡ des1 &
- ⇩*[des1] K1 ≡ K2 &
- ⇧*[des1] V2 ≡ V1 &
- L1 = K1. 𝕓{I} V1.
-*)
\ No newline at end of file
projects / helm.git / commitdiff