matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpce.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground_2/xoa/ex_2_4.ma".
  16 include "basic_2/notation/relations/pconveta_5.ma".
  17 include "basic_2/rt_computation/cpms.ma".
  18
  19 (* CONTEXT-SENSITIVE PARALLEL ETA-CONVERSION FOR TERMS **********************)
  20
  21 (* avtivate genv *)
  22 inductive cpce (h): relation4 genv lenv term term ≝
  23 | cpce_sort: ∀G,L,s. cpce h G L (⋆s) (⋆s)
  24 | cpce_ldef: ∀G,K,V. cpce h G (K.ⓓV) (#0) (#0)
  25 | cpce_ldec: ∀n,G,K,V,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s →
  26              cpce h G (K.ⓛV) (#0) (#0)
  27 | cpce_eta : ∀n,p,G,K,V,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T →
  28              cpce h G (K.ⓛV) (#0) (+ⓛW.ⓐ#0.#1)
  29 | cpce_lref: ∀I,G,K,T,U,i. cpce h G K (#i) T →
  30              ⬆*[1] T ≘ U → cpce h G (K.ⓘ{I}) (#↑i) U
  31 | cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
  32              cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
  33              cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
  34 | cpce_flat: ∀I,G,L,V1,V2,T1,T2.
  35              cpce h G L V1 V2 → cpce h G L T1 T2 →
  36              cpce h G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
  37 .
  38
  39 interpretation
  40    "context-sensitive parallel eta-conversion (term)"
  41    'PConvEta h G L T1 T2 = (cpce h G L T1 T2).
  42
  43 (* Basic inversion lemmas ***************************************************)
  44
  45 lemma cpce_inv_sort_sn (h) (G) (L) (X2):
  46       ∀s. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2.
  47 #h #G #Y #X2 #s0
  48 @(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2
  49 [ #G #L #s #_ //
  50 | #G #K #V #_ //
  51 | #n #G #K #V #s #_ #_ //
  52 | #n #p #G #K #V #W #T #_ #H destruct
  53 | #I #G #K #T #U #i #_ #_ #H destruct
  54 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
  55 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
  56 ]
  57 qed-.
  58
  59 lemma cpce_inv_ldef_sn (h) (G) (K) (X2):
  60       ∀V. ⦃G,K.ⓓV⦄ ⊢ #0 ⬌η[h] X2 → #0 = X2.
  61 #h #G #Y #X2 #X
  62 @(insert_eq_0 … (Y.ⓓX)) #Y1
  63 @(insert_eq_0 … (#0)) #X1
  64 * -G -Y1 -X1 -X2
  65 [ #G #L #s #_ #_ //
  66 | #G #K #V #_ #_ //
  67 | #n #G #K #V #s #_ #_ #_ //
  68 | #n #p #G #K #V #W #T #_ #_ #H destruct
  69 | #I #G #K #T #U #i #_ #_ #H #_ destruct
  70 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  71 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  72 ]
  73 qed-.
  74
  75 lemma cpce_inv_ldec_sn (h) (G) (K) (X2):
  76       ∀V. ⦃G,K.ⓛV⦄ ⊢ #0 ⬌η[h] X2 →
  77       ∨∨ ∃∃n,s. ⦃G,K⦄ ⊢ V ➡*[n,h] ⋆s & #0 = X2
  78        | ∃∃n,p,W,T. ⦃G,K⦄ ⊢ V ➡*[n,h] ⓛ{p}W.T & +ⓛW.ⓐ#0.#1 = X2.
  79 #h #G #Y #X2 #X
  80 @(insert_eq_0 … (Y.ⓛX)) #Y1
  81 @(insert_eq_0 … (#0)) #X1
  82 * -G -Y1 -X1 -X2
  83 [ #G #L #s #H #_ destruct
  84 | #G #K #V #_ #H destruct
  85 | #n #G #K #V #s #HV #_ #H destruct /3 width=3 by ex2_2_intro, or_introl/
  86 | #n #p #G #K #V #W #T #HV #_ #H destruct /3 width=6 by or_intror, ex2_4_intro/
  87 | #I #G #K #T #U #i #_ #_ #H #_ destruct
  88 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  89 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  90 ]
  91 qed-.
  92
  93 lemma cpce_inv_lref_sn (h) (G) (K) (X2):
  94       ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
  95       ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⬆*[1] T2 ≘ X2.
  96 #h #G #Y #X2 #Z #j
  97 @(insert_eq_0 … (Y.ⓘ{Z})) #Y1
  98 @(insert_eq_0 … (#↑j)) #X1
  99 * -G -Y1 -X1 -X2
 100 [ #G #L #s #H #_ destruct
 101 | #G #K #V #H #_ destruct
 102 | #n #G #K #V #s #_ #H #_ destruct
 103 | #n #p #G #K #V #W #T #_ #H #_ destruct
 104 | #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/
 105 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 106 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 107 ]
 108 qed-.
 109
 110 lemma cpce_inv_bind_sn (h) (G) (K) (X2):
 111       ∀p,I,V1,T1. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 →
 112       ∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2.
 113 #h #G #Y #X2 #q #Z #U #X
 114 @(insert_eq_0 … (ⓑ{q,Z}U.X)) #X1 * -G -Y -X1 -X2
 115 [ #G #L #s #H destruct
 116 | #G #K #V #H destruct
 117 | #n #G #K #V #s #_ #H destruct
 118 | #n #p #G #K #V #W #T #_ #H destruct
 119 | #I #G #K #T #U #i #_ #_ #H destruct
 120 | #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
 121 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 122 ]
 123 qed-.
 124
 125 lemma cpce_inv_flat_sn (h) (G) (L) (X2):
 126       ∀I,V1,T1. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 →
 127       ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,L⦄ ⊢ T1 ⬌η[h] T2 & ⓕ{I}V2.T2 = X2.
 128 #h #G #Y #X2 #Z #U #X
 129 @(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2
 130 [ #G #L #s #H destruct
 131 | #G #K #V #H destruct
 132 | #n #G #K #V #s #_ #H destruct
 133 | #n #p #G #K #V #W #T #_ #H destruct
 134 | #I #G #K #T #U #i #_ #_ #H destruct
 135 | #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 136 | #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
 137 ]
 138 qed-.