]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/static_2/syntax/teqx.ma
update in delayed_updating
[helm.git] / 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-.