(* TPPmark 2016 Coq/Ssreflect+Equations version by Mitsuharu Yamamoto *)
(* Equations: https://www.irif.fr/~sozeau/research/coq/equations.en.html *)
From Equations Require Import Equations.
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssrnat seq.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Section RemoveList.

Variable A : Type.

Inductive vector : nat -> Type :=
| VNil : vector 0
| VCons n of A & vector n : vector n.+1.

Inductive vector2 : list nat -> Type :=
| V2Nil : vector2 [::]
| V2Cons n l of vector n & vector2 l : vector2 (n :: l).

Inductive pos : nat -> Type :=
| PO {n} : pos n.+1
| PS n of pos n : pos n.+1.

Inductive pos2 : list nat -> Type :=
| P2O n l of pos n : pos2 (n :: l)
| P2S n l of pos2 l : pos2 (n :: l).

(* Order of the clauses matters *)
Equations remove_aux {n} (v : vector n.+1) (j : pos n.+1) : vector n :=
remove_aux (VCons (S _) first rest) (PS _ j) := VCons first (remove_aux rest j);
remove_aux (VCons _     _     rest) (PO _)   := rest.

Equations remove {n} (v : vector n) (j : pos n) : vector n.-1 :=
remove (VCons _ first rest) j := remove_aux (VCons first rest) j.

Definition remove_equation :=
  (remove_equation_2,
   remove_aux_equation_1, remove_aux_equation_3, remove_aux_equation_4).

Equations remove_lst_type {l} (pp : pos2 l) : list nat :=
remove_lst_type (P2O n l _)  := n.-1 :: l ;
remove_lst_type (P2S n _ pp) := n :: remove_lst_type pp.

Equations(noind) remove_lst {l} (v : 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).

Definition remove_lst_equation :=
  (remove_lst_equation_2, remove_lst_equation_3).

End RemoveList.

Arguments VNil {A}.
Arguments V2Nil {A}.
Arguments PO {n}.
Arguments P2O {n l} _.
Arguments P2S {n l} _.

Goal remove (VCons 1 (VCons 2 (VCons 3 VNil))) PO = VCons 2 (VCons 3 VNil).
Proof.
  by rewrite remove_equation_2 !(remove_aux_equation_3, remove_aux_equation_4).
Qed.

Goal remove (VCons 1 (VCons 2 (VCons 3 VNil))) (PS PO) =
      VCons 1 (VCons 3 VNil).
Proof. by rewrite !remove_equation. Qed.

Compute remove_lst_type (P2O PO : pos2 [:: 3; 2; 4]).
     (* = [:: 2; 2; 4] *)
Compute remove_lst_type (P2O (PS PO) : pos2 [:: 3; 2; 4]).
     (* = [:: 2; 2; 4] *)
Compute remove_lst_type (P2O (PS (PS PO)) : pos2 [:: 3; 2; 4]).
     (* = [:: 2; 2; 4] *)
Compute remove_lst_type (P2S (P2O PO) : pos2 [:: 3; 2; 4]).
     (* = [:: 3; 1; 4] *)
Compute remove_lst_type (P2S (P2S (P2O (PS PO))) : pos2 [:: 3; 2; 4]).
     (* = [:: 3; 2; 3] *)

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))).
Definition ll := V2Cons xyz (V2Cons uv (V2Cons abcd V2Nil)).
Check ll.
(* ll *)
(*      : vector2 nat [:: 3; 2; 4] *)

Goal remove_lst ll (P2O PO)
      = V2Cons (VCons 2 (VCons 3 VNil)) (V2Cons uv (V2Cons abcd V2Nil)).
Proof. by rewrite !remove_lst_equation !remove_equation. Qed.

Goal remove_lst ll (P2O (PS PO))
     = V2Cons (VCons 1 (VCons 3 VNil)) (V2Cons uv (V2Cons abcd V2Nil)).
Proof. by rewrite !remove_lst_equation !remove_equation. Qed.

Goal remove_lst ll (P2O (PS (PS PO)))
     = V2Cons (VCons 1 (VCons 2 VNil)) (V2Cons uv (V2Cons abcd V2Nil)).
Proof. by rewrite !remove_lst_equation !remove_equation. Qed.

Goal remove_lst ll (P2S (P2O PO))
     = V2Cons xyz (V2Cons (VCons 12 VNil) (V2Cons abcd V2Nil)).
Proof. by rewrite !remove_lst_equation !remove_equation. Qed.

Goal remove_lst ll (P2S (P2S (P2O (PS PO))))
     = V2Cons xyz (V2Cons uv (V2Cons (VCons 21 (VCons 23 (VCons 24 VNil))) V2Nil)).
Proof. by rewrite !remove_lst_equation !remove_equation. Qed.

Inductive tvector (T : Type) (eT : T -> Type) : list T -> Type :=
| TNil : tvector eT [::]
| TCons t l of eT t & tvector eT l : tvector eT (t :: l).

Inductive tpos (T : Type) (pT : T -> Type) : list T -> Type :=
| TO t l of pT t : tpos pT (t :: l)       (* "vertical" move *)
| TS t l of tpos pT l : tpos pT (t :: l). (* "horizontal" move *)

Equations apply_pth_type {T : Type} {pT : T -> Type}
          (g : forall t : T, pT t -> T) {l : list T} (p : tpos pT l) : list T :=
apply_pth_type g (TO t l p) := g t p :: l ;
apply_pth_type g (TS t l pp) := t :: apply_pth_type g pp.

Equations apply_pth {T : Type} {eT pT : T -> Type}
          {g : forall t : T, pT t -> T}
          (f : forall t, eT t -> forall p : pT t, eT (g t p))
          {l : list T} (v : tvector eT l) (p : tpos pT l)
  : tvector eT (apply_pth_type g p) :=
apply_pth f (TCons t l first rest) (TO _ _ p)  :=
  TCons (f _ first p) rest ;
apply_pth f (TCons t l first rest) (TS _ _ pp) :=
  TCons first (apply_pth f rest pp).

Definition apply_pth_equation := (apply_pth_equation_2, apply_pth_equation_3).

Arguments TNil {T eT}.
Arguments TO {T pT t l} _.
Arguments TS {T pT t l} _.
Arguments apply_pth {T eT pT g} f [l] v p.

Section RemoveList2.

Variable A : Type.

(*Definition vector n := tvector (fun=> A) (nseq n tt).*)
Definition vector2' := tvector (vector A).
Definition vector3' := tvector vector2'.

(*Definition pos n := tpos (fun=> unit) (nseq n tt).*)
Definition pos2' := tpos pos.
Definition pos3' := tpos pos2'.

Definition remove_type (l : list nat) (ij : pos2' l) :=
  apply_pth_type (fun n _ => n.-1) 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.

Check TNil: vector2' nat [::].
Check TCons VNil TNil : vector2' nat [:: 0].
Check TCons VNil (TCons VNil TNil) : vector2' nat [:: 0; 0].
Check TCons (VCons 3 VNil) (TCons VNil TNil) : vector2' nat [:: 1; 0].

Check TO (PO : pos 3) : pos2' [:: 3; 2; 4].
Check remove_type (TO PO : pos2' [:: 3; 2; 4]).
Compute remove_type (TO PO : pos2' [:: 3; 2; 4]).
     (* = [:: 2; 2; 4] *)
Check TO (PS PO) : pos2' [:: 3; 2; 4].
Check remove_type (TO (PS PO) : pos2' [:: 3; 2; 4]).
Compute remove_type (TO (PS PO) : pos2' [:: 3; 2; 4]).
     (* = [:: 2; 2; 4] *)
Compute remove_type (TO (PS (PS PO)) : pos2' [:: 3; 2; 4]).
     (* = [:: 2; 2; 4] *)
Compute remove_type (TS (TO PO) : pos2' [:: 3; 2; 4]).
     (* = [:: 3; 1; 4] *)
Compute remove_type (TS (TS (TO (PS PO))) : pos2' [:: 3; 2; 4]).
     (* = [:: 3; 2; 3] *)

Definition ll' := TCons xyz (TCons uv (TCons abcd TNil)).
Check ll'.
(* ll' *)
(*      : tvector (vector nat) [:: 3; 2; 4] *)
Definition lll' := TCons ll' (TCons (TCons xyz (TCons abcd TNil)) TNil).
Check lll'.
(* lll' *)
(*      : tvector (tvector (vector nat)) [:: [:: 3; 2; 4]; [:: 3; 4]] *)

Goal remove_lst' ll' (TO PO)
     = TCons (VCons 2 (VCons 3 VNil)) (TCons uv (TCons abcd TNil)).
Proof. by rewrite /remove_lst' !apply_pth_equation !remove_equation. Qed.

Goal remove_lst' ll' (TO (PS PO))
     = TCons (VCons 1 (VCons 3 VNil)) (TCons uv (TCons abcd TNil)).
Proof. by rewrite /remove_lst' !apply_pth_equation !remove_equation. Qed.

Goal remove_lst' ll' (TO (PS (PS PO)))
     = TCons (VCons 1 (VCons 2 VNil)) (TCons uv (TCons abcd TNil)).
Proof. by rewrite /remove_lst' !apply_pth_equation !remove_equation. Qed.

Goal remove_lst' ll' (TS (TO PO))
     = TCons xyz (TCons (VCons 12 VNil) (TCons abcd TNil)).
Proof. by rewrite /remove_lst' !apply_pth_equation !remove_equation. Qed.

Goal remove_lst' ll' (TS (TS (TO (PS PO))))
     = TCons xyz (TCons uv (TCons (VCons 21 (VCons 23 (VCons 24 VNil))) TNil)).
Proof. by rewrite /remove_lst' !apply_pth_equation !remove_equation. Qed.