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_5_7.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_atom: ∀G,i. cpce h G (⋆) (#i) (#i)
  25 | cpce_zero: ∀G,K,I. (∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥) →
  26              cpce h G (K.ⓘ{I}) (#0) (#0)
  27 | cpce_eta : ∀n,p,G,K,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U →
  28              cpce h G K V1 V2 → ⬆*[1] V2 ≘ W2 → cpce h G (K.ⓛW) (#0) (+ⓛW2.ⓐ#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_gref: ∀G,L,l. cpce h G L (§l) (§l)
  32 | cpce_bind: ∀p,I,G,K,V1,V2,T1,T2.
  33              cpce h G K V1 V2 → cpce h G (K.ⓑ{I}V1) T1 T2 →
  34              cpce h G K (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2)
  35 | cpce_flat: ∀I,G,L,V1,V2,T1,T2.
  36              cpce h G L V1 V2 → cpce h G L T1 T2 →
  37              cpce h G L (ⓕ{I}V1.T1) (ⓕ{I}V2.T2)
  38 .
  39
  40 interpretation
  41   "context-sensitive parallel eta-conversion (term)"
  42   'PConvEta h G L T1 T2 = (cpce h G L T1 T2).
  43
  44 (* Basic inversion lemmas ***************************************************)
  45
  46 lemma cpce_inv_sort_sn (h) (G) (L) (X2):
  47       ∀s. ⦃G,L⦄ ⊢ ⋆s ⬌η[h] X2 → ⋆s = X2.
  48 #h #G #Y #X2 #s0
  49 @(insert_eq_0 … (⋆s0)) #X1 * -G -Y -X1 -X2
  50 [ #G #L #s #_ //
  51 | #G #i #_ //
  52 | #G #K #I #_ #_ //
  53 | #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
  54 | #I #G #K #T #U #i #_ #_ #H destruct
  55 | #G #L #l #_ //
  56 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
  57 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
  58 ]
  59 qed-.
  60
  61 lemma cpce_inv_atom_sn (h) (G) (X2):
  62       ∀i. ⦃G,⋆⦄ ⊢ #i ⬌η[h] X2 → #i = X2.
  63 #h #G #X2 #j
  64 @(insert_eq_0 … LAtom) #Y
  65 @(insert_eq_0 … (#j)) #X1
  66 * -G -Y -X1 -X2
  67 [ #G #L #s #_ #_ //
  68 | #G #i #_ #_ //
  69 | #G #K #I #_ #_ #_ //
  70 | #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #_ #H destruct
  71 | #I #G #K #T #U #i #_ #_ #_ #H destruct
  72 | #G #L #l #_ #_ //
  73 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  74 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  75 ]
  76 qed-.
  77
  78 lemma cpce_inv_zero_sn (h) (G) (K) (X2):
  79       ∀I. ⦃G,K.ⓘ{I}⦄ ⊢ #0 ⬌η[h] X2 →
  80       ∨∨ ∧∧ ∀n,p,W,V,U. I = BPair Abst W → ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V.U → ⊥ & #0 = X2
  81        | ∃∃n,p,W,V1,V2,W2,U. ⦃G,K⦄ ⊢ W ➡*[n,h] ⓛ{p}V1.U & ⦃G,K⦄ ⊢ V1 ⬌η[h] V2
  82                            & ⬆*[1] V2 ≘ W2 & I = BPair Abst W & +ⓛW2.ⓐ#0.#1 = X2.
  83 #h #G #Y0 #X2 #Z
  84 @(insert_eq_0 … (Y0.ⓘ{Z})) #Y
  85 @(insert_eq_0 … (#0)) #X1
  86 * -G -Y -X1 -X2
  87 [ #G #L #s #H #_ destruct
  88 | #G #i #_ #H destruct
  89 | #G #K #I #HI #_ #H destruct /4 width=7 by or_introl, conj/
  90 | #n #p #G #K #W #V1 #V2 #W2 #U #HWU #HV12 #HVW2 #_ #H destruct /3 width=12 by or_intror, ex5_7_intro/
  91 | #I #G #K #T #U #i #_ #_ #H #_ destruct
  92 | #G #L #l #H #_ destruct
  93 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  94 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
  95 ]
  96 qed-.
  97
  98 lemma cpce_inv_lref_sn (h) (G) (K) (X2):
  99       ∀I,i. ⦃G,K.ⓘ{I}⦄ ⊢ #↑i ⬌η[h] X2 →
 100       ∃∃T2. ⦃G,K⦄ ⊢ #i ⬌η[h] T2 & ⬆*[1] T2 ≘ X2.
 101 #h #G #Y0 #X2 #Z #j
 102 @(insert_eq_0 … (Y0.ⓘ{Z})) #Y
 103 @(insert_eq_0 … (#↑j)) #X1
 104 * -G -Y -X1 -X2
 105 [ #G #L #s #H #_ destruct
 106 | #G #i #_ #H destruct
 107 | #G #K #I #_ #H #_ destruct
 108 | #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H #_ destruct
 109 | #I #G #K #T #U #i #Hi #HTU #H1 #H2 destruct /2 width=3 by ex2_intro/
 110 | #G #L #l #H #_ destruct
 111 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 112 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H #_ destruct
 113 ]
 114 qed-.
 115
 116 lemma cpce_inv_gref_sn (h) (G) (L) (X2):
 117       ∀l. ⦃G,L⦄ ⊢ §l ⬌η[h] X2 → §l = X2.
 118 #h #G #Y #X2 #k
 119 @(insert_eq_0 … (§k)) #X1 * -G -Y -X1 -X2
 120 [ #G #L #s #_ //
 121 | #G #i #_ //
 122 | #G #K #I #_ #_ //
 123 | #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
 124 | #I #G #K #T #U #i #_ #_ #H destruct
 125 | #G #L #l #_ //
 126 | #p #I #G #K #V1 #V2 #T1 #T2 #_ #_ #H destruct
 127 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 128 ]
 129 qed-.
 130
 131 lemma cpce_inv_bind_sn (h) (G) (K) (X2):
 132       ∀p,I,V1,T1. ⦃G,K⦄ ⊢ ⓑ{p,I}V1.T1 ⬌η[h] X2 →
 133       ∃∃V2,T2. ⦃G,K⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,K.ⓑ{I}V1⦄ ⊢ T1 ⬌η[h] T2 & ⓑ{p,I}V2.T2 = X2.
 134 #h #G #Y #X2 #q #Z #U #X
 135 @(insert_eq_0 … (ⓑ{q,Z}U.X)) #X1 * -G -Y -X1 -X2
 136 [ #G #L #s #H destruct
 137 | #G #i #H destruct
 138 | #G #K #I #_ #H destruct
 139 | #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
 140 | #I #G #K #T #U #i #_ #_ #H destruct
 141 | #G #L #l #H destruct
 142 | #p #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
 143 | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 144 ]
 145 qed-.
 146
 147 lemma cpce_inv_flat_sn (h) (G) (L) (X2):
 148       ∀I,V1,T1. ⦃G,L⦄ ⊢ ⓕ{I}V1.T1 ⬌η[h] X2 →
 149       ∃∃V2,T2. ⦃G,L⦄ ⊢ V1 ⬌η[h] V2 & ⦃G,L⦄ ⊢ T1 ⬌η[h] T2 & ⓕ{I}V2.T2 = X2.
 150 #h #G #Y #X2 #Z #U #X
 151 @(insert_eq_0 … (ⓕ{Z}U.X)) #X1 * -G -Y -X1 -X2
 152 [ #G #L #s #H destruct
 153 | #G #i #H destruct
 154 | #G #K #I #_ #H destruct
 155 | #n #p #G #K #W #V1 #V2 #W2 #U #_ #_ #_ #H destruct
 156 | #I #G #K #T #U #i #_ #_ #H destruct
 157 | #G #L #l #H destruct
 158 | #p #I #G #L #V1 #V2 #T1 #T2 #_ #_ #H destruct
 159 | #I #G #K #V1 #V2 #T1 #T2 #HV #HT #H destruct /2 width=5 by ex3_2_intro/
 160 ]
 161 qed-.