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