matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.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 "basic_2/rt_transition/cpm_drops.ma".
  16 include "basic_2/rt_transition/cpr.ma".
  17 include "apps_2/functional/mf_exteq.ma".
  18
  19 (* MULTIPLE FILLING FOR TERMS ***********************************************)
  20
  21 (* Properties with relocation ***********************************************)
  22
  23 lemma mf_delta_drops (h) (G): ∀K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 →
  24                               ∀T,L,l. ⬇*[l] L ≘ K.ⓓV1 →
  25                               ∀gv,lv. ⦃G, L⦄ ⊢ ●[gv,⇡[l←#l]lv]T ➡[h] ●[gv,⇡[l←↑[↑l]V2]lv]T.
  26 #h #G #K #V1 #V2 #HV #T elim T -T * //
  27 [ #i #L #l #HKL #gv #lv
  28   >mf_lref >mf_lref
  29   elim (lt_or_eq_or_gt i l) #Hl destruct
  30   [ >(mf_vpush_lt … Hl) >(mf_vpush_lt … Hl) //
  31   | >mf_vpush_eq >mf_vpush_eq
  32     /2 width=6 by cpm_delta_drops/
  33   | >(mf_vpush_gt … Hl) >(mf_vpush_gt … Hl) //
  34   ]
  35 | #p #I #V #T #IHV #IHT #L #l #HLK #gv #lv
  36   >mf_bind >mf_bind
  37   >(mf_comp … T) in ⊢ (?????%?);
  38   [2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
  39   >(mf_comp … T) in ⊢ (??????%);
  40   [2: @mf_vpush_swap // |4: @exteq_refl |3,5: skip ]
  41   >(flifts_lref_uni 1 l) >(flifts_compose_uni 1 (↑l))
  42   /4 width=1 by cpm_bind, drops_drop/
  43 | #I #V #T #IHV #IHT #L #l #HLK #gv #lv
  44   >mf_flat >mf_flat /3 width=1 by cpr_flat/
  45 ]
  46 qed.