matita/matita/contribs/lambdadelta/delayed_updating/unwind0/unwind1_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/substitution/lift_length.ma".
  16 include "delayed_updating/notation/functions/black_downtriangle_1.ma".
  17 include "ground/relocation/tr_uni.ma".
  18
  19 (* BASIC UNWIND FOR PATH ****************************************************)
  20
  21 rec definition unwind1_path_pnat (n) (p) on n ≝
  22 match n with
  23 [ punit   ⇒ p
  24 | psucc m ⇒
  25   match p with
  26   [ list_empty     ⇒ 𝐞
  27   | list_lcons l q ⇒
  28     match l with
  29     [ label_d n ⇒
  30       match q with
  31       [ list_empty     ⇒ l◗(unwind1_path_pnat m q)
  32       | list_lcons _ _ ⇒ unwind1_path_pnat m (↑[𝐮❨n❩]q)
  33       ]
  34     | label_m   ⇒ unwind1_path_pnat m q
  35     | label_L   ⇒ 𝗟◗(unwind1_path_pnat m q)
  36     | label_A   ⇒ 𝗔◗(unwind1_path_pnat m q)
  37     | label_S   ⇒ 𝗦◗(unwind1_path_pnat m q)
  38     ]
  39   ]
  40 ].
  41
  42 definition unwind1_path (p) ≝
  43            unwind1_path_pnat (↑❘p❘) p.
  44
  45 interpretation
  46   "basic unwind (path)"
  47   'BlackDownTriangle p = (unwind1_path p).
  48
  49 (* Basic constructions ******************************************************)
  50
  51 lemma unwind1_path_unfold (p):
  52       unwind1_path_pnat (↑❘p❘) p = ▼p.
  53 // qed-.
  54
  55 lemma unwind1_path_empty:
  56       (𝐞) = ▼𝐞.
  57 // qed.
  58
  59 lemma unwind1_path_d_empty (n):
  60       (𝗱n◗𝐞) = ▼(𝗱n◗𝐞).
  61 // qed.
  62
  63 lemma unwind1_path_d_lcons (p) (l) (n:pnat):
  64       ▼(↑[𝐮❨n❩](l◗p)) = ▼(𝗱n◗l◗p).
  65 #p #l #n
  66 <unwind1_path_unfold <lift_path_length //
  67 qed.
  68
  69 lemma unwind1_path_m_sn (p):
  70       ▼p = ▼(𝗺◗p).
  71 // qed.
  72
  73 lemma unwind1_path_L_sn (p):
  74       (𝗟◗▼p) = ▼(𝗟◗p).
  75 // qed.
  76
  77 lemma unwind1_path_A_sn (p):
  78       (𝗔◗▼p) = ▼(𝗔◗p).
  79 // qed.
  80
  81 lemma unwind1_path_S_sn (p):
  82       (𝗦◗▼p) = ▼(𝗦◗p).
  83 // qed.
  84
  85 (* Main constructions *******************************************************)
  86
  87 fact unwind1_path_fix_aux (k) (p):
  88      k = ❘p❘ → ▼p = ▼▼p.
  89 #k @(nat_ind_succ … k) -k
  90 [ #p #H0 >(list_length_inv_zero_sn … H0) -p //
  91 | #k #IH *
  92   [ #H0 elim (eq_inv_nsucc_zero … H0)
  93   | * [ #n ] #p #H0
  94     lapply (eq_inv_nsucc_bi … H0) -H0
  95     [ cases p -p [ -IH | #l #p ] #H0 destruct //
  96       <unwind1_path_d_lcons <IH -IH //
  97     | #H0 destruct <unwind1_path_m_sn <IH -IH //
  98     | #H0 destruct <unwind1_path_L_sn <unwind1_path_L_sn <IH -IH //
  99     | #H0 destruct <unwind1_path_A_sn <unwind1_path_A_sn <IH -IH //
 100     | #H0 destruct <unwind1_path_S_sn <unwind1_path_S_sn <IH -IH //
 101     ]
 102   ]
 103 ]
 104 qed-.
 105
 106 theorem unwind1_path_fix (p):
 107         ▼p = ▼▼p.
 108 /2 width=2 by unwind1_path_fix_aux/ qed.