X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frt_conversion%2Fcpce.ma;h=3da6a15983bd05a8893b04f7f5d01cf76e30128c;hb=6b4da5fa47d474dcf2f203ec7f5ed36938739c9b;hp=b9d1625300acb3ef26fcb012da7c14f7b5db1035;hpb=3c6ff3987c3cc5e2df03fb76d07697c28c89c0a8;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma
index b9d162530..3da6a1598 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-include "ground_2/xoa/ex_2_4.ma".
+include "ground_2/xoa/ex_5_7.ma".
 include "basic_2/notation/relations/pconveta_5.ma".
 include "basic_2/rt_computation/cpms.ma".
 
@@ -21,13 +21,14 @@ include "basic_2/rt_computation/cpms.ma".
 (* avtivate genv *)
 inductive cpce (h): relation4 genv lenv term term ≝
 | cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s)
-| cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0)
-| cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s →
-             cpce h G (K.ⓛV) (#0) (#0)
-| cpce_eta : ∀n,p,G,K,V,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T →
-             cpce h G (K.ⓛV) (#0) (+ⓛW.ⓐ#0.#1)
+| cpce_atom: ∀G,i. cpce h G (⋆) (#i) (#i)
+| cpce_zero: ∀G,K,I. (∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
+             cpce h G (K.ⓘ{I}) (#0) (#0)
+| cpce_eta : ∀n,p,G,K,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
+             cpce h G K V1 V2 → ⬆*[1] V2 ≘ W2 → cpce h G (K.ⓛW) (#0) (+ⓛW2.ⓐ#0.#1)
 | cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
              ⬆*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U
+| cpce_gref: ∀G,L,l. cpce h G L (§l) (§l)
 | cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
              cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
              cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
@@ -37,8 +38,8 @@ inductive cpce (h): relation4 genv lenv term term ≝
 .
 
 interpretation
-   "context-sensitive parallel eta-conversion (term)"
-   'PConvEta h G L T1 T2 = (cpce h G L T1 T2).
+  "context-sensitive parallel eta-conversion (term)"
+  'PConvEta h G L T1 T2 = (cpce h G L T1 T2).
 
 (* Basic inversion lemmas ***************************************************)
 
@@ -47,44 +48,48 @@ lemma cpce_inv_sort_sn (h) (G) (L) (X2):
 #h #G #Y #X2 #s0
 @(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2
 [ #G #L #s #_ //
-| #G #K #V #_ //
-| #n #G #K #V #s #_ #_ //
-| #n #p #G #K #V #W #T #_ #H destruct
+| #G #i #_ //
+| #G #K #I #_ #_ //
+| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
 | #I #G #K #T #U #i #_ #_ #H destruct
+| #G #L #l #_ //
 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 ]
 qed-.
 
-lemma cpce_inv_ldef_sn (h) (G) (K) (X2):
-      ∀V. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
-#h #G #Y #X2 #X
-@(insert_eq_0 … (Y.ⓓX)) #Y1
-@(insert_eq_0 … (#0)) #X1
-* -G -Y1 -X1 -X2
+lemma cpce_inv_atom_sn (h) (G) (X2):
+      ∀i. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2.
+#h #G #X2 #j
+@(insert_eq_0 … LAtom) #Y
+@(insert_eq_0 … (#j)) #X1
+* -G -Y -X1 -X2
 [ #G #L #s #_ #_ //
-| #G #K #V #_ #_ //
-| #n #G #K #V #s #_ #_ #_ //
-| #n #p #G #K #V #W #T #_ #_ #H destruct
-| #I #G #K #T #U #i #_ #_ #H #_ destruct
+| #G #i #_ #_ //
+| #G #K #I #_ #_ #_ //
+| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #_ #H destruct
+| #G #L #l #_ #_ //
 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 ]
 qed-.
 
-lemma cpce_inv_ldec_sn (h) (G) (K) (X2):
-      ∀V. ⦃G,K.ⓛV⦄ ⊢ #0 ⬌η[h] X2 →
-      ∨∨ ∃∃n,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s & #0 = X2
-       | ∃∃n,p,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T & +ⓛW.ⓐ#0.#1 = X2.
-#h #G #Y #X2 #X
-@(insert_eq_0 … (Y.ⓛX)) #Y1
+lemma cpce_inv_zero_sn (h) (G) (K) (X2):
+      ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #0 ⬌η[h] X2 →
+      ∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2
+       | ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2
+                           & ⬆*[1] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#1 = X2.
+#h #G #Y0 #X2 #Z
+@(insert_eq_0 … (Y0.ⓘ{Z})) #Y
 @(insert_eq_0 … (#0)) #X1
-* -G -Y1 -X1 -X2
+* -G -Y -X1 -X2
 [ #G #L #s #H #_ destruct
-| #G #K #V #_ #H destruct
-| #n #G #K #V #s #HV #_ #H destruct /3 width=3 by ex2_2_intro, or_introl/
-| #n #p #G #K #V #W #T #HV #_ #H destruct /3 width=6 by or_intror, ex2_4_intro/
+| #G #i #_ #H destruct
+| #G #K #I #HI #_ #H destruct /4 width=7 by or_introl, conj/
+| #n #p #G #K #W #V1 #V2 #W2 #U #HWU #HV12 #HVW2 #_ #H destruct /3 width=12 by or_intror, ex5_7_intro/
 | #I #G #K #T #U #i #_ #_ #H #_ destruct
+| #G #L #l #H #_ destruct
 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 ]
@@ -93,30 +98,47 @@ qed-.
 lemma cpce_inv_lref_sn (h) (G) (K) (X2):
       ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
       ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⬆*[1] T2 ≘ X2.
-#h #G #Y #X2 #Z #j
-@(insert_eq_0 … (Y.ⓘ{Z})) #Y1
+#h #G #Y0 #X2 #Z #j
+@(insert_eq_0 … (Y0.ⓘ{Z})) #Y
 @(insert_eq_0 … (#↑j)) #X1
-* -G -Y1 -X1 -X2
+* -G -Y -X1 -X2
 [ #G #L #s #H #_ destruct
-| #G #K #V #H #_ destruct
-| #n #G #K #V #s #_ #H #_ destruct
-| #n #p #G #K #V #W #T #_ #H #_ destruct
+| #G #i #_ #H destruct
+| #G #K #I #_ #H #_ destruct
+| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H #_ destruct
 | #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/
+| #G #L #l #H #_ destruct
 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 ]
 qed-.
 
+lemma cpce_inv_gref_sn (h) (G) (L) (X2):
+      ∀l. ⦃G,L⦄ ⊢ §l ⬌η[h] X2 → §l = X2.
+#h #G #Y #X2 #k
+@(insert_eq_0 … (§k)) #X1 * -G -Y -X1 -X2
+[ #G #L #s #_ //
+| #G #i #_ //
+| #G #K #I #_ #_ //
+| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
+| #I #G #K #T #U #i #_ #_ #H destruct
+| #G #L #l #_ //
+| #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
+| #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
+]
+qed-.
+
 lemma cpce_inv_bind_sn (h) (G) (K) (X2):
       ∀p,I,V1,T1. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 →
       ∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2.
 #h #G #Y #X2 #q #Z #U #X
 @(insert_eq_0 … (ⓑ{q,Z}U.X)) #X1 * -G -Y -X1 -X2
 [ #G #L #s #H destruct
-| #G #K #V #H destruct
-| #n #G #K #V #s #_ #H destruct
-| #n #p #G #K #V #W #T #_ #H destruct
+| #G #i #H destruct
+| #G #K #I #_ #H destruct
+| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
 | #I #G #K #T #U #i #_ #_ #H destruct
+| #G #L #l #H destruct
 | #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 ]
@@ -128,10 +150,11 @@ lemma cpce_inv_flat_sn (h) (G) (L) (X2):
 #h #G #Y #X2 #Z #U #X
 @(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2
 [ #G #L #s #H destruct
-| #G #K #V #H destruct
-| #n #G #K #V #s #_ #H destruct
-| #n #p #G #K #V #W #T #_ #H destruct
+| #G #i #H destruct
+| #G #K #I #_ #H destruct
+| #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
 | #I #G #K #T #U #i #_ #_ #H destruct
+| #G #L #l #H destruct
 | #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 | #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
 ]