\import Data.Fin
\import Data.List
\import Logic.Rewriting.TRS.Utils.FinFunctions
\import Meta
\import Paths
\import Paths.Meta
\import Data.SubList

\func shift-index {A : \Set} {a b : List A} (sublist : SubList a b) (ind : Index a) : Fin (length b)
  \elim a, b, sublist, ind
  | x :: xs, y :: ys, sublist-match p sublist, zero => zero
  | x :: xs, y :: ys, sublist-match p sublist, suc ind => suc (shift-index sublist ind)
  | l, y :: ys, sublist-skip sublist, ind => suc (shift-index sublist ind)

\module Shifts \where {
  \func proof {A : \Set} {a b : List A} {point : A} (sublist : SubList a b) (ind : Index a) (p : point = a !! ind)
    : point = b !! shift-index sublist ind
    \elim a, b, sublist, ind, p
    | x :: xs, y :: ys, sublist-match p sublist, zero, idp => p
    | x :: xs, y :: ys, sublist-match p sublist, suc ind, idp => proof sublist ind idp
    | nil, y :: ys, sublist-skip sublist, ind, idp => proof sublist ind idp
    | x :: a, y :: b, sublist-skip sublist, ind, idp => proof sublist ind idp

  \lemma over-identity {A : \Set} {a : List A} (ind : Index a)
    : shift-index SubList.identity ind = ind
    \elim a, ind
    | a :: a1, zero => idp
    | a :: a1, suc ind => pmap fsuc (over-identity ind)

  \lemma over-skip {A : \Set} {a b : List A} {point' : A} (sublist : SubList a b) (ind : Index a)
    : shift-index {_} {_} {point' :: b} (sublist-skip sublist) ind = suc (shift-index sublist ind)
    \elim a
    | x :: a => idp
    | nil => idp

  \lemma over-shrink {A : \Set} {x : A} {a b : List A} (sublist : SubList (x :: a) b) (ind : Index a)
    : shift-index (SubList.shrink sublist) ind  = shift-index sublist (fsuc ind)
    \elim a, b, sublist
    | nil, y :: b, sublist-match p1 sublist => idp
    | a :: a1, y :: b, sublist-match p1 sublist => idp
    | a :: a1, y :: b, sublist-skip sublist => rewrite (over-shrink sublist ind) idp

  \lemma over-right-single {A : \Set} {a b : List A} (ind : Index a)
    : shift-index (SubList.extend-right-single SubList.identity) ind = expand-fin-left {A} {a} {b} ind
    \elim a, ind
    | a :: a1,  => idp
    | a :: a1, suc ind => pmap fsuc (over-right-single ind)

  \lemma over-left-single {A : \Set} {a b : List A} (ind : Index b)
    : shift-index {A} {b} {a ++ b} SubList.id+left ind = expand-fin-right ind
    \elim a
    | nil => over-identity _
    | a :: a1 => rewrite over-skip (pmap fsuc (over-left-single ind))

  \lemma over-right-both {A : \Set} {a b c : List A} (sublist : SubList a b) (fin : Index c)
    : shift-index (SubList.extend-right-both sublist) (expand-fin-right fin) = expand-fin-right fin \elim a, b, c, sublist, fin
    | nil, nil, a :: c, sublist-nil,  => idp
    | nil, nil, a :: c, sublist-nil, suc fin => pmap fsuc (over-right-both sublist-nil fin)
    | x :: a, y :: b, c, sublist-match p sublist, fin => pmap fsuc (over-right-both sublist fin)
    | nil, y :: b, a :: c, sublist-skip sublist,  => pmap fsuc (over-right-both sublist )
    | nil, y :: b, a :: c, sublist-skip sublist, suc fin => pmap fsuc (over-right-both {_} {_} {_} {a :: c} sublist (suc fin))
    | a :: a1, y :: b, c, sublist-skip sublist, fin => pmap fsuc (over-right-both sublist fin)

  \lemma right-extension {A : \Set} {a b : List A} (ind : Index a) :
    \Sigma (eq : (a !! ind) = (a ++ b) !! expand-fin-left ind)
           ((shift-index SubList.id+right ind, proof SubList.id+right ind idp)
             = {\Sigma (ind' : Fin (length (a ++ b))) (a !! ind = (a ++ b) !! ind')}
           (expand-fin-left ind, eq))
    \elim a, ind
    | a :: a1,  => (idp, ext idp)
    | a :: a1, suc ind => \have sig => right-extension {_} {a1} {b} ind
                          \in (sig., ext (pmap fsuc (pmap __. sig.)))

  \lemma left-extension-generic {A : \Set} {a b : List A} {point : A} (ind : Index b) {point-eq : point = b !! ind} :
    \Sigma (eq2 : point = (a ++ b) !! expand-fin-right ind)
           ((shift-index (SubList.extend-left-single SubList.identity ) ind, proof (SubList.extend-left-single SubList.identity) ind point-eq)
             = {\Sigma (ind' : Fin (length (a ++ b))) (point = (a ++ b) !! ind')}
           (expand-fin-right ind, eq2))
    \elim a, point-eq
    | nil, idp => (idp, ext (over-identity ind))
    | a :: a1, idp =>
      \have sig => left-extension-generic {_} {a1} {b} ind {idp}
      \in (sig., ext (later (rewrite over-skip (pmap fsuc (pmap __. sig.)))))

  \lemma left-extension {A : \Set} {a b : List A} (ind : Index b)
    : (shift-index {A} {b} {a ++ b} SubList.id+left ind, proof SubList.id+left ind idp)
      = {\Sigma (ind' : Fin (length (a ++ b))) (b !! ind = (a ++ b) !! ind')}
      (expand-fin-right ind, inv (expand-fin-right.correct {_} {a} ind))
    => ext (over-left-single ind)

  \func right-both-after-expand-left {A : \Set} {a b c : List A} (sublist : SubList a b) (index : Index a)
    : shift-index (SubList.extend-right-both sublist {c}) (expand-fin-left index)
      = shift-index (SubList.extend-right-single SubList.identity) (shift-index sublist index)
    \elim a, b, sublist, index
    | x :: a, y :: b, sublist-match p sublist,  => idp
    | x :: a, y :: b, sublist-match p sublist, suc index => pmap fsuc (right-both-after-expand-left sublist index)
    | a :: a1, y :: b, sublist-skip sublist, index => pmap fsuc (right-both-after-expand-left sublist index)

  \func right-both-after-expand-right {A : \Set} {a b : List A} (sublist : SubList a b) {c : List A} (index : Index c)
    : shift-index (SubList.extend-right-both sublist {c}) (expand-fin-right index)
      = shift-index (SubList.extend-left-single SubList.identity) index
    \elim a, b, sublist, c, index
    | nil, nil, sublist-nil, a :: c, index => idp
    | x :: a, y :: b, sublist-match p sublist, a1 :: c,  => pmap fsuc (right-both-after-expand-right sublist )
    | x :: a, y :: b, sublist-match idp sublist, a1 :: c, suc index => pmap fsuc (right-both-after-expand-right sublist {a1 :: c} (fsuc index))
    | nil, y :: b, sublist-skip sublist, a1 :: c, ind => pmap fsuc (right-both-after-expand-right sublist {a1 :: c} ind)
    | a :: a2, y :: b, sublist-skip sublist, a1 :: c, ind => pmap fsuc (right-both-after-expand-right sublist {a1 :: c} ind)
}