matita/matita/contribs/lambdadelta/static_2/syntax/tweq.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 "static_2/notation/relations/approxeq_2.ma".
  16 include "static_2/syntax/term_weight.ma".
  17
  18 lemma tw_le_pair_dx (I): ∀V,T. ♯{T} < ♯{②{I}V.T}.
  19 #I #V #T /2 width=1 by le_S_S/
  20 qed.
  21
  22 (* SORT-IRRELEVANT WHD EQUIVALENCE ON TERMS *********************************)
  23
  24 inductive tweq: relation term ≝
  25 | tweq_sort: ∀s1,s2. tweq (⋆s1) (⋆s2)
  26 | tweq_lref: ∀i. tweq (#i) (#i)
  27 | tweq_gref: ∀l. tweq (§l) (§l)
  28 | tweq_abbr: ∀p,V1,V2,T1,T2. (p=Ⓣ→tweq T1 T2) → tweq (ⓓ{p}V1.T1) (ⓓ{p}V2.T2)
  29 | tweq_abst: ∀p,V1,V2,T1,T2. tweq (ⓛ{p}V1.T1) (ⓛ{p}V2.T2)
  30 | tweq_appl: ∀V1,V2,T1,T2. tweq T1 T2 → tweq (ⓐV1.T1) (ⓐV2.T2)
  31 | tweq_cast: ∀V1,V2,T1,T2. tweq V1 V2 → tweq T1 T2 → tweq (ⓝV1.T1) (ⓝV2.T2)
  32 .
  33
  34 interpretation
  35    "context-free tail sort-irrelevant equivalence (term)"
  36    'ApproxEq T1 T2 = (tweq T1 T2).
  37
  38 (* Basic properties *********************************************************)
  39
  40 lemma tweq_abbr_pos: ∀V1,V2,T1,T2. T1 ≅ T2 → +ⓓV1.T1 ≅ +ⓓV2.T2.
  41 /3 width=1 by tweq_abbr/ qed.
  42
  43 lemma tweq_abbr_neg: ∀V1,V2,T1,T2. -ⓓV1.T1 ≅ -ⓓV2.T2.
  44 #V1 #V2 #T1 #T2
  45 @tweq_abbr #H destruct
  46 qed.
  47
  48 lemma tweq_refl: reflexive … tweq.
  49 #T elim T -T * [||| #p * | * ]
  50 /2 width=1 by tweq_sort, tweq_lref, tweq_gref, tweq_abbr, tweq_abst, tweq_appl, tweq_cast/
  51 qed.
  52
  53 lemma tweq_sym: symmetric … tweq.
  54 #T1 #T2 #H elim H -T1 -T2
  55 /3 width=3 by tweq_sort, tweq_lref, tweq_gref, tweq_abbr, tweq_abst, tweq_appl, tweq_cast/
  56 qed-.
  57
  58 (* Left basic inversion lemmas **********************************************)
  59
  60 fact tweq_inv_sort_sn_aux:
  61      ∀X,Y. X ≅ Y → ∀s1. X = ⋆s1 → ∃s2. Y = ⋆s2.
  62 #X #Y * -X -Y
  63 [1  : #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
  64 |2,3: #i #s #H destruct
  65 |4  : #p #V1 #V2 #T1 #T2 #_ #s #H destruct
  66 |5  : #p #V1 #V2 #T1 #T2 #s #H destruct
  67 |6  : #V1 #V2 #T1 #T2 #_ #s #H destruct
  68 |7  : #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
  69 ]
  70 qed-.
  71
  72 lemma tweq_inv_sort_sn:
  73       ∀Y,s1. ⋆s1 ≅ Y → ∃s2. Y = ⋆s2.
  74 /2 width=4 by tweq_inv_sort_sn_aux/ qed-.
  75
  76 fact tweq_inv_lref_sn_aux:
  77      ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i.
  78 #X #Y * -X -Y
  79 [1  : #s1 #s2 #j #H destruct
  80 |2,3: //
  81 |4  : #p #V1 #V2 #T1 #T2 #_ #j #H destruct
  82 |5  : #p #V1 #V2 #T1 #T2 #j #H destruct
  83 |6  : #V1 #V2 #T1 #T2 #_ #j #H destruct
  84 |7  : #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
  85 ]
  86 qed-.
  87
  88 lemma tweq_inv_lref_sn: ∀Y,i. #i ≅ Y → Y = #i.
  89 /2 width=5 by tweq_inv_lref_sn_aux/ qed-.
  90
  91 fact tweq_inv_gref_sn_aux:
  92      ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l.
  93 #X #Y * -X -Y
  94 [1  : #s1 #s2 #k #H destruct
  95 |2,3: //
  96 |4  : #p #V1 #V2 #T1 #T2 #_ #k #H destruct
  97 |5  : #p #V1 #V2 #T1 #T2 #k #H destruct
  98 |6  : #V1 #V2 #T1 #T2 #_ #k #H destruct
  99 |7  : #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
 100 ]
 101 qed-.
 102
 103 lemma tweq_inv_gref_sn:
 104       ∀Y,l. §l ≅ Y → Y = §l.
 105 /2 width=5 by tweq_inv_gref_sn_aux/ qed-.
 106
 107 fact tweq_inv_abbr_sn_aux:
 108      ∀X,Y. X ≅ Y → ∀p,V1,T1. X = ⓓ{p}V1.T1 →
 109      ∃∃V2,T2. p = Ⓣ → T1 ≅ T2 & Y = ⓓ{p}V2.T2.
 110 #X #Y * -X -Y
 111 [1  : #s1 #s2 #q #W1 #U1 #H destruct
 112 |2,3: #i #q #W1 #U1 #H destruct
 113 |4  : #p #V1 #V2 #T1 #T2 #HT #q #W1 #U1 #H destruct /3 width=4 by ex2_2_intro/
 114 |5  : #p #V1 #V2 #T1 #T2 #q #W1 #U1 #H destruct
 115 |6  : #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
 116 |7  : #V1 #V2 #T1 #T2 #_ #_ #q #W1 #U1 #H destruct
 117 ]
 118 qed-.
 119
 120 lemma tweq_inv_abbr_sn:
 121       ∀p,V1,T1,Y. ⓓ{p}V1.T1 ≅ Y →
 122       ∃∃V2,T2. p = Ⓣ → T1 ≅ T2 & Y = ⓓ{p}V2.T2.
 123 /2 width=4 by tweq_inv_abbr_sn_aux/ qed-.
 124
 125 fact tweq_inv_abst_sn_aux:
 126      ∀X,Y. X ≅ Y → ∀p,V1,T1. X = ⓛ{p}V1.T1 →
 127      ∃∃V2,T2. Y = ⓛ{p}V2.T2.
 128 #X #Y * -X -Y
 129 [1  : #s1 #s2 #q #W1 #U1 #H destruct
 130 |2,3: #i #q #W1 #U1 #H destruct
 131 |4  : #p #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
 132 |5  : #p #V1 #V2 #T1 #T2 #q #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
 133 |6  : #V1 #V2 #T1 #T2 #_ #q #W1 #U1 #H destruct
 134 |7  : #V1 #V2 #T1 #T2 #_ #_ #q #W1 #U1 #H destruct
 135 ]
 136 qed-.
 137
 138 lemma tweq_inv_abst_sn:
 139       ∀p,V1,T1,Y. ⓛ{p}V1.T1 ≅ Y →
 140       ∃∃V2,T2. Y = ⓛ{p}V2.T2.
 141 /2 width=5 by tweq_inv_abst_sn_aux/ qed-.
 142
 143 fact tweq_inv_appl_sn_aux:
 144      ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓐV1.T1 →
 145      ∃∃V2,T2. T1 ≅ T2 & Y = ⓐV2.T2.
 146 #X #Y * -X -Y
 147 [1  : #s1 #s2 #W1 #U1 #H destruct
 148 |2,3: #i #W1 #U1 #H destruct
 149 |4  : #p #V1 #V2 #T1 #T2 #HT #W1 #U1 #H destruct
 150 |5  : #p #V1 #V2 #T1 #T2 #W1 #U1 #H destruct
 151 |6  : #V1 #V2 #T1 #T2 #HT #W1 #U1 #H destruct /2 width=4 by ex2_2_intro/
 152 |7  : #V1 #V2 #T1 #T2 #_ #_ #W1 #U1 #H destruct
 153 ]
 154 qed-.
 155
 156 lemma tweq_inv_appl_sn:
 157       ∀V1,T1,Y. ⓐV1.T1 ≅ Y →
 158       ∃∃V2,T2. T1 ≅ T2 & Y = ⓐV2.T2.
 159 /2 width=4 by tweq_inv_appl_sn_aux/ qed-.
 160
 161 fact tweq_inv_cast_sn_aux:
 162      ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 →
 163      ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
 164 #X #Y * -X -Y
 165 [1  : #s1 #s2 #W1 #U1 #H destruct
 166 |2,3: #i #W1 #U1 #H destruct
 167 |4  : #p #V1 #V2 #T1 #T2 #_ #W1 #U1 #H destruct
 168 |5  : #p #V1 #V2 #T1 #T2 #W1 #U1 #H destruct
 169 |6  : #V1 #V2 #T1 #T2 #_ #W1 #U1 #H destruct
 170 |7  : #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
 171 ]
 172 qed-.
 173
 174 lemma tweq_inv_cast_sn:
 175       ∀V1,T1,Y. ⓝV1.T1 ≅ Y →
 176       ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
 177 /2 width=3 by tweq_inv_cast_sn_aux/ qed-.
 178
 179 (* Advanced inversion lemmas ************************************************)
 180
 181 lemma tweq_inv_abbr_pos_sn:
 182       ∀V1,T1,Y. +ⓓV1.T1 ≅ Y → ∃∃V2,T2. T1 ≅ T2 & Y = +ⓓV2.T2.
 183 #V1 #V2 #Y #H
 184 elim (tweq_inv_abbr_sn … H) -H #V2 #T2
 185 /3 width=4 by ex2_2_intro/
 186 qed-.
 187
 188 lemma tweq_inv_abbr_neg_sn:
 189       ∀V1,T1,Y. -ⓓV1.T1 ≅ Y → ∃∃V2,T2. Y = -ⓓV2.T2.
 190 #V1 #V2 #Y #H
 191 elim (tweq_inv_abbr_sn … H) -H #V2 #T2 #_
 192 /2 width=3 by ex1_2_intro/
 193 qed-.
 194
 195 lemma tweq_inv_abbr_pos_bi:
 196       ∀V1,V2,T1,T2. +ⓓV1.T1 ≅ +ⓓV2.T2 → T1 ≅ T2.
 197 #V1 #V2 #T1 #T2 #H
 198 elim (tweq_inv_abbr_pos_sn … H) -H #W2 #U2 #HTU #H destruct //
 199 qed-.
 200
 201 lemma tweq_inv_appl_bi:
 202       ∀V1,V2,T1,T2. ⓐV1.T1 ≅ ⓐV2.T2 → T1 ≅ T2.
 203 #V1 #V2 #T1 #T2 #H
 204 elim (tweq_inv_appl_sn … H) -H #W2 #U2 #HTU #H destruct //
 205 qed-.
 206
 207 lemma tweq_inv_cast_bi:
 208       ∀V1,V2,T1,T2. ⓝV1.T1 ≅ ⓝV2.T2 → ∧∧ V1 ≅ V2 & T1 ≅ T2.
 209 #V1 #V2 #T1 #T2 #H
 210 elim (tweq_inv_cast_sn … H) -H #W2 #U2 #HVW #HTU #H destruct
 211 /2 width=1 by conj/
 212 qed-.
 213
 214 lemma tweq_inv_cast_sn_XY_Y: ∀T,V. ⓝV.T ≅ T → ⊥.
 215 @(f_ind … tw) #n #IH #T #Hn #V #H destruct
 216 elim (tweq_inv_cast_sn … H) -H #X1 #X2 #_ #HX2 #H destruct -V
 217 /2 width=4 by/
 218 qed-.
 219
 220 (* Advanced forward lemmas **************************************************)
 221
 222 lemma tweq_fwd_pair_sn (I):
 223       ∀V1,T1,X2. ②{I}V1.T1 ≅ X2 → ∃∃V2,T2. X2 = ②{I}V2.T2.
 224 * [ #p ] * [ cases p -p ] #V1 #T1 #X2 #H
 225 [ elim (tweq_inv_abbr_pos_sn … H) -H #V2 #T2 #_ #H
 226 | elim (tweq_inv_abbr_neg_sn … H) -H #V2 #T2 #H
 227 | elim (tweq_inv_abst_sn … H) -H #V2 #T2 #H
 228 | elim (tweq_inv_appl_sn … H) -H #V2 #T2 #_ #H
 229 | elim (tweq_inv_cast_sn … H) -H #V2 #T2 #_ #_ #H
 230 ] /2 width=3 by ex1_2_intro/
 231 qed-.
 232
 233 lemma tweq_fwd_pair_bi (I1) (I2):
 234       ∀V1,V2,T1,T2. ②{I1}V1.T1 ≅ ②{I2}V2.T2 → I1 = I2.
 235 #I1 #I2 #V1 #V2 #T1 #T2 #H
 236 elim (tweq_fwd_pair_sn … H) -H #W2 #U2 #H destruct //
 237 qed-.
 238
 239 (* Advanced properties ******************************************************)
 240
 241 lemma tweq_dec: ∀T1,T2. Decidable (T1 ≅ T2).
 242 #T1 elim T1 -T1 [ * #s1 | #I1 #V1 #T1 #IHV #IHT ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
 243 [ /3 width=1 by tweq_sort, or_introl/
 244 |2,3,13:
 245   @or_intror #H
 246   elim (tweq_inv_sort_sn … H) -H #x #H destruct
 247 |4,6,14:
 248   @or_intror #H
 249   lapply (tweq_inv_lref_sn … H) -H #H destruct
 250 |5:
 251   elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
 252   @or_intror #H
 253   lapply (tweq_inv_lref_sn … H) -H #H destruct /2 width=1 by/
 254 |7,8,15:
 255   @or_intror #H
 256   lapply (tweq_inv_gref_sn … H) -H #H destruct
 257 |9:
 258   elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
 259   @or_intror #H
 260   lapply (tweq_inv_gref_sn … H) -H #H destruct /2 width=1 by/
 261 |10,11,12:
 262   @or_intror #H
 263   elim (tweq_fwd_pair_sn … H) -H #X1 #X2 #H destruct
 264 |16:
 265   elim (eq_item2_dec I1 I2) #HI12 destruct
 266   [ cases I2 -I2 [ #p ] * [ cases p -p ]
 267     [ elim (IHT T2) -IHT #HT12
 268       [ /3 width=1 by tweq_abbr_pos, or_introl/
 269       | /4 width=3 by tweq_inv_abbr_pos_bi, or_intror/
 270       ]
 271     | /3 width=1 by tweq_abbr_neg, or_introl/
 272     | /3 width=1 by tweq_abst, or_introl/
 273     | elim (IHT T2) -IHT #HT12
 274       [ /3 width=1 by tweq_appl, or_introl/
 275       | /4 width=3 by tweq_inv_appl_bi, or_intror/
 276       ]
 277     | elim (IHV V2) -IHV #HV12
 278       elim (IHT T2) -IHT #HT12
 279       [1: /3 width=1 by tweq_cast, or_introl/
 280       |*: @or_intror #H
 281           elim (tweq_inv_cast_bi … H) -H #HV12 #HT12
 282           /2 width=1 by/
 283       ]
 284     ]
 285   | /4 width=5 by tweq_fwd_pair_bi, or_intror/
 286   ]
 287 ]
 288 qed-.