X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv_eval.ma;h=44bd544d711728108309b5eee903ad2b6b94d2ce;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;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..44bd544d7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_eval.ma @@ -12,30 +12,24 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/cpue_csx.ma". -include "basic_2/rt_equivalence/cpes_cprs.ma". -include "basic_2/dynamic/cnv_cpue.ma". +include "basic_2/rt_computation/cpmuwe_cpmuwe.ma". +include "basic_2/rt_equivalence/cpes_cpes.ma". +include "basic_2/dynamic/cnv_cpmuwe.ma". (**) (* should be included by the next *) +include "basic_2/dynamic/cnv_cpmuwe_cpmre.ma". include "basic_2/dynamic/cnv_cpes.ma". 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): - Decidable (⦃G,L⦄ ⊢ T ![a,h]). -#a #h #G #L #T +theorem cnv_dec (h) (a) (G) (L) (T): ac_props a → + Decidable (❪G,L❫ ⊢ T ![h,a]). +#h #a #G #L #T #Ha @(fqup_wf_ind_eq (Ⓣ) … G L T) -G -L -T #G0 #L0 #T0 #IH #G #L * * [|||| * ] -[ #s #HG #HL #HT destruct -IH +[ #s #HG #HL #HT destruct -Ha -IH /2 width=1 by cnv_sort, or_introl/ -| #i #HG #HL #HT destruct +| #i #HG #HL #HT destruct -Ha elim (drops_F_uni L i) [| * * ] [ /3 width=8 by cnv_inv_lref_atom, or_intror/ | /3 width=9 by cnv_inv_lref_unit, or_intror/ @@ -45,11 +39,11 @@ theorem cnv_dec (a) (h) (G) (L) (T): | /4 width=5 by cnv_inv_lref_pair, or_intror/ ] ] -| #l #HG #HL #HT destruct -IH +| #l #HG #HL #HT destruct -Ha -IH /3 width=6 by cnv_inv_gref, or_intror/ -| #p #I #V #T #HG #HL #HT destruct +| #p #I #V #T #HG #HL #HT destruct -Ha elim (IH G L V) [| -IH | // ] #HV - [ elim (IH G (L.ⓑ{I}V) T) -IH [3: // ] #HT + [ elim (IH G (L.ⓑ[I]V) T) -IH [3: // ] #HT [ /3 width=1 by cnv_bind, or_introl/ ] ] @or_intror #H @@ -57,60 +51,48 @@ 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 - elim (abst_dec X) [ * ] - [ #p #W #U #H #HTU destruct + [ #HT #HV + elim (cnv_R_cpmuwe_total … HT) #n #Hn + elim (dec_min (R_cpmuwe h G L T) … Hn) -Hn + [| /2 width=2 by cnv_R_cpmuwe_dec/ ] #n0 #_ -n + elim (ac_dec … Ha n0) -Ha + [ * #n #Ha #Hn * #X0 #HX0 #_ + elim (abst_dec X0) + [ * #p #W #U0 #H destruct elim (cnv_cpes_dec … 1 0 … HV W) [ #HVW | #HnVW ] - [ elim HTU -HTU #HTU #_ + [ lapply (cpmuwe_fwd_cpms … HX0) -HX0 #HTU0 + elim (cnv_fwd_cpms_abst_dx_le … HT … HTU0 … Hn) #U #HTU #_ -U0 -n0 /3 width=7 by 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_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/ - | lapply (cnv_cpme_trans … HT … HTU) -T #H - elim (cnv_inv_bind … H) -H #HW #_ // - ] - | #HnTU #HTX - @or_intror #H - elim (cnv_inv_appl_SO_cpes … H) -H #m1 #q #W0 #U0 #Hm1 #_ #_ #_ - >Hm1 -m1 [| // ] #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/ - ] - | elim (cpue_total_csx h G L T) - [| /3 width=2 by cnv_fwd_fsb, fsb_inv_csx/ ] #X - elim (abst_dec X) [ * ] - [ #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 - | @or_intror #H - elim (cnv_inv_appl_SO_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 - /3 width=3 by cpes_cprs_trans/ - | lapply (cnv_cpue_trans … HT … HTU) -T #H +(* Note: argument type mismatch *) + | @or_intror #H -n + elim (cnv_inv_appl_cpes … H) -H #m0 #q #WX #UX #_ #_ #_ #HVWX #HTUX + lapply (cpmuwe_abst … HTUX) -HTUX #HTUX + elim (cnv_cpmuwe_mono … HT … HTUX … HX0) -a -T #H #_ + elim (cpes_fwd_abst_bi … H) -H #_ #HWX -n0 -m0 -p -q -UX -U0 + /3 width=3 by cpes_cpes_trans/ + | lapply (cnv_cpmuwe_trans … HT … HX0) -T #H elim (cnv_inv_bind … H) -H #HW #_ // ] - | #HnTU #HTX +(* Note: no expected type *) + | #HnX0 @or_intror #H - elim (cnv_inv_appl_SO_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 + elim (cnv_inv_appl_cpes … H) -H #m0 #q #W0 #U0 #_ #_ #_ #_ #HTU0 + lapply (cpmuwe_abst … HTU0) -HTU0 #HTU0 + elim (cnv_cpmuwe_mono … HT … HTU0 … HX0) -T #_ #H + elim (tweq_inv_abst_sn … H) -W0 -U0 #W0 #U0 #H destruct /2 width=4 by/ ] +(* Note: failed applicability *) + | #Hge #_ #Hlt + @or_intror #H + elim (cnv_inv_appl … H) -H #m0 #q #W0 #U0 #Hm0 #_ #_ #_ #HTU0 + elim (lt_or_ge m0 n0) #H0 [| /3 width=3 by ex2_intro/ ] -Hm0 -Hge + /4 width=6 by cpmuwe_abst, ex_intro/ ] ] ] @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