X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fdynamic%2Fcnv.ma;h=256b798b50a2c1694874654586e618844e95aa22;hb=bd53c4e895203eb049e75434f638f26b5a161a2b;hp=fe0b19cf370b71d7c6f8587959310226fa0b674b;hpb=87f57ddc367303c33e19c83cd8989cd561f3185b;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 fe0b19cf3..256b798b5 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
@@ -12,41 +12,35 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/ynat/ynat_lt.ma".
+include "ground_2/xoa/ex_2_3.ma".
+include "static_2/syntax/ac.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: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. 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)
+inductive cnv (h) (a): relation3 genv lenv term ≝
+| cnv_sort: ∀G,L,s. cnv h a G L (⋆s)
+| cnv_zero: ∀I,G,K,V. cnv h a G K V → cnv h a G (K.ⓑ[I]V) (#0)
+| cnv_lref: ∀I,G,K,i. cnv h a G K (#i) → cnv h a G (K.ⓘ[I]) (#↑i)
+| cnv_bind: ∀p,I,G,L,V,T. cnv h a G L V → cnv h a G (L.ⓑ[I]V) T → cnv h a G L (ⓑ[p,I]V.T)
+| cnv_appl: ∀n,p,G,L,V,W0,T,U0. ad a n → cnv h a G L V → cnv h a G L T →
+            ❪G,L❫ ⊢ V ➡*[1,h] W0 → ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[p]W0.U0 → cnv h a G L (ⓐV.T)
+| cnv_cast: ∀G,L,U,T,U0. cnv h a G L U → cnv h a G L T →
+            ❪G,L❫ ⊢ U ➡*[h] U0 → ❪G,L❫ ⊢ T ➡*[1,h] U0 → cnv h a G L (ⓝU.T)
 .
 
 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).
+  'Exclaim h a G L T = (cnv h a G L T).
 
 (* Basic inversion lemmas ***************************************************)
 
-fact cnv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → X = #0 →
-                               ∃∃I,K,V. ⦃G, K⦄ ⊢ V ![a, h] & L = K.ⓑ{I}V.
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_zero_aux (h) (a):
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → X = #0 →
+     ∃∃I,K,V. ❪G,K❫ ⊢ V ![h,a] & L = K.ⓑ[I]V.
+#h #a #G #L #X * -G -L -X
 [ #G #L #s #H destruct
 | #I #G #K #V #HV #_ /2 width=5 by ex2_3_intro/
 | #I #G #K #i #_ #H destruct
@@ -56,13 +50,15 @@ fact cnv_inv_zero_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → X = #0 →
 ]
 qed-.
 
-lemma cnv_inv_zero (a) (h): ∀G,L. ⦃G, L⦄ ⊢ #0 ![a, h] →
-                            ∃∃I,K,V. ⦃G, K⦄ ⊢ V ![a, h] & L = K.ⓑ{I}V.
+lemma cnv_inv_zero (h) (a):
+      ∀G,L. ❪G,L❫ ⊢ #0 ![h,a] →
+      ∃∃I,K,V. ❪G,K❫ ⊢ V ![h,a] & L = K.ⓑ[I]V.
 /2 width=3 by cnv_inv_zero_aux/ qed-.
 
-fact cnv_inv_lref_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀i. X = #(↑i) →
-                              ∃∃I,K. ⦃G, K⦄ ⊢ #i ![a, h] & L = K.ⓘ{I}.
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_lref_aux (h) (a):
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀i. X = #(↑i) →
+     ∃∃I,K. ❪G,K❫ ⊢ #i ![h,a] & L = K.ⓘ[I].
+#h #a #G #L #X * -G -L -X
 [ #G #L #s #j #H destruct
 | #I #G #K #V #_ #j #H destruct
 | #I #G #L #i #Hi #j #H destruct /2 width=4 by ex2_2_intro/
@@ -72,12 +68,13 @@ fact cnv_inv_lref_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀i. X =
 ]
 qed-.
 
-lemma cnv_inv_lref (a) (h): ∀G,L,i. ⦃G, L⦄ ⊢ #↑i ![a, h] →
-                            ∃∃I,K. ⦃G, K⦄ ⊢ #i ![a, h] & L = K.ⓘ{I}.
+lemma cnv_inv_lref (h) (a):
+      ∀G,L,i. ❪G,L❫ ⊢ #↑i ![h,a] →
+      ∃∃I,K. ❪G,K❫ ⊢ #i ![h,a] & L = K.ⓘ[I].
 /2 width=3 by cnv_inv_lref_aux/ qed-.
 
-fact cnv_inv_gref_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀l. X = §l → ⊥.
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_gref_aux (h) (a): ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀l. X = §l → ⊥.
+#h #a #G #L #X * -G -L -X
 [ #G #L #s #l #H destruct
 | #I #G #K #V #_ #l #H destruct
 | #I #G #K #i #_ #l #H destruct
@@ -88,14 +85,14 @@ fact cnv_inv_gref_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀l. X =
 qed-.
 
 (* Basic_2A1: uses: snv_inv_gref *)
-lemma cnv_inv_gref (a) (h): ∀G,L,l. ⦃G, L⦄ ⊢ §l ![a, h] → ⊥.
+lemma cnv_inv_gref (h) (a): ∀G,L,l. ❪G,L❫ ⊢ §l ![h,a] → ⊥.
 /2 width=8 by cnv_inv_gref_aux/ qed-.
 
-fact cnv_inv_bind_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] →
-                               ∀p,I,V,T. X = ⓑ{p,I}V.T →
-                               ∧∧ ⦃G, L⦄ ⊢ V ![a, h]
-                                & ⦃G, L.ⓑ{I}V⦄ ⊢ T ![a, h].
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_bind_aux (h) (a):
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] →
+     ∀p,I,V,T. X = ⓑ[p,I]V.T →
+     ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L.ⓑ[I]V❫ ⊢ T ![h,a].
+#h #a #G #L #X * -G -L -X
 [ #G #L #s #q #Z #X1 #X2 #H destruct
 | #I #G #K #V #_ #q #Z #X1 #X2 #H destruct
 | #I #G #K #i #_ #q #Z #X1 #X2 #H destruct
@@ -106,15 +103,16 @@ fact cnv_inv_bind_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] →
 qed-.
 
 (* Basic_2A1: uses: snv_inv_bind *)
-lemma cnv_inv_bind (a) (h): ∀p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T ![a, h] →
-                            ∧∧ ⦃G, L⦄ ⊢ V ![a, h]
-                             & ⦃G, L.ⓑ{I}V⦄ ⊢ T ![a, h].
+lemma cnv_inv_bind (h) (a):
+      ∀p,I,G,L,V,T. ❪G,L❫ ⊢ ⓑ[p,I]V.T ![h,a] →
+      ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L.ⓑ[I]V❫ ⊢ T ![h,a].
 /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. 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
+fact cnv_inv_appl_aux (h) (a):
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀V,T. X = ⓐV.T →
+     ∃∃n,p,W0,U0. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+                  ❪G,L❫ ⊢ V ➡*[1,h] W0 & ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[p]W0.U0.
+#h #a #G #L #X * -L -X
 [ #G #L #s #X1 #X2 #H destruct
 | #I #G #K #V #_ #X1 #X2 #H destruct
 | #I #G #K #i #_ #X1 #X2 #H destruct
@@ -125,15 +123,17 @@ fact cnv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀V,T. X
 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. 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.
+lemma cnv_inv_appl (h) (a):
+      ∀G,L,V,T. ❪G,L❫ ⊢ ⓐV.T ![h,a] →
+      ∃∃n,p,W0,U0. ad a n & ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+                   ❪G,L❫ ⊢ V ➡*[1,h] W0 & ❪G,L❫ ⊢ T ➡*[n,h] ⓛ[p]W0.U0.
 /2 width=3 by cnv_inv_appl_aux/ qed-.
 
-fact cnv_inv_cast_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀U,T. X = ⓝU.T →
-                               ∃∃U0. ⦃G, L⦄ ⊢ U ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
-                                     ⦃G, L⦄ ⊢ U ➡*[h] U0 & ⦃G, L⦄ ⊢ T ➡*[1, h] U0.
-#a #h #G #L #X * -G -L -X
+fact cnv_inv_cast_aux (h) (a):
+     ∀G,L,X. ❪G,L❫ ⊢ X ![h,a] → ∀U,T. X = ⓝU.T →
+     ∃∃U0. ❪G,L❫ ⊢ U ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+           ❪G,L❫ ⊢ U ➡*[h] U0 & ❪G,L❫ ⊢ T ➡*[1,h] U0.
+#h #a #G #L #X * -G -L -X
 [ #G #L #s #X1 #X2 #H destruct
 | #I #G #K #V #_ #X1 #X2 #H destruct
 | #I #G #K #i #_ #X1 #X2 #H destruct
@@ -143,26 +143,27 @@ fact cnv_inv_cast_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀U,T. X
 ]
 qed-.
 
-(* Basic_2A1: uses: snv_inv_appl *)
-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.
+(* Basic_2A1: uses: snv_inv_cast *)
+lemma cnv_inv_cast (h) (a):
+      ∀G,L,U,T. ❪G,L❫ ⊢ ⓝU.T ![h,a] →
+      ∃∃U0. ❪G,L❫ ⊢ U ![h,a] & ❪G,L❫ ⊢ T ![h,a] &
+            ❪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
+lemma cnv_fwd_flat (h) (a) (I) (G) (L):
+      ∀V,T. ❪G,L❫ ⊢ ⓕ[I]V.T ![h,a] →
+      ∧∧ ❪G,L❫ ⊢ V ![h,a] & ❪G,L❫ ⊢ T ![h,a].
+#h #a * #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
+lemma cnv_fwd_pair_sn (h) (a) (I) (G) (L):
+      ∀V,T. ❪G,L❫ ⊢ ②[I]V.T ![h,a] → ❪G,L❫ ⊢ V ![h,a].
+#h #a * [ #p ] #I #G #L #V #T #H
 [ elim (cnv_inv_bind … H) -H #HV #_
 | elim (cnv_fwd_flat … H) -H #HV #_
 ] //