matita/matita/contribs/lambdadelta/apps_2/functional/mf_vpush_exteq.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground/lib/functions.ma".
  16 include "apps_2/functional/flifts_flifts_basic.ma".
  17 include "apps_2/functional/mf_vpush.ma".
  18
  19 (* MULTIPLE FILLING PUSH ****************************************************)
  20
  21 (* Properties with extensional equivalence **********************************)
  22
  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 //
  26 qed.
  27
  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 //
  34 ]
  35 qed-.
  36
  37 (* Main properties with extensional equivalence *****************************)
  38
  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/
  52   ]
  53 ]
  54 qed-.