(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "delayed_updating/unwind1/unwind_eq.ma".
include "delayed_updating/syntax/path_structure.ma".
include "delayed_updating/syntax/path_inner.ma".
include "delayed_updating/syntax/path_proper.ma".
include "ground/xoa/ex_4_2.ma".

(* UNWIND FOR PATH *********************************************************)

(* Basic constructions with structure **************************************)

lemma structure_unwind (p) (f):
      ⊗p = ⊗▼[f]p.
#p @(path_ind_unwind … p) -p // #p #IH #f
<unwind_path_L_sn //
qed.

lemma unwind_structure (p) (f):
      ⊗p = ▼[f]⊗p.
#p @(path_ind_unwind … p) -p //
qed.

(* Destructions with structure **********************************************)

lemma unwind_des_structure (q) (p) (f):
      ⊗q = ▼[f]p → ⊗q = ⊗p.
// qed-.

(* Constructions with proper condition for path *****************************)

lemma unwind_append_proper_dx (p2) (p1) (f): p2 ϵ 𝐏 →
      (⊗p1)●(▼[▼[p1]f]p2) = ▼[f](p1●p2).
#p2 #p1 @(path_ind_unwind … p1) -p1 //
[ #n | #n #l #p1 |*: #p1 ] #IH #f #Hp2
[ elim (ppc_inv_lcons … Hp2) -Hp2 #l #q #H destruct //
| <unwind_path_d_lcons <IH //
| <unwind_path_m_sn <IH //
| <unwind_path_L_sn <IH //
| <unwind_path_A_sn <IH //
| <unwind_path_S_sn <IH //
]
qed-.

(* Constructions with inner condition for path ******************************)

lemma unwind_append_inner_sn (p1) (p2) (f): p1 ϵ 𝐈 →
      (⊗p1)●(▼[▼[p1]f]p2) = ▼[f](p1●p2).
#p1 @(list_ind_rcons … p1) -p1 // #p1 *
[ #n ] #_ #p2 #f #Hp1
[ elim (pic_inv_d_dx … Hp1)
| <list_append_rcons_sn <unwind_append_proper_dx //
| <list_append_rcons_sn <unwind_append_proper_dx //
  <structure_L_dx <list_append_rcons_sn //
| <list_append_rcons_sn <unwind_append_proper_dx //
  <structure_A_dx <list_append_rcons_sn //
| <list_append_rcons_sn <unwind_append_proper_dx //
  <structure_S_dx <list_append_rcons_sn //
]
qed-.

(* Advanced constructions with proj_path ************************************)

lemma unwind_path_d_empty_dx (n) (p) (f):
      (⊗p)◖𝗱((▼[p]f)＠⧣❨n❩) = ▼[f](p◖𝗱n).
#n #p #f <unwind_append_proper_dx // 
qed.

lemma unwind_path_m_dx (p) (f):
      ⊗p = ▼[f](p◖𝗺).
#p #f <unwind_append_proper_dx //
qed.

lemma unwind_path_L_dx (p) (f):
      (⊗p)◖𝗟 = ▼[f](p◖𝗟).
#p #f <unwind_append_proper_dx //
qed.

lemma unwind_path_A_dx (p) (f):
      (⊗p)◖𝗔 = ▼[f](p◖𝗔).
#p #f <unwind_append_proper_dx //
qed.

lemma unwind_path_S_dx (p) (f):
      (⊗p)◖𝗦 = ▼[f](p◖𝗦).
#p #f <unwind_append_proper_dx //
qed.

lemma unwind_path_root (f) (p):
      ∃∃r. 𝐞 = ⊗r & ⊗p●r = ▼[f]p.
#f #p @(list_ind_rcons … p) -p
[ /2 width=3 by ex2_intro/
| #p * [ #n ] /2 width=3 by ex2_intro/
]
qed-.

(* Advanced inversions with proj_path ***************************************)

lemma unwind_path_inv_d_sn (k) (q) (p) (f):
      (𝗱k◗q) = ▼[f]p →
      ∃∃r,h. 𝐞 = ⊗r & (▼[r]f)＠⧣❨h❩ = k & 𝐞 = q & r◖𝗱h = p.
#k #q #p @(path_ind_unwind … p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <unwind_path_empty #H destruct
| <unwind_path_d_empty #H destruct -IH
  /2 width=5 by ex4_2_intro/
| <unwind_path_d_lcons #H
  elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
  /2 width=5 by ex4_2_intro/
| <unwind_path_m_sn #H
  elim (IH … H) -IH -H #r #h #Hr #Hh #Hq #Hp destruct
  /2 width=5 by ex4_2_intro/
| <unwind_path_L_sn #H destruct
| <unwind_path_A_sn #H destruct
| <unwind_path_S_sn #H destruct
]
qed-.

lemma unwind_path_inv_m_sn (q) (p) (f):
      (𝗺◗q) = ▼[f]p → ⊥.
#q #p @(path_ind_unwind … p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <unwind_path_empty #H destruct
| <unwind_path_d_empty #H destruct
| <unwind_path_d_lcons #H /2 width=2 by/
| <unwind_path_m_sn #H /2 width=2 by/
| <unwind_path_L_sn #H destruct
| <unwind_path_A_sn #H destruct
| <unwind_path_S_sn #H destruct
]
qed-.

lemma unwind_path_inv_L_sn (q) (p) (f):
      (𝗟◗q) = ▼[f]p →
      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[⫯▼[r1]f]r2 & r1●𝗟◗r2 = p.
#q #p @(path_ind_unwind … p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <unwind_path_empty #H destruct
| <unwind_path_d_empty #H destruct
| <unwind_path_d_lcons #H
  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
  /2 width=5 by ex3_2_intro/
| <unwind_path_m_sn #H
  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
  /2 width=5 by ex3_2_intro/
| <unwind_path_L_sn #H destruct -IH
  /2 width=5 by ex3_2_intro/
| <unwind_path_A_sn #H destruct
| <unwind_path_S_sn #H destruct
]
qed-.

lemma unwind_path_inv_A_sn (q) (p) (f):
      (𝗔◗q) = ▼[f]p →
      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▼[r1]f]r2 & r1●𝗔◗r2 = p.
#q #p @(path_ind_unwind … p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <unwind_path_empty #H destruct
| <unwind_path_d_empty #H destruct
| <unwind_path_d_lcons #H
  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
  /2 width=5 by ex3_2_intro/
| <unwind_path_m_sn #H
  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
  /2 width=5 by ex3_2_intro/
| <unwind_path_L_sn #H destruct
| <unwind_path_A_sn #H destruct -IH
  /2 width=5 by ex3_2_intro/
| <unwind_path_S_sn #H destruct
]
qed-.

lemma unwind_path_inv_S_sn (q) (p) (f):
      (𝗦◗q) = ▼[f]p →
      ∃∃r1,r2. 𝐞 = ⊗r1 & q = ▼[▼[r1]f]r2 & r1●𝗦◗r2 = p.
#q #p @(path_ind_unwind … p) -p
[| #n | #n #l #p |*: #p ] [|*: #IH ] #f
[ <unwind_path_empty #H destruct
| <unwind_path_d_empty #H destruct
| <unwind_path_d_lcons #H
  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
  /2 width=5 by ex3_2_intro/
| <unwind_path_m_sn #H
  elim (IH … H) -IH -H #r1 #r2 #Hr1 #Hq #Hp destruct
  /2 width=5 by ex3_2_intro/| <unwind_path_L_sn #H destruct
| <unwind_path_A_sn #H destruct
| <unwind_path_S_sn #H destruct -IH
  /2 width=5 by ex3_2_intro/
]
qed-.

(* Inversions with proper condition for path ********************************)

lemma unwind_inv_append_proper_dx (q2) (q1) (p) (f):
      q2 ϵ 𝐏 → q1●q2 = ▼[f]p →
      ∃∃p1,p2. ⊗p1 = q1 & ▼[▼[p1]f]p2 = q2 & p1●p2 = p.
#q2 #q1 elim q1 -q1
[ #p #f #Hq2 <list_append_empty_sn #H destruct
  /2 width=5 by ex3_2_intro/
| * [ #n1 ] #q1 #IH #p #f #Hq2 <list_append_lcons_sn #H
  [ elim (unwind_path_inv_d_sn … H) -H #r1 #m1 #_ #_ #H0 #_ -IH
    elim (eq_inv_list_empty_append … H0) -H0 #_ #H0 destruct
    elim Hq2 -Hq2 //
  | elim (unwind_path_inv_m_sn … H)
  | elim (unwind_path_inv_L_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
    @(ex3_2_intro … (r1●𝗟◗p1)) //
    <structure_append <Hr1 -Hr1 //
  | elim (unwind_path_inv_A_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
    @(ex3_2_intro … (r1●𝗔◗p1)) //
    <structure_append <Hr1 -Hr1 //
  | elim (unwind_path_inv_S_sn … H) -H #r1 #s1 #Hr1 #Hs1 #H0 destruct
    elim (IH … Hs1) -IH -Hs1 // -Hq2 #p1 #p2 #H1 #H2 #H3 destruct
    @(ex3_2_intro … (r1●𝗦◗p1)) //
    <structure_append <Hr1 -Hr1 //
  ]
]
qed-.

(* Inversions with inner condition for path *********************************)

lemma unwind_inv_append_inner_sn (q1) (q2) (p) (f):
      q1 ϵ 𝐈 → q1●q2 = ▼[f]p →
      ∃∃p1,p2. ⊗p1 = q1 & ▼[▼[p1]f]p2 = q2 & p1●p2 = p.
#q1 @(list_ind_rcons … q1) -q1
[ #q2 #p #f #Hq1 <list_append_empty_sn #H destruct
  /2 width=5 by ex3_2_intro/
| #q1 * [ #n1 ] #_ #q2 #p #f #Hq2
  [ elim (pic_inv_d_dx … Hq2)
  | <list_append_rcons_sn #H0
    elim (unwind_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
    elim (unwind_path_inv_m_sn … (sym_eq … H2))
  | <list_append_rcons_sn #H0
    elim (unwind_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
    elim (unwind_path_inv_L_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
    @(ex3_2_intro … (p1●r2◖𝗟)) [1,3: // ]
    [ <structure_append <structure_L_dx <Hr2 -Hr2 //
    | <list_append_assoc <list_append_rcons_sn //
    ]
  | <list_append_rcons_sn #H0
    elim (unwind_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
    elim (unwind_path_inv_A_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
    @(ex3_2_intro … (p1●r2◖𝗔)) [1,3: // ]
    [ <structure_append <structure_A_dx <Hr2 -Hr2 //
    | <list_append_assoc <list_append_rcons_sn //
    ]
  | <list_append_rcons_sn #H0
    elim (unwind_inv_append_proper_dx … H0) -H0 // #p1 #p2 #H1 #H2 #H3 destruct
    elim (unwind_path_inv_S_sn … (sym_eq … H2)) -H2 #r2 #s2 #Hr2 #Hs2 #H0 destruct
    @(ex3_2_intro … (p1●r2◖𝗦)) [1,3: // ]
    [ <structure_append <structure_S_dx <Hr2 -Hr2 //
    | <list_append_assoc <list_append_rcons_sn //
    ]
  ]
]
qed-.