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_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".
  19
  20 (* MULTIPLE FILLING PUSH ****************************************************)
  21
  22 (* Properties with extensional equivalence **********************************)
  23
  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 //
  27 qed.
  28
  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 //
  35 ]
  36 qed-.
  37
  38 (* Main properties with extensional equivalence *****************************)
  39
  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/
  53   ]
  54 ]
  55 qed-.