From a0b7db9844126ebcdf4b5dbb586514854cef5d93 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 17 Apr 2019 20:30:00 +0200 Subject: [PATCH] update in basic_2 + decidability of type inference + decidability of type checking --- .../lambdadelta/basic_2/dynamic/cnv_aaa.ma | 32 ++++++++++++++++ .../lambdadelta/basic_2/dynamic/cnv_cpcs.ma | 30 ++++++--------- .../lambdadelta/basic_2/dynamic/cnv_cpes.ma | 21 +++++++++- .../lambdadelta/basic_2/dynamic/cnv_eval.ma | 19 +++------- .../basic_2/dynamic/cnv_preserve.ma | 21 ---------- .../basic_2/dynamic/cnv_preserve_cpcs.ma | 38 +++++++++++++++++++ .../basic_2/dynamic/cnv_preserve_cpes.ma | 11 ------ .../lambdadelta/basic_2/dynamic/nta_eval.ma | 35 +++++++++++++++++ .../basic_2/dynamic/nta_preserve.ma | 10 +---- .../lambdadelta/basic_2/etc/nta/nta.etc | 3 ++ .../lambdadelta/basic_2/etc/nta/nta_1a.etc | 37 ++++++++++++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../lambdadelta/static_2/syntax/term.ma | 7 ++++ 13 files changed, 192 insertions(+), 76 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_1a.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma index cad9f2318..cb2f97f55 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_aaa.ma @@ -58,3 +58,35 @@ lemma cnv_fwd_cpms_total (a) (h) (n) (G) (L): elim (cnv_fwd_aaa … H) -H #A #HA /2 width=2 by cpms_total_aaa/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma cnv_inv_appl_SO (a) (h) (G) (L): + ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → + ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & + ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0. +* #h #G #L #V #T #H +elim (cnv_inv_appl … H) -H [ * [| #n ] | #n ] #p #W #U #Ha #HV #HT #HVW #HTU +[ elim (cnv_fwd_aaa … HT) #A #HA + elim (aaa_cpm_SO h … (ⓛ{p}W.U)) + [|*: /2 width=8 by cpms_aaa_conf/ ] #X #HU0 + elim (cpm_inv_abst1 … HU0) #W0 #U0 #HW0 #_ #H0 destruct + lapply (cpms_step_dx … HVW … HW0) -HVW -HW0 #HVW0 + lapply (cpms_step_dx … HTU … HU0) -HTU -HU0 #HTU0 + /2 width=7 by ex5_4_intro/ +| lapply (Ha ?) -Ha [ // ] #Ha + lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Ha #H destruct + /2 width=7 by ex5_4_intro/ +| @(ex5_4_intro … HV HT HVW HTU) #H destruct +] +qed-. + +lemma cnv_inv_appl_true (h) (G) (L): + ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] → + ∃∃p,W0,U0. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] & + ⦃G,L⦄ ⊢ V ➡*[1,h] W0 & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W0.U0. +#h #G #L #V #T #H +elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn +>Hn -n [| // ] #HV #HT #HVW #HTU +/2 width=5 by ex4_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma index ba4b824ce..ba65bce5b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpcs.ma @@ -12,27 +12,19 @@ (* *) (**************************************************************************) -include "basic_2/rt_equivalence/cpcs_cprs.ma". -include "basic_2/dynamic/cnv_preserve.ma". +include "basic_2/rt_computation/csx_aaa.ma". +include "basic_2/rt_equivalence/cpcs_csx.ma". +include "basic_2/dynamic/cnv_aaa.ma". (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) -(* Forward lemmas with r-equivalence ****************************************) +(* Properties with r-equivalence ********************************************) -lemma cnv_cpms_conf_eq (a) (h) (n) (G) (L): - ∀T. ⦃G,L⦄ ⊢ T ![a,h] → - ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2. -#a #h #n #G #L #T #HT #T1 #HT1 #T2 #HT2 -elim (cnv_cpms_conf … HT … HT1 … HT2) -T Hn -n [| // ] #HV #HT #HVW #HTU +/2 width=5 by ex4_3_intro/ +qed-. + lemma cnv_inv_cast_cpes (a) (h) (G) (L): ∀U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] → ∧∧ ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & ⦃G, L⦄ ⊢ U ⬌*[h,0,1] T. 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..2574f3703 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): @@ -66,8 +59,7 @@ theorem cnv_dec (a) (h) (G) (L) (T): [ elim HTU -HTU #HTU #_ /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_inv_appl_true_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 +68,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_true_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/ @@ -90,7 +81,7 @@ theorem cnv_dec (a) (h) (G) (L) (T): [ 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_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 +91,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 +101,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 diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma index 297a86498..483ea690e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve.ma @@ -73,24 +73,3 @@ lemma cnv_lprs_trans (a) (h) (G): #a #h #G #L1 #T #HT #L2 #H @(lprs_ind_dx … H) -L2 /2 width=3 by cnv_lpr_trans/ qed-. - -(* Advanced inversion lemmas ************************************************) - -lemma cnv_inv_appl_SO (a) (h) (G) (L): - ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] → - ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] & - ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0. -* #h #G #L #V #T #H -elim (cnv_inv_appl … H) -H [ * [| #n ] | #n ] #p #W #U #Ha #HV #HT #HVW #HTU -[ elim (cnv_fwd_cpm_SO … (ⓛ{p}W.U)) - [|*: /2 width=8 by cnv_cpms_trans/ ] #X #HU0 - elim (cpm_inv_abst1 … HU0) #W0 #U0 #HW0 #_ #H0 destruct - lapply (cpms_step_dx … HVW … HW0) -HVW -HW0 #HVW0 - lapply (cpms_step_dx … HTU … HU0) -HTU -HU0 #HTU0 - /2 width=7 by ex5_4_intro/ -| lapply (Ha ?) -Ha [ // ] #Ha - lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Ha #H destruct - /2 width=7 by ex5_4_intro/ -| @(ex5_4_intro … HV HT HVW HTU) #H destruct -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma new file mode 100644 index 000000000..ba4b824ce --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpcs.ma @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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_equivalence/cpcs_cprs.ma". +include "basic_2/dynamic/cnv_preserve.ma". + +(* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************) + +(* Forward lemmas with r-equivalence ****************************************) + +lemma cnv_cpms_conf_eq (a) (h) (n) (G) (L): + ∀T. ⦃G,L⦄ ⊢ T ![a,h] → + ∀T1. ⦃G,L⦄ ⊢ T ➡*[n,h] T1 → ∀T2. ⦃G,L⦄ ⊢ T ➡*[n,h] T2 → ⦃G,L⦄ ⊢ T1 ⬌*[h] T2. +#a #h #n #G #L #T #HT #T1 #HT1 #T2 #HT2 +elim (cnv_cpms_conf … HT … HT1 … HT2) -T + (e:?; u:?; d:?) (getl d c (CHead e (Bind Void) u)) -> + (a:?) (drop (1) d c a) -> + (EX y1 y2 | t1 = (lift (1) d y1) & + t2 = (lift (1) d y2) & + (ty3 g a y1 y2) + ). + +Lemma ty3_gen_appl_nf2: (g:?; c:?; w,v,x:?) (ty3 g c (THead (Flat Appl) w v) x) -> + (EX u t | (pc3 c (THead (Flat Appl) w (THead (Bind Abst) u t)) x) & + (ty3 g c v (THead (Bind Abst) u t)) & + (ty3 g c w u) & + (nf2 c (THead (Bind Abst) u t)) + ). + +Lemma ty3_arity: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) -> + (EX a1 | (arity g c t1 a1) & + (arity g c t2 (asucc g a1)) + ). + +Lemma ty3_acyclic: (g:?; c:?; t,u:?) + (ty3 g c t u) -> (pc3 c u t) -> (P:Prop) P. + +Theorem pc3_abst_dec: (g:?; c:?; u1,t1:?) (ty3 g c u1 t1) -> + (u2,t2:?) (ty3 g c u2 t2) -> + (EX u v2 | (pc3 c u1 (THead (Bind Abst) u2 u)) & + (ty3 g c (THead (Bind Abst) v2 u) t1) & + (pr3 c u2 v2) & (nf2 c v2) + ) \/ + ((u:?) (pc3 c u1 (THead (Bind Abst) u2 u)) -> False). + +file ty3_nf2_gen + +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index efbca8468..a97c0a360 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -20,12 +20,12 @@ table { class "magenta" [ { "dynamic typing" * } { [ { "context-sensitive native type assignment" * } { - [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" * ] + [ [ "for terms" ] "nta" + "( ⦃?,?⦄ ⊢ ? :[?,?] ? )" + "( ⦃?,?⦄ ⊢ ? :[?] ? )" + "( ⦃?,?⦄ ⊢ ? :*[?] ? )" "nta_drops" + "nta_aaa" + "nta_fsb" + "nta_cpms" + "nta_cpcs" + "nta_preserve" + "nta_preserve_cpcs" + "nta_ind" + "nta_eval" * ] } ] [ { "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_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpue" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" * ] + [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" + "( ⦃?,?⦄ ⊢ ? ![?] )" + "( ⦃?,?⦄ ⊢ ? !*[?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" + "cnv_cpm_conf" + "cnv_cpm_tdeq" + "cnv_cpm_tdeq_trans" + "cnv_cpm_tdeq_conf" + "cnv_cpms_tdeq" + "cnv_cpms_conf" + "cnv_cpms_tdeq_conf" + "cnv_cpme" + "cnv_cpue" + "cnv_eval" + "cnv_cpes" + "cnv_cpcs" + "cnv_preserve_sub" + "cnv_preserve" + "cnv_preserve_cpes" + "cnv_preserve_cpcs" * ] } ] } diff --git a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma index 93cce0ffc..b0fc86df3 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma +++ b/matita/matita/contribs/lambdadelta/static_2/syntax/term.ma @@ -92,6 +92,13 @@ interpretation "native type annotation (term)" (* Basic properties *********************************************************) +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-. + (* Basic_1: was: term_dec *) lemma eq_term_dec: ∀T1,T2:term. Decidable (T1 = T2). #T1 elim T1 -T1 #I1 [| #V1 #T1 #IHV1 #IHT1 ] * #I2 [2,4: #V2 #T2 ] -- 2.39.2