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/syntax/teqw.ma".
16 include "static_2/relocation/lifts_lifts.ma".
18 (* GENERIC RELOCATION FOR TERMS *********************************************)
20 (* Properties with sort-irrelevant whd equivalence for terms ****************)
22 lemma teqw_lifts_sn: liftable2_sn teqw.
23 #T1 #T2 #H elim H -T1 -T2
24 [ #s1 #s2 #f #X #H >(lifts_inv_sort1 … H) -H
25 /3 width=3 by lifts_sort, teqw_sort, ex2_intro/
26 | #i #f #X #H elim (lifts_inv_lref1 … H) -H
27 /3 width=3 by lifts_lref, teqw_lref, ex2_intro/
28 | #l #f #X #H >(lifts_inv_gref1 … H) -H
29 /2 width=3 by lifts_gref, teqw_gref, ex2_intro/
30 | #p #V1 #V2 #T1 #T2 #_ #IHT #f #X #H
31 elim (lifts_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
32 elim (lifts_total V2 f) #W2 #HVW2
33 elim (true_or_false p) #H destruct
34 [ elim (IHT … HTU1) -T1 [| // ] #U2 #HTU2 #HU12
35 | elim (lifts_total T2 (⫯f)) #U2 #HTU2
37 /3 width=4 by teqw_abbr_pos, lifts_bind, ex2_intro/
38 | #p #V1 #V2 #T1 #T2 #f #X #H
39 elim (lifts_inv_bind1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
40 elim (lifts_total V2 f) #W2 #HVW2
41 elim (lifts_total T2 (⫯f)) #U2 #HTU2
42 /3 width=3 by lifts_bind, ex2_intro/
43 | #V1 #V2 #T1 #T2 #_ #IHT #f #X #H
44 elim (lifts_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
45 elim (lifts_total V2 f) #W2 #HVW2
46 elim (IHT … HTU1) -T1 #U2 #HTU2 #HU12
47 /3 width=4 by lifts_flat, teqw_appl, ex2_intro/
48 | #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H
49 elim (lifts_inv_flat1 … H) -H #W1 #U1 #HVW1 #HTU1 #H destruct
50 elim (IHV … HVW1) -V1 #W2 #HVW2 #HW12
51 elim (IHT … HTU1) -T1 #U2 #HTU2 #HU12
52 /3 width=5 by lifts_flat, teqw_cast, ex2_intro/
56 lemma teqw_lifts_dx: liftable2_dx teqw.
57 /3 width=3 by teqw_lifts_sn, liftable2_sn_dx, teqw_sym/ qed-.
59 lemma teqw_lifts_bi: liftable2_bi teqw.
60 /3 width=6 by teqw_lifts_sn, liftable2_sn_bi/ qed-.
62 (* Inversion lemmas with sort-irrelevant whd equivalence for terms **********)
64 lemma teqw_inv_lifts_bi: deliftable2_bi teqw.
65 #U1 #U2 #H elim H -U1 -U2
66 [ #s1 #s2 #f #X1 #H1 #X2 #H2
67 >(lifts_inv_sort2 … H1) -H1 >(lifts_inv_sort2 … H2) -H2
68 /1 width=1 by teqw_sort/
69 | #j #f #X1 #H1 #X2 #H2
70 elim (lifts_inv_lref2 … H1) -H1 #i1 #Hj1 #H destruct
71 elim (lifts_inv_lref2 … H2) -H2 #i2 #Hj2 #H destruct
72 <(pr_pat_inj … Hj2 … Hj1) -j -f -i1
73 /1 width=1 by teqw_lref/
74 | #l #f #X1 #H1 #X2 #H2
75 >(lifts_inv_gref2 … H1) -H1 >(lifts_inv_gref2 … H2) -H2
76 /1 width=1 by teqw_gref/
77 | #p #W1 #W2 #U1 #U2 #_ #IH #f #X1 #H1 #X2 #H2
78 elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #HTU1 #H destruct -W1
79 elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #HTU2 #H destruct -W2
80 elim (true_or_false p) #H destruct
81 [ /3 width=3 by teqw_abbr_pos/
82 | /1 width=1 by teqw_abbr_neg/
84 | #p #W1 #W2 #U1 #U2 #f #X1 #H1 #X2 #H2
85 elim (lifts_inv_bind2 … H1) -H1 #V1 #T1 #_ #_ #H destruct -W1 -U1
86 elim (lifts_inv_bind2 … H2) -H2 #V2 #T2 #_ #_ #H destruct -W2 -U2
87 /1 width=1 by teqw_abst/
88 | #W1 #W2 #U1 #U2 #_ #IH #f #X1 #H1 #X2 #H2
89 elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #_ #HTU1 #H destruct -W1
90 elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #_ #HTU2 #H destruct -W2
91 /3 width=3 by teqw_appl/
92 | #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X1 #H1 #X2 #H2
93 elim (lifts_inv_flat2 … H1) -H1 #V1 #T1 #HVW1 #HTU1 #H destruct
94 elim (lifts_inv_flat2 … H2) -H2 #V2 #T2 #HVW2 #HTU2 #H destruct
95 /3 width=3 by teqw_cast/
99 lemma teqw_inv_abbr_pos_x_lifts_y_y (T) (f):
100 ∀V,U. +ⓓV.U ≃ T → ⇧*[f]T ≘ U → ⊥.
101 @(wf1_ind_nlt … tw) #n #IH #T #Hn #f #V #U #H1 #H2 destruct
102 elim (teqw_inv_abbr_pos_sn … H1) -H1 #X1 #X2 #HX2 #H destruct -V
103 elim (lifts_inv_bind1 … H2) -H2 #Y1 #Y2 #_ #HXY2 #H destruct