(* TPPmark 2016 Coq/Ssreflect version by Mitsuharu Yamamoto *)
Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import all_ssreflect.

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

(* Solution 1 : Use different types for 1st and 2nd levels. *)

Module Solution1.

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).

Lemma not_pos0 : pos 0 -> False.
Proof. by case E: 0 /. Qed.

Lemma not_pos2nil : pos2 [::] -> False.
Proof. by case E: [::] /. Qed.

Definition remove n (v : vector n) (j : pos n) : vector (n.-1).
  elim: v j => {n} [/not_pos0 //|n first rest IHfirst].
  case E: n.+1 / => [?|? j].
  - move: E => [] <-.
    exact: rest.
  - move: E j => [] <- {rest}.
    case: n IHfirst => [_ /not_pos0 //|n IHfirst j'].
    exact: (VCons first (IHfirst j')).
Defined.

Definition remove_lst_type (l : list nat) (ij : pos2 l) : list nat.
  elim: l ij => [/not_pos2nil //|n l IHl].
  case E: (n :: l) / => [|? ? pp].
  - exact: (n.-1 :: l).
  - move: E pp => [] _ <- l'.
    exact: (n :: IHl l').
Defined.

Definition remove_lst (l : list nat) (vv : vector2 l) (ij : pos2 l)
  : vector2 (remove_lst_type ij).
  elim: vv ij => {l} [ij|n l first rest IHfirst];
    first by move/not_pos2nil: (ij).
  case E: (n :: l) / => [? ? p|? ? pp].
  - move: E p => [] <- <- p.
    exact: (V2Cons (remove first p) rest).
  - move: E pp => [] <- <- pp.
    exact: (V2Cons first (IHfirst pp)).
Defined.

End RemoveList.

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

Compute remove (VCons 1 (VCons 2 (VCons 3 VNil))) PO.
     (* = VCons 2 (VCons 3 VNil) *)
     (* : vector nat 3.-1 *)
Compute remove (VCons 1 (VCons 2 (VCons 3 VNil))) (PS PO).
     (* = VCons 1 (VCons 3 VNil) *)
     (* : vector nat 3.-1 *)
Compute remove (VCons 1 (VCons 2 (VCons 3 VNil))) (PS (PS PO)).
     (* = VCons 1 (VCons 2 VNil) *)
     (* : vector nat 3.-1 *)

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] *)

Compute remove_lst ll (P2O PO).
     (* = V2Cons (VCons 2 (VCons 3 VNil)) *)
     (*     (V2Cons (VCons 11 (VCons 12 VNil)) *)
     (*        (V2Cons (VCons 21 (VCons 22 (VCons 23 (VCons 24 VNil)))) V2Nil)) *)
     (* : vector2 nat (remove_lst_type (P2O PO)) *)
Compute remove_lst ll (P2O (PS PO)).
     (* = V2Cons (VCons 1 (VCons 3 VNil)) *)
     (*     (V2Cons (VCons 11 (VCons 12 VNil)) *)
     (*        (V2Cons (VCons 21 (VCons 22 (VCons 23 (VCons 24 VNil)))) V2Nil)) *)
     (* : vector2 nat (remove_lst_type (P2O (PS PO))) *)
Compute remove_lst ll (P2O (PS (PS PO))).
     (* = V2Cons (VCons 1 (VCons 2 VNil)) *)
     (*     (V2Cons (VCons 11 (VCons 12 VNil)) *)
     (*        (V2Cons (VCons 21 (VCons 22 (VCons 23 (VCons 24 VNil)))) V2Nil)) *)
     (* : vector2 nat (remove_lst_type (P2O (PS (PS PO)))) *)
Compute remove_lst ll (P2S (P2O PO)).
     (* = V2Cons (VCons 1 (VCons 2 (VCons 3 VNil))) *)
     (*     (V2Cons (VCons 12 VNil) *)
     (*        (V2Cons (VCons 21 (VCons 22 (VCons 23 (VCons 24 VNil)))) V2Nil)) *)
     (* : vector2 nat (remove_lst_type (P2S (P2O PO))) *)
Compute remove_lst ll (P2S (P2S (P2O (PS PO)))).
     (* = V2Cons (VCons 1 (VCons 2 (VCons 3 VNil))) *)
     (*     (V2Cons (VCons 11 (VCons 12 VNil)) *)
     (*        (V2Cons (VCons 21 (VCons 23 (VCons 24 VNil))) V2Nil)) *)
     (* : vector2 nat (remove_lst_type (P2S (P2S (P2O (PS PO))))) *)

End Solution1.

(* Solution 2 : Use the same type for 1st, 2nd (and 3rd, ...) levels. *)

Module Solution2.

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).

Arguments TNil {T eT}.

Check (TCons 1 (TCons true (TCons 2 (TCons false TNil))))
      : tvector (id : Set -> Type) [:: nat ; bool; nat; bool].
Check (TCons [:: 1] (TCons [:: true] (TCons [:: 2] (TCons [:: false] TNil))))
      : tvector (list : Set -> Type) [:: nat; bool; nat; bool].

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 *)

Lemma not_tpos_nil (T : Type) (pT : T -> Type) : tpos pT [::] -> False.
Proof. by case E: [::] /. Qed.

Definition apply_pth_type (T : Type) (pT : T -> Type)
           (g : forall t : T, pT t -> T) (l : list T) (p : tpos pT l) : list T.
  elim: l p => [/not_tpos_nil //|t l IHl].
  case E: (t :: l) / => [? ? p|? ? pp].
  - move: E p => [] <- _ p.
    exact (g t p :: l).
  - move: E pp => [] _ <- l'.
    exact (t :: IHl l').
Defined.

Definition 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).
  elim: v p => {l} [p|t l first rest IHfirst]; first by move/not_tpos_nil: (p).
  case E: (t :: l) / => [? ? p|? ? pp].
  - move: E p => [] <- <- p.
    exact: (TCons (f _ first p) rest).
  - move: E pp => [] <- <- pp.
    exact: (TCons first (IHfirst pp)).
Defined.

Arguments TNil {T eT}.
Arguments TO {T pT t l} _.
Arguments TS {T pT t l} _.

Section RemoveList2.

Variable A : Type.

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

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

Definition remove n (v : vector n) (j : pos n) : vector (n.-1).
  move: v j; rewrite /vector /pos.
  move: {-2}(nseq n tt) (erefl (nseq n tt)) => l E v.
  elim: v n E => {l} [_ _ /not_tpos_nil // | t l first rest IHfirst].
  case=> [//|n [] _ El].
  case E': (t :: l) / => [|? ? j].
  - rewrite -El.
    exact rest.
  - move: E' j => [] _ <- {rest}.
    case: n El => [-> /not_tpos_nil //|n El j'].
    exact: (TCons first (IHfirst _ El j')).
Defined.

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.

Definition remove_lst_lst := apply_pth remove_lst.


End RemoveList2.

Check TNil: vector nat 0.
Check TCons 3 TNil : vector nat 1.
Check TCons 3 (TCons 1 (TCons 4 TNil)) : vector nat 3.

Check TNil: vector2 nat [::].
Check TCons (TNil : vector nat 0) TNil : vector2 nat [:: 0].
Check TCons (TNil : vector nat 0) (TCons (TNil : vector nat 0) TNil)
  : vector2 nat [:: 0; 0].
Check TCons (TCons 3 TNil : vector nat 1) (TCons (TNil : vector nat 0) TNil)
  : vector2 nat [:: 1; 0].

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

Compute remove (TCons 1 (TCons 2 (TCons 3 TNil)) : vector nat 3) (TO tt).
     (* = TCons 2 (TCons 3 TNil) *)
     (* : vector nat 3.-1 *)
Compute remove (TCons 1 (TCons 2 (TCons 3 TNil)) : vector nat 3) (TS (TO tt)).
     (* = TCons 1 (TCons 3 TNil) *)
     (* : vector nat 3.-1 *)
Compute remove (TCons 1 (TCons 2 (TCons 3 TNil)) : vector nat 3) (TS (TS (TO tt))).
     (* = TCons 1 (TCons 2 TNil) *)
     (* : vector nat 3.-1 *)

Definition xyz := TCons 1 (TCons 2 (TCons 3 TNil)) : vector nat 3.
Definition uv := TCons 11 (TCons 12 TNil) : vector nat 2.
Definition abcd := TCons 21 (TCons 22 (TCons 23 (TCons 24 TNil))) : vector nat 4.
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]] *)


Compute remove_lst ll (TO (TO tt : pos 3)).
     (* = TCons (TCons 2 (TCons 3 TNil)) *)
     (*     (TCons (TCons 11 (TCons 12 TNil)) *)
     (*        (TCons (TCons 21 (TCons 22 (TCons 23 (TCons 24 TNil)))) TNil)) *)
     (* : vector2 nat (remove_type (TO (TO tt : pos 3))) *)
Compute remove_lst ll (TO (TS (TO tt) : pos 3)).
     (* = TCons (TCons 1 (TCons 3 TNil)) *)
     (*     (TCons (TCons 11 (TCons 12 TNil)) *)
     (*        (TCons (TCons 21 (TCons 22 (TCons 23 (TCons 24 TNil)))) TNil)) *)
     (* : vector2 nat (remove_type (TO (TS (TO tt) : pos 3))) *)
Compute remove_lst ll (TO (TS (TS (TO tt)) : pos 3)).
     (* = TCons (TCons 1 (TCons 2 TNil)) *)
     (*     (TCons (TCons 11 (TCons 12 TNil)) *)
     (*        (TCons (TCons 21 (TCons 22 (TCons 23 (TCons 24 TNil)))) TNil)) *)
     (* : vector2 nat (remove_type (TO (TS (TS (TO tt)) : pos 3))) *)
Compute remove_lst ll (TS (TO (TO tt : pos 2))).
     (* = TCons (TCons 1 (TCons 2 (TCons 3 TNil))) *)
     (*     (TCons (TCons 12 TNil) *)
     (*        (TCons (TCons 21 (TCons 22 (TCons 23 (TCons 24 TNil)))) TNil)) *)
     (* : vector2 nat (remove_type (TS (TO (TO tt : pos 2)))) *)
Compute remove_lst ll (TS (TS (TO (TS (TO tt) : pos 4)))).
     (* = TCons (TCons 1 (TCons 2 (TCons 3 TNil))) *)
     (*     (TCons (TCons 11 (TCons 12 TNil)) *)
     (*        (TCons (TCons 21 (TCons 23 (TCons 24 TNil))) TNil)) *)
     (* : vector2 nat (remove_type (TS (TS (TO (TS (TO tt) : pos 4))))) *)

End Solution2.