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/shift.ma".
16 include "apps_2/models/vlifts.ma".
18 (* MULTIPLE LIFT FOR MODEL EVALUATIONS **************************************)
20 (* Properties with shift for restricted closures ****************************)
22 lemma vlifts_shift (M): is_model M → is_extensional M →
24 (∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v]) →
25 ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv].
26 #M #H1M #H2M #L elim L -L [| #K * [| * ]]
27 [ #T1 #T2 #gv #lv #H12
28 >shift_atom >shift_atom
29 /4 width=1 by vlifts_atom, veq_refl/
30 | #I #IH #T1 #T2 #gv #lv #H12
31 >shift_unit >shift_unit
32 /5 width=1 by vlifts_unit, mx, mr/
33 | #V #IH #T1 #T2 #gv #lv #H12
34 >shift_pair >shift_pair
36 @(mq … H1M) [3:|*: /3 width=2 by seq_sym, md/ ]
37 /4 width=1 by vlifts_abbr, mr/
38 | #W #IH #T1 #T2 #gv #lv #H12
39 >shift_pair >shift_pair
40 /5 width=1 by vlifts_abst, mx, mr/
44 (* Inversion lemmas with shift for restricted closures **********************)
46 lemma vlifts_inv_shift (M): is_model M →
47 ∀L,T1,T2,gv,lv. ⟦L+T1⟧[gv, lv] ≗{M} ⟦L+T2⟧[gv, lv] →
48 ∀v. L ⨁[gv] lv ≘ v → ⟦T1⟧[gv, v] ≗ ⟦T2⟧[gv, v].
49 #M #HM #L elim L -L [| #K * [| * ]]
51 >shift_atom >shift_atom #H12 #v #H
52 lapply (vlifts_inv_atom … H) -H // #Hv
53 /4 width=7 by ti_comp, veq_refl, mq/
54 | #I #IH #T1 #T2 #gv #lv
55 >shift_unit >shift_unit #H12 #y #H
56 elim (vlifts_inv_unit … H) -H // #v #d #Hlv #Hv
57 lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12
58 /4 width=7 by ti_comp, ti_fwd_mx_dx, veq_refl, mq/
59 | #V #IH #T1 #T2 #gv #lv
60 >shift_pair >shift_pair #H12 #y #H
61 elim (vlifts_inv_abbr … H) -H // #v #Hlv #Hv
62 lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12
63 /4 width=7 by ti_comp, veq_refl, md, mq/
64 | #W #IH #T1 #T2 #gv #lv
65 >shift_pair >shift_pair #H12 #y #H
66 elim (vlifts_inv_abst … H) -H // #v #d #Hlv #Hv
67 lapply (IH … H12 … Hlv) -IH -H12 -Hlv #H12
68 /4 width=7 by ti_comp, ti_fwd_mx_dx, veq_refl, mq/