X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_eval.ma;h=7dc23b79a183afca7908cdc2536b6adf6770dbce;hb=87f57ddc367303c33e19c83cd8989cd561f3185b;hp=0052d7cb47b46644efe8497f9127f1407d9b4237;hpb=31be09cc0d040577917783e050e1d38c0daa8f01;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma index 0052d7cb4..7dc23b79a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma @@ -20,13 +20,6 @@ include "basic_2/dynamic/cnv_preserve_cpes.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -lemma abst_dec (X): ∨∨ ∃∃p,W,T. X = ⓛ{p}W.T - | (∀p,W,T. X = ⓛ{p}W.T → ⊥). -* [ #I | * [ #p * | #I ] #V #T ] -[3: /3 width=4 by ex1_3_intro, or_introl/ ] -@or_intror #q #W #U #H destruct -qed-. - (* main properties with evaluations for rt-transition on terms **************) theorem cnv_dec (a) (h) (G) (L) (T): @@ -57,17 +50,19 @@ theorem cnv_dec (a) (h) (G) (L) (T): | #V #T #HG #HL #HT destruct elim (IH G L V) [| -IH #HV | // ] [ elim (IH G L T) -IH [| #HT #HV | // ] - [ cases a #HT #HV - [ elim (cnv_fwd_aaa … HT) #A #HA - elim (cpme_total_aaa h 1 … HA) #X + [ cases a -a [ * [| #a ]] #HT #HV + [ @or_intror #H + elim (cnv_inv_appl … H) -H #n #p #W #U #H #_ #_ #_ #_ + /3 width=2 by lt_zero_false, ylt_inv_inj/ + | elim (cnv_fwd_aaa … HT) #A #HA + elim (cpme_total_aaa h a … HA) #X elim (abst_dec X) [ * ] [ #p #W #U #H #HTU destruct elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ] [ elim HTU -HTU #HTU #_ - /3 width=7 by cnv_appl_cpes, or_introl/ + /4 width=7 by ylt_inj, cnv_appl_cpes, or_introl/ | @or_intror #H - elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #Hm1 #_ #_ #HVW0 - >Hm1 -m1 [| // ] #HTU0 + elim (cnv_inv_appl_pred_cpes … H) -H #q #W0 #U0 #_ #_ #HVW0 #HTU0 elim (cnv_cpme_cpms_conf … HT … HTU0 … HTU) -T #HU0 #_ elim (cpms_inv_abst_bi … HU0) -HU0 #_ #HW0 #_ -p -q -U0 /3 width=3 by cpes_cprs_trans/ @@ -76,8 +71,7 @@ theorem cnv_dec (a) (h) (G) (L) (T): ] | #HnTU #HTX @or_intror #H - elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #Hm1 #_ #_ #_ - >Hm1 -m1 [| // ] #HTU0 + elim (cnv_inv_appl_pred_cpes … H) -H #q #W0 #U0 #_ #_ #_ #HTU0 elim (cnv_cpme_cpms_conf … HT … HTU0 … HTX) -T #HX #_ elim (cpms_inv_abst_sn … HX) -HX #V0 #T0 #_ #_ #H destruct -W0 -U0 /2 width=4 by/ @@ -88,9 +82,9 @@ theorem cnv_dec (a) (h) (G) (L) (T): [ #p #W #U #H #HTU destruct elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ] [ elim HTU -HTU #n #HTU #_ - @or_introl @(cnv_appl_cpes … HV … HT … HVW … HTU) #H destruct + /3 width=7 by cnv_appl_cpes, or_introl/ | @or_intror #H - elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #HVW0 #HTU0 + elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #HVW0 #HTU0 elim (cnv_cpue_cpms_conf … HT … HTU0 … HTU) -m1 -T #X * #m2 #HU0X #_ #HUX elim (tueq_inv_bind1 … HUX) -HUX #X0 #_ #H destruct -U elim (cpms_inv_abst_bi … HU0X) -HU0X #_ #HW0 #_ -p -q -m2 -U0 -X0 @@ -100,7 +94,7 @@ theorem cnv_dec (a) (h) (G) (L) (T): ] | #HnTU #HTX @or_intror #H - elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #_ #HTU0 + elim (cnv_inv_appl_cpes … H) -H #m1 #q #W0 #U0 #_ #_ #_ #_ #HTU0 elim (cnv_cpue_cpms_conf … HT … HTU0 … HTX) -m1 -T #X0 * #m2 #HUX0 #_ #HX0 elim (cpms_inv_abst_sn … HUX0) -HUX0 #V0 #T0 #_ #_ #H destruct -m2 -W0 -U0 elim (tueq_inv_bind2 … HX0) -HX0 #X0 #_ #H destruct @@ -110,7 +104,7 @@ theorem cnv_dec (a) (h) (G) (L) (T): ] ] @or_intror #H - elim (cnv_inv_appl_SO … H) -H /2 width=1 by/ + elim (cnv_inv_appl … H) -H /2 width=1 by/ | #U #T #HG #HL #HT destruct elim (IH G L U) [| -IH | // ] #HU [ elim (IH G L T) -IH [3: // ] #HT