matita/matita/contribs/lambdadelta/static_2/syntax/theq.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/topiso_4.ma".
  16 include "static_2/syntax/item_sd.ma".
  17 include "static_2/syntax/term.ma".
  18
  19 (* HEAD EQUIVALENCE FOR TERMS ***********************************************)
  20
  21 (* Basic_2A1: includes: tsts_atom tsts_pair *)
  22 inductive theq (h) (o): relation term ≝
  23 | theq_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → theq h o (⋆s1) (⋆s2)
  24 | theq_lref: ∀i. theq h o (#i) (#i)
  25 | theq_gref: ∀l. theq h o (§l) (§l)
  26 | theq_pair: ∀I,V1,V2,T1,T2. theq h o (②{I}V1.T1) (②{I}V2.T2)
  27 .
  28
  29 interpretation "head equivalence (term)" 'TopIso h o T1 T2 = (theq h o T1 T2).
  30
  31 (* Basic inversion lemmas ***************************************************)
  32
  33 fact theq_inv_sort1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀s1. X = ⋆s1 →
  34                          ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2.
  35 #h #o #X #Y * -X -Y
  36 [ #s1 #s2 #d #Hs1 #Hs2 #s #H destruct /2 width=5 by ex3_2_intro/
  37 | #i #s #H destruct
  38 | #l #s #H destruct
  39 | #I #V1 #V2 #T1 #T2 #s #H destruct
  40 ]
  41 qed-.
  42
  43 (* Basic_1: was just: iso_gen_sort *)
  44 lemma theq_inv_sort1: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y →
  45                       ∃∃s2,d. deg h o s1 d & deg h o s2 d & Y = ⋆s2.
  46 /2 width=3 by theq_inv_sort1_aux/ qed-.
  47
  48 fact theq_inv_lref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀i. X = #i → Y = #i.
  49 #h #o #X #Y * -X -Y //
  50 [ #s1 #s2 #d #_ #_ #j #H destruct
  51 | #I #V1 #V2 #T1 #T2 #j #H destruct
  52 ]
  53 qed-.
  54
  55 (* Basic_1: was: iso_gen_lref *)
  56 lemma theq_inv_lref1: ∀h,o,Y,i. #i ⩳[h, o] Y → Y = #i.
  57 /2 width=5 by theq_inv_lref1_aux/ qed-.
  58
  59 fact theq_inv_gref1_aux: ∀h,o,X,Y. X ⩳[h, o] Y → ∀l. X = §l → Y = §l.
  60 #h #o #X #Y * -X -Y //
  61 [ #s1 #s2 #d #_ #_ #k #H destruct
  62 | #I #V1 #V2 #T1 #T2 #k #H destruct
  63 ]
  64 qed-.
  65
  66 lemma theq_inv_gref1: ∀h,o,Y,l. §l ⩳[h, o] Y → Y = §l.
  67 /2 width=5 by theq_inv_gref1_aux/ qed-.
  68
  69 fact theq_inv_pair1_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 →
  70                          ∀J,W1,U1. T1 = ②{J}W1.U1 →
  71                          ∃∃W2,U2. T2 = ②{J}W2.U2.
  72 #h #o #T1 #T2 * -T1 -T2
  73 [ #s1 #s2 #d #_ #_ #J #W1 #U1 #H destruct
  74 | #i #J #W1 #U1 #H destruct
  75 | #l #J #W1 #U1 #H destruct
  76 | #I #V1 #V2 #T1 #T2 #J #W1 #U1 #H destruct /2 width=3 by ex1_2_intro/
  77 ]
  78 qed-.
  79
  80 (* Basic_1: was: iso_gen_head *)
  81 (* Basic_2A1: was: tsts_inv_pair1 *)
  82 lemma theq_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 →
  83                       ∃∃W2,U2. T2 = ②{J}W2. U2.
  84 /2 width=7 by theq_inv_pair1_aux/ qed-.
  85
  86 fact theq_inv_pair2_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 →
  87                          ∀J,W2,U2. T2 = ②{J}W2.U2 →
  88                          ∃∃W1,U1. T1 = ②{J}W1.U1.
  89 #h #o #T1 #T2 * -T1 -T2
  90 [ #s1 #s2 #d #_ #_ #J #W2 #U2 #H destruct
  91 | #i #J #W2 #U2 #H destruct
  92 | #l #J #W2 #U2 #H destruct
  93 | #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
  94 ]
  95 qed-.
  96
  97 (* Basic_2A1: was: tsts_inv_pair2 *)
  98 lemma theq_inv_pair2: ∀h,o,J,T1,W2,U2. T1 ⩳[h, o] ②{J}W2.U2 →
  99                       ∃∃W1,U1. T1 = ②{J}W1.U1.
 100 /2 width=7 by theq_inv_pair2_aux/ qed-.
 101
 102 (* Advanced inversion lemmas ************************************************)
 103
 104 lemma theq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d →
 105                           ∃∃s2. deg h o s2 d & Y = ⋆s2.
 106 #h #o #Y #s1 #H #d #Hs1 elim (theq_inv_sort1 … H) -H
 107 #s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/
 108 qed-.
 109
 110 lemma theq_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ⩳[h, o] ⋆s2 →
 111                          ∀d1,d2. deg h o s1 d1 → deg h o s2 d2 →
 112                          d1 = d2.
 113 #h #o #s1 #y #H #d1 #d2 #Hs1 #Hy
 114 elim (theq_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct
 115 <(deg_mono h o … Hy … Hs2) -s2 -d1 //
 116 qed-.
 117
 118 lemma theq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳[h, o] ②{I2}V2.T2 →
 119                      I1 = I2.
 120 #h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (theq_inv_pair1 … H) -H
 121 #V0 #T0 #H destruct //
 122 qed-.
 123
 124 (* Basic properties *********************************************************)
 125
 126 (* Basic_1: was: iso_refl *)
 127 (* Basic_2A1: was: tsts_refl *)
 128 lemma theq_refl: ∀h,o. reflexive … (theq h o).
 129 #h #o * //
 130 * /2 width=1 by theq_lref, theq_gref/
 131 #s elim (deg_total h o s) /2 width=3 by theq_sort/
 132 qed.
 133
 134 (* Basic_2A1: was: tsts_sym *)
 135 lemma theq_sym: ∀h,o. symmetric … (theq h o).
 136 #h #o #T1 #T2 * -T1 -T2 /2 width=3 by theq_sort/
 137 qed-.
 138
 139 (* Basic_2A1: was: tsts_dec *)
 140 lemma theq_dec: ∀h,o,T1,T2. Decidable (T1 ⩳[h, o] T2).
 141 #h #o * [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
 142 [ elim (deg_total h o s1) #d1 #H1
 143   elim (deg_total h o s2) #d2 #H2
 144   elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by theq_sort, or_introl/
 145   @or_intror #H
 146   lapply (theq_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/
 147 |2,3,13:
 148   @or_intror #H
 149   elim (theq_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct
 150 |4,6,14:
 151   @or_intror #H
 152   lapply (theq_inv_lref1 … H) -H #H destruct
 153 |5:
 154   elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
 155   @or_intror #H
 156   lapply (theq_inv_lref1 … H) -H #H destruct /2 width=1 by/
 157 |7,8,15:
 158   @or_intror #H
 159   lapply (theq_inv_gref1 … H) -H #H destruct
 160 |9:
 161   elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
 162   @or_intror #H
 163   lapply (theq_inv_gref1 … H) -H #H destruct /2 width=1 by/
 164 |10,11,12:
 165   @or_intror #H
 166   elim (theq_inv_pair1 … H) -H #X1 #X2 #H destruct
 167 |16:
 168   elim (eq_item2_dec I1 I2) #HI12 destruct
 169   [ /3 width=1 by theq_pair, or_introl/ ]
 170   @or_intror #H
 171   lapply (theq_inv_pair … H) -H /2 width=1 by/
 172 ]
 173 qed-.
 174
 175 (* Basic_2A1: removed theorems 2:
 176               tsts_inv_atom1 tsts_inv_atom2
 177 *)