matita/matita/contribs/lambdadelta/basic_2/syntax/tsts.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 "basic_2/notation/relations/topiso_4.ma".
  16 include "basic_2/syntax/item_sd.ma".
  17 include "basic_2/syntax/term.ma".
  18
  19 (* SAME TOP TERM STRUCTURE **************************************************)
  20
  21 (* Basic_2A1: includes: tsts_atom *)
  22 inductive tsts (h) (o): relation term ≝
  23 | tsts_sort: ∀s1,s2,d. deg h o s1 d → deg h o s2 d → tsts h o (⋆s1) (⋆s2)
  24 | tsts_lref: ∀i. tsts h o (#i) (#i)
  25 | tsts_gref: ∀l. tsts h o (§l) (§l)
  26 | tsts_pair: ∀I,V1,V2,T1,T2. tsts h o (②{I}V1.T1) (②{I}V2.T2)
  27 .
  28
  29 interpretation "same top structure (term)" 'TopIso h o T1 T2 = (tsts h o T1 T2).
  30
  31 (* Basic inversion lemmas ***************************************************)
  32
  33 fact tsts_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 tsts_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 tsts_inv_sort1_aux/ qed-.
  47
  48 fact tsts_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 tsts_inv_lref1: ∀h,o,Y,i. #i ⩳[h, o] Y → Y = #i.
  57 /2 width=5 by tsts_inv_lref1_aux/ qed-.
  58
  59 fact tsts_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 tsts_inv_gref1: ∀h,o,Y,l. §l ⩳[h, o] Y → Y = §l.
  67 /2 width=5 by tsts_inv_gref1_aux/ qed-.
  68
  69 fact tsts_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 lemma tsts_inv_pair1: ∀h,o,J,W1,U1,T2. ②{J}W1.U1 ⩳[h, o] T2 →
  82                       ∃∃W2,U2. T2 = ②{J}W2. U2.
  83 /2 width=7 by tsts_inv_pair1_aux/ qed-.
  84
  85 fact tsts_inv_pair2_aux: ∀h,o,T1,T2. T1 ⩳[h, o] T2 →
  86                          ∀J,W2,U2. T2 = ②{J}W2.U2 →
  87                          ∃∃W1,U1. T1 = ②{J}W1.U1.
  88 #h #o #T1 #T2 * -T1 -T2
  89 [ #s1 #s2 #d #_ #_ #J #W2 #U2 #H destruct
  90 | #i #J #W2 #U2 #H destruct
  91 | #l #J #W2 #U2 #H destruct
  92 | #I #V1 #V2 #T1 #T2 #J #W2 #U2 #H destruct /2 width=3 by ex1_2_intro/
  93 ]
  94 qed-.
  95
  96 lemma tsts_inv_pair2: ∀h,o,J,T1,W2,U2. T1 ⩳[h, o] ②{J}W2.U2 →
  97                       ∃∃W1,U1. T1 = ②{J}W1.U1.
  98 /2 width=7 by tsts_inv_pair2_aux/ qed-.
  99
 100 (* Advanced inversion lemmas ************************************************)
 101
 102 lemma tsts_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ⩳[h, o] Y → ∀d. deg h o s1 d →
 103                           ∃∃s2. deg h o s2 d & Y = ⋆s2.
 104 #h #o #Y #s1 #H #d #Hs1 elim (tsts_inv_sort1 … H) -H
 105 #s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/
 106 qed-.
 107
 108 lemma tsts_inv_sort_deg: ∀h,o,s1,s2. ⋆s1 ⩳[h, o] ⋆s2 →
 109                          ∀d1,d2. deg h o s1 d1 → deg h o s2 d2 →
 110                          d1 = d2.
 111 #h #o #s1 #y #H #d1 #d2 #Hs1 #Hy
 112 elim (tsts_inv_sort1_deg … H … Hs1) -s1 #s2 #Hs2 #H destruct
 113 <(deg_mono h o … Hy … Hs2) -s2 -d1 //
 114 qed-.
 115
 116 lemma tsts_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ⩳[h, o] ②{I2}V2.T2 →
 117                      I1 = I2.
 118 #h #o #I1 #I2 #V1 #V2 #T1 #T2 #H elim (tsts_inv_pair1 … H) -H
 119 #V0 #T0 #H destruct //
 120 qed-.
 121
 122 (* Basic properties *********************************************************)
 123
 124 (* Basic_1: was: iso_refl *)
 125 lemma tsts_refl: ∀h,o. reflexive … (tsts h o).
 126 #h #o * //
 127 * /2 width=1 by tsts_lref, tsts_gref/
 128 #s elim (deg_total h o s) /2 width=3 by tsts_sort/
 129 qed.
 130
 131 lemma tsts_sym: ∀h,o. symmetric … (tsts h o).
 132 #h #o #T1 #T2 * -T1 -T2 /2 width=3 by tsts_sort/
 133 qed-.
 134
 135 lemma tsts_dec: ∀h,o,T1,T2. Decidable (T1 ⩳[h, o] T2).
 136 #h #o * [ * #s1 | #I1 #V1 #T1 ] * [1,3,5,7: * #s2 |*: #I2 #V2 #T2 ]
 137 [ elim (deg_total h o s1) #d1 #H1
 138   elim (deg_total h o s2) #d2 #H2
 139   elim (eq_nat_dec d1 d2) #Hd12 destruct /3 width=3 by tsts_sort, or_introl/
 140   @or_intror #H
 141   lapply (tsts_inv_sort_deg … H … H1 H2) -H -H1 -H2 /2 width=1 by/
 142 |2,3,13:
 143   @or_intror #H
 144   elim (tsts_inv_sort1 … H) -H #x1 #x2 #_ #_ #H destruct
 145 |4,6,14:
 146   @or_intror #H
 147   lapply (tsts_inv_lref1 … H) -H #H destruct
 148 |5:
 149   elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
 150   @or_intror #H
 151   lapply (tsts_inv_lref1 … H) -H #H destruct /2 width=1 by/
 152 |7,8,15:
 153   @or_intror #H
 154   lapply (tsts_inv_gref1 … H) -H #H destruct
 155 |9:
 156   elim (eq_nat_dec s1 s2) #Hs12 destruct /2 width=1 by or_introl/
 157   @or_intror #H
 158   lapply (tsts_inv_gref1 … H) -H #H destruct /2 width=1 by/
 159 |10,11,12:
 160   @or_intror #H
 161   elim (tsts_inv_pair1 … H) -H #X1 #X2 #H destruct
 162 |16:
 163   elim (eq_item2_dec I1 I2) #HI12 destruct
 164   [ /3 width=1 by tsts_pair, or_introl/ ]
 165   @or_intror #H
 166   lapply (tsts_inv_pair … H) -H /2 width=1 by/
 167 ]
 168 qed-.
 169
 170 (* Basic_2A1: removed theorems 4:
 171               tsts_inv_atom1 tsts_inv_atom2
 172 *)