1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "static_2/notation/relations/approxeq_2.ma".
16 include "static_2/syntax/term.ma".
18 (* TAIL SORT-IRRELEVANT EQUIVALENCE ON TERMS ********************************)
20 inductive tueq: relation term ≝
21 | tueq_sort: ∀s1,s2. tueq (⋆s1) (⋆s2)
22 | tueq_lref: ∀i. tueq (#i) (#i)
23 | tueq_gref: ∀l. tueq (§l) (§l)
24 | tueq_bind: ∀p,I,V,T1,T2. tueq T1 T2 → tueq (ⓑ{p,I}V.T1) (ⓑ{p,I}V.T2)
25 | tueq_appl: ∀V,T1,T2. tueq T1 T2 → tueq (ⓐV.T1) (ⓐV.T2)
26 | tueq_cast: ∀V1,V2,T1,T2. tueq V1 V2 → tueq T1 T2 → tueq (ⓝV1.T1) (ⓝV2.T2)
30 "context-free tail sort-irrelevant equivalence (term)"
31 'ApproxEq T1 T2 = (tueq T1 T2).
33 (* Basic properties *********************************************************)
35 lemma tueq_refl: reflexive … tueq.
36 #T elim T -T * [|||| * ]
37 /2 width=1 by tueq_sort, tueq_lref, tueq_gref, tueq_bind, tueq_appl, tueq_cast/
40 lemma tueq_sym: symmetric … tueq.
41 #T1 #T2 #H elim H -T1 -T2
42 /2 width=3 by tueq_sort, tueq_bind, tueq_appl, tueq_cast/
45 (* Left basic inversion lemmas **********************************************)
47 fact tueq_inv_sort1_aux: ∀X,Y. X ≅ Y → ∀s1. X = ⋆s1 →
50 [ #s1 #s2 #s #H destruct /2 width=2 by ex_intro/
53 | #p #I #V #T1 #T2 #_ #s #H destruct
54 | #V #T1 #T2 #_ #s #H destruct
55 | #V1 #V2 #T1 #T2 #_ #_ #s #H destruct
59 lemma tueq_inv_sort1: ∀Y,s1. ⋆s1 ≅ Y →
61 /2 width=4 by tueq_inv_sort1_aux/ qed-.
63 fact tueq_inv_lref1_aux: ∀X,Y. X ≅ Y → ∀i. X = #i → Y = #i.
65 [ #s1 #s2 #j #H destruct
66 | #p #I #V #T1 #T2 #_ #j #H destruct
67 | #V #T1 #T2 #_ #j #H destruct
68 | #V1 #V2 #T1 #T2 #_ #_ #j #H destruct
72 lemma tueq_inv_lref1: ∀Y,i. #i ≅ Y → Y = #i.
73 /2 width=5 by tueq_inv_lref1_aux/ qed-.
75 fact tueq_inv_gref1_aux: ∀X,Y. X ≅ Y → ∀l. X = §l → Y = §l.
77 [ #s1 #s2 #k #H destruct
78 | #p #I #V #T1 #T2 #_ #k #H destruct
79 | #V #T1 #T2 #_ #k #H destruct
80 | #V1 #V2 #T1 #T2 #_ #_ #k #H destruct
84 lemma tueq_inv_gref1: ∀Y,l. §l ≅ Y → Y = §l.
85 /2 width=5 by tueq_inv_gref1_aux/ qed-.
87 fact tueq_inv_bind1_aux: ∀X,Y. X ≅ Y → ∀p,I,V,T1. X = ⓑ{p,I}V.T1 →
88 ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
90 [ #s1 #s2 #q #J #W #U1 #H destruct
91 | #i #q #J #W #U1 #H destruct
92 | #l #q #J #W #U1 #H destruct
93 | #p #I #V #T1 #T2 #HT #q #J #W #U1 #H destruct /2 width=3 by ex2_intro/
94 | #V #T1 #T2 #_ #q #J #W #U1 #H destruct
95 | #V1 #V2 #T1 #T2 #_ #_ #q #J #W #U1 #H destruct
99 lemma tueq_inv_bind1: ∀p,I,V,T1,Y. ⓑ{p,I}V.T1 ≅ Y →
100 ∃∃T2. T1 ≅ T2 & Y = ⓑ{p,I}V.T2.
101 /2 width=3 by tueq_inv_bind1_aux/ qed-.
103 fact tueq_inv_appl1_aux: ∀X,Y. X ≅ Y → ∀V,T1. X = ⓐV.T1 →
104 ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
106 [ #s1 #s2 #W #U1 #H destruct
107 | #i #W #U1 #H destruct
108 | #l #W #U1 #H destruct
109 | #p #I #V #T1 #T2 #_ #W #U1 #H destruct
110 | #V #T1 #T2 #HT #W #U1 #H destruct /2 width=3 by ex2_intro/
111 | #V1 #V2 #T1 #T2 #_ #_ #W #U1 #H destruct
115 lemma tueq_inv_appl1: ∀V,T1,Y. ⓐV.T1 ≅ Y →
116 ∃∃T2. T1 ≅ T2 & Y = ⓐV.T2.
117 /2 width=3 by tueq_inv_appl1_aux/ qed-.
119 fact tueq_inv_cast1_aux: ∀X,Y. X ≅ Y → ∀V1,T1. X = ⓝV1.T1 →
120 ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
122 [ #s1 #s2 #W1 #U1 #H destruct
123 | #i #W1 #U1 #H destruct
124 | #l #W1 #U1 #H destruct
125 | #p #I #V #T1 #T2 #_ #W1 #U1 #H destruct
126 | #V #T1 #T2 #_ #W1 #U1 #H destruct
127 | #V1 #V2 #T1 #T2 #HV #HT #W1 #U1 #H destruct /2 width=5 by ex3_2_intro/
131 lemma tueq_inv_cast1: ∀V1,T1,Y. ⓝV1.T1 ≅ Y →
132 ∃∃V2,T2. V1 ≅ V2 & T1 ≅ T2 & Y = ⓝV2.T2.
133 /2 width=3 by tueq_inv_cast1_aux/ qed-.
135 (* Right basic inversion lemmas *********************************************)
137 lemma tueq_inv_bind2: ∀p,I,V,T2,X1. X1 ≅ ⓑ{p,I}V.T2 →
138 ∃∃T1. T1 ≅ T2 & X1 = ⓑ{p,I}V.T1.
140 elim (tueq_inv_bind1 p I V T2 X1)
141 [ #T1 #HT #H destruct ]
142 /3 width=3 by tueq_sym, ex2_intro/