update in basic_2

+ decidability of type inference
+ decidability of type checking

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 cad9f2318eb1f978613c2fd894441da4bd011dc3..cb2f97f5576fd60f04b8e2423aee028c5961280d 100644 (file)
--- 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-.
 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 ba4b824ced241b76dbdafca37c778f710bc191b4..ba65bce5b0eeea2b3b6e5614472a4bf7fdbac009 100644 (file)
--- 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 ******************************)
 
 
 (* 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 <minus_n_n #T #HT1 #HT2
-/2 width=3 by cprs_div/
-qed-.
-
-lemma cnv_cpms_fwd_appl_sn_decompose (a) (h) (G) (L):
-      ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → ∀n,X. ⦃G,L⦄ ⊢ ⓐV.T ➡*[n,h] X →
-      ∃∃U. ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X.
-#a #h #G #L #V #T #H0 #n #X #HX
-elim (cnv_inv_appl … H0) #m #p #W #U #_ #_ #HT #_ #_ -m -p -W -U
-elim (cnv_fwd_cpms_total … h n … HT) #U #HTU
-lapply (cpms_appl_dx … V V … HTU) [ // ] #H
-/3 width=8 by cnv_cpms_conf_eq, ex3_intro/
+lemma cnv_cpcs_dec (a) (h) (G) (L):
+      ∀T1. ⦃G,L⦄ ⊢ T1 ![a,h] → ∀T2. ⦃G,L⦄ ⊢ T2 ![a,h] →
+      Decidable … (⦃G,L⦄ ⊢ T1 ⬌*[h] T2).
+#a #h #G #L #T1 #HT1 #T2 #HT2
+elim (cnv_fwd_aaa … HT1) -HT1 #A1 #HA1
+elim (cnv_fwd_aaa … HT2) -HT2 #A2 #HA2
+/3 width=2 by csx_cpcs_dec, aaa_csx/

 qed-.
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
index c7da941590a5815b2a641d6ced968601c48e4405..3437d2629855bef48a42c12ceaa5a4729a4f1607 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpes.ma
@@ -14,7 +14,7 @@
 
 include "basic_2/rt_computation/cpms_cpms.ma".
 include "basic_2/rt_equivalence/cpes.ma".
 
 include "basic_2/rt_computation/cpms_cpms.ma".
 include "basic_2/rt_equivalence/cpes.ma".

-include "basic_2/dynamic/cnv.ma".
+include "basic_2/dynamic/cnv_aaa.ma".

 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
 
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
 


@@ -46,6 +46,25 @@ elim (cnv_inv_appl … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
 /3 width=7 by cpms_div, ex5_4_intro/
 qed-.
 
 /3 width=7 by cpms_div, ex5_4_intro/
 qed-.
 

+lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
+      ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
+      ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+                 ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
+#a #h #G #L #V #T #H
+elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
+/3 width=7 by cpms_div, ex5_4_intro/
+qed-.
+
+lemma cnv_inv_appl_true_cpes (h) (G) (L):
+      ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![h] →
+      ∃∃p,W,U. ⦃G,L⦄ ⊢ V ![h] & ⦃G,L⦄ ⊢ T ![h] &
+                 ⦃G,L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G,L⦄ ⊢ T ➡*[1,h] ⓛ{p}W.U.
+#h #G #L #V #T #H
+elim (cnv_inv_appl_SO_cpes … H) -H #n #p #W #U #Hn
+>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.
 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 0052d7cb47b46644efe8497f9127f1407d9b4237..2574f370393a4fa558a5e6275e3d56dbbe32dd22 100644 (file)
--- 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 ******************************)
 
 
 (* 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):
 (* 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 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/
             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
           ]
         | #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/
           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 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
             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
           ]
         | #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
           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
     ]
   ]
   @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
 | #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 297a86498220e60fbcbf38df9caecd7f8bbe5337..483ea690e474445d45732dfc15511d7b84143d40 100644 (file)
--- 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-.
 #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 (file)
index 0000000..ba4b824
--- /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 <minus_n_n #T #HT1 #HT2
+/2 width=3 by cprs_div/
+qed-.
+
+lemma cnv_cpms_fwd_appl_sn_decompose (a) (h) (G) (L):
+      ∀V,T. ⦃G,L⦄ ⊢ ⓐV.T ![a,h] → ∀n,X. ⦃G,L⦄ ⊢ ⓐV.T ➡*[n,h] X →
+      ∃∃U. ⦃G,L⦄ ⊢ T ![a,h] & ⦃G,L⦄ ⊢ T ➡*[n,h] U & ⦃G,L⦄ ⊢ ⓐV.U ⬌*[h] X.
+#a #h #G #L #V #T #H0 #n #X #HX
+elim (cnv_inv_appl … H0) #m #p #W #U #_ #_ #HT #_ #_ -m -p -W -U
+elim (cnv_fwd_cpms_total … h n … HT) #U #HTU
+lapply (cpms_appl_dx … V V … HTU) [ // ] #H
+/3 width=8 by cnv_cpms_conf_eq, ex3_intro/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma
index f266bb5813fe1ba8aa6dbf88a8ecb2d62d45dc23..60fc0d0daacff9da2c426afd9574dc8c580c9ed8 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_preserve_cpes.ma
@@ -39,14 +39,3 @@ elim (eq_term_dec U1 U2) [ #H destruct | #HnU12 ]
   /3 width=6 by cpre_mono/
 ]
 qed-.
   /3 width=6 by cpre_mono/
 ]
 qed-.

-
-(* Advanced inversion lemmas with t-bound rt-equivalence for terms **********)
-
-lemma cnv_inv_appl_SO_cpes (a) (h) (G) (L):
-      ∀V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
-      ∃∃n,p,W,U. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
-                 ⦃G, L⦄ ⊢ V ⬌*[h,1,0] W & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W.U.
-#a #h #G #L #V #T #H
-elim (cnv_inv_appl_SO … H) -H #n #p #W #U #Hn #HV #HT #HVW #HTU
-/3 width=7 by cpms_div, ex5_4_intro/
-qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma
new file mode 100644 (file)
index 0000000..ab9f1c4
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_eval.ma
@@ -0,0 +1,35 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/dynamic/cnv_eval.ma".
+include "basic_2/dynamic/nta_preserve.ma".
+
+(* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
+
+(* Properties with evaluations for rt-transition on terms *******************)
+
+lemma nta_typecheck_dec (a) (h) (G) (L):
+      ∀T,U. Decidable … (⦃G,L⦄ ⊢ T :[a,h] U).
+/2 width=1 by cnv_dec/ qed-.
+
+(* Basic_1: uses: ty3_inference *)
+lemma nta_inference_dec (a) (h) (G) (L) (T):
+      ∨∨ ∃U. ⦃G,L⦄ ⊢ T :[a,h] U
+       | ∀U. (⦃G,L⦄ ⊢ T :[a,h] U → ⊥).
+#a #h #G #L #T
+elim (cnv_dec a h G L T)
+[ /3 width=1 by cnv_nta_sn, or_introl/
+| /4 width=2 by nta_fwd_cnv_sn, or_intror/
+]
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
index 8d69b3ca21f7a2bc1246e88499586634eb6a363c..daf753fb366872d53b58eee1c8769676f5554780 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/nta_preserve.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/rt_equivalence/cpcs_cpcs.ma".
 (**************************************************************************)
 
 include "basic_2/rt_equivalence/cpcs_cpcs.ma".

-include "basic_2/dynamic/cnv_cpcs.ma".
+include "basic_2/dynamic/cnv_preserve_cpcs.ma".

 include "basic_2/dynamic/nta.ma".
 
 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)
 include "basic_2/dynamic/nta.ma".
 
 (* NATIVE TYPE ASSIGNMENT FOR TERMS *****************************************)


@@ -169,13 +169,7 @@ lemma nta_inv_appl_sn (h) (G) (L) (X2):
       ∃∃p,W,U. ⦃G,L⦄ ⊢ V :[h] W & ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h].
 #h #G #L #X2 #V #T #H
 elim (cnv_inv_cast … H) -H #X #HX2 #H1 #HX2 #H2
       ∃∃p,W,U. ⦃G,L⦄ ⊢ V :[h] W & ⦃G,L⦄ ⊢ T :[h] ⓛ{p}W.U & ⦃G,L⦄ ⊢ ⓐV.ⓛ{p}W.U ⬌*[h] X2 & ⦃G,L⦄ ⊢ X2 ![h].
 #h #G #L #X2 #V #T #H
 elim (cnv_inv_cast … H) -H #X #HX2 #H1 #HX2 #H2

-elim (cnv_inv_appl … H1) * [ | #n ] #p #W #U #Hn #HV #HT #HVW #HTU
-[ lapply (cnv_cpms_trans … HT … HTU) #H
-  elim (cnv_inv_bind … H) -H #_ #HU
-  elim (cnv_fwd_cpm_SO … HU) #U0 #HU0 -HU
-  lapply (cpms_step_dx … HTU 1 (ⓛ{p}W.U0) ?) -HTU [ /2 width=1 by cpm_bind/ ] #HTU
-| lapply (le_n_O_to_eq n ?) [ /3 width=1 by le_S_S_to_le/ ] -Hn #H destruct
-]
+elim (cnv_inv_appl_true … H1) #p #W #U #HV #HT #HVW #HTU

 /5 width=11 by cnv_cpms_nta, cnv_cpms_conf_eq, cpcs_cprs_div, cpms_appl_dx, ex4_3_intro/
 qed-.
 
 /5 width=11 by cnv_cpms_nta, cnv_cpms_conf_eq, cpcs_cprs_div, cpms_appl_dx, ex4_3_intro/
 qed-.
 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
index 166fd2105a13bd98cf1938e2ccc1a2470d3f3912..9d0831b470b2281e7058e91ed2dfd76f8fb77829 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta.etc
@@ -20,6 +20,9 @@ lemma nta_inv_lref_sn_drops
 (* Basic_1: uses: ty3_gen_abst_abst *)
 lemma nta_inv_abst_bi
 
 (* Basic_1: uses: ty3_gen_abst_abst *)
 lemma nta_inv_abst_bi
 

+(* Basic_1: uses: pc3_dec *)
+lemma nta_cpcs_dec
+

 (* Advanced properties ******************************************************)
 
 | ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U
 (* Advanced properties ******************************************************)
 
 | ntaa_cast: ∀L,T,U,W. ntaa h L T U → ntaa h L U W → ntaa h L (ⓝU. T) U

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_1a.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_1a.etc
new file mode 100644 (file)
index 0000000..e0ee809
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc/nta/nta_1a.etc
@@ -0,0 +1,37 @@
+(* FROM BASIC_1
+
+(* NOTE: This can be generalized removing the last premise *)
+      Lemma ty3_gen_cvoid: (g:?; c:?; t1,t2:?) (ty3 g c t1 t2) ->
+                           (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 efbca84686b94f283199a8f4e87c79a1cdf77cf2..a97c0a360c6bf2b383fe494d418a1566d4df82ec 100644 (file)
--- 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" * } {
    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" * ]
           }
         ]
         [ { "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 93cce0ffc42f2a142fddbf8217b4d215b68aa690..b0fc86df39784d2b617d14228c26adc45628c734 100644 (file)
--- 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 *********************************************************)
 
 
 (* 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 ]
 (* 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 ]