include "basic_2/rt_computation/cpms_fpbg.ma".
include "basic_2/rt_computation/cpms_cpms.ma".
include "basic_2/dynamic/cnv_drops.ma".
-include "basic_2/dynamic/cnv_preserve_far.ma".
+include "basic_2/dynamic/cnv_preserve_sub.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Far diamond propery with t-bound rt-transition for terms *****************)
+(* Sub diamond propery with t-bound rt-transition for terms *****************)
fact cnv_cpm_conf_lpr_atom_atom_aux (h) (G) (L1) (L2) (I):
∃∃T. ⦃G,L1⦄ ⊢ ⓪{I} ➡*[0,h] T & ⦃G, L2⦄ ⊢ ⓪{I} ➡*[O,h] T.
elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct
lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2
lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
-elim (cnv_cpm_conf_lpr_far … IH … HV1 … HVX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
+elim (cnv_cpm_conf_lpr_sub … IH … HV1 … HVX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
<minus_O_n <minus_n_O #V #HV1 #HVX
elim (cpms_lifts_sn … HVX … HLK2 … HXV) -XV -HLK2 #XV #HVX #HXV
/3 width=6 by cpms_delta_drops, ex2_intro/
elim (lpr_inv_pair_sn … H2) -H2 #K2 #W2 #HK2 #_ #H destruct
lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2
lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
-elim (cnv_cpm_conf_lpr_far … IH … HW1 … HWX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -W
+elim (cnv_cpm_conf_lpr_sub … IH … HW1 … HWX … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -W
<minus_O_n <minus_n_O #W #HW1 #HWX
elim (cpms_lifts_sn … HWX … HLK2 … HXW) -XW -HLK2 #XW #HWX #HXW
/3 width=6 by cpms_ell_drops, ex2_intro/
elim (lpr_inv_pair_sn … H2) -H2 #K2 #V2 #HK2 #_ #H destruct
lapply (drops_isuni_fwd_drop2 … HLK2) -V2 // #HLK2
lapply (fqup_lref (Ⓣ) … G … HLK) -HLK #HLK
-elim (cnv_cpm_conf_lpr_far … IH … HVX1 … HVX2 … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
+elim (cnv_cpm_conf_lpr_sub … IH … HVX1 … HVX2 … HK1 … HK2) [|*: /2 width=1 by fqup_fpbg/ ] -L -K -V
#V #HVX1 #HVX2
elim (cpms_lifts_sn … HVX1 … HLK1 … HXV1) -XV1 -HLK1 #W1 #HVW1 #HXW1
/3 width=11 by cpms_lifts_bi, ex2_intro/
#L1 #HL01 #L2 #HL02
elim (cnv_inv_bind … H0) -H0 #HV0 #HT0
elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
-elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
#T #HT1 #HT2 -L0 -V0 -T0
/3 width=5 by cpms_bind_dx, ex2_intro/
qed-.
[ /3 width=3 by drops_refl, drops_drop/ ] #HT2
elim (cpm_inv_lifts_sn … HT01 (Ⓣ) … L0 … HT20) -HT01
[| /3 width=1 by drops_refl, drops_drop/ ] #XT1 #HXT1 #HXT12
-elim (cnv_cpm_conf_lpr_far … IH … HXT12 … HXT2 … HL01 … HL02)
+elim (cnv_cpm_conf_lpr_sub … IH … HXT12 … HXT2 … HL01 … HL02)
[|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 -V0 #T #HT1 #HT2
/3 width=3 by cpms_zeta, ex2_intro/
qed-.
lapply (lifts_inj … HT10 … HT20) -HT10 #H destruct
lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HT20) -HT0
[ /3 width=3 by drops_refl, drops_drop/ ] #HT2
-elim (cnv_cpm_conf_lpr_far … IH … HXT1 … HXT2 … HL01 … HL02)
+elim (cnv_cpm_conf_lpr_sub … IH … HXT1 … HXT2 … HL01 … HL02)
[|*: /3 width=1 by fqup_fpbg, fqup_zeta/ ] -L0 -T0 #T #HT1 #HT2
/2 width=3 by ex2_intro/
qed-.
#L1 #HL01 #L2 #HL02
elim (cnv_inv_appl … H0) -H0 #n0 #p0 #X01 #X02 #_ #HV0 #HT0 #_ #_ -n0 -p0 -X01 -X02
elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
-elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
#T #HT1 #HT2 -L0 -V0 -T0
/3 width=5 by cpms_appl_dx, ex2_intro/
qed-.
elim (cpm_inv_abst1 … HX) -HX #W1 #T1 #HW01 #HT01 #H destruct
elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
-elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
#T #HT1 #HT2 -L0 -V0 -W0 -T0
lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 [ /2 width=1 by lsubr_beta/ ] #HT2
/4 width=5 by cpms_beta_dx, cpms_bind_dx, cpm_cast, ex2_intro/
[ #W1 #T1 #HW01 #HT01 #H destruct
elim (cpm_lifts_sn … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2) -HVU2 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU2
elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
- elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+ elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
#T #HT1 #HT2 -L0 -V0 -W0 -T0
/4 width=7 by cpms_theta_dx, cpms_appl_dx, cpms_bind_dx, ex2_intro/
| #X0 #HXT0 #H1X0 #H destruct
lapply (cnv_inv_lifts … HT0 (Ⓣ) … L0 … HXT0) -HT0 [ /3 width=3 by drops_refl, drops_drop/ ] #H2X0
elim (cpm_inv_lifts_sn … HT02 (Ⓣ) … L0 … HXT0) -HT02 [| /3 width=1 by drops_refl, drops_drop/ ] #X2 #HXT2 #HX02
- elim (cnv_cpm_conf_lpr_far … IH … H1X0 … HX02 … HL01 … HL02)
+ elim (cnv_cpm_conf_lpr_sub … IH … H1X0 … HX02 … HL01 … HL02)
[|*: /4 width=5 by fqup_fpbg, fqup_strap1, fqu_drop/ ] #T #HT1 #HT2 -L0 -V0 -W0 -T0
/4 width=8 by cpms_zeta, cpms_appl_dx, lifts_flat, ex2_intro/
]
elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
-elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
#T #HT1 #HT2 -L0 -V0 -W0 -T0
lapply (lsubr_cpms_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/ #HT1
lapply (lsubr_cpms_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ #HT2
elim (cnv_inv_bind … H0) -H0 #HW0 #HT0
elim (cpr_conf_lpr … HV01 … HV02 … HL01 … HL02) #V #HV1 #HV2
elim (cpr_conf_lpr … HW01 … HW02 … HL01 … HL02) #W #HW1 #HW2
-elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) [|*: /2 width=1 by fqup_fpbg, lpr_pair/ ]
#T #HT1 #HT2 -L0 -V0 -W0 -T0
elim (cpm_lifts_sn … HV1 (Ⓣ) … (L1.ⓓW1) … HVU1) -V1 [| /3 width=1 by drops_refl, drops_drop/ ] #U #HVU #HU1
lapply (cpm_lifts_bi … HV2 (Ⓣ) … (L2.ⓓW2) … HVU2 … HVU) -V2 -V [ /3 width=1 by drops_refl, drops_drop/ ] #HU2
#n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01 #T2 #HT02
#L1 #HL01 #L2 #HL02
elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
-elim (cnv_cpm_conf_lpr_far … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
-elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
#T #HT1 #HT2 #V #HV1 #HV2 -L0 -V0 -T0
/3 width=5 by cpms_cast, ex2_intro/
qed-.
#n1 #V1 #HV01 #T1 #HT01 #n2 #T2 #HT02
#L1 #HL01 #L2 #HL02
elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #_ #_ -X0
-elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
#T #HT1 #HT2 -L0 -V0 -T0
/3 width=3 by cpms_eps, ex2_intro/
qed-.
#n1 #V1 #HV01 #n2 #V2 #HV02 #T1 #HT01
#L1 #HL01 #L2 #HL02 -HV01
elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
-lapply (cnv_cpms_trans_lpr_far … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
-elim (cnv_cpms_strip_lpr_far … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
-elim (cnv_cpms_strip_lpr_far … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
+lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
+elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
-HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
#n1 #T1 #HT01 #n2 #T2 #HT02
#L1 #HL01 #L2 #HL02
elim (cnv_inv_cast … H0) -H0 #X0 #_ #HT0 #_ #_ -X0
-elim (cnv_cpm_conf_lpr_far … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HT01 … HT02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
#T #HT1 #HT2 -L0 -V0 -T0
/2 width=3 by ex2_intro/
qed-.
#n1 #T1 #HT01 #n2 #V2 #HV02
#L1 #HL01 #L2 #HL02
elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #HT0 #HVX0 #HTX0
-lapply (cnv_cpms_trans_lpr_far … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
-elim (cnv_cpms_strip_lpr_far … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
-elim (cnv_cpms_strip_lpr_far … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
+lapply (cnv_cpms_trans_lpr_sub … IH2 … HVX0 … L0 ?) [4:|*: /2 width=1 by fqup_fpbg/ ] #HX0
+elim (cnv_cpms_strip_lpr_sub … IH1 … HVX0 … HV02 … L0 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpms_strip_lpr_sub … IH1 … HTX0 … HT01 … L0 … HL01) [|*: /2 width=1 by fqup_fpbg/ ]
-HV02 -HTX0 -HT01 <minus_O_n <minus_n_O #T #HT2 #HT1 #V #HV1 #HV2
elim (IH1 … HV1 … HT2 … HL02 … HL01) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ]
-L0 -V0 -T0 -X0 #U #HVU #HTU
#n1 #V1 #HV01 #n2 #V2 #HV02
#L1 #HL01 #L2 #HL02
elim (cnv_inv_cast … H0) -H0 #X0 #HV0 #_ #_ #_ -X0
-elim (cnv_cpm_conf_lpr_far … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
+elim (cnv_cpm_conf_lpr_sub … IH … HV01 … HV02 … HL01 … HL02) [|*: /2 width=1 by fqup_fpbg/ ]
#V #HV1 #HV2 -L0 -V0 -T0
/2 width=3 by ex2_intro/
qed-.
(* *)
(**************************************************************************)
+include "ground_2/xoa/ex_5_1.ma".
+include "ground_2/xoa/ex_9_3.ma".
+include "basic_2/rt_transition/cpm_tdeq.ma".
include "basic_2/rt_transition/cpr.ma".
include "basic_2/rt_computation/fpbg_fqup.ma".
include "basic_2/dynamic/cnv_fsb.ma".
-(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS ***************)
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Inversion lemmas with degree-based equivalence for terms *****************)
+(* Inversion lemmas with restricted rt-transition for terms *****************)
lemma cnv_cpr_tdeq_fwd_refl (a) (h) (o) (G) (L):
∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 → T1 ≛[h,o] T2 →
]
qed-.
-lemma cpm_tdeq_inv_bind (a) (h) (o) (n) (p) (I) (G) (L):
- ∀V,T1. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] →
- ∀X. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ➡[n,h] X → ⓑ{p,I}V.T1 ≛[h,o] X →
- ∃∃T2. ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓑ{p,I}V.T2.
+lemma cpm_tdeq_inv_bind_sn (a) (h) (o) (n) (p) (I) (G) (L):
+ ∀V,T1. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] →
+ ∀X. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ➡[n,h] X → ⓑ{p,I}V.T1 ≛[h,o] X →
+ ∃∃T2. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓑ{p,I}V.T2.
#a #h #o #n #p #I #G #L #V #T1 #H0 #X #H1 #H2
elim (cpm_inv_bind1 … H1) -H1 *
[ #XV #T2 #HXV #HT12 #H destruct
elim (tdeq_inv_pair … H2) -H2 #_ #H2XV #H2T12
- elim (cnv_inv_bind … H0) -H0 #HV #_
- lapply (cnv_cpr_tdeq_fwd_refl … HXV H2XV HV) #H destruct -HXV -H2XV -HV
- /2 width=4 by ex3_intro/
+ elim (cnv_inv_bind … H0) -H0 #HV #HT
+ lapply (cnv_cpr_tdeq_fwd_refl … HXV H2XV HV) #H destruct -HXV -H2XV
+ /2 width=4 by ex5_intro/
| #X1 #HXT1 #HX1 #H1 #H destruct
elim (cnv_fpbg_refl_false … o … H0) -a
@(fpbg_tdeq_div … H2) -H2
]
qed-.
-lemma cpm_tdeq_inv_appl (a) (h) (o) (n) (G) (L):
- ∀V,T1. ⦃G, L⦄ ⊢ ⓐV.T1 ![a,h] →
- ∀X. ⦃G, L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛[h,o] X →
- ∃∃T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓐV.T2.
+lemma cpm_tdeq_inv_appl_sn (a) (h) (o) (n) (G) (L):
+ ∀V,T1. ⦃G,L⦄ ⊢ ⓐV.T1 ![a,h] →
+ ∀X. ⦃G,L⦄ ⊢ ⓐV.T1 ➡[n,h] X → ⓐV.T1 ≛[h,o] X →
+ ∃∃m,q,W,U1,T2. a = Ⓣ → m ≤ 1 & ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ V ➡*[1,h] W & ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{q}W.U1
+ & ⦃G,L⦄⊢ T1 ![a,h] & ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓐV.T2.
#a #h #o #n #G #L #V #T1 #H0 #X #H1 #H2
elim (cpm_inv_appl1 … H1) -H1 *
[ #XV #T2 #HXV #HT12 #H destruct
elim (tdeq_inv_pair … H2) -H2 #_ #H2XV #H2T12
- elim (cnv_inv_appl … H0) -H0 #m #q #W #U #_ #HV #_ #_ #_ -m -q -W -U
- lapply (cnv_cpr_tdeq_fwd_refl … HXV H2XV HV) #H destruct -HXV -H2XV -HV
- /2 width=4 by ex3_intro/
+ elim (cnv_inv_appl … H0) -H0 #m #q #W #U1 #Hm #HV #HT #HVW #HTU1
+ lapply (cnv_cpr_tdeq_fwd_refl … HXV H2XV HV) #H destruct -HXV -H2XV
+ /3 width=7 by ex8_5_intro/
| #q #V2 #W1 #W2 #XT #T2 #_ #_ #_ #H1 #H destruct -H0
elim (tdeq_inv_pair … H2) -H2 #H #_ #_ destruct
| #q #V2 #XV #W1 #W2 #XT #T2 #_ #_ #_ #_ #H1 #H destruct -H0
]
qed-.
-lemma cpm_tdeq_inv_cast (a) (h) (o) (n) (G) (L):
- ∀U1,T1. ⦃G, L⦄ ⊢ ⓝU1.T1 ![a,h] →
- ∀X. ⦃G, L⦄ ⊢ ⓝU1.T1 ➡[n,h] X → ⓝU1.T1 ≛[h,o] X →
- ∃∃U2,T2. ⦃G, L⦄ ⊢ U1 ➡[n,h] U2 & U1 ≛[h,o] U2 & ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓝU2.T2.
+lemma cpm_tdeq_inv_cast_sn (a) (h) (o) (n) (G) (L):
+ ∀U1,T1. ⦃G, L⦄ ⊢ ⓝU1.T1 ![a,h] →
+ ∀X. ⦃G, L⦄ ⊢ ⓝU1.T1 ➡[n,h] X → ⓝU1.T1 ≛[h,o] X →
+ ∃∃U0,U2,T2. ⦃G,L⦄ ⊢ U1 ➡*[h] U0 & ⦃G,L⦄ ⊢ T1 ➡*[1,h] U0
+ & ⦃G, L⦄ ⊢ U1 ![a,h] & ⦃G, L⦄ ⊢ U1 ➡[n,h] U2 & U1 ≛[h,o] U2
+ & ⦃G, L⦄ ⊢ T1 ![a,h] & ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓝU2.T2.
#a #h #o #n #G #L #U1 #T1 #H0 #X #H1 #H2
elim (cpm_inv_cast1 … H1) -H1 [ * || * ]
-[ #U2 #T2 #HU12 #HT12 #H destruct -H0
+[ #U2 #T2 #HU12 #HT12 #H destruct
elim (tdeq_inv_pair … H2) -H2 #_ #H2U12 #H2T12
- /2 width=7 by ex5_2_intro/
+ elim (cnv_inv_cast … H0) -H0 #U0 #HU1 #HT1 #HU10 #HT1U0
+ /2 width=7 by ex9_3_intro/
| #HT1X
elim (cnv_fpbg_refl_false … o … H0) -a
@(fpbg_tdeq_div … H2) -H2
/3 width=6 by cpm_tdneq_cpm_fpbg, cpm_ee, tdeq_inv_pair_xy_x/
]
qed-.
+
+(* Eliminators with restricted rt-transition for terms **********************)
+
+lemma cpm_tdeq_ind (a) (h) (o) (n) (G) (Q:relation3 …):
+ (∀I,L. n = 0 → Q L (⓪{I}) (⓪{I})) →
+ (∀L,s. n = 1 → deg h o s 0 → Q L (⋆s) (⋆(next h s))) →
+ (∀p,I,L,V,T1. ⦃G,L⦄⊢ V![a,h] → ⦃G,L.ⓑ{I}V⦄⊢T1![a,h] →
+ ∀T2. ⦃G,L.ⓑ{I}V⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 →
+ Q (L.ⓑ{I}V) T1 T2 → Q L (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
+ ) →
+ (∀m. (a = Ⓣ → m ≤ 1) →
+ ∀L,V. ⦃G,L⦄ ⊢ V ![a,h] → ∀W. ⦃G, L⦄ ⊢ V ➡*[1,h] W →
+ ∀p,T1,U1. ⦃G, L⦄ ⊢ T1 ➡*[m,h] ⓛ{p}W.U1 → ⦃G,L⦄⊢ T1 ![a,h] →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 →
+ Q L T1 T2 → Q L (ⓐV.T1) (ⓐV.T2)
+ ) →
+ (∀L,U0,U1,T1. ⦃G,L⦄ ⊢ U1 ➡*[h] U0 → ⦃G,L⦄ ⊢ T1 ➡*[1,h] U0 →
+ ∀U2. ⦃G, L⦄ ⊢ U1 ![a,h] → ⦃G, L⦄ ⊢ U1 ➡[n,h] U2 → U1 ≛[h,o] U2 →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ![a,h] → ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 →
+ Q L U1 U2 → Q L T1 T2 → Q L (ⓝU1.T1) (ⓝU2.T2)
+ ) →
+ ∀L,T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → Q L T1 T2.
+#a #h #o #n #G #Q #IH1 #IH2 #IH3 #IH4 #IH5 #L #T1
+@(insert_eq_0 … G) #F
+@(fqup_wf_ind_eq (Ⓣ) … F L T1) -L -T1 -F
+#G0 #L0 #T0 #IH #F #L * [| * [| * ]]
+[ #I #_ #_ #_ #_ #HF #X #H1X #H2X destruct -G0 -L0 -T0
+ elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
+ [ #H1 #H2 destruct /2 width=1 by/
+ | #s #H1 #H2 #H3 #Hs destruct /2 width=1 by/
+ ]
+| #p #I #V #T1 #HG #HL #HT #H0 #HF #X #H1X #H2X destruct
+ elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #HV #HT1 #H1T12 #H2T12 #H destruct
+ /3 width=5 by/
+| #V #T1 #HG #HL #HT #H0 #HF #X #H1X #H2X destruct
+ elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #m #q #W #U1 #T2 #Hm #HV #HVW #HTU1 #HT1 #H1T12 #H2T12 #H destruct
+ /3 width=7 by/
+| #U1 #T1 #HG #HL #HT #H0 #HF #X #H1X #H2X destruct
+ elim (cpm_tdeq_inv_cast_sn … H0 … H1X H2X) -H0 -H1X -H2X #U0 #U2 #T2 #HU10 #HT1U0 #HU1 #H1U12 #H2U12 #HT1 #H1T12 #H2T12 #H destruct
+ /3 width=5 by/
+]
+qed-.
+
+(* Advanced properties with restricted rt-transition for terms **************)
+
+lemma cpm_tdeq_free (a) (h) (o) (n) (G) (L):
+ ∀T1. ⦃G, L⦄ ⊢ T1 ![a,h] →
+ ∀T2. ⦃G, L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 →
+ ∀F,K. ⦃F, K⦄ ⊢ T1 ➡[n,h] T2.
+#a #h #o #n #G #L #T1 #H0 #T2 #H1 #H2
+@(cpm_tdeq_ind … H0 … H1 H2) -L -T1 -T2
+[ #I #L #H #F #K destruct //
+| #L #s #H #_ #F #K destruct //
+| #p #I #L #V #T1 #_ #_ #T2 #_ #_ #IH #F #K
+ /2 width=1 by cpm_bind/
+| #m #_ #L #V #_ #W #_ #q #T1 #U1 #_ #_ #T2 #_ #_ #IH #F #K
+ /2 width=1 by cpm_appl/
+| #L #U0 #U1 #T1 #_ #_ #U2 #_ #_ #_ #T2 #_ #_ #_ #IHU #IHT #F #K
+ /2 width=1 by cpm_cast/
+]
+qed-.
+
+(* Advanced inversion lemmas with restricted rt-transition for terms ********)
+
+lemma cpm_tdeq_inv_bind_sn_void (a) (h) (o) (n) (p) (I) (G) (L):
+ ∀V,T1. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ![a,h] →
+ ∀X. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T1 ➡[n,h] X → ⓑ{p,I}V.T1 ≛[h,o] X →
+ ∃∃T2. ⦃G,L⦄ ⊢ V ![a,h] & ⦃G, L.ⓑ{I}V⦄ ⊢ T1 ![a,h] & ⦃G, L.ⓧ⦄ ⊢ T1 ➡[n,h] T2 & T1 ≛[h,o] T2 & X = ⓑ{p,I}V.T2.
+#a #h #o #n #p #I #G #L #V #T1 #H0 #X #H1 #H2
+elim (cpm_tdeq_inv_bind_sn … H0 … H1 H2) -H0 -H1 -H2 #T2 #HV #HT1 #H1T12 #H2T12 #H
+/3 width=5 by ex5_intro, cpm_tdeq_free/
+qed-.
include "basic_2/rt_computation/cprs_cprs.ma".
include "basic_2/rt_computation/lprs_cpms.ma".
include "basic_2/dynamic/cnv_drops.ma".
-include "basic_2/dynamic/cnv_preserve_far.ma".
+include "basic_2/dynamic/cnv_preserve_sub.ma".
include "basic_2/dynamic/lsubv_cnv.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Far preservation propery with t-bound rt-transition for terms ************)
+(* Sub preservation propery with t-bound rt-transition for terms ************)
fact cnv_cpm_trans_lpr_aux (a) (h) (o):
∀G0,L0,T0.
[ #V2 #T2 #HV12 #HT12 #H destruct
lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
- elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
+ elim (cnv_cpms_strip_lpr_sub … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
<minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
- elim (cnv_cpms_strip_lpr_far … IH2 … HTU1 … HT12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
+ elim (cnv_cpms_strip_lpr_sub … IH2 … HTU1 … HT12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
#X #H #HTU2 -IH2 -IH1 -L1 -V1 -T1
elim (cpms_inv_abst_sn … H) -H #W2 #U2 #HW12 #_ #H destruct
elim (cprs_conf … HXW1 … HW12) -W1 #W1 #HXW1 #HW21
lapply (IH1 … HV12 … HL12) /2 width=1 by fqup_fpbg/ #HV2
lapply (IH1 … HW120 … HL12) /2 width=1 by fqup_fpbg/ #HW20
lapply (IH1 … HT10 … HT120 … (L2.ⓛW20) ?) /2 width=1 by fqup_fpbg, lpr_pair/ -HT10 -HT120 #HT20
- elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
+ elim (cnv_cpms_strip_lpr_sub … IH2 … HVW1 … HV12 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV12
<minus_n_O <minus_O_n #XW1 #HXW1 #HXV2
- elim (cnv_cpms_strip_lpr_far … IH2 … HW130 … HW120 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW130 -HW120
+ elim (cnv_cpms_strip_lpr_sub … IH2 … HW130 … HW120 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW130 -HW120
<minus_n_O #XW30 #HXW30 #HW230 -IH2 -IH1 -L1 -V1 -W10 -T10
elim (cprs_conf … HXW1 … HXW30) -W30 #W30 #HXW1 #HXW30
lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W30
lapply (IH1 … HW02 … HL12) /2 width=1 by fqup_fpbg/ #HW2
lapply (IH1 … HV10 … HL12) /2 width=1 by fqup_fpbg/ #HV0
lapply (IH1 … HT02 (L2.ⓓW2) ?) /2 width=1 by fqup_fpbg, lpr_pair/ #HT2
- elim (cnv_cpms_strip_lpr_far … IH2 … HVW1 … HV10 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV10
+ elim (cnv_cpms_strip_lpr_sub … IH2 … HVW1 … HV10 … HL12 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HVW1 -HV10
<minus_n_O <minus_O_n #XW1 #HXW1 #HXV0
- elim (cnv_cpms_strip_lpr_far … IH2 … HTU0 … HT02 … (L2.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=2 by fqup_fpbg, lpr_pair/ ] -HTU0 -HT02 -HW02
+ elim (cnv_cpms_strip_lpr_sub … IH2 … HTU0 … HT02 … (L2.ⓓW2) … (L2.ⓓW2)) [|*: /2 width=2 by fqup_fpbg, lpr_pair/ ] -HTU0 -HT02 -HW02
#X #H #HTU2 -IH2 -IH1 -L1 -W0 -T0 -U1
elim (cpms_inv_abst_sn … H) -H #W #U2 #HW3 #_ #H destruct -U3
lapply (cnv_lifts … HV0 (Ⓣ) … (L2.ⓓW2) … HV02) /3 width=1 by drops_refl, drops_drop/ -HV0 #HV2
[ * #W2 #T2 #HW12 #HT12 #H destruct
lapply (IH1 … HW12 … HL12) /2 width=1 by fqup_fpbg/ #HW2
lapply (IH1 … HT12 … HL12) /2 width=1 by fqup_fpbg/ #HT2
- lapply (cnv_cpms_trans_lpr_far … IH1 … HTU1 L1 ?) /2 width=1 by fqup_fpbg/ #HU1
- elim (cnv_cpms_strip_lpr_far … IH2 … HWU1 … HW12 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW12
+ lapply (cnv_cpms_trans_lpr_sub … IH1 … HTU1 L1 ?) /2 width=1 by fqup_fpbg/ #HU1
+ elim (cnv_cpms_strip_lpr_sub … IH2 … HWU1 … HW12 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HW12
<minus_n_O <minus_O_n #XW1 #HXUW1 #HXW21
- elim (cnv_cpms_strip_lpr_far … IH2 … HTU1 … HT12 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
+ elim (cnv_cpms_strip_lpr_sub … IH2 … HTU1 … HT12 … L1 … HL12) [|*: /2 width=2 by fqup_fpbg/ ] -HTU1 -HT12
#XT1 #HXUT1 #HXT21
elim (IH2 … HXUW1 … HXUT1 … HL12 … HL12) [|*: /2 width=4 by fqup_cpms_fwd_fpbg/ ] -HXUW1 -HXUT1 -HWU1
>eq_minus_O // #W0 #H1 #H2 -IH2 -IH1 -L1 -W1 -T1 -U1
(* *)
(**************************************************************************)
+include "basic_2/notation/relations/predstar_7.ma".
include "basic_2/dynamic/cnv_cpm_trans.ma".
include "basic_2/dynamic/cnv_cpm_conf.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Far confluence propery with t-bound rt-computation for terms *************)
+definition cpsms (n) (h) (o): relation4 genv lenv term term ≝ λG,L,T1,T2.
+ ∃∃n1,n2,T. T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2 = n.
+
+interpretation
+ "context-sensitive parallel stratified t-bound rt-computarion (term)"
+ 'PRedStar n h o G L T1 T2 = (cpsms n h o G L T1 T2).
+
+definition IH_cnv_cpsms_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h,o] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h,o] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
+(* Sub confluence propery with t-bound rt-computation for terms *************)
fact cnv_cpsms_conf_lpr_aux (a) (h) (o):
∀G0,L0,T0.
elim (cnv_cpm_conf_lpr_aux … IH2 IH1 … HX01 … HX02 … L0 … L0) // #Z0 #HXZ10 #HXZ20
cut (⦃G0,L0,T0⦄ >[h,o] ⦃G0,L0,X1⦄) [ /4 width=5 by cpms_fwd_fpbs, cpm_fpb, ex2_3_intro/ ] #H1fpbg (**) (* cut *)
lapply (fpbg_fpbs_trans ??? G0 ? L0 ? Z0 ? … H1fpbg) [ /2 width=2 by cpms_fwd_fpbs/ ] #H2fpbg
-lapply (cnv_cpms_trans_lpr_far … IH2 … HXZ10 … L0 ?) // #HZ0
+lapply (cnv_cpms_trans_lpr_sub … IH2 … HXZ10 … L0 ?) // #HZ0
elim (IH1 … HXT1 … HXZ10 … L1 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT1 -HXZ10 #Z1 #HTZ1 #HZ01
elim (IH1 … HXT2 … HXZ20 … L2 … L0) [|*: /4 width=2 by fpb_fpbg, cpm_fpb/ ] -HXT2 -HXZ20 #Z2 #HTZ2 #HZ02
elim (IH1 … HZ01 … HZ02 L1 … L2) // -L0 -T0 -X1 -X2 -Z0 #Z #HZ01 #HZ02
--- /dev/null
+(*
+axiom cpms_tdneq_fwd_step_sn (n) (h) (o) (G) (L):
+ ∀T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[n,h] T2 → (T1 ≛[h,o] T2 → ⊥) →
+ ∃∃n1,n2,T,T0. ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T ➡*[n2,h] T0 & T0 ≛[h,o] T2 & n1+n2 = n.
+axiom plus_Sxy_y_false: ∀y,x. ↑(x+y) = y → ⊥.
+
+lemma cnv_cpm_tdeq_trans (a) (h) (o) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀n,T2. ⦃G,L⦄ ⊢ T1 ➡[n,h] T2 → T1 ≛[h,o] T2 → ⦃G,L⦄ ⊢ T2 ![a,h].
+#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
+#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
+[ #I #_ #_ #_ #H0 #n #X #H1X #H2X -G0 -L0 -T0
+ elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
+ [ #H #_ destruct //
+ | #s #H #_ #_ #_ destruct //
+ ]
+| #p #I #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
+ elim (cnv_inv_bind … H0) #HV1 #_
+ elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
+ /3 width=6 by cnv_bind/
+| #V1 #T1 #HG #HL #HT #H0 #n #X #H1X #H2X destruct
+ elim (cnv_inv_appl … H0) #m #p #W1 #U1 #Hm #HV1 #_ #HVW1 #HTU1
+ elim (cpm_tdeq_inv_appl_sn … H0 … H1X H2X) -H0 -H1X -H2X #T2 #H1T #H2T #H3T #H destruct
+ @(cnv_appl … Hm … HVW1)
+
+(* Properties with restricted rt-transition for terms ***********************)
+
+lemma pippo (a) (h) (o) (G) (L):
+ ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] →
+ ∀n1,T. ⦃G,L⦄ ⊢ T1 ➡[n1,h] T → T1 ≛[h,o] T →
+ ∀n2,T2. ⦃G,L⦄ ⊢ T ➡[n2,h] T2 →
+ ∃∃T0. ⦃G,L⦄ ⊢ T1 ➡[n2,h] T0 & ⦃G,L⦄ ⊢ T0 ➡[n1,h] T2 & T0 ≛[h,o] T2.
+#a #h #o #G #L #T1 @(fqup_wf_ind_eq (Ⓣ) … G L T1) -G -L -T1
+#G0 #L0 #T0 #IH #G #L * [| * [| * ]]
+[ #I #_ #_ #_ #_ #n1 #X1 #H1X #H2X #n2 #X2 #HX2 -G0 -L0 -T0
+ elim (cpm_tdeq_inv_atom_sn … H1X H2X) -H1X -H2X *
+ [ #H1 #H2 destruct /2 width=4 by ex3_intro/
+ | #s #H1 #H2 #H3 #Hs destruct
+ elim (cpm_inv_sort1 … HX2) -HX2 #H #Hn2 destruct >iter_n_Sm
+ /5 width=6 by cpm_sort_iter, tdeq_sort, deg_iter, deg_next, ex3_intro/
+ ]
+| #p #I #V1 #T1 #HG #HL #HT #H0 #n1 #X1 #H1X #H2X #n2 #X2 #HX2 destruct
+ elim (cpm_tdeq_inv_bind_sn … H0 … H1X H2X) -H0 -H1X -H2X #T #H1T1 #H2T1 #H3T1 #H destruct
+ elim (cpm_inv_bind1 … HX2) -HX2 *
+ [ #V2 #T2 #HV12 #HT2 #H destruct
+ elim (IH … H1T1 … H2T1 H3T1 … HT2) -IH -H1T1 -H2T1 -H3T1 -HT2 [2: // ] #T0 #HT10 #H1T02 #H2T02
+ @(ex3_intro … (ⓑ{p,I}V2.T0))
+ [ /2 width=1 by cpm_bind/
+ |
+ | /2 width=1 by tdeq_pair/
+
+*)
(* *)
(**************************************************************************)
-include "basic_2/notation/relations/predstar_7.ma".
-include "basic_2/rt_computation/fpbg.ma".
-include "basic_2/rt_computation/cpms_fpbs.ma".
-include "basic_2/dynamic/cnv.ma".
+include "basic_2/dynamic/cnv_cpm_trans.ma".
(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
-(* Inductive premises for the preservation results **************************)
+(* Far properties for preservation ******************************************)
-definition cpsms (n) (h) (o): relation4 genv lenv term term ≝ λG,L,T1,T2.
- ∃∃n1,n2,T. T1 ≛[h,o] T → ⊥ & ⦃G, L⦄ ⊢ T1 ➡[n1,h] T & ⦃G, L⦄ ⊢ T ➡*[n2,h] T2 & n1+n2 = n.
-
-interpretation
- "context-sensitive parallel stratified t-bound rt-computarion (term)"
- 'PRedStar n h o G L T1 T2 = (cpsms n h o G L T1 T2).
-
-definition IH_cnv_cpm_trans_lpr (a) (h): relation3 genv lenv term ≝
- λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
- ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡[n,h] T2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h].
-
-definition IH_cnv_cpms_trans_lpr (a) (h): relation3 genv lenv term ≝
- λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
- ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡*[n,h] T2 →
- ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h].
-
-definition IH_cnv_cpm_conf_lpr (a) (h): relation3 genv lenv term ≝
- λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
- ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
-
-definition IH_cnv_cpms_strip_lpr (a) (h): relation3 genv lenv term ≝
- λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
- ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
-
-definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
- λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
- ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
-
-definition IH_cnv_cpsms_conf_lpr (a) (h) (o): relation3 genv lenv term ≝
- λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
- ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h,o] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h,o] T2 →
- ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
- ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
-
-(* Properties for preservation **********************************************)
-
-lemma cnv_cpms_trans_lpr_far (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
-#a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
+fact cnv_cpms_trans_lpr_far (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
+#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 #T1 #HG #HL #HT #H0 #n #T2 #H destruct
@(cpms_ind_dx … H) -n -T2
-/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
+[ #L2 #HL12 @(cnv_cpm_trans_lpr_aux … IH2 IH1 … H0 … 0 T1 … HL12) -L2 -IH2 -IH1 -H0 //
+| #n2 #n2 #T #T2 #HT1 #IH #HT2 #L2 #HL12 destruct
+ @(cnv_cpm_trans_lpr_aux … o … HT2 … HL12) [1,2,3,6,7,8,9: /2 width=2 by/ ] -n2 -L2 -T2 -IH
+ /3 width=4 by cpms_fpbg_trans/
+]
qed-.
-
-lemma cnv_cpm_conf_lpr_far (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_conf_lpr a h G1 L1 T1.
-/3 width=8 by cpm_cpms/ qed-.
-
-lemma cnv_cpms_strip_lpr_far (a) (h) (o):
- ∀G0,L0,T0.
- (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
- ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1.
-/3 width=8 by cpm_cpms/ 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/rt_computation/fpbg.ma".
+include "basic_2/rt_computation/cpms_fpbs.ma".
+include "basic_2/dynamic/cnv.ma".
+
+(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
+
+(* Inductive premises for the preservation results **************************)
+
+definition IH_cnv_cpm_trans_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
+ ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡[n,h] T2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h].
+
+definition IH_cnv_cpms_trans_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L1,T1. ⦃G, L1⦄ ⊢ T1 ![a,h] →
+ ∀n,T2. ⦃G, L1⦄ ⊢ T1 ➡*[n,h] T2 →
+ ∀L2. ⦃G, L1⦄ ⊢ ➡[h] L2 → ⦃G, L2⦄ ⊢ T2 ![a,h].
+
+definition IH_cnv_cpm_conf_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
+definition IH_cnv_cpms_strip_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡[n2,h] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
+definition IH_cnv_cpms_conf_lpr (a) (h): relation3 genv lenv term ≝
+ λG,L0,T0. ⦃G, L0⦄ ⊢ T0 ![a,h] →
+ ∀n1,T1. ⦃G, L0⦄ ⊢ T0 ➡*[n1,h] T1 → ∀n2,T2. ⦃G, L0⦄ ⊢ T0 ➡*[n2,h] T2 →
+ ∀L1. ⦃G, L0⦄ ⊢ ➡[h] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h] L2 →
+ ∃∃T. ⦃G, L1⦄ ⊢ T1 ➡*[n2-n1,h] T & ⦃G, L2⦄ ⊢ T2 ➡*[n1-n2,h] T.
+
+(* Auxiliary properties for preservation ************************************)
+
+fact cnv_cpms_trans_lpr_sub (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_trans_lpr a h G1 L1 T1.
+#a #h #o #G0 #L0 #T0 #IH #G1 #L1 #T1 #H01 #HT1 #n #T2 #H
+@(cpms_ind_dx … H) -n -T2
+/4 width=7 by cpms_fwd_fpbs, fpbg_fpbs_trans/
+qed-.
+
+fact cnv_cpm_conf_lpr_sub (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_conf_lpr a h G1 L1 T1.
+/3 width=8 by cpm_cpms/ qed-.
+
+fact cnv_cpms_strip_lpr_sub (a) (h) (o):
+ ∀G0,L0,T0.
+ (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
+ ∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_strip_lpr a h G1 L1 T1.
+/3 width=8 by cpm_cpms/ qed-.
(**************************************************************************)
include "basic_2/rt_computation/fpbg_fqup.ma".
+include "basic_2/rt_computation/fpbg_fpbs.ma".
include "basic_2/rt_computation/cpms_fpbs.ma".
(* T-BOUND CONTEXT-SENSITIVE PARALLEL RT-COMPUTATION FOR TERMS **************)
lemma fqup_cpms_fwd_fpbg (h) (o): ∀G1,G2,L1,L2,T1,T. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T⦄ →
∀n,T2. ⦃G2, L2⦄ ⊢ T ➡*[n,h] T2 → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
/3 width=5 by cpms_fwd_fpbs, fqup_fpbg,fpbg_fpbs_trans/ qed-.
+
+lemma cpms_fpbg_trans (h) (o) (n): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ➡*[n,h] T →
+ ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h,o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h,o] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbs_fpbg_trans, cpms_fwd_fpbs/ qed-.
include "basic_2/rt_computation/cpxs_tdeq.ma".
include "basic_2/rt_computation/fpbs_cpxs.ma".
-include "basic_2/rt_computation/fpbg.ma".
+include "basic_2/rt_computation/fpbg_fpbs.ma".
(* PROPER PARALLEL RST-COMPUTATION FOR CLOSURES *****************************)
(* Properties with unbound context-sensitive parallel rt-computation ********)
(* Basic_2A1: was: cpxs_fpbg *)
-lemma cpxs_tdneq_fpbg: ∀h,o,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
- (T1 ≛[h, o] T2 → ⊥) → ⦃G, L, T1⦄ >[h, o] ⦃G, L, T2⦄.
+lemma cpxs_tdneq_fpbg (h) (o): ∀G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 →
+ (T1 ≛[h, o] T2 → ⊥) → ⦃G, L, T1⦄ >[h, o] ⦃G, L, T2⦄.
#h #o #G #L #T1 #T2 #H #H0
elim (cpxs_tdneq_fwd_step_sn … H … H0) -H -H0
/4 width=5 by cpxs_tdeq_fpbs, fpb_cpx, ex2_3_intro/
qed.
+
+lemma cpxs_fpbg_trans (h) (o): ∀G1,L1,T1,T. ⦃G1, L1⦄ ⊢ T1 ⬈*[h] T →
+ ∀G2,L2,T2. ⦃G1, L1, T⦄ >[h, o] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, o] ⦃G2, L2, T2⦄.
+/3 width=5 by fpbs_fpbg_trans, cpxs_fpbs/ qed-.
elim (tdeq_inv_sort1 … H) -H #s0 #d #H1 #H2 #H destruct
lapply (deg_next … H1) #H0
lapply (deg_mono … H0 … H2) -H0 -H2 #H
-<(pred_inv_refl … H) -H //
+>(pred_inv_fix_sn … H) -H //
qed-.
lemma cnx_inv_abst: ∀h,o,p,G,L,V,T. ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃ⓛ{p}V.T⦄ →
lemma cpr_refl: ∀h,G,L. reflexive … (cpm h G L 0).
/3 width=3 by cpg_refl, ex2_intro/ qed.
+(* Advanced properties ******************************************************)
+
+lemma cpm_sort_iter (h) (G) (L):
+ ∀n. n ≤ 1 →
+ ∀s. ⦃G,L⦄ ⊢ ⋆s ➡ [n,h] ⋆((next h)^n s).
+#h #G #L * //
+#n #H #s <(le_n_O_to_eq n) /2 width=1 by le_S_S_to_le/
+qed.
+
(* Basic inversion lemmas ***************************************************)
lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 →
(* Inversion lemmas with degree-based equivalence for terms *****************)
-lemma cpm_tdeq_inv_lref (n) (h) (o) (G) (L) (i):
- ∀X. ⦃G, L⦄ ⊢ #i ➡[n,h] X → #i ≛[h,o] X →
- ∧∧ X = #i & n = 0.
+lemma cpm_tdeq_inv_lref_sn (n) (h) (o) (G) (L) (i):
+ ∀X. ⦃G,L⦄ ⊢ #i ➡[n,h] X → #i ≛[h,o] X →
+ ∧∧ X = #i & n = 0.
#n #h #o #G #L #i #X #H1 #H2
lapply (tdeq_inv_lref1 … H2) -H2 #H destruct
elim (cpm_inv_lref1_drops … H1) -H1 // * [| #m ]
#K #V1 #V2 #_ #_ #H -V1
elim (lifts_inv_lref2_uni_lt … H) -H //
qed-.
+
+lemma cpm_tdeq_inv_atom_sn (n) (h) (o) (I) (G) (L):
+ ∀X. ⦃G,L⦄ ⊢ ⓪{I} ➡[n,h] X → ⓪{I} ≛[h,o] X →
+ ∨∨ ∧∧ X = ⓪{I} & n = 0
+ | ∃∃s. X = ⋆(next h s) & I = Sort s & n = 1 & deg h o s 0.
+#n #h #o * #s #G #L #X #H1 #H2
+[ elim (cpm_inv_sort1 … H1) -H1
+ cases n -n [| #n ] #H #Hn destruct
+ [ /3 width=1 by or_introl, conj/
+ | elim (tdeq_inv_sort1 … H2) -H2 #x #d #Hs
+ <(le_n_O_to_eq n) [| /2 width=3 by le_S_S_to_le/ ] -n #Hx #H destruct
+ lapply (deg_next … Hs) #H
+ lapply (deg_mono … H Hx) -H -Hx #Hd
+ lapply (pred_inv_fix_sn … Hd) -Hd #H destruct
+ /3 width=4 by refl, ex4_intro, or_intror/
+ ]
+| elim (cpm_tdeq_inv_lref_sn … H1 H2) -H1 -H2 /3 width=1 by or_introl, conj/
+| elim (cpm_inv_gref1 … H1) -H1 -H2 /3 width=1 by or_introl, conj/
+]
+qed-.
*)
[ { "context-sensitive native validity" * } {
[ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
- [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpms_conf" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
+ [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpms_conf" + "cnv_preserve_sub" + "cnv_preserve_far" (* + "cnv_preserve" *) * ]
}
]
}
[ >(le_to_leb_true … H) | >(not_le_to_leb_false … H) ] -H //
qed.
-(* Equations ****************************************************************)
+(* Equalities ***************************************************************)
lemma plus_SO: ∀n. n + 1 = ↑n.
// qed.
lemma minus_plus_m_m_commutative: ∀n,m:nat. n = m + n - m.
// qed-.
-lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
-// qed.
+lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 →
+ m1+n2 = m2+n1 → m1-n1 = m2-n2.
+#m1 #m2 #n1 #n2 #H1 #H2 #H
+@plus_to_minus >plus_minus_associative //
+qed-.
(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *)
lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y.
lemma minus_minus_comm3: ∀n,x,y,z. n-x-y-z = n-y-z-x.
// qed.
-lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
-qed-.
-
-lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
-#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/
-qed-.
-
-lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
-/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
-
-lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
- a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
-#a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/
-qed-.
-
-lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
-/2 width=1 by plus_minus/ qed-.
-
-lemma plus_to_minus_2: ∀m1,m2,n1,n2. n1 ≤ m1 → n2 ≤ m2 →
- m1+n2 = m2+n1 → m1-n1 = m2-n2.
-/2 width=1 by arith_b1/ qed-.
-
lemma idempotent_max: ∀n:nat. n = (n ∨ n).
#n normalize >le_to_leb_true //
qed.
#m #Hm * /3 width=1 by not_le_to_lt, le_S_S, or3_intro2/
qed-.
-fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
-// qed-.
-
-fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z.
-// qed-.
-
lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
/3 width=1 by monotonic_le_minus_l/ qed.
lemma max_S2_le_S: ∀n1,n2,n. (n1 ∨ n2) ≤ n → (n1 ∨ ↑n2) ≤ ↑n.
/2 width=1 by max_S1_le_S/ qed-.
-lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
-/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
-
-lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1.
-#z #x #y #n #Hzx #Hxny
->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
->plus_minus [2: /2 width=1 by lt_to_le/ ]
-/2 width=1 by monotonic_le_minus_l2/
-qed.
-
-lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n.
-#z #x #y #n #Hzx #Hyxn
->plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
->plus_minus [2: /2 width=1 by lt_to_le/ ]
-/2 width=1 by monotonic_le_minus_l2/
-qed.
-
(* Inversion & forward lemmas ***********************************************)
lemma lt_refl_false: ∀n. n < n → ⊥.
lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥.
/2 width=4 by plus_xySz_x_false/ qed-.
-lemma pred_inv_refl: ∀m. pred m = m → m = 0.
-* // normalize #m #H elim (lt_refl_false m) //
+lemma pred_inv_fix_sn: ∀x. ↓x = x → 0 = x.
+* // #x <pred_Sn #H
+elim (succ_inv_refl_sn x) //
qed-.
lemma discr_plus_xy_y: ∀x,y. x + y = y → x = 0.
lemma discr_plus_x_xy: ∀x,y. x = x + y → y = 0.
/2 width=2 by le_plus_minus_comm/ qed-.
-lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
-/2 width=1 by monotonic_pred/ qed-.
-
lemma plus2_inv_le_sn: ∀m1,m2,n1,n2. m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
#m1 #m2 #n1 #n2 #H #Hm
lapply (monotonic_le_plus_l n1 … Hm) -Hm >H -H
lemma iter_S: ∀B:Type[0]. ∀f:B→B.∀b,l. f^(S l) b = f (f^l b).
// qed.
-lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
-#B #f #b #l >commutative_plus //
-qed.
-
lemma iter_n_Sm: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^l (f b) = f (f^l b).
#B #f #b #l elim l -l normalize //
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 "ground_2/lib/arith.ma".
+
+(* ARITHMETICAL PROPERTIES FOR λδ-2B ****************************************)
+
+(* Equalities ***************************************************************)
+
+lemma plus_n_2: ∀n. n + 2 = n + 1 + 1.
+// qed.
+
+lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
+#a #b #c1 #H >minus_minus_comm >minus_le_minus_minus_comm //
+qed-.
+
+lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
+#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1 by arith_b1/
+qed-.
+
+lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
+/3 by monotonic_le_minus_l, le_to_le_to_eq, le_n/ qed.
+
+lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
+ a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
+#a1 #a2 #b #c1 #H1 #H2 >plus_minus /2 width=1 by arith_b2/
+qed-.
+
+lemma arith_i: ∀x,y,z. y < x → x+z-y-1 = x-y-1+z.
+/2 width=1 by plus_minus/ qed-.
+
+(* Properties ***************************************************************)
+
+fact le_repl_sn_conf_aux: ∀x,y,z:nat. x ≤ z → x = y → y ≤ z.
+// qed-.
+
+fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z.
+// qed-.
+
+lemma arith_j: ∀x,y,z. x-y-1 ≤ x-(y-z)-1.
+/3 width=1 by monotonic_le_minus_l, monotonic_le_minus_r/ qed.
+
+lemma arith_k_sn: ∀z,x,y,n. z < x → x+n ≤ y → x-z-1+n ≤ y-z-1.
+#z #x #y #n #Hzx #Hxny
+>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
+>plus_minus [2: /2 width=1 by lt_to_le/ ]
+/2 width=1 by monotonic_le_minus_l2/
+qed.
+
+lemma arith_k_dx: ∀z,x,y,n. z < x → y ≤ x+n → y-z-1 ≤ x-z-1+n.
+#z #x #y #n #Hzx #Hyxn
+>plus_minus [2: /2 width=1 by monotonic_le_minus_r/ ]
+>plus_minus [2: /2 width=1 by lt_to_le/ ]
+/2 width=1 by monotonic_le_minus_l2/
+qed.
+
+(* Inversion & forward lemmas ***********************************************)
+
+lemma lt_plus_SO_to_le: ∀x,y. x < y + 1 → x ≤ y.
+/2 width=1 by monotonic_pred/ qed-.
+
+(* Iterators ****************************************************************)
+
+lemma iter_SO: ∀B:Type[0]. ∀f:B→B. ∀b,l. f^(l+1) b = f (f^l b).
+#B #f #b #l >commutative_plus //
+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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+(* multiple existental quantifier (5, 1) *)
+
+notation > "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}.$P0) (λ${ident x0}.$P1) (λ${ident x0}.$P2) (λ${ident x0}.$P3) (λ${ident x0}.$P4) }.
+
+notation < "hvbox(∃∃ ident x0 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4)"
+ non associative with precedence 20
+ for @{ 'Ex (λ${ident x0}:$T0.$P0) (λ${ident x0}:$T0.$P1) (λ${ident x0}:$T0.$P2) (λ${ident x0}:$T0.$P3) (λ${ident x0}:$T0.$P4) }.
+
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+(* multiple existental quantifier (9, 3) *)
+
+notation > "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)"
+ non associative with precedence 20
+ for @{ 'Ex3 (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P0) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P1) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P2) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P3) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P4) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P5) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P6) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P7) (λ${ident x0}.λ${ident x1}.λ${ident x2}.$P8) }.
+
+notation < "hvbox(∃∃ ident x0 , ident x1 , ident x2 break . term 19 P0 break & term 19 P1 break & term 19 P2 break & term 19 P3 break & term 19 P4 break & term 19 P5 break & term 19 P6 break & term 19 P7 break & term 19 P8)"
+ non associative with precedence 20
+ for @{ 'Ex3 (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P0) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P1) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P2) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P3) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P4) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P5) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P6) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P7) (λ${ident x0}:$T0.λ${ident x1}:$T1.λ${ident x2}:$T2.$P8) }.
+
[ { "" * } {
[ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ]
[ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_length ( |?| )" * ]
- [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2b" * ]
+ [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" "arith_2a" "arith_2b" * ]
[ "ltc" "ltc_ctc" * ]
[ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" * ]
}
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+include "basics/pts.ma".
+
+include "ground_2/notation/xoa/ex_5_1.ma".
+
+(* multiple existental quantifier (5, 1) *)
+
+inductive ex5 (A0:Type[0]) (P0,P1,P2,P3,P4:A0→Prop) : Prop ≝
+ | ex5_intro: ∀x0. P0 x0 → P1 x0 → P2 x0 → P3 x0 → P4 x0 → ex5 ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (5, 1)" 'Ex P0 P1 P2 P3 P4 = (ex5 ? P0 P1 P2 P3 P4).
+
--- /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 *)
+(* *)
+(**************************************************************************)
+
+(* This file was generated by xoa.native: do not edit *********************)
+
+include "basics/pts.ma".
+
+include "ground_2/notation/xoa/ex_9_3.ma".
+
+(* multiple existental quantifier (9, 3) *)
+
+inductive ex9_3 (A0,A1,A2:Type[0]) (P0,P1,P2,P3,P4,P5,P6,P7,P8:A0→A1→A2→Prop) : Prop ≝
+ | ex9_3_intro: ∀x0,x1,x2. P0 x0 x1 x2 → P1 x0 x1 x2 → P2 x0 x1 x2 → P3 x0 x1 x2 → P4 x0 x1 x2 → P5 x0 x1 x2 → P6 x0 x1 x2 → P7 x0 x1 x2 → P8 x0 x1 x2 → ex9_3 ? ? ? ? ? ? ? ? ? ? ? ?
+.
+
+interpretation "multiple existental quantifier (9, 3)" 'Ex3 P0 P1 P2 P3 P4 P5 P6 P7 P8 = (ex9_3 ? ? ? P0 P1 P2 P3 P4 P5 P6 P7 P8).
+
<key name="objects">ground_2/xoa</key>
<key name="notations">ground_2/notation/xoa</key>
<key name="include">basics/pts.ma</key>
+ <key name="ex">5 1</key>
<key name="ex">5 7</key>
+ <key name="ex">9 3</key>
</section>
</helm_registry>
lemma ypred_inv_refl: ∀m:ynat. ↓m = m → m = 0 ∨ m = ∞.
* // #m #H lapply (yinj_inj … H) -H (**) (* destruct lemma needed *)
-/4 width=1 by pred_inv_refl, or_introl, eq_f/
+/4 width=1 by pred_inv_fix_sn, or_introl, eq_f/
qed-.
projects / helm.git / commitdiff