(* *)
(**************************************************************************)
-include "Basic_2/substitution/ldrop.ma".
+include "Basic_2/unfold/ldrops.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
definition CP3 ≝ λRR:lenv→relation term. λRP:lenv→predicate term.
∀L,V,k. RP L (𝕔{Appl}⋆k.V) → RP L V.
+definition CP4 ≝ λRR:lenv→relation term. λRS:relation term.
+ ∀L0,L,T,T0,d,e. NF … (RR L) RS T →
+ ⇓[d,e] L0 ≡ L → ⇑[d, e] T ≡ T0 → NF … (RR L0) RS T0.
+
+definition CP4s ≝ λRR:lenv→relation term. λRS:relation term.
+ ∀L0,L,des. ⇓[des] L0 ≡ L →
+ ∀T,T0. ⇑[des] T ≡ T0 →
+ NF … (RR L) RS T → NF … (RR L0) RS T0.
+
(* 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
+ cp3: CP3 RR RP;
+ cp4: CP4 RR RS
}.
+
+(* Basic properties *********************************************************)
+
+lemma acp_lifts: ∀RR,RS. CP4 RR RS → CP4s RR RS.
+#RR #RS #HRR #L1 #L2 #des #H elim H -L1 -L2 -des
+[ #L #T1 #T2 #H #HT1
+ <(lifts_inv_nil … H) -H //
+| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2
+ elim (lifts_inv_cons … H) -H /3 width=9/
+]
+qed.
include "Basic_2/static/aaa.ma".
include "Basic_2/computation/lsubc.ma".
+(*
+axiom lsubc_ldrops_trans: ∀RP,L1,L2. L1 [RP] ⊑ L2 → ∀K2,des. ⇓[des] L2 ≡ K2 →
+ ∃∃K1. ⇓[des] L1 ≡ K1 & K1 [RP] ⊑ K2.
+*)
+axiom ldrops_lsubc_trans: ∀RP,L1,K1,des. ⇓[des] L1 ≡ K1 → ∀K2. K1 [RP] ⊑ K2 →
+ ∃∃L2. L1 [RP] ⊑ L2 & ⇓[des] L2 ≡ K2.
+
+axiom lifts_trans: ∀T1,T,des1. ⇑[des1] T1 ≡ T → ∀T2:term. ∀des2. ⇑[des2] T ≡ T2 →
+ ⇑[des1 @ des2] T1 ≡ T2.
+
+axiom ldrops_trans: ∀L1,L,des1. ⇓[des1] L1 ≡ L → ∀L2,des2. ⇓[des2] L ≡ L2 →
+ ⇓[des2 @ des1] L1 ≡ L2.
(* 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〛.
+axiom 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 #L2 #HL2
+[ (*#L #k #L2 #HL2
lapply (aacr_acr … H1RP H2RP 𝕒) #HAtom
- @(s2 … HAtom … ◊) // /2 width=2/
-| * #L #K #V #B #i #HLK #_ #IHB #L2 #HL2
+ @(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
+(* @(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/
+ @(s5 … HA … ◊ ◊) // /3 width=1/ *)
+| #L #W #T #B #A #_ #_ #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
+ 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))
+ /2 width=3/ /3 width=5/ /4 width=6/
+ ]
| /3 width=1/
| #L #V #T #A #_ #_ #IH1A #IH2A #L2 #HL2
lapply (aacr_acr … H1RP H2RP A) #HA
∀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/
+@(s1 … HA) /2 width=8/
qed.
(**************************************************************************)
include "Basic_2/grammar/aarity.ma".
-include "Basic_2/grammar/term_simple.ma".
-include "Basic_2/substitution/lift_vector.ma".
+include "Basic_2/unfold/lifts_vector.ma".
include "Basic_2/computation/acp.ma".
(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
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.
+definition S7s ≝ λC:lenv→predicate term.
+ ∀L1,L2,des. ⇓[des] L2 ≡ L1 →
+ ∀T1,T2. ⇑[des] T1 ≡ T2 → C L1 T1 → 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;
let rec aacr (RP:lenv→predicate term) (A:aarity) (L:lenv) on A: predicate term ≝
λT. match A with
[ AAtom ⇒ RP L T
-| APair B A ⇒ ∀V. aacr RP B L V → aacr RP A L (𝕔{Appl} V. T)
+| APair B A ⇒ ∀L0,V0,T0,des. aacr RP B L0 V0 → ⇓[des] L0 ≡ L → ⇑[des] T ≡ T0 →
+ aacr RP A L0 (𝕔{Appl} V0. T0)
].
interpretation
(* Basic properties *********************************************************)
+lemma acr_lifts: ∀C. S7 C → S7s C.
+#C #HC #L1 #L2 #des #H elim H -L1 -L2 -des
+[ #L #T1 #T2 #H #HT1
+ <(lifts_inv_nil … H) -H //
+| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #T2 #T1 #H #HLT2
+ elim (lifts_inv_cons … H) -H /3 width=9/
+]
+qed.
+
+lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
+ ∀des,L0,L,V,V0. ⇓[des] L0 ≡ L → ⇑[des] V ≡ V0 →
+ RP L V → RP L0 V0.
+#RR #RS #RP #HRP #des #L0 #L #V #V0 #HL0 #HV0 #HV
+@acr_lifts /width=6/
+@(s7 … HRP)
+qed.
+
+lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP (λL,T. RP L T) →
+ ∀des,L0,L,Vs,V0s. ⇑[des] Vs ≡ V0s → ⇓[des] L0 ≡ L →
+ all … (RP L) Vs → all … (RP L0) V0s.
+#RR #RS #RP #HRP #des #L0 #L #Vs #V0s #H elim H -Vs -V0s normalize //
+#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s #HL0 * #HT1 #HT1s
+@conj /2 width=1/ /2 width=6 by rp_lifts/
+qed.
+
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:
+ lapply (H ? (⋆0) ? ⟠ ? ? ?) -H
+ [1,3: // |2,4: skip
+ | @(s2 … IHB … ◊) // /2 width=2/
+ | #H @(cp3 … H1RP … 0) @(s1 … IHA) //
+ ]
+| #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HB #HL0 #H
+ elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
+ lapply (s1 … IHB … HB) #HV0
+ @(s2 … IHA … (V0 :: V0s)) /2 width=4 by lifts_simple_dx/ /3 width=6/
+| #L #Vs #U #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
+ elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_flat1 … HY) -HY #U0 #X #HU0 #HX #H destruct
+ elim (lifts_inv_bind1 … HX) -HX #W0 #T0 #HW0 #HT0 #H destruct
+ @(s3 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /4 width=5/
+| #L #V1s #V2s #HV12s #V #T #HA #HV #L0 #V10 #X #des #HB #HL0 #H
+ elim (lifts_inv_applv1 … H) -H #V10s #Y #HV10s #HY #H destruct
+ elim (lifts_inv_bind1 … HY) -HY #V0 #T0 #HV0 #HT0 #H destruct
+ elim (lift_total V10 0 1) #V20 #HV120
+ elim (liftv_total 0 1 V10s) #V20s #HV120s
+ @(s5 … IHA … (V10 :: V10s) (V20 :: V20s)) /2 width=1/ /2 width=6 by rp_lifts/
+ @(HA … (ss des)) /2 width=1/
+ [ @(s7 … IHB … HB … HV120) /2 width=1/
+ | @liftsv_applv //
+ ]
+| #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HB #HL0 #H
+ elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
+ @(s6 … IHA … (V0 :: V0s)) /2 width=6 by rp_lifts/ /3 width=4/
+| /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 →
- (∀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
+ ∀L,W,T,A,B. RP L W → (
+ ∀L0,V0,T0,des. ⇓[des] L0 ≡ L → ⇑[ss des] T ≡ T0 →
+ ⦃L0, V0⦄ [RP] ϵ 〚B〛→ ⦃L0. 𝕓{Abbr} V0, T0⦄ [RP] ϵ 〚A〛
+ ) →
+ ⦃L, 𝕓{Abst} W. T⦄ [RP] ϵ 〚𝕔 B. A〛.
+#RR #RS #RP #H1RP #H2RP #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HB #HL0 #H
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/
+elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
+lapply (s1 … HCB) -HCB #HCB
+@(s3 … HCA … ◊) /2 width=6 by rp_lifts/
+@(s5 … HCA … ◊ ◊) // /2 width=1/ /2 width=3/
qed.
(* *)
(**************************************************************************)
-include "Basic_2/grammar/term_simple.ma".
include "Basic_2/substitution/tps.ma".
(* CONTEXT-FREE PARALLEL REDUCTION ON TERMS *********************************)
(**************************************************************************)
include "Basic_2/grammar/term_weight.ma".
+include "Basic_2/grammar/term_simple.ma".
(* RELOCATION ***************************************************************)
#d #e #T1 #T2 #H elim H -d -e -T1 -T2 normalize //
qed-.
+lemma lift_simple_dx: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
+elim (simple_inv_bind … H)
+qed-.
+
+lemma lift_simple_sn: ∀d,e,T1,T2. ⇑[d, e] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
+#d #e #T1 #T2 #H elim H -d -e -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #d #e #_ #_ #_ #_ #H
+elim (simple_inv_bind … H)
+qed-.
+
(* Basic properties *********************************************************)
(* Basic_1: was: lift_lref_gt *)
interpretation "relocation (vector)" 'RLift d e T1s T2s = (liftv d e T1s T2s).
+(* Basic properties *********************************************************)
+
+lemma liftv_total: ∀d,e. ∀T1s:list term. ∃T2s. ⇑[d, e] T1s ≡ T2s.
+#d #e #T1s elim T1s -T1s
+[ /2 width=2/
+| #T1 #T1s * #T2s #HT12s
+ elim (lift_total T1 d e) /3 width=2/
+]
+qed-.
inductive ldrops: list2 nat nat → relation lenv ≝
| ldrops_nil : ∀L. ldrops ⟠ L L
| ldrops_cons: ∀L1,L,L2,des,d,e.
- ⇓[d,e] L1 ≡ L → ldrops des L L2 → ldrops ({d, e} :: des) L1 L2
+ ldrops des L1 L → ⇓[d,e] L ≡ L2 → ldrops ({d, e} :: des) L1 L2
.
interpretation "generic local environment slicing"
- 'RDrop des T1 T2 = (ldrops des T1 T2).
+ 'RLDrop des T1 T2 = (ldrops des T1 T2).
+
+(* Basic properties *********************************************************)
+
+lemma ldrops_skip: ∀L1,L2,des. ⇓[des] L1 ≡ L2 → ∀V1,V2. ⇑[des] V2 ≡ V1 →
+ ∀I. ⇓[ss des] L1. 𝕓{I} V1 ≡ L2. 𝕓{I} V2.
+#L1 #L2 #des #H elim H -L1 -L2 -des
+[ #L #V1 #V2 #HV12 #I
+ >(lifts_inv_nil … HV12) -HV12 //
+| #L1 #L #L2 #des #d #e #_ #HL2 #IHL #V1 #V2 #H #I
+ elim (lifts_inv_cons … H) -H /3 width=5/
+].
+qed.
(* *)
(**************************************************************************)
-include "Basic_2/substitution/lift_vector.ma".
+include "Basic_2/grammar/term_vector.ma".
+include "Basic_2/substitution/lift.ma".
(* GENERIC RELOCATION *******************************************************)
+let rec ss (des:list2 nat nat) ≝ match des with
+[ nil2 ⇒ ⟠
+| cons2 d e des ⇒ {d + 1, e} :: ss des
+].
+
inductive lifts: list2 nat nat → relation term ≝
| lifts_nil : ∀T. lifts ⟠ T T
| lifts_cons: ∀T1,T,T2,des,d,e.
.
interpretation "generic relocation" 'RLift des T1 T2 = (lifts des T1 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact lifts_inv_nil_aux: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → des = ⟠ → T1 = T2.
+#T1 #T2 #des * -T1 -T2 -des //
+#T1 #T #T2 #d #e #des #_ #_ #H destruct
+qed.
+
+lemma lifts_inv_nil: ∀T1,T2. ⇑[⟠] T1 ≡ T2 → T1 = T2.
+/2 width=3/ qed-.
+
+fact lifts_inv_cons_aux: ∀T1,T2,des. ⇑[des] T1 ≡ T2 →
+ ∀d,e,tl. des = {d, e} :: tl →
+ ∃∃T. ⇑[d, e] T1 ≡ T & ⇑[tl] T ≡ T2.
+#T1 #T2 #des * -T1 -T2 -des
+[ #T #d #e #tl #H destruct
+| #T1 #T #T2 #des #d #e #HT1 #HT2 #hd #he #tl #H destruct
+ /2 width=3/
+qed.
+
+lemma lifts_inv_cons: ∀T1,T2,d,e,des. ⇑[{d, e} :: des] T1 ≡ T2 →
+ ∃∃T. ⇑[d, e] T1 ≡ T & ⇑[des] T ≡ T2.
+/2 width=3/ qed-.
+
+lemma lifts_inv_bind1: ∀I,T2,des,V1,U1. ⇑[des] 𝕓{I} V1. U1 ≡ T2 →
+ ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[ss des] U1 ≡ U2 &
+ T2 = 𝕓{I} V2. U2.
+#I #T2 #des elim des -des
+[ #V1 #U1 #H
+ <(lifts_inv_nil … H) -H /2 width=5/
+| #d #e #des #IHdes #V1 #U1 #H
+ elim (lifts_inv_cons … H) -H #X #H #HT2
+ elim (lift_inv_bind1 … H) -H #V #U #HV1 #HU1 #H destruct
+ elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
+ /3 width=5/
+]
+qed-.
+
+lemma lifts_inv_flat1: ∀I,T2,des,V1,U1. ⇑[des] 𝕗{I} V1. U1 ≡ T2 →
+ ∃∃V2,U2. ⇑[des] V1 ≡ V2 & ⇑[des] U1 ≡ U2 &
+ T2 = 𝕗{I} V2. U2.
+#I #T2 #des elim des -des
+[ #V1 #U1 #H
+ <(lifts_inv_nil … H) -H /2 width=5/
+| #d #e #des #IHdes #V1 #U1 #H
+ elim (lifts_inv_cons … H) -H #X #H #HT2
+ elim (lift_inv_flat1 … H) -H #V #U #HV1 #HU1 #H destruct
+ elim (IHdes … HT2) -IHdes -HT2 #V2 #U2 #HV2 #HU2 #H destruct
+ /3 width=5/
+]
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma lifts_simple_dx: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → 𝕊[T1] → 𝕊[T2].
+#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_dx/
+qed-.
+
+lemma lifts_simple_sn: ∀T1,T2,des. ⇑[des] T1 ≡ T2 → 𝕊[T2] → 𝕊[T1].
+#T1 #T2 #des #H elim H -T1 -T2 -des // /3 width=5 by lift_simple_sn/
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma lifts_bind: ∀I,T2,V1,V2,des. ⇑[des] V1 ≡ V2 →
+ ∀T1. ⇑[ss des] T1 ≡ T2 →
+ ⇑[des] 𝕓{I} V1. T1 ≡ 𝕓{I} V2. T2.
+#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+[ #V #T1 #H >(lifts_inv_nil … H) -H //
+| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
+ elim (lifts_inv_cons … H) -H /3 width=3/
+]
+qed.
+
+lemma lifts_flat: ∀I,T2,V1,V2,des. ⇑[des] V1 ≡ V2 →
+ ∀T1. ⇑[des] T1 ≡ T2 →
+ ⇑[des] 𝕗{I} V1. T1 ≡ 𝕗{I} V2. T2.
+#I #T2 #V1 #V2 #des #H elim H -V1 -V2 -des
+[ #V #T1 #H >(lifts_inv_nil … H) -H //
+| #V1 #V #V2 #des #d #e #HV1 #_ #IHV #T1 #H
+ elim (lifts_inv_cons … H) -H /3 width=3/
+]
+qed.
+
+lemma lifts_total: ∀des,T1. ∃T2. ⇑[des] T1 ≡ T2.
+#des elim des -des /2 width=2/
+#d #e #des #IH #T1
+elim (lift_total T1 d e) #T #HT1
+elim (IH T) -IH /3 width=4/
+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/substitution/lift_vector.ma".
+include "Basic_2/unfold/lifts.ma".
+
+(* GENERIC RELOCATION *******************************************************)
+
+inductive liftsv (des:list2 nat nat) : relation (list term) ≝
+| liftsv_nil : liftsv des ◊ ◊
+| liftsv_cons: ∀T1s,T2s,T1,T2.
+ ⇑[des] T1 ≡ T2 → liftsv des T1s T2s →
+ liftsv des (T1 :: T1s) (T2 :: T2s)
+.
+
+interpretation "generic relocation (vector)"
+ 'RLift des T1s T2s = (liftsv des T1s T2s).
+
+(* Basic inversion lemmas ***************************************************)
+
+axiom lifts_inv_applv1: ∀V1s,U1,T2,des. ⇑[des] Ⓐ V1s. U1 ≡ T2 →
+ ∃∃V2s,U2. ⇑[des] V1s ≡ V2s & ⇑[des] U1 ≡ U2 &
+ T2 = Ⓐ V2s. U2.
+
+(* Basic properties *********************************************************)
+
+lemma liftsv_applv: ∀V1s,V2s,des. ⇑[des] V1s ≡ V2s →
+ ∀T1,T2. ⇑[des] T1 ≡ T2 →
+ ⇑[des] Ⓐ V1s. T1 ≡ Ⓐ V2s. T2.
+#V1s #V2s #des #H elim H -V1s -V2s // /3 width=1/
+qed.
interpretation "nil (list of pairs)" 'Nil2 = (nil2 ? ?). (**) (* 'Nil causes unification error in aacr_abst *)
interpretation "cons (list of pairs)" 'Cons hd1 hd2 tl = (cons2 ? ? hd1 hd2 tl).
+
+let rec append2 (A1,A2:Type[0]) (l1,l2:list2 A1 A2) on l1 ≝ match l1 with
+[ nil2 ⇒ l2
+| cons2 a1 a2 tl ⇒ {a1, a2} :: append2 A1 A2 tl l2
+].
+
+interpretation "append (list of pairs)"
+ 'Append l1 l2 = (append2 ? ? l1 l2).
for @{'Nil2}.
notation "hvbox( { hd1 , break hd2 } :: break tl )"
- non associative with precedence 45
+ non associative with precedence 47
for @{'Cons $hd1 $hd2 $tl}.
projects / helm.git / commitdiff