+++ /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/genv.ma".
-include "basic_2/multiple/drops.ma".
-
-(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
-
-definition candidate: Type[0] ≝ relation3 genv lenv term.
-
-definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
- ∀G,L0,L,T,T0,s,d,e. NF … (RR G L) RS T →
- ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0.
-
-definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term.
- ∀G,L0,L,s,des. ⇩*[s, des] L0 ≡ L →
- ∀T,T0. ⇧*[des] T ≡ T0 →
- NF … (RR G L) RS T → NF … (RR G L0) RS T0.
-
-definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
- ∀G,L. ∃k. NF … (RR G L) RS (⋆k).
-
-definition CP2 ≝ λRP:candidate.
- ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T.
-
-(* requirements for abstract computation properties *)
-record acp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝
-{ cp0: CP0 RR RS;
- cp1: CP1 RR RS;
- cp2: CP2 RP
-}.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: nf2_lift1 *)
-lemma acp_lifts: ∀RR,RS. CP0 RR RS → CP0s RR RS.
-#RR #RS #HRR #G #L1 #L2 #s #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=10 by/
-]
-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/multiple/lifts_lifts.ma".
-include "basic_2/multiple/drops_drops.ma".
-include "basic_2/static/aaa_lifts.ma".
-include "basic_2/static/aaa_aaa.ma".
-include "basic_2/computation/lsubc_drops.ma".
-
-(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was: sc3_arity_csubc *)
-theorem aacr_aaa_csubc_lifts: ∀RR,RS,RP.
- acp RR RS RP → acr RR RS RP RP →
- ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 →
- ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
- ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
-#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
-[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20
- >(lifts_inv_sort1 … H) -H
- lapply (aacr_acr … H1RP H2RP (⓪)) #HAtom
- @(s4 … HAtom … (◊)) //
-| #I #G #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 (drop_fwd_drop2 … HLK1) #HK1b
- elim (drops_drop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1
- >(at_mono … Hi1 … Hi0) -i1
- elim (drops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct
- elim (lsubc_drop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
- elim (lsubc_inv_pair2 … H) -H *
- [ #K2 #HK20 #H destruct
- elim (lift_total V0 0 (i0 +1)) #V #HV0
- elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2
- @(s5 … HB … (◊) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
- | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
- #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct
- lapply (drop_fwd_drop2 … HLK2) #HLK2b
- lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
- lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B
- elim (lift_total V0 0 (i0 +1)) #V3 #HV03
- elim (lift_total V2 0 (i0 +1)) #V #HV2
- @(s5 … HB … (◊) … (ⓝV3.V) … HLK2) [2: /2 width=1 by lift_flat/ ]
- @(s7 … HB … (◊)) [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ]
- ]
-| #a #G #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
- lapply (aacr_acr … H1RP H2RP B) #HB
- lapply (s1 … HB) -HB #HB
- @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, drops_skip, liftv_nil/
-| #a #G #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) [ /2 width=5 by/ ]
- #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B
- elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
- lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
- @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
- /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
-| #G #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
- /3 width=10 by drops_nil, lifts_nil/
-| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
- elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
- lapply (aacr_acr … H1RP H2RP A) #HA
- @(s7 … HA … (◊)) /2 width=5 by/
-]
-qed.
-
-(* Basic_1: was: sc3_arity *)
-lemma aacr_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
- ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
-/2 width=8 by drops_nil, lifts_nil, aacr_aaa_csubc_lifts/ qed.
-
-lemma acp_aaa: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
- ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
-#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
-lapply (aacr_acr … H1RP H2RP A) #HA
-@(s1 … HA) /2 width=4 by aacr_aaa/
-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/notation/relations/ineint_5.ma".
-include "basic_2/grammar/aarity.ma".
-include "basic_2/multiple/gr2_gr2.ma".
-include "basic_2/multiple/lifts_lift_vector.ma".
-include "basic_2/multiple/drops_drop.ma".
-include "basic_2/computation/acp.ma".
-
-(* ABSTRACT COMPUTATION PROPERTIES ******************************************)
-
-definition S0 ≝ λC:candidate. ∀G,L2,L1,T1,d,e.
- C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2.
-
-definition S0s ≝ λC:candidate.
- ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 →
- ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2.
-
-(* Note: this is Girard's CR1 *)
-definition S1 ≝ λRP,C:candidate.
- ∀G,L,T. C G L T → RP G L T.
-
-(* Note: this is Tait's iii, or Girard's CR4 *)
-definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate.
- ∀G,L,Vs. all … (RP G L) Vs →
- ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T).
-
-(* Note: this generalizes Tait's ii *)
-definition S3 ≝ λC:candidate.
- ∀a,G,L,Vs,V,T,W.
- C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T).
-
-definition S4 ≝ λRP,C:candidate.
- ∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k).
-
-definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i.
- C G L (ⒶVs.V2) → ⇧[0, i+1] V1 ≡ V2 →
- ⇩[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
-
-definition S6 ≝ λRP,C:candidate.
- ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀a,V,T. C G (L.ⓓV) (ⒶV2s.T) → RP G L V → C G L (ⒶV1s.ⓓ{a}V.T).
-
-definition S7 ≝ λC:candidate.
- ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T).
-
-(* properties of the abstract candidate of reducibility *)
-record acr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝
-{ s0: S0 C;
- s1: S1 RP C;
- s2: S2 RR RS RP C;
- s3: S3 C;
- s4: S4 RP C;
- s5: S5 C;
- s6: S6 RP C;
- s7: S7 C
-}.
-
-(* the functional construction for candidates *)
-definition cfun: candidate → candidate → candidate ≝
- λC1,C2,G,K,T. ∀L,V,U,des.
- ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L V → C2 G L (ⓐV.U).
-
-(* the candidate associated to an atomic arity *)
-let rec aacr (RP:candidate) (A:aarity) on A: candidate ≝
-match A with
-[ AAtom ⇒ RP
-| APair B A ⇒ cfun (aacr RP B) (aacr RP A)
-].
-
-interpretation
- "candidate of reducibility of an atomic arity (abstract)"
- 'InEInt RP G L T A = (aacr RP A G L T).
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: sc3_lift1 *)
-lemma acr_lifts: ∀C. S0 C → S0s C.
-#C #HC #G #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=10 by/
-]
-qed.
-
-lemma rp_lifts: ∀RR,RS,RP. acr RR RS RP RP →
- ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 →
- RP G L V → RP G L0 V0.
-#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV
-@acr_lifts /width=7 by/
-@(s0 … HRP)
-qed.
-
-(* Basic_1: was only: sns3_lifts1 *)
-lemma rp_liftsv_all: ∀RR,RS,RP. acr RR RS RP RP →
- ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s →
- all … (RP G L) Vs → all … (RP G L0) V0s.
-#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize //
-#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/
-qed.
-
-(* Basic_1: was:
- sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift
-*)
-lemma aacr_acr: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
- ∀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
-[ /3 width=7 by drops_cons, lifts_cons/
-| #G #L #T #H
- elim (cp1 … H1RP G L) #k #HK
- lapply (H ? (⋆k) ? (⟠) ? ? ?) -H
- [3,5: // |2,4: skip
- | @(s2 … IHB … (◊)) //
- | #H @(cp2 … H1RP … k) @(s1 … IHA) //
- ]
-| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB
- elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
- lapply (s1 … IHB … HB) #HV0
- @(s2 … IHA … (V0 @ V0s))
- /3 width=14 by rp_liftsv_all, acp_lifts, cp0, lifts_simple_dx, conj/
-| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HL0 #H #HB
- 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)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
-| #G #L #Vs #HVs #k #L0 #V0 #X #des #HL0 #H #HB
- elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
- >(lifts_inv_sort1 … HY) -Y
- lapply (s1 … IHB … HB) #HV0
- @(s4 … IHA … (V0 @ V0s)) /3 width=7 by rp_liftsv_all, conj/
-| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB
- elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
- elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
- elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
- >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
- elim (drops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct
- elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
- elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
- >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
- @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/
-| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HL0 #H #HB
- 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
- @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/
- @(HA … (des + 1)) /2 width=2 by drops_skip/
- [ @lifts_applv //
- elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
- >(liftv_mono … HV12s … HV10s) -V1s //
- | @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/
- ]
-| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HL0 #H #HB
- elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
- elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
- @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/
-]
-qed.
-
-lemma aacr_abst: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
- ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
- ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] W ≡ W0 → ⇧*[des + 1] T ≡ T0 →
- ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
- ) →
- ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
-#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB
-lapply (aacr_acr … H1RP H2RP A) #HCA
-lapply (aacr_acr … H1RP H2RP B) #HCB
-elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
-lapply (acr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0
-@(s3 … HCA … (◊))
-@(s6 … HCA … (◊) (◊)) //
-[ @(HA … HL0) //
-| lapply (s1 … HCB) -HCB #HCB
- @(s7 … H2RP … (◊)) /2 width=1 by/
-]
-qed.
-
-(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *)
-(* Basic_1: removed local theorems 1: sc3_sn3_abst *)
+++ /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/tstc.ma".
-include "basic_2/computation/lpxs_cpxs.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
-
-(* Forward lemmas involving same top term constructor ***********************)
-
-lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≂ U.
-#h #g #G #L #T #HT #U #H
->(cpxs_inv_cnx1 … H HT) -G -L -T //
-qed-.
-
-lemma cpxs_fwd_sort: ∀h,g,G,L,U,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U →
- ⋆k ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h k) ➡*[h, g] U.
-#h #g #G #L #U #k #H
-elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus … n) -n
-[ #k #_ #H -l destruct /2 width=1 by or_introl/
-| #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct
- lapply (deg_next_SO … Hnl) -Hnl #Hnl
- elim (IHn … Hnl) -IHn
- [ #H lapply (tstc_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
- | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n
- /4 width=3 by cpxs_strap2, cpx_st, or_intror/
- | >iter_SO >iter_n_Sm //
- ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_beta *)
-lemma cpxs_fwd_beta: ∀h,g,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[h, g] U →
- ⓐV.ⓛ{a}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[h, g] U.
-#h #g #a #G #L #V #W #T #U #H
-elim (cpxs_inv_appl1 … H) -H *
-[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
-| #b #W0 #T0 #HT0 #HU
- elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
- lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
- /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
-| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
- elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
-]
-qed-.
-
-(* Note: probably this is an inversion lemma *)
-lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
- ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
- ∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U →
- #i ≂ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U.
-#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
-elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/
-* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
-lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
-/4 width=10 by cpxs_lift, drop_fwd_drop2, or_intror/
-qed-.
-
-lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U →
- ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨
- ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U.
-#h #g #a #G #L #V1 #V #T #U #H #V2 #HV12
-elim (cpxs_inv_appl1 … H) -H *
-[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
-| #b #W #T0 #HT0 #HU
- elim (cpxs_inv_abbr1 … HT0) -HT0 *
- [ #V3 #T3 #_ #_ #H destruct
- | #X #HT2 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
- @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
- /4 width=7 by cpx_zeta, lift_bind, lift_flat/
- ]
-| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
- @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
- elim (cpxs_inv_abbr1 … HT0) -HT0 *
- [ #V5 #T5 #HV5 #HT5 #H destruct
- lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3
- /3 width=2 by cpxs_flat, cpxs_bind, drop_drop/
- | #X #HT1 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
- lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=2 by drop_drop/ #HV24
- @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
- @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5
- @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/
- ]
-]
-qed-.
-
-lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U →
- ∨∨ ⓝW. T ≂ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U.
-#h #g #G #L #W #T #U #H
-elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
-#W0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/
-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/grammar/tstc_vector.ma".
-include "basic_2/substitution/lift_vector.ma".
-include "basic_2/computation/cpxs_tstc.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
-
-(* Vector form of forward lemmas involving same top term constructor ********)
-
-(* Basic_1: was just: nf2_iso_appls_lref *)
-lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
- ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≂ U.
-#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
-#V #Vs #IHVs #U #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair/
-| #a #W0 #T0 #HT0 #HU
- lapply (IHVs … HT0) -IHVs -HT0 #HT0
- elim (tstc_inv_bind_applv_simple … HT0) //
-| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
- lapply (IHVs … HT0) -IHVs -HT0 #HT0
- elim (tstc_inv_bind_applv_simple … HT0) //
-]
-qed-.
-
-lemma cpxs_fwd_sort_vector: ∀h,g,G,L,k,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆k ➡*[h, g] U →
- ⒶVs.⋆k ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h k) ➡*[h, g] U.
-#h #g #G #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
-#V #Vs #IHVs #U #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
-| #a #W1 #T1 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1 #HT1
- [ elim (tstc_inv_bind_applv_simple … HT1) //
- | @or_intror (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
- ]
-| #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1 #HT1
- [ elim (tstc_inv_bind_applv_simple … HT1) //
- | @or_intror (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
- ]
-]
-qed-.
-
-
-(* Basic_1: was just: pr3_iso_appls_beta *)
-lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U →
- ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U.
-#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
-#V0 #Vs #IHVs #V #W #T #U #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
-| #b #W1 #T1 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1 #HT1
- [ elim (tstc_inv_bind_applv_simple … HT1) //
- | @or_intror (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
- ]
-| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
- elim (IHVs … HT1) -IHVs -HT1 #HT1
- [ elim (tstc_inv_bind_applv_simple … HT1) //
- | @or_intror (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
- ]
-]
-qed-.
-
-lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
- ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
- ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ➡*[h, g] U →
- ⒶVs.#i ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ➡*[h, g] U.
-#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/
-#V #Vs #IHVs #U #H -K -V1
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
-| #b #W0 #T0 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (tstc_inv_bind_applv_simple … HT0) //
- | @or_intror -i (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
- ]
-| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (tstc_inv_bind_applv_simple … HT0) //
- | @or_intror -i (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
- ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_appls_abbr *)
-lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U →
- ⒶV1s. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U.
-#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1 by or_intror/
-#V1s #V2s #V1a #V2a #HV12a #HV12s #a
-generalize in match HV12a; -HV12a
-generalize in match V2a; -V2a
-generalize in match V1a; -V1a
-elim HV12s -V1s -V2s /2 width=1 by cpxs_fwd_theta/
-#V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or_introl/
-| #b #W0 #T0 #HT0 #HU
- elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0
- [ -HV12a -HV12b -HU
- elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct
- | @or_intror -V1s (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- elim (cpxs_inv_abbr1 … HT0) -HT0 *
- [ -HV12a -HV12b #V1 #T1 #_ #_ #H destruct
- | -V1b #X #HT1 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
- @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s
- @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0))
- /4 width=7 by cpxs_beta_dx, cpx_zeta, lift_bind, lift_flat/
- ]
- ]
-| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
- elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0
- [ -HV12a -HV10a -HV0a -HU
- elim (tstc_inv_pair1 … HT0) #V1 #T1 #H destruct
- | @or_intror -V1s -V1b (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- elim (cpxs_inv_abbr1 … HT0) -HT0 *
- [ #V1 #T1 #HV1 #HT1 #H destruct
- lapply (cpxs_lift … HV10a (L.ⓓV) (Ⓕ) … HV12a … HV0a) -V1a -V0a [ /2 width=1 by drop_drop/ ] #HV2a
- @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
- | #X #HT1 #H #H0 destruct
- elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
- lapply (cpxs_lift … HV10a (L.ⓓV0) (Ⓕ) … HV12a … HV0a) -V0a [ /2 width=1 by drop_drop/ ] #HV2a
- @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s
- @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1
- @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/
- ]
- ]
-]
-qed-.
-
-(* Basic_1: was just: pr3_iso_appls_cast *)
-lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U →
- ∨∨ ⒶVs. ⓝW. T ≂ U
- | ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U
- | ⦃G, L⦄ ⊢ ⒶVs.W ➡*[h, g] U.
-#h #g #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
-#V #Vs #IHVs #W #T #U #H
-elim (cpxs_inv_appl1 … H) -H *
-[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tstc_pair, or3_intro0/
-| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (tstc_inv_bind_applv_simple … HT0) //
- | @or3_intro1 -W (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
- | @or3_intro2 -T (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
- ]
-| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
- elim (IHVs … HT0) -IHVs -HT0 #HT0
- [ elim (tstc_inv_bind_applv_simple … HT0) //
- | @or3_intro1 -W (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
- | @or3_intro2 -T (**) (* explicit constructor *)
- @(cpxs_trans … HU) -U
- @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
- ]
-]
-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/grammar/tsts.ma".
+include "basic_2/computation/lpxs_cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Forward lemmas involving same top term structure *************************)
+
+lemma cpxs_fwd_cnx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ → ∀U. ⦃G, L⦄ ⊢ T ➡*[h, g] U → T ≂ U.
+#h #g #G #L #T #HT #U #H
+>(cpxs_inv_cnx1 … H HT) -G -L -T //
+qed-.
+
+lemma cpxs_fwd_sort: ∀h,g,G,L,U,k. ⦃G, L⦄ ⊢ ⋆k ➡*[h, g] U →
+ ⋆k ≂ U ∨ ⦃G, L⦄ ⊢ ⋆(next h k) ➡*[h, g] U.
+#h #g #G #L #U #k #H
+elim (cpxs_inv_sort1 … H) -H #n #l generalize in match k; -k @(nat_ind_plus … n) -n
+[ #k #_ #H -l destruct /2 width=1 by or_introl/
+| #n #IHn #k >plus_plus_comm_23 #Hnl #H destruct
+ lapply (deg_next_SO … Hnl) -Hnl #Hnl
+ elim (IHn … Hnl) -IHn
+ [ #H lapply (tsts_inv_atom1 … H) -H #H >H -H /2 width=1 by or_intror/
+ | generalize in match Hnl; -Hnl @(nat_ind_plus … n) -n
+ /4 width=3 by cpxs_strap2, cpx_st, or_intror/
+ | >iter_SO >iter_n_Sm //
+ ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_beta *)
+lemma cpxs_fwd_beta: ∀h,g,a,G,L,V,W,T,U. ⦃G, L⦄ ⊢ ⓐV.ⓛ{a}W.T ➡*[h, g] U →
+ ⓐV.ⓛ{a}W.T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}ⓝW.V.T ➡*[h, g] U.
+#h #g #a #G #L #V #W #T #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #b #W0 #T0 #HT0 #HU
+ elim (cpxs_inv_abst1 … HT0) -HT0 #W1 #T1 #HW1 #HT1 #H destruct
+ lapply (lsubr_cpxs_trans … HT1 (L.ⓓⓝW.V) ?) -HT1
+ /5 width=3 by cpxs_trans, cpxs_bind, cpxs_pair_sn, lsubr_beta, or_intror/
+| #b #V1 #V2 #V0 #T1 #_ #_ #HT1 #_
+ elim (cpxs_inv_abst1 … HT1) -HT1 #W2 #T2 #_ #_ #H destruct
+]
+qed-.
+
+(* Note: probably this is an inversion lemma *)
+lemma cpxs_fwd_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
+ ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+ ∀U. ⦃G, L⦄ ⊢ #i ➡*[h, g] U →
+ #i ≂ U ∨ ⦃G, L⦄ ⊢ V2 ➡*[h, g] U.
+#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #U #H
+elim (cpxs_inv_lref1 … H) -H /2 width=1 by or_introl/
+* #I0 #K0 #V0 #U0 #HLK0 #HVU0 #HU0
+lapply (drop_mono … HLK0 … HLK) -HLK0 #H destruct
+/4 width=10 by cpxs_lift, drop_fwd_drop2, or_intror/
+qed-.
+
+lemma cpxs_fwd_theta: ∀h,g,a,G,L,V1,V,T,U. ⦃G, L⦄ ⊢ ⓐV1.ⓓ{a}V.T ➡*[h, g] U →
+ ∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1.ⓓ{a}V.T ≂ U ∨
+ ⦃G, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[h, g] U.
+#h #g #a #G #L #V1 #V #T #U #H #V2 #HV12
+elim (cpxs_inv_appl1 … H) -H *
+[ -HV12 #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #b #W #T0 #HT0 #HU
+ elim (cpxs_inv_abbr1 … HT0) -HT0 *
+ [ #V3 #T3 #_ #_ #H destruct
+ | #X #HT2 #H #H0 destruct
+ elim (lift_inv_bind1 … H) -H #W2 #T2 #HW2 #HT02 #H destruct
+ @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓛ{b}W2.T2)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓛ{b}W.T0)) [2: /2 width=1 by cpxs_beta_dx/ ]
+ /4 width=7 by cpx_zeta, lift_bind, lift_flat/
+ ]
+| #b #V3 #V4 #V0 #T0 #HV13 #HV34 #HT0 #HU
+ @or_intror @(cpxs_trans … HU) -U (**) (* explicit constructor *)
+ elim (cpxs_inv_abbr1 … HT0) -HT0 *
+ [ #V5 #T5 #HV5 #HT5 #H destruct
+ lapply (cpxs_lift … HV13 (L.ⓓV) … HV12 … HV34) -V1 -V3
+ /3 width=2 by cpxs_flat, cpxs_bind, drop_drop/
+ | #X #HT1 #H #H0 destruct
+ elim (lift_inv_bind1 … H) -H #V5 #T5 #HV05 #HT05 #H destruct
+ lapply (cpxs_lift … HV13 (L.ⓓV0) … HV12 … HV34) -V3 /2 width=2 by drop_drop/ #HV24
+ @(cpxs_trans … (+ⓓV.ⓐV2.ⓓ{b}V5.T5)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T
+ @(cpxs_strap2 … (ⓐV1.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V5 -T5
+ @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/
+ ]
+]
+qed-.
+
+lemma cpxs_fwd_cast: ∀h,g,G,L,W,T,U. ⦃G, L⦄ ⊢ ⓝW.T ➡*[h, g] U →
+ ∨∨ ⓝW. T ≂ U | ⦃G, L⦄ ⊢ T ➡*[h, g] U | ⦃G, L⦄ ⊢ W ➡*[h, g] U.
+#h #g #G #L #W #T #U #H
+elim (cpxs_inv_cast1 … H) -H /2 width=1 by or3_intro1, or3_intro2/ *
+#W0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/
+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/grammar/tsts_vector.ma".
+include "basic_2/substitution/lift_vector.ma".
+include "basic_2/computation/cpxs_tsts.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Vector form of forward lemmas involving same top term structure **********)
+
+(* Basic_1: was just: nf2_iso_appls_lref *)
+lemma cpxs_fwd_cnx_vector: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
+ ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U → ⒶVs.T ≂ U.
+#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ @(cpxs_fwd_cnx … H2T) ] (**) (* /2 width=3 by cpxs_fwd_cnx/ does not work *)
+#V #Vs #IHVs #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair/
+| #a #W0 #T0 #HT0 #HU
+ lapply (IHVs … HT0) -IHVs -HT0 #HT0
+ elim (tsts_inv_bind_applv_simple … HT0) //
+| #a #V1 #V2 #V0 #T0 #HV1 #HV12 #HT0 #HU
+ lapply (IHVs … HT0) -IHVs -HT0 #HT0
+ elim (tsts_inv_bind_applv_simple … HT0) //
+]
+qed-.
+
+lemma cpxs_fwd_sort_vector: ∀h,g,G,L,k,Vs,U. ⦃G, L⦄ ⊢ ⒶVs.⋆k ➡*[h, g] U →
+ ⒶVs.⋆k ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.⋆(next h k) ➡*[h, g] U.
+#h #g #G #L #k #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_sort/
+#V #Vs #IHVs #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #a #W1 #T1 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (tsts_inv_bind_applv_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV.ⓛ{a}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
+ ]
+| #a #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (tsts_inv_bind_applv_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV1.ⓓ{a}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
+ ]
+]
+qed-.
+
+
+(* Basic_1: was just: pr3_iso_appls_beta *)
+lemma cpxs_fwd_beta_vector: ∀h,g,a,G,L,Vs,V,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓐV.ⓛ{a}W.T ➡*[h, g] U →
+ ⒶVs. ⓐV. ⓛ{a}W. T ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.ⓓ{a}ⓝW.V.T ➡*[h, g] U.
+#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_beta/
+#V0 #Vs #IHVs #V #W #T #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V1 #T1 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #b #W1 #T1 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (tsts_inv_bind_applv_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓛ{b}W1.T1)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
+ ]
+| #b #V1 #V2 #V3 #T1 #HV01 #HV12 #HT1 #HU
+ elim (IHVs … HT1) -IHVs -HT1 #HT1
+ [ elim (tsts_inv_bind_applv_simple … HT1) //
+ | @or_intror (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV1.ⓓ{b}V3.T1)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
+ ]
+]
+qed-.
+
+lemma cpxs_fwd_delta_vector: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
+ ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+ ∀Vs,U. ⦃G, L⦄ ⊢ ⒶVs.#i ➡*[h, g] U →
+ ⒶVs.#i ≂ U ∨ ⦃G, L⦄ ⊢ ⒶVs.V2 ➡*[h, g] U.
+#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs /2 width=5 by cpxs_fwd_delta/
+#V #Vs #IHVs #U #H -K -V1
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #b #W0 #T0 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tsts_inv_bind_applv_simple … HT0) //
+ | @or_intror -i (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /3 width=1 by cpxs_flat_dx, cpr_cpx, cpr_beta/
+ ]
+| #b #V0 #V1 #V3 #T0 #HV0 #HV01 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tsts_inv_bind_applv_simple … HT0) //
+ | @or_intror -i (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V3.T0)) /3 width=3 by cpxs_flat, cpr_cpx, cpr_theta/
+ ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_abbr *)
+lemma cpxs_fwd_theta_vector: ∀h,g,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀a,V,T,U. ⦃G, L⦄ ⊢ ⒶV1s.ⓓ{a}V.T ➡*[h, g] U →
+ ⒶV1s. ⓓ{a}V. T ≂ U ∨ ⦃G, L⦄ ⊢ ⓓ{a}V.ⒶV2s.T ➡*[h, g] U.
+#h #g #G #L #V1s #V2s * -V1s -V2s /3 width=1 by or_intror/
+#V1s #V2s #V1a #V2a #HV12a #HV12s #a
+generalize in match HV12a; -HV12a
+generalize in match V2a; -V2a
+generalize in match V1a; -V1a
+elim HV12s -V1s -V2s /2 width=1 by cpxs_fwd_theta/
+#V1s #V2s #V1b #V2b #HV12b #_ #IHV12s #V1a #V2a #HV12a #V #T #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHV12s -HV12a -HV12b #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or_introl/
+| #b #W0 #T0 #HT0 #HU
+ elim (IHV12s … HV12b … HT0) -IHV12s -HT0 #HT0
+ [ -HV12a -HV12b -HU
+ elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct
+ | @or_intror -V1s (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ elim (cpxs_inv_abbr1 … HT0) -HT0 *
+ [ -HV12a -HV12b #V1 #T1 #_ #_ #H destruct
+ | -V1b #X #HT1 #H #H0 destruct
+ elim (lift_inv_bind1 … H) -H #W1 #T1 #HW01 #HT01 #H destruct
+ @(cpxs_trans … (+ⓓV.ⓐV2a.ⓛ{b}W1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s
+ @(cpxs_strap2 … (ⓐV1a.ⓛ{b}W0.T0))
+ /4 width=7 by cpxs_beta_dx, cpx_zeta, lift_bind, lift_flat/
+ ]
+ ]
+| #b #V0a #Va #V0 #T0 #HV10a #HV0a #HT0 #HU
+ elim (IHV12s … HV12b … HT0) -HV12b -IHV12s -HT0 #HT0
+ [ -HV12a -HV10a -HV0a -HU
+ elim (tsts_inv_pair1 … HT0) #V1 #T1 #H destruct
+ | @or_intror -V1s -V1b (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ elim (cpxs_inv_abbr1 … HT0) -HT0 *
+ [ #V1 #T1 #HV1 #HT1 #H destruct
+ lapply (cpxs_lift … HV10a (L.ⓓV) (Ⓕ) … HV12a … HV0a) -V1a -V0a [ /2 width=1 by drop_drop/ ] #HV2a
+ @(cpxs_trans … (ⓓ{a}V.ⓐV2a.T1)) /3 width=1 by cpxs_bind, cpxs_pair_sn, cpxs_flat_dx, cpxs_bind_dx/
+ | #X #HT1 #H #H0 destruct
+ elim (lift_inv_bind1 … H) -H #V1 #T1 #HW01 #HT01 #H destruct
+ lapply (cpxs_lift … HV10a (L.ⓓV0) (Ⓕ) … HV12a … HV0a) -V0a [ /2 width=1 by drop_drop/ ] #HV2a
+ @(cpxs_trans … (+ⓓV.ⓐV2a.ⓓ{b}V1.T1)) [ /3 width=1 by cpxs_flat_dx, cpxs_bind_dx/ ] -T -V2b -V2s
+ @(cpxs_strap2 … (ⓐV1a.ⓓ{b}V0.T0)) [ /4 width=7 by cpx_zeta, lift_bind, lift_flat/ ] -V -V1 -T1
+ @(cpxs_strap2 … (ⓓ{b}V0.ⓐV2a.T0)) /3 width=3 by cpxs_pair_sn, cpxs_bind_dx, cpr_cpx, cpr_theta/
+ ]
+ ]
+]
+qed-.
+
+(* Basic_1: was just: pr3_iso_appls_cast *)
+lemma cpxs_fwd_cast_vector: ∀h,g,G,L,Vs,W,T,U. ⦃G, L⦄ ⊢ ⒶVs.ⓝW.T ➡*[h, g] U →
+ ∨∨ ⒶVs. ⓝW. T ≂ U
+ | ⦃G, L⦄ ⊢ ⒶVs.T ➡*[h, g] U
+ | ⦃G, L⦄ ⊢ ⒶVs.W ➡*[h, g] U.
+#h #g #G #L #Vs elim Vs -Vs /2 width=1 by cpxs_fwd_cast/
+#V #Vs #IHVs #W #T #U #H
+elim (cpxs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1 by tsts_pair, or3_intro0/
+| #b #W0 #T0 #HT0 #HU elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tsts_inv_bind_applv_simple … HT0) //
+ | @or3_intro1 -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
+ | @or3_intro2 -T (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV.ⓛ{b}W0.T0)) /2 width=1 by cpxs_flat_dx, cpx_beta/
+ ]
+| #b #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tsts_inv_bind_applv_simple … HT0) //
+ | @or3_intro1 -W (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
+ | @or3_intro2 -T (**) (* explicit constructor *)
+ @(cpxs_trans … HU) -U
+ @(cpxs_strap1 … (ⓐV0.ⓓ{b}V2.T0)) /2 width=3 by cpxs_flat, cpx_theta/
+ ]
+]
+qed-.
(* *)
(**************************************************************************)
-include "basic_2/computation/acp_aaa.ma".
+include "basic_2/computation/gcp_aaa.ma".
include "basic_2/computation/cpxs_aaa.ma".
-include "basic_2/computation/csx_tstc_vector.ma".
+include "basic_2/computation/csx_tsts_vector.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
theorem aaa_csx: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T.
#h #g #G #L #T #A #H
-@(acp_aaa … (csx_acp h g) (csx_acr h g) … H)
+@(gcr_aaa … (csx_gcp h g) (csx_gcr h g) … H)
qed.
(* Advanced eliminators *****************************************************)
(**************************************************************************)
include "basic_2/reduction/cnx_lift.ma".
-include "basic_2/computation/acp.ma".
+include "basic_2/computation/gcp.ma".
include "basic_2/computation/csx.ma".
(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************)
(* Main properties **********************************************************)
-theorem csx_acp: ∀h,g. acp (cpx h g) (eq …) (csx h g).
-#h #g @mk_acp
+theorem csx_gcp: ∀h,g. gcp (cpx h g) (eq …) (csx h g).
+#h #g @mk_gcp
[ /3 width=13 by cnx_lift/
| #G #L elim (deg_total h g 0) /3 width=8 by cnx_sort_iter, ex_intro/
| /2 width=3 by csx_fwd_flat_dx/
(* *)
(**************************************************************************)
-include "basic_2/grammar/tstc_tstc.ma".
+include "basic_2/grammar/tsts_tsts.ma".
include "basic_2/computation/cpxs_cpxs.ma".
include "basic_2/computation/csx_alt.ma".
include "basic_2/computation/csx_lift.ma".
/2 width=5 by csx_appl_theta_aux/ qed.
(* Basic_1: was just: sn3_appl_appl *)
-lemma csx_appl_simple_tstc: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
+lemma csx_appl_simple_tsts: ∀h,g,G,L,V. ⦃G, L⦄ ⊢ ⬊*[h, g] V → ∀T1. ⦃G, L⦄ ⊢ ⬊*[h, g] T1 →
(∀T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 ≂ T2 → ⊥) → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T2) →
𝐒⦃T1⦄ → ⦃G, L⦄ ⊢ ⬊*[h, g] ⓐV.T1.
#h #g #G #L #V #H @(csx_ind … H) -V #V #_ #IHV #T1 #H @(csx_ind … H) -T1 #T1 #H1T1 #IHT1 #H2T1 #H3T1
@(csx_cpx_trans … (ⓐV0.T1)) /2 width=1 by cpx_flat/ -HLT10
@IHV -IHV /4 width=3 by csx_cpx_trans, cpx_pair_sn/
| -IHV -H1T1 -HLV0 * #H #H1T10 destruct
- elim (tstc_dec T1 T0) #H2T10
- [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tstc_canc_sn, simple_tstc_repl_dx/
+ elim (tsts_dec T1 T0) #H2T10
+ [ @IHT1 -IHT1 /4 width=3 by cpxs_strap2, cpxs_strap1, tsts_canc_sn, simple_tsts_repl_dx/
| -IHT1 -H3T1 -H1T10 /3 width=1 by cpx_cpxs/
]
]
+++ /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_cr.ma".
-include "basic_2/computation/cpxs_tstc_vector.ma".
-include "basic_2/computation/csx_lpx.ma".
-include "basic_2/computation/csx_vector.ma".
-
-(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************)
-
-(* Advanced properties ******************************************************)
-
-(* Basic_1: was just: sn3_appls_lref *)
-lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
- ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T.
-#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
-#V #Vs #IHV #H
-elim (csxv_inv_cons … H) -H #HV #HVs
-@csx_appl_simple_tstc /2 width=1 by applv_simple/ -IHV -HV -HVs
-#X #H #H0
-lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
-elim (H0) -H0 //
-qed.
-
-lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
-#h #g #G #L #k elim (deg_total h g k)
-#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ]
-#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
-#Hkl #Vs elim Vs -Vs /2 width=1 by/
-#V #Vs #IHVs #HVVs
-elim (csxv_inv_cons … HVVs) #HV #HVs
-@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs
-#X #H #H0
-elim (cpxs_fwd_sort_vector … H) -H #H
-[ elim H0 -H0 //
-| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1 by cpxs_flat_dx/
-]
-qed.
-
-(* Basic_1: was just: sn3_appls_beta *)
-lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
- ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T.
-#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
-#V0 #Vs #IHV #V #W #T #H1T
-lapply (csx_fwd_pair_sn … H1T) #HV0
-lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
-#X #H #H0
-elim (cpxs_fwd_beta_vector … H) -H #H
-[ -H1T elim H0 -H0 //
-| -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
-]
-qed.
-
-lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
- ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
- ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
-#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
-[ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/
-| #V #Vs #IHV #H1T
- lapply (csx_fwd_pair_sn … H1T) #HV
- lapply (csx_fwd_flat_dx … H1T) #H2T
- @csx_appl_simple_tstc /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T
- #X #H #H0
- elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
- [ -H1T elim H0 -H0 //
- | -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
- ]
-]
-qed.
-
-(* Basic_1: was just: sn3_appls_abbr *)
-lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T →
- ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T.
-#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/
-#V1s #V2s #V1 #V2 #HV12 #H
-generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
-elim H -V1s -V2s /2 width=3 by csx_appl_theta/
-#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H
-lapply (csx_appl_theta … HW12 … H) -H -HW12 #H
-lapply (csx_fwd_pair_sn … H) #HW1
-lapply (csx_fwd_flat_dx … H) #H1
-@csx_appl_simple_tstc /2 width=3 by simple_flat/ -IHV12s -HW1 -H1 #X #H1 #H2
-elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -HV12s -HV12
-[ -H #H elim H2 -H2 //
-| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
-]
-qed.
-
-(* Basic_1: was just: sn3_appls_cast *)
-lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
- ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T.
-#h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
-#V #Vs #IHV #W #T #H1W #H1T
-lapply (csx_fwd_pair_sn … H1W) #HV
-lapply (csx_fwd_flat_dx … H1W) #H2W
-lapply (csx_fwd_flat_dx … H1T) #H2T
-@csx_appl_simple_tstc /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T
-#X #H #H0
-elim (cpxs_fwd_cast_vector … H) -H #H
-[ -H1W -H1T elim H0 -H0 //
-| -H1W -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
-| -H1T -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
-]
-qed.
-
-theorem csx_acr: ∀h,g. acr (cpx h g) (eq …) (csx h g) (csx h g).
-#h #g @mk_acr //
-[ /2 width=8 by csx_lift/
-| /3 width=1 by csx_applv_cnx/
-|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/
-| /2 width=7 by csx_applv_delta/
-| #G #L #V1s #V2s #HV12s #a #V #T #H #HV
- @(csx_applv_theta … HV12s) -HV12s
- @csx_abbr //
-]
-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/computation/gcp_cr.ma".
+include "basic_2/computation/cpxs_tsts_vector.ma".
+include "basic_2/computation/csx_lpx.ma".
+include "basic_2/computation/csx_vector.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERM VECTORS *************)
+
+(* Advanced properties ******************************************************)
+
+(* Basic_1: was just: sn3_appls_lref *)
+lemma csx_applv_cnx: ∀h,g,G,L,T. 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ ➡[h, g] 𝐍⦃T⦄ →
+ ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T.
+#h #g #G #L #T #H1T #H2T #Vs elim Vs -Vs [ #_ @(cnx_csx … H2T) ] (**) (* /2 width=1/ does not work *)
+#V #Vs #IHV #H
+elim (csxv_inv_cons … H) -H #HV #HVs
+@csx_appl_simple_tsts /2 width=1 by applv_simple/ -IHV -HV -HVs
+#X #H #H0
+lapply (cpxs_fwd_cnx_vector … H) -H // -H1T -H2T #H
+elim (H0) -H0 //
+qed.
+
+lemma csx_applv_sort: ∀h,g,G,L,k,Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] Vs → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.⋆k.
+#h #g #G #L #k elim (deg_total h g k)
+#l generalize in match k; -k @(nat_ind_plus … l) -l [ /3 width=6 by csx_applv_cnx, cnx_sort, simple_atom/ ]
+#l #IHl #k #Hkl lapply (deg_next_SO … Hkl) -Hkl
+#Hkl #Vs elim Vs -Vs /2 width=1 by/
+#V #Vs #IHVs #HVVs
+elim (csxv_inv_cons … HVVs) #HV #HVs
+@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHVs -HV -HVs
+#X #H #H0
+elim (cpxs_fwd_sort_vector … H) -H #H
+[ elim H0 -H0 //
+| -H0 @(csx_cpxs_trans … (Ⓐ(V@Vs).⋆(next h k))) /2 width=1 by cpxs_flat_dx/
+]
+qed.
+
+(* Basic_1: was just: sn3_appls_beta *)
+lemma csx_applv_beta: ∀h,g,a,G,L,Vs,V,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓓ{a}ⓝW.V.T →
+ ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs. ⓐV.ⓛ{a}W.T.
+#h #g #a #G #L #Vs elim Vs -Vs /2 width=1 by csx_appl_beta/
+#V0 #Vs #IHV #V #W #T #H1T
+lapply (csx_fwd_pair_sn … H1T) #HV0
+lapply (csx_fwd_flat_dx … H1T) #H2T
+@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV0 -H2T
+#X #H #H0
+elim (cpxs_fwd_beta_vector … H) -H #H
+[ -H1T elim H0 -H0 //
+| -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
+]
+qed.
+
+lemma csx_applv_delta: ∀h,g,I,G,L,K,V1,i. ⇩[i] L ≡ K.ⓑ{I}V1 →
+ ∀V2. ⇧[0, i + 1] V1 ≡ V2 →
+ ∀Vs. ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.V2) → ⦃G, L⦄ ⊢ ⬊*[h, g] (ⒶVs.#i).
+#h #g #I #G #L #K #V1 #i #HLK #V2 #HV12 #Vs elim Vs -Vs
+[ /4 width=12 by csx_inv_lift, csx_lref_bind, drop_fwd_drop2/
+| #V #Vs #IHV #H1T
+ lapply (csx_fwd_pair_sn … H1T) #HV
+ lapply (csx_fwd_flat_dx … H1T) #H2T
+ @csx_appl_simple_tsts /2 width=1 by applv_simple, simple_atom/ -IHV -HV -H2T
+ #X #H #H0
+ elim (cpxs_fwd_delta_vector … HLK … HV12 … H) -HLK -HV12 -H #H
+ [ -H1T elim H0 -H0 //
+ | -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
+ ]
+]
+qed.
+
+(* Basic_1: was just: sn3_appls_abbr *)
+lemma csx_applv_theta: ∀h,g,a,G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀V,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⓓ{a}V.ⒶV2s.T →
+ ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶV1s.ⓓ{a}V.T.
+#h #g #a #G #L #V1s #V2s * -V1s -V2s /2 width=1 by/
+#V1s #V2s #V1 #V2 #HV12 #H
+generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
+elim H -V1s -V2s /2 width=3 by csx_appl_theta/
+#V1s #V2s #V1 #V2 #HV12 #HV12s #IHV12s #W1 #W2 #HW12 #V #T #H
+lapply (csx_appl_theta … HW12 … H) -H -HW12 #H
+lapply (csx_fwd_pair_sn … H) #HW1
+lapply (csx_fwd_flat_dx … H) #H1
+@csx_appl_simple_tsts /2 width=3 by simple_flat/ -IHV12s -HW1 -H1 #X #H1 #H2
+elim (cpxs_fwd_theta_vector … (V2@V2s) … H1) -H1 /2 width=1 by liftv_cons/ -HV12s -HV12
+[ -H #H elim H2 -H2 //
+| -H2 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
+]
+qed.
+
+(* Basic_1: was just: sn3_appls_cast *)
+lemma csx_applv_cast: ∀h,g,G,L,Vs,W,T. ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.W → ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.T →
+ ⦃G, L⦄ ⊢ ⬊*[h, g] ⒶVs.ⓝW.T.
+#h #g #G #L #Vs elim Vs -Vs /2 width=1 by csx_cast/
+#V #Vs #IHV #W #T #H1W #H1T
+lapply (csx_fwd_pair_sn … H1W) #HV
+lapply (csx_fwd_flat_dx … H1W) #H2W
+lapply (csx_fwd_flat_dx … H1T) #H2T
+@csx_appl_simple_tsts /2 width=1 by applv_simple, simple_flat/ -IHV -HV -H2W -H2T
+#X #H #H0
+elim (cpxs_fwd_cast_vector … H) -H #H
+[ -H1W -H1T elim H0 -H0 //
+| -H1W -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
+| -H1T -H0 /3 width=5 by csx_cpxs_trans, cpxs_flat_dx/
+]
+qed.
+
+theorem csx_gcr: ∀h,g. gcr (cpx h g) (eq …) (csx h g) (csx h g).
+#h #g @mk_gcr //
+[ /2 width=8 by csx_lift/
+| /3 width=1 by csx_applv_cnx/
+|3,4,7: /2 width=1 by csx_applv_beta, csx_applv_sort, csx_applv_cast/
+| /2 width=7 by csx_applv_delta/
+| #G #L #V1s #V2s #HV12s #a #V #T #H #HV
+ @(csx_applv_theta … HV12s) -HV12s
+ @csx_abbr //
+]
+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/grammar/genv.ma".
+include "basic_2/multiple/drops.ma".
+
+(* GENERIC COMPUTATION PROPERTIES *******************************************)
+
+definition candidate: Type[0] ≝ relation3 genv lenv term.
+
+definition CP0 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+ ∀G,L0,L,T,T0,s,d,e. NF … (RR G L) RS T →
+ ⇩[s, d, e] L0 ≡ L → ⇧[d, e] T ≡ T0 → NF … (RR G L0) RS T0.
+
+definition CP0s ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+ ∀G,L0,L,s,des. ⇩*[s, des] L0 ≡ L →
+ ∀T,T0. ⇧*[des] T ≡ T0 →
+ NF … (RR G L) RS T → NF … (RR G L0) RS T0.
+
+definition CP1 ≝ λRR:relation4 genv lenv term term. λRS:relation term.
+ ∀G,L. ∃k. NF … (RR G L) RS (⋆k).
+
+definition CP2 ≝ λRP:candidate.
+ ∀G,L,T,k. RP G L (ⓐ⋆k.T) → RP G L T.
+
+(* requirements for generic computation properties *)
+record gcp (RR:relation4 genv lenv term term) (RS:relation term) (RP:candidate) : Prop ≝
+{ cp0: CP0 RR RS;
+ cp1: CP1 RR RS;
+ cp2: CP2 RP
+}.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: nf2_lift1 *)
+lemma gcp_lifts: ∀RR,RS. CP0 RR RS → CP0s RR RS.
+#RR #RS #HRR #G #L1 #L2 #s #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=10 by/
+]
+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/multiple/lifts_lifts.ma".
+include "basic_2/multiple/drops_drops.ma".
+include "basic_2/static/aaa_lifts.ma".
+include "basic_2/static/aaa_aaa.ma".
+include "basic_2/computation/lsubc_drops.ma".
+
+(* GENERIC COMPUTATION PROPERTIES *******************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: sc3_arity_csubc *)
+theorem acr_aaa_csubc_lifts: ∀RR,RS,RP.
+ gcp RR RS RP → gcr RR RS RP RP →
+ ∀G,L1,T,A. ⦃G, L1⦄ ⊢ T ⁝ A → ∀L0,des. ⇩*[Ⓕ, des] L0 ≡ L1 →
+ ∀T0. ⇧*[des] T ≡ T0 → ∀L2. G ⊢ L2 ⫃[RP] L0 →
+ ⦃G, L2, T0⦄ ϵ[RP] 〚A〛.
+#RR #RS #RP #H1RP #H2RP #G #L1 #T #A #H elim H -G -L1 -T -A
+[ #G #L #k #L0 #des #HL0 #X #H #L2 #HL20
+ >(lifts_inv_sort1 … H) -H
+ lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
+ @(s4 … HAtom … (◊)) //
+| #I #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #des #HL01 #X #H #L2 #HL20
+ lapply (acr_gcr … H1RP H2RP B) #HB
+ elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct
+ lapply (drop_fwd_drop2 … HLK1) #HK1b
+ elim (drops_drop_trans … HL01 … HLK1) #X #des1 #i0 #HL0 #H #Hi0 #Hdes1
+ >(at_mono … Hi1 … Hi0) -i1
+ elim (drops_inv_skip2 … Hdes1 … H) -des1 #K0 #V0 #des0 #Hdes0 #HK01 #HV10 #H destruct
+ elim (lsubc_drop_O1_trans … HL20 … HL0) -HL0 #X #HLK2 #H
+ elim (lsubc_inv_pair2 … H) -H *
+ [ #K2 #HK20 #H destruct
+ elim (lift_total V0 0 (i0 +1)) #V #HV0
+ elim (lifts_lift_trans … Hi0 … Hdes0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2
+ @(s5 … HB … (◊) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
+ | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hdes0
+ #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct
+ lapply (drop_fwd_drop2 … HLK2) #HLK2b
+ lapply (aaa_lifts … HK01 … HV10 HKV1B) -HKV1B -HK01 -HV10 #HKV0B
+ lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B
+ elim (lift_total V0 0 (i0 +1)) #V3 #HV03
+ elim (lift_total V2 0 (i0 +1)) #V #HV2
+ @(s5 … HB … (◊) … (ⓝV3.V) … HLK2) [2: /2 width=1 by lift_flat/ ]
+ @(s7 … HB … (◊)) [ @(s0 … HB … HKV2A) // | @(s0 … HB … H1KV0A) // ]
+ ]
+| #a #G #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 (acr_gcr … H1RP H2RP A) #HA
+ lapply (acr_gcr … H1RP H2RP B) #HB
+ lapply (s1 … HB) -HB #HB
+ @(s6 … HA … (◊) (◊)) /3 width=5 by lsubc_pair, drops_skip, liftv_nil/
+| #a #G #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
+ @(acr_abst … H1RP H2RP) [ /2 width=5 by/ ]
+ #L3 #V3 #W3 #T3 #des3 #HL32 #HW03 #HT03 #H1B #H2B
+ elim (drops_lsubc_trans … H1RP H2RP … HL32 … HL02) -L2 #L2 #HL32 #HL20
+ lapply (aaa_lifts … L2 W3 … (des @@ des3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B
+ @(IHA (L2. ⓛW3) … (des + 1 @@ des3 + 1)) -IHA
+ /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/
+| #G #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
+ /3 width=10 by drops_nil, lifts_nil/
+| #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #des #HL0 #X #H #L2 #HL20
+ elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct
+ lapply (acr_gcr … H1RP H2RP A) #HA
+ @(s7 … HA … (◊)) /2 width=5 by/
+]
+qed.
+
+(* Basic_1: was: sc3_arity *)
+lemma acr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
+ ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L, T⦄ ϵ[RP] 〚A〛.
+/2 width=8 by drops_nil, lifts_nil, acr_aaa_csubc_lifts/ qed.
+
+lemma gcr_aaa: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
+ ∀G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → RP G L T.
+#RR #RS #RP #H1RP #H2RP #G #L #T #A #HT
+lapply (acr_gcr … H1RP H2RP A) #HA
+@(s1 … HA) /2 width=4 by acr_aaa/
+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/notation/relations/ineint_5.ma".
+include "basic_2/grammar/aarity.ma".
+include "basic_2/multiple/mr2_mr2.ma".
+include "basic_2/multiple/lifts_lift_vector.ma".
+include "basic_2/multiple/drops_drop.ma".
+include "basic_2/computation/gcp.ma".
+
+(* GENERIC COMPUTATION PROPERTIES *******************************************)
+
+definition S0 ≝ λC:candidate. ∀G,L2,L1,T1,d,e.
+ C G L1 T1 → ∀T2. ⇩[Ⓕ, d, e] L2 ≡ L1 → ⇧[d, e] T1 ≡ T2 → C G L2 T2.
+
+definition S0s ≝ λC:candidate.
+ ∀G,L1,L2,des. ⇩*[Ⓕ, des] L2 ≡ L1 →
+ ∀T1,T2. ⇧*[des] T1 ≡ T2 → C G L1 T1 → C G L2 T2.
+
+(* Note: this is Girard's CR1 *)
+definition S1 ≝ λRP,C:candidate.
+ ∀G,L,T. C G L T → RP G L T.
+
+(* Note: this is Tait's iii, or Girard's CR4 *)
+definition S2 ≝ λRR:relation4 genv lenv term term. λRS:relation term. λRP,C:candidate.
+ ∀G,L,Vs. all … (RP G L) Vs →
+ ∀T. 𝐒⦃T⦄ → NF … (RR G L) RS T → C G L (ⒶVs.T).
+
+(* Note: this generalizes Tait's ii *)
+definition S3 ≝ λC:candidate.
+ ∀a,G,L,Vs,V,T,W.
+ C G L (ⒶVs.ⓓ{a}ⓝW.V.T) → C G L (ⒶVs.ⓐV.ⓛ{a}W.T).
+
+definition S4 ≝ λRP,C:candidate.
+ ∀G,L,Vs. all … (RP G L) Vs → ∀k. C G L (ⒶVs.⋆k).
+
+definition S5 ≝ λC:candidate. ∀I,G,L,K,Vs,V1,V2,i.
+ C G L (ⒶVs.V2) → ⇧[0, i+1] V1 ≡ V2 →
+ ⇩[i] L ≡ K.ⓑ{I}V1 → C G L (ⒶVs.#i).
+
+definition S6 ≝ λRP,C:candidate.
+ ∀G,L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
+ ∀a,V,T. C G (L.ⓓV) (ⒶV2s.T) → RP G L V → C G L (ⒶV1s.ⓓ{a}V.T).
+
+definition S7 ≝ λC:candidate.
+ ∀G,L,Vs,T,W. C G L (ⒶVs.T) → C G L (ⒶVs.W) → C G L (ⒶVs.ⓝW.T).
+
+(* requirements for the generic reducibility candidate *)
+record gcr (RR:relation4 genv lenv term term) (RS:relation term) (RP,C:candidate) : Prop ≝
+{ s0: S0 C;
+ s1: S1 RP C;
+ s2: S2 RR RS RP C;
+ s3: S3 C;
+ s4: S4 RP C;
+ s5: S5 C;
+ s6: S6 RP C;
+ s7: S7 C
+}.
+
+(* the functional construction for candidates *)
+definition cfun: candidate → candidate → candidate ≝
+ λC1,C2,G,K,T. ∀L,V,U,des.
+ ⇩*[Ⓕ, des] L ≡ K → ⇧*[des] T ≡ U → C1 G L V → C2 G L (ⓐV.U).
+
+(* the reducibility candidate associated to an atomic arity *)
+let rec acr (RP:candidate) (A:aarity) on A: candidate ≝
+match A with
+[ AAtom ⇒ RP
+| APair B A ⇒ cfun (acr RP B) (acr RP A)
+].
+
+interpretation
+ "candidate of reducibility of an atomic arity (abstract)"
+ 'InEInt RP G L T A = (acr RP A G L T).
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: sc3_lift1 *)
+lemma gcr_lifts: ∀C. S0 C → S0s C.
+#C #HC #G #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=10 by/
+]
+qed.
+
+lemma rp_lifts: ∀RR,RS,RP. gcr RR RS RP RP →
+ ∀des,G,L0,L,V,V0. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] V ≡ V0 →
+ RP G L V → RP G L0 V0.
+#RR #RS #RP #HRP #des #G #L0 #L #V #V0 #HL0 #HV0 #HV
+@gcr_lifts /width=7 by/
+@(s0 … HRP)
+qed.
+
+(* Basic_1: was only: sns3_lifts1 *)
+lemma rp_liftsv_all: ∀RR,RS,RP. gcr RR RS RP RP →
+ ∀des,G,L0,L,Vs,V0s. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] Vs ≡ V0s →
+ all … (RP G L) Vs → all … (RP G L0) V0s.
+#RR #RS #RP #HRP #des #G #L0 #L #Vs #V0s #HL0 #H elim H -Vs -V0s normalize //
+#T1s #T2s #T1 #T2 #HT12 #_ #IHT2s * /3 width=7 by rp_lifts, conj/
+qed.
+
+(* Basic_1: was:
+ sc3_sn3 sc3_abst sc3_appl sc3_abbr sc3_bind sc3_cast sc3_lift
+*)
+lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
+ ∀A. gcr RR RS RP (acr RP A).
+#RR #RS #RP #H1RP #H2RP #A elim A -A normalize //
+#B #A #IHB #IHA @mk_gcr normalize
+[ /3 width=7 by drops_cons, lifts_cons/
+| #G #L #T #H
+ elim (cp1 … H1RP G L) #k #HK
+ lapply (H ? (⋆k) ? (⟠) ? ? ?) -H
+ [3,5: // |2,4: skip
+ | @(s2 … IHB … (◊)) //
+ | #H @(cp2 … H1RP … k) @(s1 … IHA) //
+ ]
+| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #des #HL0 #H #HB
+ elim (lifts_inv_applv1 … H) -H #V0s #T0 #HV0s #HT0 #H destruct
+ lapply (s1 … IHB … HB) #HV0
+ @(s2 … IHA … (V0 @ V0s))
+ /3 width=14 by rp_liftsv_all, gcp_lifts, cp0, lifts_simple_dx, conj/
+| #a #G #L #Vs #U #T #W #HA #L0 #V0 #X #des #HL0 #H #HB
+ 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)) /5 width=6 by lifts_applv, lifts_flat, lifts_bind/
+| #G #L #Vs #HVs #k #L0 #V0 #X #des #HL0 #H #HB
+ elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ >(lifts_inv_sort1 … HY) -Y
+ lapply (s1 … IHB … HB) #HV0
+ @(s4 … IHA … (V0 @ V0s)) /3 width=7 by rp_liftsv_all, conj/
+| #I #G #L #K #Vs #V1 #V2 #i #HA #HV12 #HLK #L0 #V0 #X #des #HL0 #H #HB
+ elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_lref1 … HY) -HY #i0 #Hi0 #H destruct
+ elim (drops_drop_trans … HL0 … HLK) #X #des0 #i1 #HL02 #H #Hi1 #Hdes0
+ >(at_mono … Hi1 … Hi0) in HL02; -i1 #HL02
+ elim (drops_inv_skip2 … Hdes0 … H) -H -des0 #L2 #W1 #des0 #Hdes0 #HLK #HVW1 #H destruct
+ elim (lift_total W1 0 (i0 + 1)) #W2 #HW12
+ elim (lifts_lift_trans … Hdes0 … HVW1 … HW12) // -Hdes0 -Hi0 #V3 #HV13 #HVW2
+ >(lift_mono … HV13 … HV12) in HVW2; -V3 #HVW2
+ @(s5 … IHA … (V0 @ V0s) … HW12 HL02) /3 width=5 by lifts_applv/
+| #G #L #V1s #V2s #HV12s #a #V #T #HA #HV #L0 #V10 #X #des #HL0 #H #HB
+ 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
+ @(s6 … IHA … (V10 @ V10s) (V20 @ V20s)) /3 width=7 by rp_lifts, liftv_cons/
+ @(HA … (des + 1)) /2 width=2 by drops_skip/
+ [ @lifts_applv //
+ elim (liftsv_liftv_trans_le … HV10s … HV120s) -V10s #V10s #HV10s #HV120s
+ >(liftv_mono … HV12s … HV10s) -V1s //
+ | @(s0 … IHB … HB … HV120) /2 width=2 by drop_drop/
+ ]
+| #G #L #Vs #T #W #HA #HW #L0 #V0 #X #des #HL0 #H #HB
+ elim (lifts_inv_applv1 … H) -H #V0s #Y #HV0s #HY #H destruct
+ elim (lifts_inv_flat1 … HY) -HY #W0 #T0 #HW0 #HT0 #H destruct
+ @(s7 … IHA … (V0 @ V0s)) /3 width=5 by lifts_applv/
+]
+qed.
+
+lemma acr_abst: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
+ ∀a,G,L,W,T,A,B. ⦃G, L, W⦄ ϵ[RP] 〚B〛 → (
+ ∀L0,V0,W0,T0,des. ⇩*[Ⓕ, des] L0 ≡ L → ⇧*[des] W ≡ W0 → ⇧*[des + 1] T ≡ T0 →
+ ⦃G, L0, V0⦄ ϵ[RP] 〚B〛 → ⦃G, L0, W0⦄ ϵ[RP] 〚B〛 → ⦃G, L0.ⓓⓝW0.V0, T0⦄ ϵ[RP] 〚A〛
+ ) →
+ ⦃G, L, ⓛ{a}W.T⦄ ϵ[RP] 〚②B.A〛.
+#RR #RS #RP #H1RP #H2RP #a #G #L #W #T #A #B #HW #HA #L0 #V0 #X #des #HL0 #H #HB
+lapply (acr_gcr … H1RP H2RP A) #HCA
+lapply (acr_gcr … H1RP H2RP B) #HCB
+elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct
+lapply (gcr_lifts … HL0 … HW0 HW) -HW [ @(s0 … HCB) ] #HW0
+@(s3 … HCA … (◊))
+@(s6 … HCA … (◊) (◊)) //
+[ @(HA … HL0) //
+| lapply (s1 … HCB) -HCB #HCB
+ @(s7 … H2RP … (◊)) /2 width=1 by/
+]
+qed.
+
+(* Basic_1: removed theorems 2: sc3_arity_gen sc3_repl *)
+(* Basic_1: removed local theorems 1: sc3_sn3_abst *)
(**************************************************************************)
include "basic_2/notation/relations/lrsubeqc_4.ma".
+include "basic_2/static/lsubr.ma".
include "basic_2/static/aaa.ma".
-include "basic_2/computation/acp_cr.ma".
+include "basic_2/computation/gcp_cr.ma".
-(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
inductive lsubc (RP) (G): relation lenv ≝
| lsubc_atom: lsubc RP G (⋆) (⋆)
.
interpretation
- "local environment refinement (abstract candidates of reducibility)"
+ "local environment refinement (generic reducibility)"
'LRSubEqC RP G L1 L2 = (lsubc RP G L1 L2).
(* Basic inversion lemmas ***************************************************)
L1 = K1.ⓓⓝW.V & I = Abst.
/2 width=3 by lsubc_inv_pair2_aux/ qed-.
+(* Basic forward lemmas *****************************************************)
+
+lemma lsubc_fwd_lsubr: ∀RP,G,L1,L2. G ⊢ L1 ⫃[RP] L2 → L1 ⫃ L2.
+#RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubr_pair, lsubr_beta/
+qed-.
+
(* Basic properties *********************************************************)
(* Basic_1: was just: csubc_refl *)
include "basic_2/static/aaa_lift.ma".
include "basic_2/computation/lsubc.ma".
-(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
(* Properties concerning basic local environment slicing ********************)
(* Basic_1: was: csubc_drop_conf_rev *)
lemma drop_lsubc_trans: ∀RR,RS,RP.
- acp RR RS RP → acr RR RS RP RP →
+ gcp RR RS RP → gcr RR RS RP RP →
∀G,L1,K1,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩[Ⓕ, d, e] L2 ≡ K2.
-#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
+#RR #RS #RP #Hgcp #Hgcr #G #L1 #K1 #d #e #H elim H -L1 -K1 -d -e
[ #d #e #He #X #H elim (lsubc_inv_atom1 … H) -H
>He /2 width=3 by ex2_intro/
| #L1 #I #V1 #X #H
| #K2 #V #W2 #A #HV2 #H1W2 #H2W2 #HK12 #H1 #H2 #H3 destruct
elim (lift_inv_flat1 … HV21) -HV21 #W3 #V3 #HW23 #HV3 #H destruct
elim (IHLK1 … HK12) #K #HL1K #HK2
- lapply (aacr_acr … Hacp Hacr A) -Hacp -Hacr #HA
+ lapply (acr_gcr … Hgcp Hgcr A) -Hgcp -Hgcr #HA
lapply (s0 … HA … HV2 … HLK1 HV3) -HV2
lapply (s0 … HA … H1W2 … HLK1 HW23) -H1W2
/4 width=11 by lsubc_beta, aaa_lift, drop_skip, ex2_intro/
include "basic_2/computation/lsubc_drop.ma".
-(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
(* Properties concerning generic local environment slicing ******************)
(* Basic_1: was: csubc_drop1_conf_rev *)
lemma drops_lsubc_trans: ∀RR,RS,RP.
- acp RR RS RP → acr RR RS RP RP →
+ gcp RR RS RP → gcr RR RS RP RP →
∀G,L1,K1,des. ⇩*[Ⓕ, des] L1 ≡ K1 → ∀K2. G ⊢ K1 ⫃[RP] K2 →
∃∃L2. G ⊢ L1 ⫃[RP] L2 & ⇩*[Ⓕ, des] L2 ≡ K2.
-#RR #RS #RP #Hacp #Hacr #G #L1 #K1 #des #H elim H -L1 -K1 -des
+#RR #RS #RP #Hgcp #Hgcr #G #L1 #K1 #des #H elim H -L1 -K1 -des
[ /2 width=3 by drops_nil, ex2_intro/
| #L1 #L #K1 #des #d #e #_ #HLK1 #IHL #K2 #HK12
- elim (drop_lsubc_trans … Hacp Hacr … HLK1 … HK12) -Hacp -Hacr -K1 #K #HLK #HK2
+ elim (drop_lsubc_trans … Hgcp Hgcr … HLK1 … HK12) -Hgcp -Hgcr -K1 #K #HLK #HK2
elim (IHL … HLK) -IHL -HLK /3 width=5 by drops_cons, ex2_intro/
]
qed-.
(**************************************************************************)
include "basic_2/static/lsuba.ma".
-include "basic_2/computation/acp_aaa.ma".
+include "basic_2/computation/gcp_aaa.ma".
-(* LOCAL ENVIRONMENT REFINEMENT FOR ABSTRACT CANDIDATES OF REDUCIBILITY *****)
+(* LOCAL ENVIRONMENT REFINEMENT FOR GENERIC REDUCIBILITY ********************)
(* properties concerning lenv refinement for atomic arity assignment ********)
-lemma lsuba_lsubc: ∀RR,RS,RP. acp RR RS RP → acr RR RS RP RP →
+lemma lsuba_lsubc: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP →
∀G,L1,L2. G ⊢ L1 ⫃⁝ L2 → G ⊢ L1 ⫃[RP] L2.
#RR #RS #RP #H1RP #H2RP #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsubc_pair/
-#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by aacr_aaa, lsubc_beta/
+#L1 #L2 #W #V #A #H elim (aaa_inv_cast … H) -H /3 width=4 by acr_aaa, lsubc_beta/
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/notation/relations/topiso_2.ma".
-include "basic_2/grammar/term_simple.ma".
-
-(* SAME TOP TERM CONSTRUCTOR ************************************************)
-
-inductive tstc: relation term ≝
- | tstc_atom: ∀I. tstc (⓪{I}) (⓪{I})
- | tstc_pair: ∀I,V1,V2,T1,T2. tstc (②{I}V1.T1) (②{I}V2.T2)
-.
-
-interpretation "same top constructor (term)" 'TopIso T1 T2 = (tstc T1 T2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact tstc_inv_atom1_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}.
-#T1 #T2 * -T1 -T2 //
-#J #V1 #V2 #T1 #T2 #I #H destruct
-qed-.
-
-(* Basic_1: was: iso_gen_sort iso_gen_lref *)
-lemma tstc_inv_atom1: ∀I,T2. ⓪{I} ≂ T2 → T2 = ⓪{I}.
-/2 width=3 by tstc_inv_atom1_aux/ qed-.
-
-fact tstc_inv_pair1_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 →
- ∃∃W2,U2. T2 = ②{I}W2. U2.
-#T1 #T2 * -T1 -T2
-[ #J #I #W1 #U1 #H destruct
-| #J #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
-]
-qed-.
-
-(* Basic_1: was: iso_gen_head *)
-lemma tstc_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≂ T2 →
- ∃∃W2,U2. T2 = ②{I}W2. U2.
-/2 width=5 by tstc_inv_pair1_aux/ qed-.
-
-fact tstc_inv_atom2_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}.
-#T1 #T2 * -T1 -T2 //
-#J #V1 #V2 #T1 #T2 #I #H destruct
-qed-.
-
-lemma tstc_inv_atom2: ∀I,T1. T1 ≂ ⓪{I} → T1 = ⓪{I}.
-/2 width=3 by tstc_inv_atom2_aux/ qed-.
-
-fact tstc_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 →
- ∃∃W1,U1. T1 = ②{I}W1.U1.
-#T1 #T2 * -T1 -T2
-[ #J #I #W2 #U2 #H destruct
-| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
-]
-qed-.
-
-lemma tstc_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 →
- ∃∃W1,U1. T1 = ②{I}W1.U1.
-/2 width=5 by tstc_inv_pair2_aux/ qed-.
-
-(* Basic properties *********************************************************)
-
-(* Basic_1: was: iso_refl *)
-lemma tstc_refl: reflexive … tstc.
-#T elim T -T //
-qed.
-
-lemma tstc_sym: symmetric … tstc.
-#T1 #T2 #H elim H -T1 -T2 //
-qed-.
-
-lemma tstc_dec: ∀T1,T2. Decidable (T1 ≂ T2).
-* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ]
-[ elim (eq_item2_dec I1 I2) #HI12
- [ destruct /2 width=1 by tstc_pair, or_introl/
- | @or_intror #H
- elim (tstc_inv_pair1 … H) -H #V #T #H destruct /2 width=1 by/
- ]
-| @or_intror #H
- lapply (tstc_inv_atom1 … H) -H #H destruct
-| @or_intror #H
- lapply (tstc_inv_atom2 … H) -H #H destruct
-| elim (eq_item0_dec I1 I2) #HI12
- [ destruct /2 width=1 by or_introl/
- | @or_intror #H
- lapply (tstc_inv_atom2 … H) -H #H destruct /2 width=1 by/
- ]
-]
-qed.
-
-lemma simple_tstc_repl_dx: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
-#T1 #T2 * -T1 -T2 //
-#I #V1 #V2 #T1 #T2 #H
-elim (simple_inv_pair … H) -H #J #H destruct //
-qed-.
-
-lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
-/3 width=3 by simple_tstc_repl_dx, tstc_sym/ 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/grammar/tstc.ma".
-
-(* SAME TOP TERM CONSTRUCTOR ************************************************)
-
-(* Main properties **********************************************************)
-
-(* Basic_1: was: iso_trans *)
-theorem tstc_trans: Transitive … tstc.
-#T1 #T * -T1 -T //
-#I #V1 #V #T1 #T #X #H
-elim (tstc_inv_pair1 … H) -H #V2 #T2 #H destruct //
-qed-.
-
-theorem tstc_canc_sn: ∀T,T1. T ≂ T1 → ∀T2. T ≂ T2 → T1 ≂ T2.
-/3 width=3 by tstc_trans, tstc_sym/ qed-.
-
-theorem tstc_canc_dx: ∀T1,T. T1 ≂ T → ∀T2. T2 ≂ T → T1 ≂ T2.
-/3 width=3 by tstc_trans, tstc_sym/ 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/grammar/term_vector.ma".
-include "basic_2/grammar/tstc.ma".
-
-(* SAME TOP TERM CONSTRUCTOR ************************************************)
-
-(* Advanced inversion lemmas ************************************************)
-
-(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
-lemma tstc_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 →
- 𝐒⦃T1⦄ → ⊥.
-#a #I #Vs #V2 #T1 #T2 #H
-elim (tstc_inv_pair2 … H) -H #V0 #T0
-elim Vs -Vs normalize
-[ #H destruct #H /2 width=5 by simple_inv_bind/
-| #V #Vs #_ #H destruct
-]
-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/notation/relations/topiso_2.ma".
+include "basic_2/grammar/term_simple.ma".
+
+(* SAME TOP TERM STRUCTURE **************************************************)
+
+inductive tsts: relation term ≝
+ | tsts_atom: ∀I. tsts (⓪{I}) (⓪{I})
+ | tsts_pair: ∀I,V1,V2,T1,T2. tsts (②{I}V1.T1) (②{I}V2.T2)
+.
+
+interpretation "same top structure (term)" 'TopIso T1 T2 = (tsts T1 T2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact tsts_inv_atom1_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T1 = ⓪{I} → T2 = ⓪{I}.
+#T1 #T2 * -T1 -T2 //
+#J #V1 #V2 #T1 #T2 #I #H destruct
+qed-.
+
+(* Basic_1: was: iso_gen_sort iso_gen_lref *)
+lemma tsts_inv_atom1: ∀I,T2. ⓪{I} ≂ T2 → T2 = ⓪{I}.
+/2 width=3 by tsts_inv_atom1_aux/ qed-.
+
+fact tsts_inv_pair1_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W1,U1. T1 = ②{I}W1.U1 →
+ ∃∃W2,U2. T2 = ②{I}W2. U2.
+#T1 #T2 * -T1 -T2
+[ #J #I #W1 #U1 #H destruct
+| #J #V1 #V2 #T1 #T2 #I #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
+]
+qed-.
+
+(* Basic_1: was: iso_gen_head *)
+lemma tsts_inv_pair1: ∀I,W1,U1,T2. ②{I}W1.U1 ≂ T2 →
+ ∃∃W2,U2. T2 = ②{I}W2. U2.
+/2 width=5 by tsts_inv_pair1_aux/ qed-.
+
+fact tsts_inv_atom2_aux: ∀T1,T2. T1 ≂ T2 → ∀I. T2 = ⓪{I} → T1 = ⓪{I}.
+#T1 #T2 * -T1 -T2 //
+#J #V1 #V2 #T1 #T2 #I #H destruct
+qed-.
+
+lemma tsts_inv_atom2: ∀I,T1. T1 ≂ ⓪{I} → T1 = ⓪{I}.
+/2 width=3 by tsts_inv_atom2_aux/ qed-.
+
+fact tsts_inv_pair2_aux: ∀T1,T2. T1 ≂ T2 → ∀I,W2,U2. T2 = ②{I}W2.U2 →
+ ∃∃W1,U1. T1 = ②{I}W1.U1.
+#T1 #T2 * -T1 -T2
+[ #J #I #W2 #U2 #H destruct
+| #J #V1 #V2 #T1 #T2 #I #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
+]
+qed-.
+
+lemma tsts_inv_pair2: ∀I,T1,W2,U2. T1 ≂ ②{I}W2.U2 →
+ ∃∃W1,U1. T1 = ②{I}W1.U1.
+/2 width=5 by tsts_inv_pair2_aux/ qed-.
+
+(* Basic properties *********************************************************)
+
+(* Basic_1: was: iso_refl *)
+lemma tsts_refl: reflexive … tsts.
+#T elim T -T //
+qed.
+
+lemma tsts_sym: symmetric … tsts.
+#T1 #T2 #H elim H -T1 -T2 //
+qed-.
+
+lemma tsts_dec: ∀T1,T2. Decidable (T1 ≂ T2).
+* #I1 [2: #V1 #T1 ] * #I2 [2,4: #V2 #T2 ]
+[ elim (eq_item2_dec I1 I2) #HI12
+ [ destruct /2 width=1 by tsts_pair, or_introl/
+ | @or_intror #H
+ elim (tsts_inv_pair1 … H) -H #V #T #H destruct /2 width=1 by/
+ ]
+| @or_intror #H
+ lapply (tsts_inv_atom1 … H) -H #H destruct
+| @or_intror #H
+ lapply (tsts_inv_atom2 … H) -H #H destruct
+| elim (eq_item0_dec I1 I2) #HI12
+ [ destruct /2 width=1 by or_introl/
+ | @or_intror #H
+ lapply (tsts_inv_atom2 … H) -H #H destruct /2 width=1 by/
+ ]
+]
+qed.
+
+lemma simple_tsts_repl_dx: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T1⦄ → 𝐒⦃T2⦄.
+#T1 #T2 * -T1 -T2 //
+#I #V1 #V2 #T1 #T2 #H
+elim (simple_inv_pair … H) -H #J #H destruct //
+qed-.
+
+lemma simple_tsts_repl_sn: ∀T1,T2. T1 ≂ T2 → 𝐒⦃T2⦄ → 𝐒⦃T1⦄.
+/3 width=3 by simple_tsts_repl_dx, tsts_sym/ 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/grammar/tsts.ma".
+
+(* SAME TOP TERM STRUCTURE **************************************************)
+
+(* Main properties **********************************************************)
+
+(* Basic_1: was: iso_trans *)
+theorem tsts_trans: Transitive … tsts.
+#T1 #T * -T1 -T //
+#I #V1 #V #T1 #T #X #H
+elim (tsts_inv_pair1 … H) -H #V2 #T2 #H destruct //
+qed-.
+
+theorem tsts_canc_sn: ∀T,T1. T ≂ T1 → ∀T2. T ≂ T2 → T1 ≂ T2.
+/3 width=3 by tsts_trans, tsts_sym/ qed-.
+
+theorem tsts_canc_dx: ∀T1,T. T1 ≂ T → ∀T2. T2 ≂ T → T1 ≂ T2.
+/3 width=3 by tsts_trans, tsts_sym/ 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/grammar/term_vector.ma".
+include "basic_2/grammar/tsts.ma".
+
+(* SAME TOP TERM STRUCTURE **************************************************)
+
+(* Advanced inversion lemmas ************************************************)
+
+(* Basic_1: was only: iso_flats_lref_bind_false iso_flats_flat_bind_false *)
+lemma tsts_inv_bind_applv_simple: ∀a,I,Vs,V2,T1,T2. ⒶVs.T1 ≂ ⓑ{a,I} V2. T2 →
+ 𝐒⦃T1⦄ → ⊥.
+#a #I #Vs #V2 #T1 #T2 #H
+elim (tsts_inv_pair2 … H) -H #V0 #T0
+elim Vs -Vs normalize
+[ #H destruct #H /2 width=5 by simple_inv_bind/
+| #V #Vs #_ #H destruct
+]
+qed-.
include "basic_2/notation/relations/rdropstar_3.ma".
include "basic_2/notation/relations/rdropstar_4.ma".
include "basic_2/substitution/drop.ma".
-include "basic_2/multiple/gr2_minus.ma".
+include "basic_2/multiple/mr2_minus.ma".
include "basic_2/multiple/lifts.ma".
(* ITERATED LOCAL ENVIRONMENT SLICING ***************************************)
+++ /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/notation/relations/rat_3.ma".
-include "basic_2/grammar/term_vector.ma".
-
-(* GENERIC RELOCATION WITH PAIRS ********************************************)
-
-inductive at: list2 nat nat → relation nat ≝
-| at_nil: ∀i. at (⟠) i i
-| at_lt : ∀des,d,e,i1,i2. i1 < d →
- at des i1 i2 → at ({d, e} @ des) i1 i2
-| at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
- at des (i1 + e) i2 → at ({d, e} @ des) i1 i2
-.
-
-interpretation "application (generic relocation with pairs)"
- 'RAt i1 des i2 = (at des i1 i2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = i2.
-#des #i1 #i2 * -des -i1 -i2
-[ //
-| #des #d #e #i1 #i2 #_ #_ #H destruct
-| #des #d #e #i1 #i2 #_ #_ #H destruct
-]
-qed-.
-
-lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2.
-/2 width=3 by at_inv_nil_aux/ qed-.
-
-fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →
- ∀d,e,des0. des = {d, e} @ des0 →
- i1 < d ∧ @⦃i1, des0⦄ ≡ i2 ∨
- d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2.
-#des #i1 #i2 * -des -i1 -i2
-[ #i #d #e #des #H destruct
-| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/
-| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_intror, conj/
-]
-qed-.
-
-lemma at_inv_cons: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
- i1 < d ∧ @⦃i1, des⦄ ≡ i2 ∨
- d ≤ i1 ∧ @⦃i1 + e, des⦄ ≡ i2.
-/2 width=3 by at_inv_cons_aux/ qed-.
-
-lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
- i1 < d → @⦃i1, des⦄ ≡ i2.
-#des #d #e #i1 #e2 #H
-elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d
-lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
-elim (lt_refl_false … Hd)
-qed-.
-
-lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
- d ≤ i1 → @⦃i1 + e, des⦄ ≡ i2.
-#des #d #e #i1 #e2 #H
-elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1
-lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
-elim (lt_refl_false … Hd)
-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/multiple/gr2.ma".
-
-(* GENERIC RELOCATION WITH PAIRS ********************************************)
-
-(* Main properties **********************************************************)
-
-theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ i2 → i1 = i2.
-#des #i #i1 #H elim H -des -i -i1
-[ #i #x #H <(at_inv_nil … H) -x //
-| #des #d #e #i #i1 #Hid #_ #IHi1 #x #H
- lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1 by/
-| #des #d #e #i #i1 #Hdi #_ #IHi1 #x #H
- lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1 by/
-]
-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/notation/relations/rminus_3.ma".
-include "basic_2/multiple/gr2.ma".
-
-(* GENERIC RELOCATION WITH PAIRS ********************************************)
-
-inductive minuss: nat → relation (list2 nat nat) ≝
-| minuss_nil: ∀i. minuss i (⟠) (⟠)
-| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
- minuss i ({d, e} @ des1) ({d - i, e} @ des2)
-| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
- minuss i ({d, e} @ des1) des2
-.
-
-interpretation "minus (generic relocation with pairs)"
- 'RMinus des1 i des2 = (minuss i des1 des2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠.
-#des1 #des2 #i * -des1 -des2 -i
-[ //
-| #des1 #des2 #d #e #i #_ #_ #H destruct
-| #des1 #des2 #d #e #i #_ #_ #H destruct
-]
-qed-.
-
-lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠.
-/2 width=4 by minuss_inv_nil1_aux/ qed-.
-
-fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
- ∀d,e,des. des1 = {d, e} @ des →
- d ≤ i ∧ des ▭ e + i ≡ des2 ∨
- ∃∃des0. i < d & des ▭ i ≡ des0 &
- des2 = {d - i, e} @ des0.
-#des1 #des2 #i * -des1 -des2 -i
-[ #i #d #e #des #H destruct
-| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3 by ex3_intro, or_intror/
-| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/
-]
-qed-.
-
-lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
- d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨
- ∃∃des. i < d & des1 ▭ i ≡ des &
- des2 = {d - i, e} @ des.
-/2 width=3 by minuss_inv_cons1_aux/ qed-.
-
-lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
- d ≤ i → des1 ▭ e + i ≡ des2.
-#des1 #des2 #d #e #i #H
-elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi
-lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
-elim (lt_refl_false … Hi)
-qed-.
-
-lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
- i < d →
- ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des.
-#des1 #des2 #d #e #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
-#Hdi #_ #Hid lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi
-#Hi elim (lt_refl_false … Hi)
-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/multiple/gr2.ma".
-
-(* GENERIC RELOCATION WITH PAIRS ********************************************)
-
-let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
-[ nil2 ⇒ ⟠
-| cons2 d e des ⇒ {d + i, e} @ pluss des i
-].
-
-interpretation "plus (generic relocation with pairs)"
- 'plus x y = (pluss x y).
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma pluss_inv_nil2: ∀i,des. des + i = ⟠ → des = ⟠.
-#i * // normalize
-#d #e #des #H destruct
-qed.
-
-lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} @ des2 →
- ∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1.
-#i #d #e #des2 * normalize
-[ #H destruct
-| #d1 #e1 #des1 #H destruct /2 width=3/
-]
-qed-.
include "basic_2/notation/relations/rliftstar_3.ma".
include "basic_2/substitution/lift.ma".
-include "basic_2/multiple/gr2_plus.ma".
+include "basic_2/multiple/mr2_plus.ma".
(* GENERIC TERM RELOCATION **************************************************)
(**************************************************************************)
include "basic_2/substitution/lift_lift.ma".
-include "basic_2/multiple/gr2_minus.ma".
+include "basic_2/multiple/mr2_minus.ma".
include "basic_2/multiple/lifts.ma".
(* GENERIC TERM RELOCATION **************************************************)
--- /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/notation/relations/rat_3.ma".
+include "basic_2/grammar/term_vector.ma".
+
+(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
+
+inductive at: list2 nat nat → relation nat ≝
+| at_nil: ∀i. at (⟠) i i
+| at_lt : ∀des,d,e,i1,i2. i1 < d →
+ at des i1 i2 → at ({d, e} @ des) i1 i2
+| at_ge : ∀des,d,e,i1,i2. d ≤ i1 →
+ at des (i1 + e) i2 → at ({d, e} @ des) i1 i2
+.
+
+interpretation "application (multiple relocation with pairs)"
+ 'RAt i1 des i2 = (at des i1 i2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact at_inv_nil_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 → des = ⟠ → i1 = i2.
+#des #i1 #i2 * -des -i1 -i2
+[ //
+| #des #d #e #i1 #i2 #_ #_ #H destruct
+| #des #d #e #i1 #i2 #_ #_ #H destruct
+]
+qed-.
+
+lemma at_inv_nil: ∀i1,i2. @⦃i1, ⟠⦄ ≡ i2 → i1 = i2.
+/2 width=3 by at_inv_nil_aux/ qed-.
+
+fact at_inv_cons_aux: ∀des,i1,i2. @⦃i1, des⦄ ≡ i2 →
+ ∀d,e,des0. des = {d, e} @ des0 →
+ i1 < d ∧ @⦃i1, des0⦄ ≡ i2 ∨
+ d ≤ i1 ∧ @⦃i1 + e, des0⦄ ≡ i2.
+#des #i1 #i2 * -des -i1 -i2
+[ #i #d #e #des #H destruct
+| #des1 #d1 #e1 #i1 #i2 #Hid1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/
+| #des1 #d1 #e1 #i1 #i2 #Hdi1 #Hi12 #d2 #e2 #des2 #H destruct /3 width=1 by or_intror, conj/
+]
+qed-.
+
+lemma at_inv_cons: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
+ i1 < d ∧ @⦃i1, des⦄ ≡ i2 ∨
+ d ≤ i1 ∧ @⦃i1 + e, des⦄ ≡ i2.
+/2 width=3 by at_inv_cons_aux/ qed-.
+
+lemma at_inv_cons_lt: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
+ i1 < d → @⦃i1, des⦄ ≡ i2.
+#des #d #e #i1 #e2 #H
+elim (at_inv_cons … H) -H * // #Hdi1 #_ #Hi1d
+lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
+elim (lt_refl_false … Hd)
+qed-.
+
+lemma at_inv_cons_ge: ∀des,d,e,i1,i2. @⦃i1, {d, e} @ des⦄ ≡ i2 →
+ d ≤ i1 → @⦃i1 + e, des⦄ ≡ i2.
+#des #d #e #i1 #e2 #H
+elim (at_inv_cons … H) -H * // #Hi1d #_ #Hdi1
+lapply (le_to_lt_to_lt … Hdi1 Hi1d) -Hdi1 -Hi1d #Hd
+elim (lt_refl_false … Hd)
+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/notation/relations/rminus_3.ma".
+include "basic_2/multiple/mr2.ma".
+
+(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
+
+inductive minuss: nat → relation (list2 nat nat) ≝
+| minuss_nil: ∀i. minuss i (⟠) (⟠)
+| minuss_lt : ∀des1,des2,d,e,i. i < d → minuss i des1 des2 →
+ minuss i ({d, e} @ des1) ({d - i, e} @ des2)
+| minuss_ge : ∀des1,des2,d,e,i. d ≤ i → minuss (e + i) des1 des2 →
+ minuss i ({d, e} @ des1) des2
+.
+
+interpretation "minus (multiple relocation with pairs)"
+ 'RMinus des1 i des2 = (minuss i des1 des2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact minuss_inv_nil1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 → des1 = ⟠ → des2 = ⟠.
+#des1 #des2 #i * -des1 -des2 -i
+[ //
+| #des1 #des2 #d #e #i #_ #_ #H destruct
+| #des1 #des2 #d #e #i #_ #_ #H destruct
+]
+qed-.
+
+lemma minuss_inv_nil1: ∀des2,i. ⟠ ▭ i ≡ des2 → des2 = ⟠.
+/2 width=4 by minuss_inv_nil1_aux/ qed-.
+
+fact minuss_inv_cons1_aux: ∀des1,des2,i. des1 ▭ i ≡ des2 →
+ ∀d,e,des. des1 = {d, e} @ des →
+ d ≤ i ∧ des ▭ e + i ≡ des2 ∨
+ ∃∃des0. i < d & des ▭ i ≡ des0 &
+ des2 = {d - i, e} @ des0.
+#des1 #des2 #i * -des1 -des2 -i
+[ #i #d #e #des #H destruct
+| #des1 #des #d1 #e1 #i1 #Hid1 #Hdes #d2 #e2 #des2 #H destruct /3 width=3 by ex3_intro, or_intror/
+| #des1 #des #d1 #e1 #i1 #Hdi1 #Hdes #d2 #e2 #des2 #H destruct /3 width=1 by or_introl, conj/
+]
+qed-.
+
+lemma minuss_inv_cons1: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
+ d ≤ i ∧ des1 ▭ e + i ≡ des2 ∨
+ ∃∃des. i < d & des1 ▭ i ≡ des &
+ des2 = {d - i, e} @ des.
+/2 width=3 by minuss_inv_cons1_aux/ qed-.
+
+lemma minuss_inv_cons1_ge: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
+ d ≤ i → des1 ▭ e + i ≡ des2.
+#des1 #des2 #d #e #i #H
+elim (minuss_inv_cons1 … H) -H * // #des #Hid #_ #_ #Hdi
+lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi #Hi
+elim (lt_refl_false … Hi)
+qed-.
+
+lemma minuss_inv_cons1_lt: ∀des1,des2,d,e,i. {d, e} @ des1 ▭ i ≡ des2 →
+ i < d →
+ ∃∃des. des1 ▭ i ≡ des & des2 = {d - i, e} @ des.
+#des1 #des2 #d #e #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/
+#Hdi #_ #Hid lapply (lt_to_le_to_lt … Hid Hdi) -Hid -Hdi
+#Hi elim (lt_refl_false … Hi)
+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/multiple/mr2.ma".
+
+(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
+
+(* Main properties **********************************************************)
+
+theorem at_mono: ∀des,i,i1. @⦃i, des⦄ ≡ i1 → ∀i2. @⦃i, des⦄ ≡ i2 → i1 = i2.
+#des #i #i1 #H elim H -des -i -i1
+[ #i #x #H <(at_inv_nil … H) -x //
+| #des #d #e #i #i1 #Hid #_ #IHi1 #x #H
+ lapply (at_inv_cons_lt … H Hid) -H -Hid /2 width=1 by/
+| #des #d #e #i #i1 #Hdi #_ #IHi1 #x #H
+ lapply (at_inv_cons_ge … H Hdi) -H -Hdi /2 width=1 by/
+]
+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/multiple/mr2.ma".
+
+(* MULTIPLE RELOCATION WITH PAIRS *******************************************)
+
+let rec pluss (des:list2 nat nat) (i:nat) on des ≝ match des with
+[ nil2 ⇒ ⟠
+| cons2 d e des ⇒ {d + i, e} @ pluss des i
+].
+
+interpretation "plus (multiple relocation with pairs)"
+ 'plus x y = (pluss x y).
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma pluss_inv_nil2: ∀i,des. des + i = ⟠ → des = ⟠.
+#i * // normalize
+#d #e #des #H destruct
+qed.
+
+lemma pluss_inv_cons2: ∀i,d,e,des2,des. des + i = {d, e} @ des2 →
+ ∃∃des1. des1 + i = des2 & des = {d - i, e} @ des1.
+#i #d #e #des2 * normalize
+[ #H destruct
+| #d1 #e1 #des1 #H destruct /2 width=3/
+]
+qed-.
pp. 53-78].
</body>
<table name="basic_2_sum"/>
+
+ <subsection>Stage "B"</subsection>
<news date="In progress.">
Context-sensitive subject equivalence
for native type assignment.
</news>
+
+ <subsection>Stage "A": "Weakening the Applicability Condition"</subsection>
<news date="2014 June 18.">
Preservation of stratified native validity
for context-sensitive computation on terms.
[ { "strongly normalizing extended computation" * } {
[ "lcosx ( ? ⊢ ~⬊*[?,?,?] ? )" "lcosx_cpx" * ]
[ "lsx ( ? ⊢ ⬊*[?,?,?,?] ? )" "lsx_alt ( ? ⊢ ⬊⬊*[?,?,?,?] ? )" "lsx_drop" + "lsx_lpx" + "lsx_lpxs" + "llsx_csx" * ]
- [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tstc_vector" + "csx_aaa" * ]
+ [ "csx_vector ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_tsts_vector" + "csx_aaa" * ]
[ "csx ( ⦃?,?⦄ ⊢ ⬊*[?,?] ? )" "csx_alt ( ⦃?,?⦄ ⊢ ⬊⬊*[?,?] ? )" "csx_lift" + "csx_lleq" + "csx_lpx" + "csx_lpxs" + "csx_fpbs" * ]
}
]
]
[ { "context-sensitive extended computation" * } {
[ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ]
- [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tstc" + "cpxs_tstc_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?,?] ? )" "cpxs_tsts" + "cpxs_tsts_vector" + "cpxs_leq" + "cpxs_lift" + "cpxs_lleq" + "cpxs_aaa" + "cpxs_cpxs" * ]
}
]
[ { "context-sensitive computation" * } {
[ "cprs ( ⦃?,?⦄ ⊢ ? ➡* ?)" "cprs_lift" + "cprs_cprs" * ]
}
]
- [ { "local env. ref. for abstract candidates of reducibility" * } {
+ [ { "local env. ref. for generic reducibility" * } {
[ "lsubc ( ? ⊢ ? ⫃[?] ? )" "lsubc_drop" + "lsubc_drops" + "lsubc_lsuba" * ]
}
]
- [ { "support for abstract computation properties" * } {
- [ "acp" "acp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "acp_aaa" * ]
+ [ { "support for generic computation properties" * } {
+ [ "gcp" "gcp_cr ( ⦃?,?,?⦄ ϵ[?] 〚?〛 )" "gcp_aaa" * ]
}
]
}
[ "lifts ( ⇧*[?] ? ≡ ? )" "lifts_lift" + "lifts_lifts" * ]
}
]
- [ { "support for generic relocation" * } {
- [ "gr2 ( @⦃?,?⦄ ≡ ? )" "gr2_plus ( ? + ? )" "gr2_minus ( ? ▭ ? ≡ ? )" "gr2_gr2" * ]
+ [ { "support for multiple relocation" * } {
+ [ "mr2 ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" "mr2_mr2" * ]
}
]
}
[ "leq ( ? ⩬[?,?] ? )" "leq_leq" * ]
}
]
- [ { "same top term constructor" * } {
- [ "tstc ( ? ≂ ? )" "tstc_tstc" + "tstc_vector" * ]
+ [ { "same top term structure" * } {
+ [ "tsts ( ? ≂ ? )" "tsts_tsts" + "tsts_vector" * ]
}
]
[ { "closures" * } {
projects / helm.git / commitdiff