some work on supclosure and extended reduction ...
lemma cprs_beta_dx: ∀a,L,V1,V2,W,T1,T2.
L ⊢ V1 ➡ V2 → L.ⓛW ⊢ T1 ➡* T2 →
L ⊢ ⓐV1.ⓛ{a}W.T1 ➡* ⓓ{a}V2.T2.
-#a #L #V1 #V2 #W #T1 #T2 #HV12 #H elim H -T2 /3 width=1/
-#T #T2 #_ #HT2 #IHT1
-@(cprs_strap1 … IHT1) -V1 -T1 /3 width=2/
+#a #L #V1 #V2 #W #T1 #T2 #HV12 * -T2 /3 width=1/
+/4 width=6 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_beta/ (**) (* auto too slow without trace *)
qed.
-lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,T1,T2.
+lemma cprs_theta_dx: ∀a,L,V1,V,V2,W1,W2,T1,T2.
L ⊢ V1 ➡ V → ⇧[0, 1] V ≡ V2 → L.ⓓW1 ⊢ T1 ➡* T2 →
- ∀W2. L ⊢ W1 ➡ W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
-#a #L #V1 #V #V2 #W1 #T1 #T2 #HV1 #HV2 #H elim H -T2 [ /3 width=3/ ]
-#T #T2 #_ #HT2 #IHT1 #W2 #HW12
-lapply (IHT1 W1 ?) -IHT1 // #HT1
-@(cprs_strap1 … HT1) -HT1 -V -V1 /3 width=1/
+ L ⊢ W1 ➡ W2 → L ⊢ ⓐV1.ⓓ{a}W1.T1 ➡* ⓓ{a}W2.ⓐV2.T2.
+#a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
+/4 width=9 by cprs_strap1, cprs_bind_dx, cprs_flat_dx, cpr_theta/ (**) (* auto too slow without trace *)
qed.
(* Basic inversion lemmas ***************************************************)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "basic_2/reduction/cpx.ma".
+include "basic_2/computation/cprs.ma".
+
+(* EXTENDED CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS *****************)
+
+definition cpxs: ∀h. sd h → lenv → relation term ≝
+ λh,g. LTC … (cpx h g).
+
+interpretation "extended context-sensitive parallel computation (term)"
+ 'PRedStar h g L T1 T2 = (cpxs h g L T1 T2).
+
+(* Basic eliminators ********************************************************)
+
+lemma cpxs_ind: ∀h,g,L,T1. ∀R:predicate term. R T1 →
+ (∀T,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T → ⦃h, L⦄ ⊢ T ➡[g] T2 → R T → R T2) →
+ ∀T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → R T2.
+#h #g #L #T1 #R #HT1 #IHT1 #T2 #HT12
+@(TC_star_ind … HT1 IHT1 … HT12) //
+qed-.
+
+lemma cpxs_ind_dx: ∀h,g,L,T2. ∀R:predicate term. R T2 →
+ (∀T1,T. ⦃h, L⦄ ⊢ T1 ➡[g] T → ⦃h, L⦄ ⊢ T ➡*[g] T2 → R T → R T1) →
+ ∀T1. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → R T1.
+#h #g #L #T2 #R #HT2 #IHT2 #T1 #HT12
+@(TC_star_ind_dx … HT2 IHT2 … HT12) //
+qed-.
+
+(* Basic properties *********************************************************)
+
+lemma cpxs_refl: ∀h,g,L,T. ⦃h, L⦄ ⊢ T ➡*[g] T.
+/2 width=1/ qed.
+
+lemma cpx_cpxs: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+/2 width=1/ qed.
+
+lemma cpxs_strap1: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 ➡*[g] T →
+ ∀T2. ⦃h, L⦄ ⊢ T ➡[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+normalize /2 width=3/ qed.
+
+lemma cpxs_strap2: ∀h,g,L,T1,T. ⦃h, L⦄ ⊢ T1 ➡[g] T →
+ ∀T2. ⦃h, L⦄ ⊢ T ➡*[g] T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+normalize /2 width=3/ qed.
+
+lemma cprs_cpxs: ∀h,g,L,T1,T2. L ⊢ T1 ➡* T2 → ⦃h, L⦄ ⊢ T1 ➡*[g] T2.
+#h #g #L #T1 #T2 #H @(cprs_ind … H) -T2 // /3 width=3/
+qed.
+
+lemma cpxs_bind_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
+ ∀I,T1,T2. ⦃h, L. ⓑ{I}V1⦄ ⊢ T1 ➡*[g] T2 →
+ ∀a. ⦃h, L⦄ ⊢ ⓑ{a,I}V1.T1 ➡*[g] ⓑ{a,I}V2.T2.
+#h #g #L #V1 #V2 #HV12 #I #T1 #T2 #HT12 #a @(cpxs_ind_dx … HT12) -T1
+/3 width=1/ /3 width=3/
+qed.
+
+lemma cpxs_flat_dx: ∀h,g,L,V1,V2. ⦃h, L⦄ ⊢ V1 ➡[g] V2 →
+ ∀T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 →
+ ∀I. ⦃h, L⦄ ⊢ ⓕ{I} V1. T1 ➡*[g] ⓕ{I} V2. T2.
+#h #g #L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cpxs_ind … HT12) -T2 /3 width=1/ /3 width=5/
+qed.
+
+lemma cpxs_flat_sn: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡[g] T2 →
+ ∀V1,V2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 →
+ ∀I. ⦃h, L⦄ ⊢ ⓕ{I} V1. T1 ➡*[g] ⓕ{I} V2. T2.
+#h #g #L #T1 #T2 #HT12 #V1 #V2 #H @(cpxs_ind … H) -V2 /3 width=1/ /3 width=5/
+qed.
+
+lemma cpxs_zeta: ∀h,g,L,V,T1,T,T2. ⇧[0, 1] T2 ≡ T →
+ ⦃h, L.ⓓV⦄ ⊢ T1 ➡*[g] T → ⦃h, L⦄ ⊢ +ⓓV.T1 ➡*[g] T2.
+#h #g #L #V #T1 #T #T2 #HT2 #H @(TC_ind_dx … T1 H) -T1 /3 width=3/
+qed.
+
+lemma cpxs_tau: ∀h,g,L,T1,T2. ⦃h, L⦄ ⊢ T1 ➡*[g] T2 → ∀V. ⦃h, L⦄ ⊢ ⓝV.T1 ➡*[g] T2.
+#h #g #L #T1 #T2 #H elim H -T2 /2 width=3/ /3 width=1/
+qed.
+
+lemma cpxs_beta_dx: ∀h,g,a,L,V1,V2,W,T1,T2.
+ ⦃h, L⦄ ⊢ V1 ➡[g] V2 → ⦃h, L.ⓛW⦄ ⊢ T1 ➡*[g] T2 →
+ ⦃h, L⦄ ⊢ ⓐV1.ⓛ{a}W.T1 ➡*[g] ⓓ{a}V2.T2.
+#h #g #a #L #V1 #V2 #W #T1 #T2 #HV12 * -T2 /3 width=1/
+/4 width=6 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_beta/ (**) (* auto too slow without trace *)
+qed.
+
+lemma cpxs_theta_dx: ∀h,g,a,L,V1,V,V2,W1,W2,T1,T2.
+ ⦃h, L⦄ ⊢ V1 ➡[g] V → ⇧[0, 1] V ≡ V2 → ⦃h, L.ⓓW1⦄ ⊢ T1 ➡*[g] T2 →
+ ⦃h, L⦄ ⊢ W1 ➡[g] W2 → ⦃h, L⦄ ⊢ ⓐV1.ⓓ{a}W1.T1 ➡*[g] ⓓ{a}W2.ⓐV2.T2.
+#h #g #a #L #V1 #V #V2 #W1 #W2 #T1 #T2 #HV1 #HV2 * -T2 [ /3 width=3/ ]
+/4 width=9 by cpxs_strap1, cpxs_bind_dx, cpxs_flat_dx, cpx_theta/ (**) (* auto too slow without trace *)
+qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma cpxs_inv_sort1: ∀h,g,L,U2,k. ⦃h, L⦄ ⊢ ⋆k ➡*[g] U2 →
+ ∃∃n,l. deg h g k (n+l) & U2 = ⋆((next h)^n k).
+#h #g #L #U2 #k #H @(cpxs_ind … H) -U2
+[ elim (deg_total h g k) #l #Hkl
+ @(ex2_2_intro … 0 … Hkl) -Hkl //
+| #U #U2 #_ #HU2 * #n #l #Hknl #H destruct
+ elim (cpx_inv_sort1 … HU2) -HU2
+ [ #H destruct /2 width=4/
+ | * #l0 #Hkl0 #H destruct -l
+ @(ex2_2_intro … (n+1) l0) /2 width=1/ >iter_SO //
+ ]
+]
+qed-.
+
+lemma cpxs_inv_appl1: ∀h,g,L,V1,T1,U2. ⦃h, L⦄ ⊢ ⓐV1.T1 ➡*[g] U2 →
+ ∨∨ ∃∃V2,T2. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 &
+ U2 = ⓐV2. T2
+ | ∃∃a,V2,W,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V2 &
+ ⦃h, L⦄ ⊢ T1 ➡*[g] ⓛ{a}W.T & ⦃h, L⦄ ⊢ ⓓ{a}V2.T ➡*[g] U2
+ | ∃∃a,V0,V2,V,T. ⦃h, L⦄ ⊢ V1 ➡*[g] V0 & ⇧[0,1] V0 ≡ V2 &
+ ⦃h, L⦄ ⊢ T1 ➡*[g] ⓓ{a}V.T & ⦃h, L⦄ ⊢ ⓓ{a}V.ⓐV2.T ➡*[g] U2.
+#h #g #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 [ /3 width=5/ ]
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpx_inv_appl1 … HU2) -HU2 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+ | #a #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct
+ lapply (cpxs_strap1 … HV10 … HV02) -V0 /5 width=7/
+ | #a #V #V2 #W0 #W2 #T #T2 #HV0 #HV2 #HW02 #HT2 #H1 #H2 destruct
+ @or3_intro2 @(ex4_5_intro … HV2 HT10) /2 width=3/ /3 width=1/ (**) (* explicit constructor. /5 width=8/ is too slow because TC_transitive gets in the way *)
+ ]
+| /4 width=9/
+| /4 width=11/
+]
+qed-.
+
+lemma cpxs_inv_cast1: ∀h,g,L,W1,T1,U2. ⦃h, L⦄ ⊢ ⓝW1.T1 ➡*[g] U2 → ⦃h, L⦄ ⊢ T1 ➡*[g] U2 ∨
+ ∃∃W2,T2. ⦃h, L⦄ ⊢ W1 ➡*[g] W2 & ⦃h, L⦄ ⊢ T1 ➡*[g] T2 & U2 = ⓝW2.T2.
+#h #g #L #W1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5/
+#U2 #U #_ #HU2 * /3 width=3/ *
+#W #T #HW1 #HT1 #H destruct
+elim (cpx_inv_cast1 … HU2) -HU2 /3 width=3/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+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/reduction/cpx_lift.ma".
+include "basic_2/computation/cpxs.ma".
+
+(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************)
+
+(* Advanced properties ******************************************************)
+
+lemma cpxs_delta: ∀h,g,I,L,K,V,V2,i.
+ ⇩[0, i] L ≡ K. ⓑ{I}V → ⦃h, K⦄ ⊢ V ➡*[g] V2 →
+ ∀W2. ⇧[0, i + 1] V2 ≡ W2 → ⦃h, L⦄ ⊢ #i ➡*[g] W2.
+#h #g #I #L #K #V #V2 #i #HLK #H elim H -V2 [ /3 width=9/ ]
+#V1 #V2 #_ #HV12 #IHV1 #W2 #HVW2
+lapply (ldrop_fwd_ldrop2 … HLK) -HLK #HLK
+elim (lift_total V1 0 (i+1)) /4 width=11 by cpx_lift, cpxs_strap1/
+qed.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma cpxs_inv_lref1: ∀h,g,L,T2,i. ⦃h, L⦄ ⊢ #i ➡*[g] T2 →
+ T2 = #i ∨
+ ∃∃I,K,V1,T1. ⇩[0, i] L ≡ K.ⓑ{I}V1 & ⦃h, K⦄ ⊢ V1 ➡*[g] T1 &
+ ⇧[0, i + 1] T1 ≡ T2.
+#h #g #L #T2 #i #H @(cpxs_ind … H) -T2 /2 width=1/
+#T #T2 #_ #HT2 *
+[ #H destruct
+ elim (cpx_inv_lref1 … HT2) -HT2 /2 width=1/
+ * /4 width=7/
+| * #I #K #V1 #T1 #HLK #HVT1 #HT1
+ lapply (ldrop_fwd_ldrop2 … HLK) #H0LK
+ elim (cpx_inv_lift1 … HT2 … H0LK … HT1) -H0LK -T /4 width=7/
+]
+qed-.
+
+(* Relocation properties ****************************************************)
+
+(* Basic_1: was: pr3_lift *)
+lemma cpxs_lift: ∀h,g. l_liftable (cpxs h g).
+/3 width=9/ qed.
+
+(* Basic_1: was: pr3_gen_lift *)
+lemma cpxs_inv_lift1: ∀h,g. l_deliftable_sn (cpxs h g).
+/3 width=5 by l_deliftable_sn_LTC, cpx_inv_lift1/
+qed-.
+
+(* Properties on supclosure *************************************************)
+
+include "basic_2/substitution/fsups.ma".
+
+lemma fsupq_cpxs_trans: ∀h,g,L1,L2,T2,U2. ⦃h, L2⦄ ⊢ T2 ➡*[g] U2 →
+ ∀T1. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡*[g] U1 & ⦃L1, U1⦄ ⊃* ⦃L2, U2⦄.
+#h #g #L1 #L2 #T2 #U2 #H @(cpxs_ind_dx … H) -T2 [ (* /3 width=3/ *) |
+#T #T2 #HT2 #_ #IHTU2 #T1 #HT1
+elim (fsupq_cpx_trans … HT1 … HT2) -T #T #HT1 #HT2
+elim (IHTU2 … HT2) -T2 /3 width=3/
+
+
+(*
+ elim H -L1 -L2 -T1 -T2 [2,3,4,5: /3 width=5/ ]
+[ #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+ elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2
+ elim (lift_total T d e) #U #HTU
+ lapply (cpx_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
+| #I #L1 #V2 #U2 #HVU2
+ elim (lift_total U2 0 1) /4 width=9/
+]
+qed-.
+
+lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+/3 width=4 by fsup_cpx_trans, ssta_cpx/ qed-.
+*)
\ No newline at end of file
non associative with precedence 45
for @{ 'SupTermOpt $L1 $T1 $L2 $T2 }.
+notation "hvbox( ⦃ term 46 L1, break term 46 T1 ⦄ ⊃⊃⸮ break ⦃ term 46 L2 , break term 46 T2 ⦄ )"
+ non associative with precedence 45
+ for @{ 'SupTermOptAlt $L1 $T1 $L2 $T2 }.
+
notation "hvbox( L ⊢ break ⌘ ⦃ term 46 T ⦄ ≡ break term 46 k )"
non associative with precedence 45
for @{ 'ICM $L $T $k }.
/2 width=3 by cpx_inv_atom1_aux/ qed-.
lemma cpx_inv_sort1: ∀h,g,L,T2,k. ⦃h, L⦄ ⊢ ⋆k ➡[g] T2 → T2 = ⋆k ∨
- ∃∃k,l. deg h g k (l+1) & T2 = ⋆(next h k).
+ ∃∃l. deg h g k (l+1) & T2 = ⋆(next h k).
#h #g #L #T2 #k #H
elim (cpx_inv_atom1 … H) -H /2 width=1/ *
-[ #k0 #l #Hkl #H1 #H2 destruct /3 width=4/
+[ #k0 #l0 #Hkl0 #H1 #H2 destruct /3 width=4/
| #I #K #V #V2 #i #_ #_ #_ #H destruct
]
qed-.
(* Properties on supclosure *************************************************)
-lemma fsup_cpx_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
- ∀U2. ⦃h, L2⦄ ⊢ T2 ➡[g] U2 →
- ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
-#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [2,3,4,5: /3 width=5/ ]
-[ #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
+lemma fsupq_cpx_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ →
+ ∀U2. ⦃h, L2⦄ ⊢ T2 ➡[g] U2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+#h #g #L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 [1: /2 width=3/ |3,4,5: /3 width=3/ ]
+[ #I #L1 #V2 #U2 #HVU2
+ elim (lift_total U2 0 1) /4 width=9/
+| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #U2 #HTU2
elim (IHT12 … HTU2) -IHT12 -HTU2 #T #HT1 #HT2
elim (lift_total T d e) #U #HTU
lapply (cpx_lift … HT1 … HLK1 … HTU1 … HTU) -HT1 -HTU1 /3 width=11/
-| #I #L1 #V2 #U2 #HVU2
- elim (lift_total U2 0 1) /4 width=9/
]
qed-.
+lemma fsupq_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃⸮ ⦃L2, T2⦄ →
+ ∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+/3 width=4 by fsupq_cpx_trans, ssta_cpx/ qed-.
+
+lemma fsup_cpx_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
+ ∀U2. ⦃h, L2⦄ ⊢ T2 ➡[g] U2 →
+ ∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
+/3 width=3 by fsupq_cpx_trans, fsup_fsupq/ qed-.
+
lemma fsup_ssta_trans: ∀h,g,L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
∀U2,l. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l+1, U2⦄ →
∃∃U1. ⦃h, L1⦄ ⊢ T1 ➡[g] U1 & ⦃L1, U1⦄ ⊃⸮ ⦃L2, U2⦄.
-/3 width=4 by fsup_cpx_trans, ssta_cpx/ qed-.
+/3 width=4 by fsupq_ssta_trans, fsup_fsupq/ qed-.
(* SUPCLOSURE ***************************************************************)
inductive fsup: bi_relation lenv term ≝
-| fsup_lref_O : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
-| fsup_pair_sn: ∀I,L,V,T. fsup L (②{I}V.T) L V
-| fsup_bind_dx: ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
-| fsup_flat_dx: ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T
-| fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e.
- ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
- fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2
+| fsup_lref_O : ∀I,L,V. fsup (L.ⓑ{I}V) (#0) L V
+| fsup_pair_sn : ∀I,L,V,T. fsup L (②{I}V.T) L V
+| fsup_bind_dx : ∀a,I,L,V,T. fsup L (ⓑ{a,I}V.T) (L.ⓑ{I}V) T
+| fsup_flat_dx : ∀I,L,V,T. fsup L (ⓕ{I}V.T) L T
+| fsup_ldrop_lt: ∀L,K,T,U,d,e.
+ ⇩[d, e] L ≡ K → ⇧[d, e] T ≡ U → |K| < |L| → fsup L U K T
+| fsup_ldrop : ∀L1,K1,K2,T1,T2,U1,d,e.
+ ⇩[d, e] L1 ≡ K1 → ⇧[d, e] T1 ≡ U1 →
+ fsup K1 T1 K2 T2 → fsup L1 U1 K2 T2
.
interpretation
lemma fsup_fwd_fw: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ → ♯{L2, T2} < ♯{L1, T1}.
#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2 //
-#L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
-lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
-lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
-@(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/
+[ #L #K #T #U #d #e #HLK #HTU #HKL
+ lapply (ldrop_fwd_lw_lt … HLK HKL) -HKL -HLK #HKL
+ lapply (lift_fwd_tw … HTU) -d -e #H
+ normalize in ⊢ (?%%); /2 width=1/
+| #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12
+ lapply (ldrop_fwd_lw … HLK1) -HLK1 #HLK1
+ lapply (lift_fwd_tw … HTU1) -HTU1 #HTU1
+ @(lt_to_le_to_lt … IHT12) -IHT12 /2 width=1/
+]
qed-.
fact fsup_fwd_length_lref1_aux: ∀L1,L2,T1,T2. ⦃L1, T1⦄ ⊃ ⦃L2, T2⦄ →
∀i. T1 = #i → |L2| < |L1|.
#L1 #L2 #T1 #T2 #H elim H -L1 -L2 -T1 -T2
-[5: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
+[1,5: normalize //
+|3: #a
+|6: #L1 #K1 #K2 #T1 #T2 #U1 #d #e #HLK1 #HTU1 #_ #IHT12 #i #H destruct
lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1
elim (lift_inv_lref2 … HTU1) -HTU1 * #Hdei #H destruct
@(lt_to_le_to_lt … HLK1) /2 width=2/
-| normalize // |3: #a
] #I #L #V #T #j #H destruct
qed-.
]
qed-.
+lemma ldrop_fwd_lw_eq: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+ |L1| = |L2| → ♯{L2} = ♯{L1}.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e //
+[ #L1 #L2 #I #V #e #HL12 #_
+ lapply (ldrop_fwd_O1_length … HL12) -HL12 #HL21 >HL21 -HL21 normalize #H -I
+ lapply (discr_plus_xy_minus_xz … H) -e #H destruct
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #HL12 normalize in ⊢ (??%%→??%%); #H -I
+ >(lift_fwd_tw … HV21) -V2 /3 width=1 by eq_f2/ (**) (* auto is a bit slow without trace *)
+]
+qed-.
+
+lemma ldrop_fwd_lw_lt: ∀L1,L2,d,e. ⇩[d, e] L1 ≡ L2 →
+ |L2| < |L1| → ♯{L2} < ♯{L1}.
+#L1 #L2 #d #e #H elim H -L1 -L2 -d -e //
+[ #L #I #V #H elim (lt_refl_false … H)
+| #L1 #L2 #I #V #e #HL12 #_ #_
+ lapply (ldrop_fwd_lw … HL12) -HL12 #HL12
+ @(le_to_lt_to_lt … HL12) -HL12 //
+| #L1 #L2 #I #V1 #V2 #d #e #_ #HV21 #IHL12 normalize in ⊢ (?%%→?%%); #H -I
+ >(lift_fwd_tw … HV21) -V2 /4 width=2 by lt_minus_to_plus, lt_plus_to_lt_l/ (**) (* auto too slow without trace *)
+]
+qed-.
+
(* Basic_1: removed theorems 50:
drop_ctail drop_skip_flat
cimp_flat_sx cimp_flat_dx cimp_bind cimp_getl_conf
<(associative_plus l 1 1) >H <plus_minus_m_m // /2 width=3 by transitive_le/
qed.
+lemma deg_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
+#h #g #k #l @(nat_ind_plus … l) -l //
+#l #IHl #l0 >iter_SO #H
+lapply (deg_pred … H) -H <(associative_plus l0 1 1) #H
+lapply (IHl … H) -IHl -H //
+qed.
+
lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
#h #k #l <plus_n_Sm <plus_n_Sm //
qed.
[ "dxprs ( ⦃?,?⦄ ⊢ ? •*➡*[?] ? )" "dxprs_lift" + "dxprs_lpss" + "dxprs_aaa" + "dxprs_dxprs" * ]
}
]
+ [ { "context-sensitive extended computation" * } {
+ [ "cpxs ( ⦃?,?⦄ ⊢ ? ➡*[?] ? )" "cpxs_lift" * ]
+ }
+ ]
[ { "weakly normalizing computation" * } {
[ "cpe ( ? ⊢ ➡* 𝐍⦃?⦄ )" "cpe_cpe" * ]
}
// qed.
theorem times_n_1 : ∀n:nat. n = n * 1.
-#n // qed.
+// qed.
theorem minus_S_S: ∀n,m:nat.S n - S m = n -m.
// qed.
lemma plus_plus_comm_23: ∀x,y,z. x + y + z = x + z + y.
// qed.
+lemma discr_plus_xy_minus_xz: ∀x,z,y. x + y = x - z → y = 0.
+#x elim x -x // #x #IHx * normalize
+[ #y #H @(IHx 0) <minus_n_O /2 width=1/
+| #z #y >plus_n_Sm #H lapply (IHx … H) -x -z #H destruct
+]
+qed-.
+
(* Negated equalities *******************************************************)
theorem not_eq_S: ∀n,m:nat. n ≠ m → S n ≠ S m.
projects / helm.git / commitdiff