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".
include "Basic_2/computation/lsubc.ma".
(* NOTE: The constant (0) can not be generalized *)
axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇩*[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
∃∃L2. L1 [RP] ⊑ L2 & ⇩*[des] L2 ≡ K2.
+axiom aaa_mono: ∀L,T,A1. L ⊢ T ÷ A1 → ∀A2. L ⊢ T ÷ A2 → A1 = A2.
+
+axiom aaa_lifts: ∀L1,L2,T1,T2,A,des.
+ L1 ⊢ T1 ÷ A → ⇩*[des] L2 ≡ L1 → ⇧*[des] T1 ≡ T2 → L2 ⊢ T2 ÷ A.
+
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
(* Main propertis ***********************************************************)
-axiom aacr_aaa_csubc_lifts: ∀RR,RS,RP.
+theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
∀L1,T,A. L1 ⊢ T ÷ A → ∀L0,des. ⇩*[des] L0 ≡ L1 →
∀T0. ⇧*[des] T ≡ T0 → ∀L2. L2 [RP] ⊑ L0 →
⦃L2, T0⦄ [RP] ϵ 〚A〛.
-(*
#RR #RS #RP #H1RP #H2RP #L1 #T #A #H elim H -L1 -T -A
[ #L #k #L0 #des #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom
@(s2 … HAtom … ◊) // /2 width=2/
-| #I #L1 #K1 #V1 #B #i #HLK1 #_ #IHB #L0 #des #HL01 #X #H #L2 #HL20
+| #I #L1 #K1 #V1 #B #i #HLK1 #HKV1B #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
>(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)).
-
-
-
-
+ [ elim (lift_total V0 0 (i0 +1)) #V #HV0
+ elim (lifts_lift_trans … HV10 … HV0 … Hi0 Hdes0) -HV10 #V2 #HV12 #HV2
+ @(s4 … HB … ◊ … HV0 HLK2) /3 width=7/ (* uses IHB HL20 V2 HV0 *)
| @(s2 … HB … ◊) // /2 width=3/
]
- | #K2 #V2 #A2 #HV2 #HV0 #HK20 #H1 #H2 destruct
+ | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
+ #K2 #V2 #A2 #HKV2A #HKV0A #_ #H1 #H2 destruct
+ lapply (ldrop_fwd_ldrop2 … HLK2) #HLK2b
+ lapply (aaa_lifts … HKV1B HK01 HV10) -HKV1B -HK01 -HV10 #HKV0B
+ >(aaa_mono … HKV0A … HKV0B) in HKV2A; -HKV0A -HKV0B #HKV2B
+ elim (lift_total V2 0 (i0 +1)) #V #HV2
+ @(s4 … HB … ◊ … HV2 HLK2)
+ @(s7 … HB … HKV2B) //
]
| #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 B) #HB
lapply (s1 … HB) -HB #HB
@(s5 … HA … ◊ ◊) // /3 width=5/
-| #L #W #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
+| #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL02
elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
@(aacr_abst … H1RP H2RP)
[ lapply (aacr_acr … H1RP H2RP B) #HB
@(s1 … HB) /2 width=5/
- | #L3 #V3 #T3 #des3 #HL32 #HT03 #HB
+ | -IHB
+ #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) … (des + 1 @ des3 + 1))
- /2 width=3/ /3 width=5/ /4 width=6/
+ lapply (aaa_lifts ? L2 ? W2 ? (des @ des3) HLWB ? ?) -HLWB /2 width=3/ #HLW2B
+ @(IHA (L2. 𝕓{Abst} W2) … (des + 1 @ des3 + 1)) -IHA
+ /2 width=3/ /3 width=5/
]
| #L #V #T #B #A #_ #_ #IHB #IHA #L0 #des #HL0 #X #H #L2 #HL20
elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
lapply (s1 … HA) #H
@(s6 … HA … ◊) /2 width=5/ /3 width=5/
]
-*)
+qed.
+
+lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+ ∀L,T,A. L ⊢ T ÷ A → ⦃L, T⦄ [RP] ϵ 〚A〛.
+/2 width=8/ qed.
+
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=8/
+@(s1 … HA) /2 width=4/
qed.
(* *)
(**************************************************************************)
+include "Basic_2/static/aaa.ma".
include "Basic_2/computation/acp_cr.ma".
(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
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_abbr: ∀L1,L2,V,W,A. ⦃L1, V⦄ [RP] ϵ 〚A〛 → L2 ⊢ W ÷ A →
lsubc RP L1 L2 → lsubc RP (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
.
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.
+ ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ 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/
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.
+ ∃∃K1,V,A. ⦃K1, V⦄ [RP] ϵ 〚A〛 & K2 ⊢ W ÷ A &
+ K1 [RP] ⊑ K2 &
+ L1 = K1. 𝕓{Abbr} V & I = Abst.
/2 width=3/ qed-.
(* Basic properties *********************************************************)
--- /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/lsuba.ma".
+include "Basic_2/computation/acp_aaa.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+
+(* properties concerning lenv refinement for atomic arity assignment ********)
+
+lemma lsubc_lsuba: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP (λL,T. RP L T) →
+ ∀L1,L2. L1 ÷⊑ L2 → L1 [RP] ⊑ L2.
+#RR #RS #RP #H1RP #H2RP #L1 #L2 #H elim H -L1 -L2
+// /2 width=1/ /3 width=4/
+qed.
non associative with precedence 45
for @{ 'AtomicArity $L $T $A }.
+notation "hvbox( T1 ÷ ⊑ break T2 )"
+ non associative with precedence 45
+ for @{ 'CrSubEqA $T1 $T2 }.
+
(* Reducibility *************************************************************)
notation "hvbox( ℝ [ T ] )"
--- /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".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR ATOMIC ARITY ASSIGNMENT *****************)
+
+inductive lsuba: relation lenv ≝
+| lsuba_atom: lsuba (⋆) (⋆)
+| lsuba_pair: ∀I,L1,L2,V. lsuba L1 L2 → lsuba (L1. 𝕓{I} V) (L2. 𝕓{I} V)
+| lsuba_abbr: ∀L1,L2,V,W,A. L1 ⊢ V ÷ A → L2 ⊢ W ÷ A →
+ lsuba L1 L2 → lsuba (L1. 𝕓{Abbr} V) (L2. 𝕓{Abst} W)
+.
+
+interpretation
+ "local environment refinement (atomic arity assigment)"
+ 'CrSubEqA L1 L2 = (lsuba L1 L2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lsuba_inv_pair2_aux: ∀L1,L2. L1 ÷⊑ L2 → ∀I,K2,W. L2 = K2. 𝕓{I} W →
+ (∃∃K1. K1 ÷⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+ ∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
+ L1 = K1. 𝕓{Abbr} V & I = Abst.
+#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 #HV1 #HW2 #HL12 #I #K2 #W #H destruct /3 width=7/
+]
+qed.
+
+lemma lsuba_inv_pair2: ∀I,L1,K2,W. L1 ÷⊑ K2. 𝕓{I} W →
+ (∃∃K1. K1 ÷⊑ K2 & L1 = K1. 𝕓{I} W) ∨
+ ∃∃K1,V,A. K1 ⊢ V ÷ A & K2 ⊢ W ÷ A & K1 ÷⊑ K2 &
+ L1 = K1. 𝕓{Abbr} V & I = Abst.
+/2 width=3/ qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lsuba_refl: ∀L. L ÷⊑ L.
+#L elim L -L // /2 width=1/
+qed.
elim (lift_trans_le … HT13 … HT3 ?) -T3 // /3 width=5/
]
qed-.
+
+(* Basic_1: was: lift1_free (right to left) *)
+axiom lifts_lift_trans: ∀T1,T0,des0. ⇧*[des0] T1 ≡ T0 →
+ ∀T2,i0. ⇧[O, i0 + 1] T0 ≡ T2 →
+ ∀des,i. @[i] des ≡ i0 → des + 1 ▭ i + 1 ≡ des0 + 1 →
+ ∃∃T. ⇧[0, i + 1] T1 ≡ T & ⇧*[des] T ≡ T2.
projects / helm.git / commitdiff