matita/matita/contribs/lambdadelta/delayed_updating/substitution/lift_eq.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 "delayed_updating/substitution/lift.ma".
  16 include "ground/notation/relations/ringeq_3.ma".
  17
  18 (* LIFT FOR PATH ***********************************************************)
  19
  20 definition lift_exteq (A): relation2 (lift_continuation A) (lift_continuation A) ≝
  21            λk1,k2. ∀f,p. k1 f p = k2 f p.
  22
  23 interpretation
  24   "extensional equivalence (lift continuation)"
  25   'RingEq A k1 k2 = (lift_exteq A k1 k2).
  26
  27 (* Constructions with lift_exteq ********************************************)
  28
  29 lemma lift_eq_repl_sn (A) (p) (k1) (k2) (f):
  30       k1 ≗{A} k2 → ↑❨k1, f, p❩ = ↑❨k2, f, p❩.
  31 #A #p @(path_ind_lift … p) -p [| #n | #n #l0 #q ]
  32 [ #k1 #k2 #f #Hk <lift_empty <lift_empty //
  33 |*: #IH #k1 #k2 #f #Hk /2 width=1 by/
  34 ]
  35 qed-.
  36
  37 (* Advanced constructions ***************************************************)
  38
  39 lemma lift_lcons_alt (A) (k) (f) (p) (l):
  40       ↑❨λg,p2. k g (l◗p2), f, p❩ = ↑{A}❨λg,p2. k g ((l◗𝐞)●p2), f, p❩.
  41 #A #k #f #p #l
  42 @lift_eq_repl_sn #p2 #g // (**) (* auto fails with typechecker failure *)
  43 qed.
  44
  45 lemma lift_append_rcons_sn (A) (k) (f) (p1) (p) (l):
  46       ↑❨λg,p2. k g (p1●l◗p2), f, p❩ = ↑{A}❨λg,p2. k g (p1◖l●p2), f, p❩.
  47 #A #k #f #p1 #p #l
  48 @lift_eq_repl_sn #p2 #g
  49 <list_append_rcons_sn //
  50 qed.
  51
  52 (* Advanced constructions with proj_path ************************************)
  53
  54 lemma lift_path_append_sn (p) (f) (q):
  55       q●↑[f]p = ↑❨(λg,p. proj_path g (q●p)), f, p❩.
  56 #p @(path_ind_lift … p) -p // [ #n #l #p |*: #p ] #IH #f #q
  57 [ <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
  58 | <lift_m_sn <lift_m_sn //
  59 | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
  60   <IH <IH -IH <list_append_rcons_sn //
  61 | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
  62   <IH <IH -IH <list_append_rcons_sn //
  63 | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
  64   <IH <IH -IH <list_append_rcons_sn //
  65 ]
  66 qed.
  67
  68 lemma lift_path_lcons (f) (p) (l):
  69       l◗↑[f]p = ↑❨(λg,p. proj_path g (l◗p)), f, p❩.
  70 #f #p #l
  71 >lift_lcons_alt <lift_path_append_sn //
  72 qed.
  73
  74 lemma lift_path_L_sn (f) (p):
  75       (𝗟◗↑[⫯f]p) = ↑[f](𝗟◗p).
  76 // qed.
  77
  78 lemma lift_path_A_sn (f) (p):
  79       (𝗔◗↑[f]p) = ↑[f](𝗔◗p).
  80 // qed.
  81
  82 lemma lift_path_S_sn (f) (p):
  83       (𝗦◗↑[f]p) = ↑[f](𝗦◗p).
  84 // qed.