matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind2_path.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/unwind0/unwind1_path.ma".
  16 include "delayed_updating/notation/functions/black_downtriangle_2.ma".
  17
  18 (* EXTENDED UNWIND FOR PATH *************************************************)
  19
  20 definition unwind2_path (f) (p) ≝
  21            ▼↑[f]p.
  22
  23 interpretation
  24   "extended unwind (path)"
  25   'BlackDownTriangle f p = (unwind2_path f p).
  26
  27 (* Basic constructions ******************************************************)
  28
  29 lemma unwind2_path_unfold (f) (p):
  30       ▼↑[f]p = ▼[f]p.
  31 // qed.
  32
  33 lemma unwind2_path_id (p):
  34       ▼p = ▼[𝐢]p.
  35 // qed.
  36
  37 lemma unwind2_path_empty (f):
  38       (𝐞) = ▼[f]𝐞.
  39 // qed.
  40
  41 lemma unwind2_path_d_empty (f) (n):
  42       (𝗱(f@❨n❩)◗𝐞) = ▼[f](𝗱n◗𝐞).
  43 // qed.
  44
  45 lemma unwind2_path_d_lcons (f) (p) (l) (n:pnat):
  46       ▼[𝐮❨f@❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
  47 #f #p #l #n
  48 <unwind2_path_unfold in ⊢ (???%);
  49 <lift_path_d_sn <lift_path_id <unwind1_path_d_lcons //
  50 qed.
  51
  52 lemma unwind2_path_m_sn (f) (p):
  53       ▼[f]p = ▼[f](𝗺◗p).
  54 #f #p
  55 <unwind2_path_unfold in ⊢ (???%);
  56 <lift_path_m_sn //
  57 qed.
  58
  59 lemma unwind2_path_L_sn (f) (p):
  60       (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
  61 #f #p
  62 <unwind2_path_unfold in ⊢ (???%);
  63 <lift_path_L_sn //
  64 qed.
  65
  66 lemma unwind2_path_A_sn (f) (p):
  67       (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
  68 #f #p
  69 <unwind2_path_unfold in ⊢ (???%);
  70 <lift_path_A_sn //
  71 qed.
  72
  73 lemma unwind2_path_S_sn (f) (p):
  74       (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
  75 #f #p
  76 <unwind2_path_unfold in ⊢ (???%);
  77 <lift_path_S_sn //
  78 qed.
  79
  80 (* Main constructions *******************************************************)
  81
  82 theorem unwind2_path_after_id_sn (p) (f):
  83         ▼[f]p = ▼▼[f]p.
  84 // qed.
  85
  86 (* Constructions with stream_eq *********************************************)
  87
  88 lemma unwind2_path_eq_repl (p):
  89       stream_eq_repl … (λf1,f2. ▼[f1]p = ▼[f2]p).
  90 #p #f1 #f2 #Hf
  91 <unwind2_path_unfold <unwind2_path_unfold
  92 <(lift_path_eq_repl … Hf) -Hf //
  93 qed.
  94
  95 (* Advanced eliminations with path ******************************************)
  96
  97 lemma path_ind_unwind2 (Q:predicate …):
  98       Q (𝐞) →
  99       (∀n. Q (𝐞) → Q (𝗱n◗𝐞)) →
 100       (∀n,l,p. Q (l◗p) → Q (𝗱n◗l◗p)) →
 101       (∀p. Q p → Q (𝗺◗p)) →
 102       (∀p. Q p → Q (𝗟◗p)) →
 103       (∀p. Q p → Q (𝗔◗p)) →
 104       (∀p. Q p → Q (𝗦◗p)) →
 105       ∀p. Q p.
 106 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
 107 elim p -p [| * [ #n * ] ]
 108 /2 width=1 by/
 109 qed-.