X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv.ma;h=fe0b19cf370b71d7c6f8587959310226fa0b674b;hb=87f57ddc367303c33e19c83cd8989cd561f3185b;hp=398ef6783217fc4019e73a3502cc076048509685;hpb=1083ac3b1acac5f1ac1fa40a9a417dd9d268dced;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
index 398ef6783..fe0b19cf3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
@@ -12,19 +12,22 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "ground_2/ynat/ynat_lt.ma".
 include "basic_2/notation/relations/exclaim_5.ma".
+include "basic_2/notation/relations/exclaim_4.ma".
+include "basic_2/notation/relations/exclaimstar_4.ma".
 include "basic_2/rt_computation/cpms.ma".
 
 (* CONTEXT-SENSITIVE NATIVE VALIDITY FOR TERMS ******************************)
 
 (* activate genv *)
 (* Basic_2A1: uses: snv *)
-inductive cnv (a) (h): relation3 genv lenv term ≝
+inductive cnv (a:ynat) (h): relation3 genv lenv term ≝
 | cnv_sort: ∀G,L,s. cnv a h G L (⋆s)
 | cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0)
 | cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i)
 | cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T)
-| cnv_appl: ∀n,p,G,L,V,W0,T,U0. (a = Ⓣ → n ≤ 1) → cnv a h G L V → cnv a h G L T →
+| cnv_appl: ∀n,p,G,L,V,W0,T,U0. yinj n < a → cnv a h G L V → cnv a h G L T →
             ⦃G, L⦄ ⊢ V ➡*[1, h] W0 → ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0 → cnv a h G L (ⓐV.T)
 | cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T →
             ⦃G, L⦄ ⊢ U ➡*[h] U0 → ⦃G, L⦄ ⊢ T ➡*[1, h] U0 → cnv a h G L (ⓝU.T)
@@ -33,6 +36,12 @@ inductive cnv (a) (h): relation3 genv lenv term ≝
 interpretation "context-sensitive native validity (term)"
    'Exclaim a h G L T = (cnv a h G L T).
 
+interpretation "context-sensitive restricted native validity (term)"
+   'Exclaim h G L T = (cnv (yinj (S (S O))) h G L T).
+
+interpretation "context-sensitive extended native validity (term)"
+   'ExclaimStar h G L T = (cnv Y h G L T).
+
 (* Basic inversion lemmas ***************************************************)
 
 fact cnv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → X = #0 →
@@ -103,7 +112,7 @@ lemma cnv_inv_bind (a) (h): ∀p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T ![a, h] 
 /2 width=4 by cnv_inv_bind_aux/ qed-.
 
 fact cnv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀V,T. X = ⓐV.T →
-                               ∃∃n,p,W0,U0. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+                               ∃∃n,p,W0,U0. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
                                             ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
 #a #h #G #L #X * -L -X
 [ #G #L #s #X1 #X2 #H destruct
@@ -117,7 +126,7 @@ qed-.
 
 (* Basic_2A1: uses: snv_inv_appl *)
 lemma cnv_inv_appl (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] &
+                            ∃∃n,p,W0,U0. yinj n < a & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
                                          ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
 /2 width=3 by cnv_inv_appl_aux/ qed-.
 
@@ -139,3 +148,26 @@ lemma cnv_inv_cast (a) (h): ∀G,L,U,T. ⦃G, L⦄ ⊢ ⓝU.T ![a, h] →
                             ∃∃U0. ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
                                   ⦃G, L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[1, h] U0.
 /2 width=3 by cnv_inv_cast_aux/ qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma cnv_fwd_flat (a) (h) (I) (G) (L):
+                   ∀V,T. ⦃G, L⦄ ⊢ ⓕ{I}V.T ![a,h] →
+                   ∧∧ ⦃G, L⦄ ⊢ V ![a,h] & ⦃G, L⦄ ⊢ T ![a,h].
+#a #h * #G #L #V #T #H
+[ elim (cnv_inv_appl … H) #n #p #W #U #_ #HV #HT #_ #_
+| elim (cnv_inv_cast … H) #U #HV #HT #_ #_
+] -H /2 width=1 by conj/
+qed-.
+
+lemma cnv_fwd_pair_sn (a) (h) (I) (G) (L):
+      ∀V,T. ⦃G,L⦄ ⊢ ②{I}V.T ![a,h] → ⦃G,L⦄ ⊢ V ![a,h].
+#a #h * [ #p ] #I #G #L #V #T #H
+[ elim (cnv_inv_bind … H) -H #HV #_
+| elim (cnv_fwd_flat … H) -H #HV #_
+] //
+qed-.
+
+(* Basic_2A1: removed theorems 3:
+              shnv_cast shnv_inv_cast snv_shnv_cast
+*)