matita/matita/contribs/lambdadelta/static_2/syntax/teqx.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/teqg.ma".
  17
  18 (* SORT-IRRELEVANT EQUIVALENCE ON TERMS *************************************)
  19
  20 definition teqx: relation term ≝
  21            teqg sfull.
  22
  23 interpretation
  24   "context-free sort-irrelevant equivalence (term)"
  25   'ApproxEq T1 T2 = (teqx T1 T2).
  26
  27 (* Basic properties *********************************************************)
  28
  29 lemma teqx_pair:
  30       ∀V1,V2. V1 ≅ V2 → ∀T1,T2. T1 ≅ T2 →
  31       ∀I. ②[I]V1.T1 ≅ ②[I]V2.T2.
  32 /2 width=1 by teqg_pair/ qed.
  33
  34 lemma teqx_refl:
  35       reflexive … teqx.
  36 /2 width=1 by teqg_refl/ qed.
  37
  38 lemma teqx_sym:
  39       symmetric … teqx.
  40 /2 width=1 by teqg_sym/ qed-.
  41
  42 lemma teqg_teqx (S):
  43       ∀T1,T2. T1 ≛[S] T2 → T1 ≅ T2.
  44 /2 width=3 by teqg_co/ qed.
  45
  46 (* Basic inversion lemmas ***************************************************)
  47
  48 lemma teqx_inv_sort1:
  49       ∀X2,s1. ⋆s1 ≅ X2 →
  50       ∃s2. X2 = ⋆s2.
  51 #X1 #s1 #H elim (teqg_inv_sort1 … H) -H /2 width=2 by ex_intro/
  52 qed-.
  53 (*
  54 lemma teqx_inv_lref1:
  55       ∀X,i. #i ≅ X → X = #i.
  56 /2 width=5 by teqg_inv_lref1/ qed-.
  57
  58 lemma teqx_inv_gref1:
  59       ∀X,l. §l ≅ X → X = §l.
  60 /2 width=5 by teqg_inv_gref1/ qed-.
  61 *)
  62 lemma teqx_inv_pair1:
  63       ∀I,V1,T1,X2. ②[I]V1.T1 ≅ X2 →
  64       ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & X2 = ②[I]V2.T2.
  65 /2 width=3 by teqg_inv_pair1/ qed-.
  66
  67 lemma teqx_inv_sort2:
  68       ∀X1,s2. X1 ≅ ⋆s2 →
  69       ∃s1. X1 = ⋆s1.
  70 #X1 #s2 #H elim (teqg_inv_sort2 … H) -H /2 width=2 by ex_intro/
  71 qed-.
  72
  73 lemma teqx_inv_pair2:
  74       ∀I,X1,V2,T2. X1 ≅ ②[I]V2.T2 →
  75       ∃∃V1,T1. V1 ≅ V2 & T1 ≅ T2 & X1 = ②[I]V1.T1.
  76 /2 width=1 by teqg_inv_pair2/ qed-.
  77
  78 (* Advanced inversion lemmas ************************************************)
  79
  80 lemma teqx_inv_pair:
  81       ∀I1,I2,V1,V2,T1,T2. ②[I1]V1.T1 ≅ ②[I2]V2.T2 →
  82       ∧∧ I1 = I2 & V1 ≅ V2 & T1 ≅ T2.
  83 /2 width=1 by teqg_inv_pair/ qed-.
  84 (*
  85 lemma teqx_inv_pair_xy_x:
  86       ∀I,V,T. ②[I]V.T ≅ V → ⊥.
  87 /2 width=5 by teqg_inv_pair_xy_x/ qed-.
  88
  89 lemma teqx_inv_pair_xy_y:
  90       ∀I,T,V. ②[I]V.T ≅ T → ⊥.
  91 /2 width=5 by teqg_inv_pair_xy_y/ qed-.
  92 *)
  93 (* Basic forward lemmas *****************************************************)
  94 (*
  95 lemma teqx_fwd_atom1:
  96       ∀I,Y. ⓪[I] ≅ Y → ∃J. Y = ⓪[J].
  97 /2 width=3 by teqg_fwd_atom1/ qed-.
  98 *)
  99 (* Advanced properties ******************************************************)
 100
 101 lemma teqx_dec:
 102       ∀T1,T2. Decidable (T1 ≅ T2).
 103 /3 width=1 by teqg_dec, or_introl/ qed-.
 104
 105 (* Negated inversion lemmas *************************************************)
 106
 107 lemma tneqx_inv_pair:
 108       ∀I1,I2,V1,V2,T1,T2.
 109       (②[I1]V1.T1 ≅ ②[I2]V2.T2 → ⊥) →
 110       ∨∨ I1 = I2 → ⊥
 111        | (V1 ≅ V2 → ⊥)
 112        | (T1 ≅ T2 → ⊥).
 113 /3 width=1 by tneqg_inv_pair, or_introl/ qed-.