pr2/props pr2_ctail
pr2/subst1 pr2_gen_cabbr
-pr3/fwd pr3_gen_sort
pr3/fwd pr3_gen_abst
-pr3/fwd pr3_gen_cast
-pr3/fwd pr3_gen_lift
pr3/fwd pr3_gen_lref
pr3/fwd pr3_gen_void
pr3/fwd pr3_gen_abbr
pr3/fwd pr3_gen_appl
pr3/fwd pr3_gen_bind
pr3/iso pr3_iso_appls_abbr
-pr3/iso pr3_iso_appls_cast
pr3/iso pr3_iso_appl_bind
pr3/iso pr3_iso_appls_appl_bind
pr3/iso pr3_iso_appls_bind
pr3/props pr3_head_12
pr3/props pr3_flat
pr3/props pr3_pr3_pr3_t
-pr3/props pr3_lift
pr3/props pr3_eta
pr3/subst1 pr3_subst1
pr3/subst1 pr3_gen_cabbr
@(cprs_strap1 … IHT2) -IHT2 /2 width=1/
qed.
+(* Basic inversion lemmas ***************************************************)
+
+(* Basic_1: was: pr3_gen_sort *)
+lemma cprs_inv_sort1: ∀L,U2,k. L ⊢ ⋆k ➡* U2 → U2 = ⋆k.
+#L #U2 #k #H @(cprs_ind … H) -U2 //
+#U2 #U #_ #HU2 #IHU2 destruct
+>(cpr_inv_sort1 … HU2) -HU2 //
+qed-.
+
+(* Basic_1: was: pr3_gen_cast *)
+lemma cprs_inv_cast1: ∀L,W1,T1,U2. L ⊢ ⓣW1.T1 ➡* U2 → L ⊢ T1 ➡* U2 ∨
+ ∃∃W2,T2. L ⊢ W1 ➡* W2 & L ⊢ T1 ➡* T2 & U2 = ⓣW2.T2.
+#L #W1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U2 #U #_ #HU2 * /3 width=3/ *
+#W #T #HW1 #HT1 #H destruct
+elim (cpr_inv_cast1 … HU2) -HU2 /3 width=3/ *
+#W2 #T2 #HW2 #HT2 #H destruct /4 width=5/
+qed-.
+
(* Basic_1: removed theorems 2: clear_pr3_trans pr3_cflat *)
(* *)
(**************************************************************************)
+include "Basic_2/reducibility/cpr_lift.ma".
include "Basic_2/reducibility/cpr_cpr.ma".
+include "Basic_2/reducibility/lcpr_cpr.ma".
include "Basic_2/computation/cprs_lcpr.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
lemma cprs_abbr_dx: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV1 ⊢ T1 ➡* T2 →
L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
#L #V1 #V2 #HV12 #T1 #T2 #HT12 @(cprs_ind_dx … HT12) -T1
-[ /3 width=1/
+[ /3 width=5/
| #T1 #T #HT1 #_ #IHT1
@(cprs_strap2 … IHT1) -IHT1 /2 width=1/
]
L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
/3 width=1/ qed.
-(* Basic_1: was only: pr3_pr2_pr3_t *)
-lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
- ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
-#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
-#T #T2 #_ #HT2 #IHT2 /3 width=5/
+lemma cpr_abbr2: ∀L,V1,V2. L ⊢ V1 ➡ V2 → ∀T1,T2. L. ⓓV2 ⊢ T1 ➡ T2 →
+ L ⊢ ⓓV1. T1 ➡* ⓓV2. T2.
+#L #V1 #V2 #HV12 #T1 #T2 #HT12
+lapply (lcpr_cpr_trans (L. ⓓV1) … HT12) /2 width=1/
qed.
-(* Main propertis ***********************************************************)
+(* Advanced inversion lemmas ************************************************)
-(* Basic_1: was: pr3_t *)
-theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
-/2 width=3/ qed.
+(* Basic_1: was pr3_gen_appl *)
+lemma cprs_inv_appl1: ∀L,V1,T1,U2. L ⊢ ⓐV1. T1 ➡* U2 →
+ ∨∨ ∃∃V2,T2. L ⊢ V1 ➡* V2 & L ⊢ T1 ➡* T2 &
+ U2 = ⓐV2. T2
+ | ∃∃V2,W,T. L ⊢ V1 ➡* V2 &
+ L ⊢ T1 ➡* ⓛW. T & L ⊢ ⓓV2. T ➡* U2
+ | ∃∃V0,V2,V,T. L ⊢ V1 ➡* V0 & ⇧[0,1] V0 ≡ V2 &
+ L ⊢ T1 ➡* ⓓV. T & L ⊢ ⓓV. ⓐV2. T ➡* U2.
+#L #V1 #T1 #U2 #H @(cprs_ind … H) -U2 /3 width=5/
+#U #U2 #_ #HU2 * *
+[ #V0 #T0 #HV10 #HT10 #H destruct
+ elim (cpr_inv_appl1 … HU2) -HU2 *
+ [ #V2 #T2 #HV02 #HT02 #H destruct /4 width=5/
+ | #V2 #W2 #T #T2 #HV02 #HT2 #H1 #H2 destruct /4 width=7/
+ | #V #V2 #W0 #W2 #T #T2 #HV0 #HW02 #HT2 #HV2 #H1 #H2 destruct
+ @or3_intro2 @(ex4_4_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=8/
+| /4 width=10/
+]
+qed-.
+
+(* Main propertis ***********************************************************)
(* Basic_1: was: pr3_confluence *)
theorem cprs_conf: ∀L,T1,T. L ⊢ T ➡* T1 → ∀T2. L ⊢ T ➡* T2 →
∃∃T0. L ⊢ T1 ➡* T0 & L ⊢ T2 ➡* T0.
/3 width=3/ qed.
+(* Basic_1: was: pr3_t *)
+theorem cprs_trans: ∀L,T1,T. L ⊢ T1 ➡* T → ∀T2. L ⊢ T ➡* T2 → L ⊢ T1 ➡* T2.
+/2 width=3/ qed.
+
+lemma cprs_flat: ∀I,L,T1,T2. L ⊢ T1 ➡* T2 → ∀V1,V2. L ⊢ V1 ➡* V2 →
+ L ⊢ ⓕ{I} V1. T1 ➡* ⓕ{I} V2. T2.
+#I #L #T1 #T2 #HT12 #V1 #V2 #HV12 @(cprs_ind … HV12) -V2 /2 width=1/
+#V #V2 #_ #HV2 #IHV1
+@(cprs_trans … IHV1) -IHV1 /2 width=1/
+qed.
+
+(* Basic_1: was only: pr3_pr2_pr3_t *)
+lemma lcpr_cprs_trans: ∀L1,L2. L1 ⊢ ➡ L2 →
+ ∀T1,T2. L2 ⊢ T1 ➡* T2 → L1 ⊢ T1 ➡* T2.
+#L1 #L2 #HL12 #T1 #T2 #H @(cprs_ind … H) -T2 //
+#T #T2 #_ #HT2 #IHT2
+@(cprs_trans … IHT2) /2 width=3/
+qed.
(**************************************************************************)
include "Basic_2/grammar/tstc.ma".
+(*
include "Basic_2/reducibility/cpr_lift.ma".
include "Basic_2/reducibility/lcpr_cpr.ma".
+*)
include "Basic_2/computation/cprs_cprs.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* Forward lemmas involving same top term constructor ***********************)
+(*
+lemma cpr_fwd_beta: ∀L,V,W,T,U. L ⊢ ⓐV. ⓛW. T ➡ U →
+ ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⓓV. T ➡* U.
+#L #V #W #T #U #H
+elim (cpr_inv_appl1 … H) -H *
+[ #V0 #X #_ #_ #H destruct /2 width=1/
+| #V0 #W0 #T1 #T2 #HV0 #HT12 #H1 #H2 destruct
+ lapply (lcpr_cpr_trans (L. ⓓV) … HT12) -HT12 /2 width=1/ /3 width=1/
+| #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #_ #H destruct
+]
+qed-.
lemma cpr_fwd_theta: ∀L,V1,V,T,U. L ⊢ ⓐV1. ⓓV. T ➡ U →
∀V2. ⇧[0, 1] V1 ≡ V2 → ⓐV1. ⓓV. T ≃ U ∨
/4 width=1/
]
qed-.
+*)
+lemma cprs_fwd_tau: ∀L,W,T,U. L ⊢ ⓣW. T ➡* U →
+ ⓣW. T ≃ U ∨ L ⊢ T ➡* U.
+#L #W #T #U #H
+elim (cprs_inv_cast1 … H) -H /2 width=1/ *
+#W0 #T0 #_ #_ #H destruct /2 width=1/
+qed-.
(* *)
(**************************************************************************)
+include "Basic_2/grammar/tstc_vector.ma".
include "Basic_2/substitution/lift_vector.ma".
include "Basic_2/computation/cprs_tstc.ma".
(* CONTEXT-SENSITIVE PARALLEL COMPUTATION ON TERMS **************************)
(* Vector form of forward lemmas involving same top term constructor ********)
+(*
+lemma cpr_fwd_beta_vector: ∀L,V,W,T,U,Vs. L ⊢ ⒶVs. ⓐV. ⓛW. T ➡ U →
+ ⒶVs. ⓐV. ⓛW. T ≃ U ∨ L ⊢ ⒶVs. ⓓV. T ➡* U.
+#L #V #W #T #U * /2 width=1 by cpr_fwd_beta/
+#V0 #Vs #H
+elim (cpr_inv_appl1_simple … H ?) -H
+[ #V1 #T1 #_ #_ #H destruct /2 width=1/
+| elim Vs -Vs //
+]
+qed-.
lemma cpr_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡ U →
elim (cpr_inv_appl1_simple … H ?) -H //
#V0 #T0 #_ #_ #H destruct /2 width=1/
qed-.
+*)
+
+(* Basic_1: was: pr3_iso_appls_cast *)
+lemma cprs_fwd_tau_vector: ∀L,Vs,W,T,U. L ⊢ ⒶVs. ⓣW. T ➡* U →
+ ⒶVs. ⓣW. T ≃ U ∨ L ⊢ ⒶVs. T ➡* U.
+#L #Vs elim Vs -Vs /2 width=1 by cprs_fwd_tau/
+#V #Vs #IHVs #W #T #U #H
+elim (cprs_inv_appl1 … H) -H *
+[ -IHVs #V0 #T0 #_ #_ #H destruct /2 width=1/
+| #V0 #W0 #T0 #HV0 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tstc_inv_bind_appls_simple … HT0 ?) //
+ | @or_intror
+ @(cprs_trans … HU) -HU
+ @(cprs_strap1 … (ⓐV0.ⓛW0.T0)) /2 width=1/ -HV0 -HT0 /3 width=1/
+ ]
+| #V0 #V1 #V2 #T0 #HV0 #HV01 #HT0 #HU
+ elim (IHVs … HT0) -IHVs -HT0 #HT0
+ [ elim (tstc_inv_bind_appls_simple … HT0 ?) //
+ | @or_intror
+ @(cprs_trans … HU) -HU
+ @(cprs_strap1 … (ⓐV0.ⓓV2.T0)) /2 width=1/ -HV0 -HT0 /3 width=3/
+]
+qed-.
axiom cprs_fwd_theta_vector: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
∀V,T,U. L ⊢ ⒶV1s. ⓓV. T ➡* U →
- ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U.
\ No newline at end of file
+ ⒶV1s. ⓓV. T ≃ U ∨ L ⊢ ⓓV. ⒶV2s. T ➡* U.
(**************************************************************************)
include "Basic_2/grammar/tstc_tstc.ma".
-include "Basic_2/reducibility/lcpr_cpr.ma".
include "Basic_2/computation/cprs_cprs.ma".
include "Basic_2/computation/csn_lift.ma".
include "Basic_2/computation/csn_cpr.ma".
qed.
*)
lemma csn_applv_theta: ∀L,V1s,V2s. ⇧[0, 1] V1s ≡ V2s →
- ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V → L ⊢ ⬇* ⒶV1s. ⓓV. T.
+ ∀V,T. L ⊢ ⬇* ⓓV. ⒶV2s. T → L ⊢ ⬇* V →
+ L ⊢ ⬇* ⒶV1s. ⓓV. T.
#L #V1s #V2s * -V1s -V2s /2 width=1/
#V1s #V2s #V1 #V2 #HV12 #H
generalize in match HV12; -HV12 generalize in match V2; -V2 generalize in match V1; -V1
| -H2 #H1 @(csn_cprs_trans … H) -H /2 width=1/
]
qed.
+
+lemma csn_applv_tau: ∀L,W. L ⊢ ⬇* W →
+ ∀Vs,T. L ⊢ ⬇* ⒶVs. T →
+ L ⊢ ⬇* ⒶVs. ⓣW. T.
+#L #W #HW #Vs elim Vs -Vs /2 width=1/ -HW
+#V #Vs #IHV #T #H1T
+lapply (csn_fwd_pair_sn … H1T) #HV
+lapply (csn_fwd_flat_dx … H1T) #H2T
+@csn_appl_simple_tstc // -HV /2 width=1/ -IHV -H2T
+[ #X #H #H0
+ elim (cprs_fwd_tau_vector … H) -H #H
+ [ -H1T elim (H0 ?) -H0 //
+ | -H0 @(csn_cprs_trans … H1T) -H1T /2 width=1/
+ ]
+| -H1T elim Vs -Vs //
+]
+qed.
(*
theorem csn_acr: acr cpr (eq …) (csn …) (λL,T. L ⊢ ⬇* T).
@mk_acr //
| #L #V1 #V2 #HV12 #V #T #H #HVT
@(csn_applv_theta … HV12) -HV12 //
@(csn_abbr) //
-|
-| @csn_lift
+| /2 width=1/
+| @csn_lift
]
qed.
*)
lemma simple_tstc_repl_sn: ∀T1,T2. T1 ≃ T2 → 𝐒[T2] → 𝐒[T1].
/3 width=3/ qed-.
-
-(* Basic_1: removed theorems 2:
- iso_flats_lref_bind_false iso_flats_flat_bind_false
-*)
@ex2_1_intro [2: @(tpr_delta … HV12 HT1 HT0) | skip | /2 width=1/ ] (**) (* /3 width=5/ is too slow *)
qed.
-
(* Basic_1: was only: pr2_head_1 *)
lemma cpr_pair_sn: ∀I,L,V1,V2,T1,T2. L ⊢ V1 ➡ V2 → T1 ➡ T2 →
L ⊢ ②{I} V1. T1 ➡ ②{I} V2. T2.
projects / helm.git / commitdiff