1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "delayed_updating/unwind0/unwind1_path.ma".
16 include "delayed_updating/notation/functions/black_downtriangle_2.ma".
18 (* EXTENDED UNWIND FOR PATH *************************************************)
20 definition unwind2_path (f) (p) ≝
24 "extended unwind (path)"
25 'BlackDownTriangle f p = (unwind2_path f p).
27 (* Basic constructions ******************************************************)
29 lemma unwind2_path_unfold (f) (p):
33 lemma unwind2_path_id (p):
37 lemma unwind2_path_empty (f):
41 lemma unwind2_path_d_empty (f) (n):
42 (𝗱(f@❨n❩)◗𝐞) = ▼[f](𝗱n◗𝐞).
45 lemma unwind2_path_d_lcons (f) (p) (l) (n:pnat):
46 ▼[𝐮❨f@❨n❩❩](l◗p) = ▼[f](𝗱n◗l◗p).
48 <unwind2_path_unfold in ⊢ (???%);
49 <lift_path_d_sn <lift_path_id <unwind1_path_d_lcons //
52 lemma unwind2_path_m_sn (f) (p):
55 <unwind2_path_unfold in ⊢ (???%);
59 lemma unwind2_path_L_sn (f) (p):
60 (𝗟◗▼[⫯f]p) = ▼[f](𝗟◗p).
62 <unwind2_path_unfold in ⊢ (???%);
66 lemma unwind2_path_A_sn (f) (p):
67 (𝗔◗▼[f]p) = ▼[f](𝗔◗p).
69 <unwind2_path_unfold in ⊢ (???%);
73 lemma unwind2_path_S_sn (f) (p):
74 (𝗦◗▼[f]p) = ▼[f](𝗦◗p).
76 <unwind2_path_unfold in ⊢ (???%);
80 (* Main constructions *******************************************************)
82 theorem unwind2_path_after_id_sn (p) (f):
86 (* Constructions with stream_eq *********************************************)
88 lemma unwind2_path_eq_repl (p):
89 stream_eq_repl … (λf1,f2. ▼[f1]p = ▼[f2]p).
91 <unwind2_path_unfold <unwind2_path_unfold
92 <(lift_path_eq_repl … Hf) -Hf //
95 (* Advanced eliminations with path ******************************************)
97 lemma path_ind_unwind2 (Q:predicate …):
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)) →
106 #Q #IH1 #IH2 #IH3 #IH4 #IH5 #IH6 #IH7 #p
107 elim p -p [| * [ #n * ] ]