(**************************************************************************)
(*       ___                                                              *)
(*      ||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/syntax/path_labels.ma".
include "delayed_updating/notation/functions/downarrowright_2.ma".
include "ground/arith/nat_plus.ma".
include "ground/arith/nat_pred_succ.ma".

(* HEAD FOR PATH ************************************************************)

rec definition path_head (n) (p) on p: path ≝
match n with
[ nzero  ⇒ 𝐞
| ninj m ⇒
  match p with
  [ list_empty     ⇒ 𝗟∗∗n
  | list_lcons l q ⇒
    match l with
    [ label_d k ⇒ (path_head (n+k) q)◖l
    | label_m   ⇒ (path_head n q)◖l
    | label_L   ⇒ (path_head (↓m) q)◖l
    | label_A   ⇒ (path_head n q)◖l
    | label_S   ⇒ (path_head n q)◖l
    ]
  ]
].

interpretation
  "head (path)"
  'DownArrowRight n p = (path_head n p).

(* basic constructions ****************************************************)

lemma path_head_zero (p):
      (𝐞) = ↳[𝟎]p.
* // qed.

lemma path_head_empty (n):
      (𝗟∗∗n) = ↳[n]𝐞.
* // qed.

lemma path_head_d_dx (p) (n) (k:pnat):
      (↳[↑n+k]p)◖𝗱k = ↳[↑n](p◖𝗱k).
// qed.

lemma path_head_m_dx (p) (n):
      (↳[↑n]p)◖𝗺 = ↳[↑n](p◖𝗺).
// qed.

lemma path_head_L_dx (p) (n):
      (↳[n]p)◖𝗟 = ↳[↑n](p◖𝗟).
#p #n
whd in ⊢ (???%); //
qed.

lemma path_head_A_dx (p) (n):
      (↳[↑n]p)◖𝗔 = ↳[↑n](p◖𝗔).
// qed.

lemma path_head_S_dx (p) (n):
      (↳[↑n]p)◖𝗦 = ↳[↑n](p◖𝗦).
// qed.

(* Basic inversions *********************************************************)

lemma eq_inv_path_head_zero_dx (q) (p):
      q = ↳[𝟎]p → 𝐞 = q.
#q * //
qed-.

lemma eq_inv_path_empty_head (p) (n):
      (𝐞) = ↳[n]p → 𝟎 = n.
*
[ #n <path_head_empty #H0
  <(eq_inv_empty_labels … H0) -n //
| * [ #k ] #p #n @(nat_ind_succ … n) -n // #n #_
  [ <path_head_d_dx
  | <path_head_m_dx
  | <path_head_L_dx
  | <path_head_A_dx
  | <path_head_S_dx
  ] #H0 destruct
]
qed-.

(* Constructions with path_append *******************************************)

lemma path_head_refl_append_bi (p) (q) (m) (n):
      p = ↳[m]p → q = ↳[n]q → p●q = ↳[n+m](p●q).
#p #q elim q -q
[ #m #n #Hp #H0
  <(eq_inv_path_empty_head … H0) -n //
| #l #q #IH #m #n #Hp
  @(nat_ind_succ … n) -n // #n #_
  cases l [ #k ]
  <list_append_lcons_sn <nplus_succ_sn
  [ <path_head_d_dx <path_head_d_dx #Hq
    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
    >(IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq
    <nplus_plus_comm_23 //
  | <path_head_m_dx <path_head_m_dx #Hq
    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
    >(IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq //
  | <path_head_L_dx <path_head_L_dx #Hq
    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
    >(IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq //
  | <path_head_A_dx <path_head_A_dx #Hq
    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
    >(IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq //
  | <path_head_S_dx <path_head_S_dx #Hq
    elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
    >(IH … Hp Hq) in ⊢ (??%?); -IH -Hp -Hq //
  ]
qed.

lemma path_head_refl_append_sn (p) (q) (n):
      q = ↳[n]q → q = ↳[n](p●q).
#p #q elim q -q
[ #n #Hn <(eq_inv_path_empty_head … Hn) -Hn //
| #l #q #IH #n @(nat_ind_succ … n) -n
  [ #Hq | #n #_ cases l [ #k ] ]
  [ lapply (eq_inv_path_head_zero_dx … Hq) -Hq #Hq destruct
  | <path_head_d_dx <path_head_d_dx
  | <path_head_m_dx <path_head_m_dx
  | <path_head_L_dx <path_head_L_dx
  | <path_head_A_dx <path_head_A_dx
  | <path_head_S_dx <path_head_S_dx
  ] #Hq
  elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  /3 width=1 by eq_f/
]
qed-.

(* Inversions with path_append **********************************************)

lemma eq_inv_path_head_refl_append_sn (p) (q) (n):
      q = ↳[n](p●q) → q = ↳[n]q.
#p #q elim q -q
[ #n #Hn <(eq_inv_path_empty_head … Hn) -p //
| #l #q #IH #n @(nat_ind_succ … n) -n //
  #n #_ cases l [ #k ]
  [ <path_head_d_dx <path_head_d_dx
  | <path_head_m_dx <path_head_m_dx
  | <path_head_L_dx <path_head_L_dx
  | <path_head_A_dx <path_head_A_dx
  | <path_head_S_dx <path_head_S_dx
  ] #Hq
  elim (eq_inv_list_lcons_bi ????? Hq) -Hq #_ #Hq
  /3 width=1 by eq_f/
]
qed-.