matita/matita/contribs/lambdadelta/static_2/syntax/tueq.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.ma".
  17
  18 (* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************)
  19
  20 inductive tueq: relation term ≝
  21 | tueq_sort: ∀s1,s2. tueq (⋆s1) (⋆s2)
  22 | tueq_lref: ∀i. tueq (#i) (#i)
  23 | tueq_gref: ∀l. tueq (§l) (§l)
  24 | tueq_bind: ∀p,I,V,T1,T2. tueq T1 T2 → tueq (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
  25 | tueq_appl: ∀V,T1,T2. tueq T1 T2 → tueq (ⓐV.T1) (ⓐV.T2)
  26 | tueq_cast: ∀V1,V2,T1,T2. tueq V1 V2 → tueq T1 T2 → tueq (ⓝV1.T1) (ⓝV2.T2)
  27 .
  28
  29 interpretation
  30    "context-free tail sort-irrelevant equivalence (term)"
  31    'ApproxEq T1 T2 = (tueq T1 T2).
  32
  33 (* Basic properties *********************************************************)
  34
  35 lemma tueq_refl: reflexive … tueq.
  36 #T elim T -T * [|||| * ]
  37 /2 width=1 by tueq_sort, tueq_lref, tueq_gref, tueq_bind, tueq_appl, tueq_cast/
  38 qed.
  39
  40 lemma tueq_sym: symmetric … tueq.
  41 #T1 #T2 #H elim H -T1 -T2
  42 /2 width=3 by tueq_sort, tueq_bind, tueq_appl, tueq_cast/
  43 qed-.
  44
  45 (* Left basic inversion lemmas **********************************************)
  46
  47 fact tueq_inv_sort1_aux: ∀X,Y. X ≅ Y → ∀s1. X = ⋆s1 →
  48                          ∃s2. Y = ⋆s2.
  49 #X #Y * -X -Y
  50 [ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
  51 | #i #s #H destruct
  52 | #l #s #H destruct
  53 | #p #I #V #T1 #T2 #_ #s #H destruct
  54 | #V #T1 #T2 #_ #s #H destruct
  55 | #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
  56 ]
  57 qed-.
  58
  59 lemma tueq_inv_sort1: ∀Y,s1. ⋆s1 ≅ Y →
  60                       ∃s2. Y = ⋆s2.
  61 /2 width=4 by tueq_inv_sort1_aux/ qed-.
  62
  63 fact tueq_inv_lref1_aux: ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i.
  64 #X #Y * -X -Y //
  65 [ #s1 #s2 #j #H destruct
  66 | #p #I #V #T1 #T2 #_ #j #H destruct
  67 | #V #T1 #T2 #_ #j #H destruct
  68 | #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
  69 ]
  70 qed-.
  71
  72 lemma tueq_inv_lref1: ∀Y,i. #i ≅ Y → Y = #i.
  73 /2 width=5 by tueq_inv_lref1_aux/ qed-.
  74
  75 fact tueq_inv_gref1_aux: ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l.
  76 #X #Y * -X -Y //
  77 [ #s1 #s2 #k #H destruct
  78 | #p #I #V #T1 #T2 #_ #k #H destruct
  79 | #V #T1 #T2 #_ #k #H destruct
  80 | #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
  81 ]
  82 qed-.
  83
  84 lemma tueq_inv_gref1: ∀Y,l. §l ≅ Y → Y = §l.
  85 /2 width=5 by tueq_inv_gref1_aux/ qed-.
  86
  87 fact tueq_inv_bind1_aux: ∀X,Y. X ≅ Y → ∀p,I,V,T1. X = ⓑ{p,I}V.T1 →
  88                          ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
  89 #X #Y * -X -Y
  90 [ #s1 #s2 #q #J #W #U1 #H destruct
  91 | #i #q #J #W #U1 #H destruct
  92 | #l #q #J #W #U1 #H destruct
  93 | #p #I #V #T1 #T2 #HT #q #J #W #U1 #H destruct /2 width=3 by ex2_intro/
  94 | #V #T1 #T2 #_ #q #J #W #U1 #H destruct
  95 | #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
  96 ]
  97 qed-.
  98
  99 lemma tueq_inv_bind1: ∀p,I,V,T1,Y. ⓑ{p,I}V.T1 ≅ Y →
 100                       ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
 101 /2 width=3 by tueq_inv_bind1_aux/ qed-.
 102
 103 fact tueq_inv_appl1_aux: ∀X,Y. X ≅ Y → ∀V,T1. X = ⓐV.T1 →
 104                          ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
 105 #X #Y * -X -Y
 106 [ #s1 #s2 #W #U1 #H destruct
 107 | #i #W #U1 #H destruct
 108 | #l #W #U1 #H destruct
 109 | #p #I #V #T1 #T2 #_ #W #U1 #H destruct
 110 | #V #T1 #T2 #HT #W #U1 #H destruct /2 width=3 by ex2_intro/
 111 | #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
 112 ]
 113 qed-.
 114
 115 lemma tueq_inv_appl1: ∀V,T1,Y. ⓐV.T1 ≅ Y →
 116                       ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
 117 /2 width=3 by tueq_inv_appl1_aux/ qed-.
 118
 119 fact tueq_inv_cast1_aux: ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 →
 120                          ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
 121 #X #Y * -X -Y
 122 [ #s1 #s2 #W1 #U1 #H destruct
 123 | #i #W1 #U1 #H destruct
 124 | #l #W1 #U1 #H destruct
 125 | #p #I #V #T1 #T2 #_ #W1 #U1 #H destruct
 126 | #V #T1 #T2 #_ #W1 #U1 #H destruct
 127 | #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
 128 ]
 129 qed-.
 130
 131 lemma tueq_inv_cast1: ∀V1,T1,Y. ⓝV1.T1 ≅ Y →
 132                       ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
 133 /2 width=3 by tueq_inv_cast1_aux/ qed-.
 134
 135 (* Right basic inversion lemmas *********************************************)
 136
 137 lemma tueq_inv_bind2: ∀p,I,V,T2,X1. X1 ≅ ⓑ{p,I}V.T2 →
 138                       ∃∃T1. T1 ≅ T2 & X1 = ⓑ{p,I}V.T1.
 139 #p #I #V #T2 #X1 #H
 140 elim (tueq_inv_bind1 p I V T2 X1)
 141 [ #T1 #HT #H destruct ]
 142 /3 width=3 by tueq_sym, ex2_intro/
 143 qed-.