Merge branch 'declarative' into matita-lablgtk3

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / rt_transition / cpm.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
index c8f746351252b275d6e2728642b8f3fe2adc824c..c069b4ca0e625ef09521d807d3266d1d63bc897a 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma
@@ -32,7 +32,7 @@ interpretation
 
 (* Basic properties *********************************************************)
 
-lemma cpm_ess: ∀h,G,L,s. ⦃G,L⦄ ⊢ ⋆s ➡[1,h] ⋆(next h s).
+lemma cpm_ess: ∀h,G,L,s. ⦃G,L⦄ ⊢ ⋆s ➡[1,h] ⋆(⫯[h]s).
 /2 width=3 by cpg_ess, ex2_intro/ qed.
 
 lemma cpm_delta: ∀n,h,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ➡[n,h] V2 →
@@ -131,7 +131,7 @@ qed.
 
 lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G,L⦄ ⊢ ⓪{J} ➡[n,h] T2 →
                      ∨∨ T2 = ⓪{J} ∧ n = 0
-                      | ∃∃s. T2 = ⋆(next h s) & J = Sort s & n = 1
+                      | ∃∃s. T2 = ⋆(⫯[h]s) & J = Sort s & n = 1
                       | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ➡[n,h] V2 & ⬆*[1] V2 ≘ T2 &
                                    L = K.ⓓV1 & J = LRef 0
                       | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ➡[m,h] V2 & ⬆*[1] V2 ≘ T2 &
@@ -175,6 +175,16 @@ lemma cpm_inv_zero1: ∀n,h,G,L,T2. ⦃G,L⦄ ⊢ #0 ➡[n,h] T2 →
 ]
 qed-.
 
+lemma cpm_inv_zero1_unit (n) (h) (I) (K) (G):
+      ∀X2. ⦃G,K.ⓤ{I}⦄ ⊢ #0 ➡[n,h] X2 → ∧∧ X2 = #0 & n = 0.
+#n #h #I #G #K #X2 #H
+elim (cpm_inv_zero1 … H) -H *
+[ #H1 #H2 destruct /2 width=1 by conj/
+| #Y #X1 #X2 #_ #_ #H destruct
+| #m #Y #X1 #X2 #_ #_ #H destruct
+]
+qed.
+
 lemma cpm_inv_lref1: ∀n,h,G,L,T2,i. ⦃G,L⦄ ⊢ #↑i ➡[n,h] T2 →
                      ∨∨ T2 = #(↑i) ∧ n = 0
                       | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ➡[n,h] T & ⬆*[1] T ≘ T2 & L = K.ⓘ{I}.
@@ -185,6 +195,21 @@ lemma cpm_inv_lref1: ∀n,h,G,L,T2,i. ⦃G,L⦄ ⊢ #↑i ➡[n,h] T2 →
 ]
 qed-.
 
+lemma cpm_inv_lref1_ctop (n) (h) (G):
+      ∀X2,i. ⦃G,⋆⦄ ⊢ #i ➡[n,h] X2 → ∧∧ X2 = #i & n = 0.
+#n #h #G #X2 * [| #i ] #H
+[ elim (cpm_inv_zero1 … H) -H *
+  [ #H1 #H2 destruct /2 width=1 by conj/
+  | #Y #X1 #X2 #_ #_ #H destruct
+  | #m #Y #X1 #X2 #_ #_ #H destruct
+  ]
+| elim (cpm_inv_lref1 … H) -H *
+  [ #H1 #H2 destruct /2 width=1 by conj/
+  | #Z #Y #X0 #_ #_ #H destruct
+  ]
+]
+qed.
+
 lemma cpm_inv_gref1: ∀n,h,G,L,T2,l. ⦃G,L⦄ ⊢ §l ➡[n,h] T2 → T2 = §l ∧ n = 0.
 #n #h #G #L #T2 #l * #c #Hc #H elim (cpg_inv_gref1 … H) -H
 #H1 #H2 destruct /3 width=1 by isrt_inv_00, conj/ 
@@ -304,7 +329,7 @@ qed-.
 
 lemma cpm_ind (h): ∀Q:relation5 nat genv lenv term term.
                    (∀I,G,L. Q 0 G L (⓪{I}) (⓪{I})) →
-                   (∀G,L,s. Q 1 G L (⋆s) (⋆(next h s))) →
+                   (∀G,L,s. Q 1 G L (⋆s) (⋆(⫯[h]s))) →
                    (∀n,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ➡[n,h] V2 → Q n G K V1 V2 →
                      ⬆*[1] V2 ≘ W2 → Q n G (K.ⓓV1) (#0) W2
                    ) → (∀n,G,K,V1,V2,W2. ⦃G,K⦄ ⊢ V1 ➡[n,h] V2 → Q n G K V1 V2 →