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. ∀p,f. k1 p f = k2 p f.
  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, p, f❩ = ↑❨k2, p, f❩.
  31 #A #p elim p -p
  32 [ #k1 #k2 #f #Hk <lift_empty <lift_empty //
  33 | * [ #n * [| #l0 ]] [|*: #q ] #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       ↑❨λp2.k(l◗p2),p,f❩ = ↑{A}❨λp2.k((l◗𝐞)●p2),p,f❩.
  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       ↑❨λp2.k(p1●l◗p2),p,f❩ = ↑{A}❨λp2.k(p1◖l●p2),p,f❩.
  47 #A #k #f #p1 #p #l
  48 @lift_eq_repl_sn #p2 #g
  49 <list_append_rcons_sn //
  50 qed.
  51
  52 (* Basic constructions with proj_path ***************************************)
  53
  54 lemma lift_append_sn (p) (f) (q):
  55       q●↑[f]p = ↑❨(λp. proj_path (q●p)), p, f❩.
  56 #p elim p -p
  57 [ //
  58 | * [ #n * [| #l ]] [|*: #p ] #IH #f #q
  59   [ <lift_d_empty_sn <lift_d_empty_sn >lift_lcons_alt >lift_append_rcons_sn
  60     <IH <IH -IH <list_append_rcons_sn //
  61   | <lift_d_lcons_sn <lift_d_lcons_sn <IH -IH //
  62   | <lift_L_sn <lift_L_sn >lift_lcons_alt >lift_append_rcons_sn
  63     <IH <IH -IH <list_append_rcons_sn //
  64   | <lift_A_sn <lift_A_sn >lift_lcons_alt >lift_append_rcons_sn
  65     <IH <IH -IH <list_append_rcons_sn //
  66   | <lift_S_sn <lift_S_sn >lift_lcons_alt >lift_append_rcons_sn
  67     <IH <IH -IH <list_append_rcons_sn //
  68   ]
  69 ]
  70 qed.
  71
  72 lemma lift_lcons (f) (p) (l):
  73       l◗↑[f]p = ↑❨(λp. proj_path (l◗p)), p, f❩.
  74 #f #p #l
  75 >lift_lcons_alt <lift_append_sn //
  76 qed.