/- TPPmark 2016 Lean version by Mitsuharu Yamamoto -/
/- Lean: https://leanprover.github.io -/
import data.list
open nat list unit

section removelist

parameter {A : Type}

inductive vector : nat → Type :=
| VNil {} : vector zero
| VCons   : Π {n}, A → vector n → vector (succ n)

inductive vector2 : list nat → Type :=
| V2Nil {} : vector2 nil
| V2Cons   : Π {n l}, vector n → vector2 l → vector2 (n :: l)

inductive pos : nat → Type :=
| PO : Π {n}, pos (succ n)
| PS : Π {n}, pos n → pos (succ n)

inductive pos2 : list nat → Type :=
| P2O : Π {n l}, pos n → pos2 (n :: l)
| P2S : Π {n l}, pos2 l → pos2 (n :: l)

open vector vector2 pos pos2

definition remove_aux : Π {n}, vector (succ n) → pos (succ n) → vector n
| remove_aux (VCons first rest) PO := rest
| remove_aux (VCons first rest) (PS j) := VCons first (remove_aux rest j)

definition remove : Π {n}, vector n → pos n → vector (pred n)
| @remove (succ n) v j := @remove_aux n v j

definition remove_lst_type : Π {l}, pos2 l → list nat
| @remove_lst_type (n :: l) (P2O _) := pred n :: l
| @remove_lst_type (n :: l) (P2S p) := n :: @remove_lst_type l p

definition remove_lst :
  Π {l}, vector2 l → Π ij : pos2 l, vector2 (remove_lst_type ij)
| remove_lst (V2Cons first rest) (P2O j) := V2Cons (remove first j) rest
| remove_lst (V2Cons first rest) (P2S p) := V2Cons first (remove_lst rest p)

end removelist

open vector vector2 pos pos2

definition xyz := VCons (1 : ℕ) (VCons 2 (VCons 3 VNil))
definition uv := VCons (11 : ℕ) (VCons 12 VNil)
definition abcd := VCons (21 : ℕ) (VCons 22 (VCons 23 (VCons 24 VNil)))

eval remove xyz PO              -- VCons 2 (VCons 3 VNil)
eval remove xyz (PS PO)         -- VCons 1 (VCons 3 VNil)

definition ll := V2Cons xyz (V2Cons uv (V2Cons abcd V2Nil))

eval remove_lst ll (P2O PO)
/- eval result:
V2Cons (VCons 2 (VCons 3 VNil))
  (V2Cons (VCons 11 (VCons 12 VNil))
     (V2Cons
        (VCons 21
           (VCons 22 (VCons 23 (VCons 24 VNil))))
        V2Nil))
-/

eval remove_lst ll (P2O (PS PO))
/- eval result:
V2Cons (VCons 1 (VCons 3 VNil))
  (V2Cons (VCons 11 (VCons 12 VNil))
     (V2Cons
        (VCons 21
           (VCons 22 (VCons 23 (VCons 24 VNil))))
        V2Nil))
-/

eval remove_lst ll (P2O (PS (PS PO)))
/- eval result:
V2Cons (VCons 1 (VCons 2 VNil))
  (V2Cons (VCons 11 (VCons 12 VNil))
     (V2Cons
        (VCons 21
           (VCons 22 (VCons 23 (VCons 24 VNil))))
        V2Nil))
-/

eval remove_lst ll (P2S (P2O PO))
/- eval result:
V2Cons (VCons 1 (VCons 2 (VCons 3 VNil)))
  (V2Cons (VCons 12 VNil)
     (V2Cons
        (VCons 21
           (VCons 22 (VCons 23 (VCons 24 VNil))))
        V2Nil))
-/

eval remove_lst ll (P2S (P2S (P2O (PS PO))))
/- eval result:
V2Cons (VCons 1 (VCons 2 (VCons 3 VNil)))
  (V2Cons (VCons 11 (VCons 12 VNil))
     (V2Cons (VCons 21 (VCons 23 (VCons 24 VNil)))
        V2Nil))
-/


inductive tvector {T : Type} (eT : T → Type) : list T → Type :=
| TNil {} : tvector eT []
| TCons : Π {t l}, eT t → tvector eT l → tvector eT (t :: l)

inductive tpos {T : Type} (pT : T → Type) : list T → Type :=
| TO : Π {t l}, pT t → tpos pT (t :: l)      -- "horizontal" move
| TS : Π {t l}, tpos pT l → tpos pT (t :: l) -- "vertical" move

open tvector tpos

definition apply_pth_type {T : Type} {pT : T → Type} (g : Π t : T, pT t → T) :
           Π {l : list T}, tpos pT l → list T
| @apply_pth_type (t :: l) (TO p) := g t p :: l
| @apply_pth_type (t :: l) (TS pp) := t :: @apply_pth_type l pp

definition apply_pth {T : Type} {eT pT : T → Type} {g : Π t : T, pT t → T}
           (f : Π {t}, eT t → forall p : pT t, eT (g t p)) :
           Π ⦃l : list T⦄, tvector eT l →
           Π p : tpos pT l, tvector eT (apply_pth_type g p)
| @apply_pth (t :: l) (TCons first rest) (TO p) :=
  TCons (f first p) rest
| @apply_pth (t :: l) (TCons first rest) (TS pp) :=
  TCons first (@apply_pth l rest pp)

section removelist2

parameter {A : Type}

/- definition vector n := tvector (λ x, A) (replicate n ⋆) -/
definition vector2' := tvector (@vector A)
definition vector3' := tvector vector2'

/- definition pos n := tpos (λ x, unit) (replicate n ⋆) -/
definition pos2' := tpos pos
definition pos3' := tpos pos2'

definition remove_type {l : list nat} (ij : pos2' l) :=
  apply_pth_type (λn x, pred n) ij

definition remove_lst' : forall {l : list nat} (vv : vector2' l) (ij : pos2' l),
    vector2' (remove_type ij) :=
  apply_pth (@remove A)

definition remove_lst_lst' := apply_pth @remove_lst'

end removelist2

eval remove_type (TO PO : pos2' [(3 : ℕ), 2, 4])      -- [2, 2, 4]
eval remove_type (TO (PS PO) : pos2' [(3 : ℕ), 2, 4]) -- [2, 2, 4]
eval remove_type (TO (PS PO) : pos2' [(3 : ℕ), 2, 4]) -- [2, 2, 4]
eval remove_type (TO (PS (PS PO)) : pos2' [(3 : ℕ), 2, 4]) -- [2, 2, 4]
eval remove_type (TS (TO PO) : pos2' [(3 : ℕ), 2, 4]) -- [3, 1, 4]
eval remove_type (TS (TS (TO (PS PO))) : pos2' [(3 : ℕ), 2, 4]) -- [3, 2, 3]

definition ll' : vector2' _ := TCons xyz (TCons uv (TCons abcd TNil))
check ll'                       -- vector2' [3, 2, 4]
definition lll' : vector3' _ := TCons ll' (TCons (TCons xyz (TCons abcd TNil)) TNil)
check lll'                      -- vector3' [[3, 2, 4], [3, 4]]

eval remove_lst' ll' (TO PO)
/- eval result:
TCons (VCons 2 (VCons 3 VNil))
  (TCons (VCons 11 (VCons 12 VNil))
     (TCons
        (VCons 21
           (VCons 22 (VCons 23 (VCons 24 VNil))))
        TNil))
-/

eval remove_lst' ll' (TO (PS PO))
/- eval result:
TCons (VCons 1 (VCons 3 VNil))
  (TCons (VCons 11 (VCons 12 VNil))
     (TCons
        (VCons 21
           (VCons 22 (VCons 23 (VCons 24 VNil))))
        TNil))
-/

eval remove_lst' ll' (TO (PS (PS PO)))
/- eval result:
TCons (VCons 1 (VCons 2 VNil))
  (TCons (VCons 11 (VCons 12 VNil))
     (TCons
        (VCons 21
           (VCons 22 (VCons 23 (VCons 24 VNil))))
        TNil))
-/

eval remove_lst' ll' (TS (TO PO))
/- eval result:
TCons (VCons 1 (VCons 2 (VCons 3 VNil)))
  (TCons (VCons 12 VNil)
     (TCons
        (VCons 21
           (VCons 22 (VCons 23 (VCons 24 VNil))))
        TNil))
-/

eval remove_lst' ll' (TS (TS (TO (PS PO))))
/- eval result:
TCons (VCons 1 (VCons 2 (VCons 3 VNil)))
  (TCons (VCons 11 (VCons 12 VNil))
     (TCons (VCons 21 (VCons 23 (VCons 24 VNil)))
        TNil))
-/