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/unwind/unwind2_path.ma".
16 include "delayed_updating/unwind/unwind_gen_structure.ma".
18 (* UNWIND FOR PATH **********************************************************)
20 (* Constructions with list_rcons ********************************************)
22 lemma unwind2_path_d_dx (f) (p) (n) :
23 (⊗p)◖𝗱((▶[f](pᴿ))@⧣❨n❩) = ▼[f](p◖𝗱n).
24 #f #p #n <unwind2_path_unfold
28 lemma unwind2_path_m_dx (f) (p):
30 #f #p <unwind2_path_unfold //
33 lemma unwind2_path_L_dx (f) (p):
35 #f #p <unwind2_path_unfold //
38 lemma unwind2_path_A_dx (f) (p):
40 #f #p <unwind2_path_unfold //
43 lemma unwind2_path_S_dx (f) (p):
45 #f #p <unwind2_path_unfold //
48 lemma unwind2_path_root (f) (p):
49 ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
51 elim (unwind_gen_root)
52 /2 width=3 by ex2_intro/
55 (* Constructions with proper condition for path *****************************)
57 lemma unwind2_path_append_proper_dx (f) (p1) (p2): p2 ϵ 𝐏 →
58 (⊗p1)●(▼[▶[f]p1ᴿ]p2) = ▼[f](p1●p2).
59 #f #p1 #p2 #Hp2 <unwind2_path_unfold <unwind2_path_unfold
60 <unwind_gen_append_proper_dx // -Hp2 <reverse_append
61 @(list_ind_rcons … p2) -p2 // #q2 #l2 #_
62 <reverse_rcons <list_tl_lcons <list_tl_lcons //
65 (* Constructions with inner condition for path ******************************)
67 lemma unwind2_path_append_inner_sn (f) (p1) (p2): p1 ϵ 𝐈 →
68 (⊗p1)●(▼[▶[f]p1ᴿ]p2) = ▼[f](p1●p2).
69 #f #p1 #p2 #Hp1 <unwind2_path_unfold <unwind2_path_unfold
70 <unwind_gen_append_inner_sn // -Hp1 <reverse_append
71 @(list_ind_rcons … p2) -p2 // #q2 #l2 #_
72 <reverse_rcons <list_tl_lcons <list_tl_lcons //
75 (* Inversions with list_lcons ***********************************************)
77 lemma unwind2_path_inv_S_sn (f) (p) (q):
79 ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▶[f]r1ᴿ]r2 & r1●𝗦◗r2 = p.
81 elim (unwind_gen_inv_S_sn … H0) -H0 #r1 #r2 #Hr1 #H1 #H2 destruct
82 <reverse_append <reverse_lcons
83 @(list_ind_rcons … r2) -r2 [ /2 width=5 by ex3_2_intro/ ] #r2 #l2 #_
84 <reverse_rcons <list_append_lcons_sn <list_append_rcons_sn
85 <list_tl_lcons <unwind2_rmap_append <unwind2_rmap_S_sn
86 /2 width=5 by ex3_2_intro/
89 (* Inversions with proper condition for path ********************************)
91 lemma unwind2_path_inv_append_proper_dx (f) (p) (q1) (q2):
92 q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
93 ∃∃p1,p2. ⊗p1 = q1 & ▼[▶[f]p1ᴿ]p2 = q2 & p1●p2 = p.
94 #f #p #q1 #q2 #Hq2 #H0
95 elim (unwind_gen_inv_append_proper_dx … Hq2 H0) -Hq2 -H0
96 #p1 #p2 #H1 #H2 #H3 destruct <reverse_append
97 @(list_ind_rcons … p2) -p2 [ /2 width=5 by ex3_2_intro/ ] #q2 #l2 #_
98 <reverse_rcons <list_tl_lcons <unwind2_rmap_append
99 @ex3_2_intro [4: |*: // ] <unwind2_path_unfold // (**) (* auto fails *)
102 (* Inversions with inner condition for path *********************************)
104 lemma unwind2_path_inv_append_inner_sn (f) (p) (q1) (q2):
105 q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
106 ∃∃p1,p2. ⊗p1 = q1 & ▼[▶[f]p1ᴿ]p2 = q2 & p1●p2 = p.
107 #f #p #q1 #q2 #Hq1 #H0
108 elim (unwind_gen_inv_append_inner_sn … Hq1 H0) -Hq1 -H0
109 #p1 #p2 #H1 #H2 #H3 destruct <reverse_append
110 @(list_ind_rcons … p2) -p2 [ /2 width=5 by ex3_2_intro/ ] #q2 #l2 #_
111 <reverse_rcons <list_tl_lcons <unwind2_rmap_append
112 @ex3_2_intro [4: |*: // ] <unwind2_path_unfold // (**) (* auto fails *)
115 (* Destructions with inner condition for path *******************************)
117 lemma unwind2_path_des_inner (f) (p):
119 #f #p @(list_ind_rcons … p) -p //
121 <unwind2_path_d_dx #H0
122 elim (pic_inv_d_dx … H0)