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 "ground/lib/functions.ma".
16 include "apps_2/functional/flifts_flifts_basic.ma".
17 include "apps_2/functional/mf_vpush.ma".
19 (* MULTIPLE FILLING PUSH ****************************************************)
21 (* Properties with extensional equivalence **********************************)
23 lemma mf_lc_id: ⇡[0←#0]mf_li ⊜ mf_li.
24 #i elim (eq_or_gt i) #Hi destruct //
25 >mf_vpush_gt // >(flifts_lref_uni 1) <(S_pred … Hi) in ⊢ (???%); -Hi //
28 lemma mf_vpush_comp (i): compatible_3 … (mf_vpush i) (eq …) (exteq …) (exteq …).
29 #i #T1 #T2 #HT12 #lv1 #lv2 #Hlv #j
30 elim (lt_or_eq_or_gt j i) #Hij destruct
31 [ >mf_vpush_lt // >mf_vpush_lt //
32 | >mf_vpush_eq >mf_vpush_eq //
33 | >mf_vpush_gt // >mf_vpush_gt //
37 (* Main properties with extensional equivalence *****************************)
39 theorem mf_vpush_swap: ∀l1,l2. l2 ≤ l1 →
40 ∀v,T1,T2. ⇡[l2←T2]⇡[l1←T1]v ⊜ ⇡[↑l1←↑[l2,1]T1]⇡[l2←T2]v.
41 #l1 #l2 #Hl21 #v #T1 #T2 #i
42 elim (lt_or_eq_or_gt i l2) #Hl2 destruct
43 [ lapply (lt_to_le_to_lt … Hl2 Hl21) #Hl1
44 >mf_vpush_lt // >mf_vpush_lt // >mf_vpush_lt /2 width=1 by lt_S/ >mf_vpush_lt //
45 | >mf_vpush_eq >mf_vpush_lt /2 width=1 by monotonic_le_plus_l/
46 | >mf_vpush_gt // elim (lt_or_eq_or_gt (↓i) l1) #Hl1 destruct
47 [ >mf_vpush_lt // >mf_vpush_lt /2 width=1 by lt_minus_to_plus/ >mf_vpush_gt //
48 | >mf_vpush_eq <(lt_succ_pred … Hl2) >mf_vpush_eq //
49 | lapply (le_to_lt_to_lt … Hl21 Hl1) -Hl2 #Hl2
50 >mf_vpush_gt // >mf_vpush_gt /2 width=1 by lt_minus_to_plus_r/ >mf_vpush_gt //
51 /2 width=1 by flifts_basic_swap/