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