From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.

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

(* ********************* *)
Fixpoint nthf (X:Type) f (l : seq X) n :=
  if l is x :: l' then if n is n'.+1 then x :: nthf f l' n' else f x :: l'
  else l.

Fixpoint nthrm (X:Type) (l : seq X) n :=
  if l is x :: l' then if n is n'.+1 then x :: nthrm l' n' else l' else l.

Definition remove_lst (X:Type) (lst : seq (seq X)) i j :=
  nthf ((@nthrm X)^~ j) lst i.

Lemma size_nthrm (X:Type) (l:seq X) n :
  n < size l -> (size (nthrm l n)).+1 = size l.
Proof. by elim : l n =>[|x l IHl][|n]//= /IHl =>->. Qed.

Lemma remove_lst_size (X:eqType) (lst : seq (seq X)) l0 i j :
  j < size (nth [::] lst i) ->
  let rem := remove_lst lst i j in
  forall n, if i == n then (size (nth l0 rem n)).+1 == size (nth l0 lst n)
            else nth l0 rem n == nth l0 lst n.
Proof.
  elim : i lst =>[|i IHi][|l lst]//= Hij [|n]//=; first by rewrite size_nthrm.
  rewrite eqSS. exact : IHi.
Qed.

(* ********************* *)
Fixpoint f_lst (X Y:Type) (f:X -> Y -> X) n :
  iter n seq X -> iter n (prod nat) Y -> iter n seq X :=
  match n return iter n seq X -> iter n (prod nat) Y -> iter n seq X with
  | 0 => fun x => fun y => f x y
  | n'.+1 => fun lst => fun v => nthf ((@f_lst _ _ f n')^~ v.2) lst v.1
  end.

Definition lst_nil (X:Type) (x0:X) n : iter n seq X :=
  match n return iter n seq X with
  | 0 => x0
  | n'.+1 => [::]
  end.

Fixpoint f_lst_hypo (X Y:Type) (x0:X) (P:X -> Y -> bool) n :
  iter n seq X -> iter n (prod nat) Y -> bool :=
  match n return iter n seq X -> iter n (prod nat) Y -> bool with
  | 0 => fun x => fun y => P x y
  | n'.+1 =>
    fun lst => fun v => (v.1 < size lst) && f_lst_hypo x0 P
                                         (nth (lst_nil x0 _) lst v.1) v.2
  end.

Fixpoint f_lst_sound (X Y:Type) (f:X -> Y -> X) (Q:X -> Y -> bool) n :
  iter n seq X -> iter n (prod nat) Y -> Prop :=
  match n return iter n seq X -> iter n (prod nat) Y -> Prop with
  | 0 => fun x => fun y => Q x y
  | n'.+1 => fun lst => fun v =>
                          forall l0 n,
                            if v.1 == n
                            then f_lst_sound f Q (nth l0 lst n) v.2
                            else nth l0 (f_lst f lst v) n = nth l0 lst n
  end.

Lemma f_lst_soundness (X Y:Type) x0 (f:X -> Y -> X) (P Q:X -> Y -> bool) n
      (lst : iter n seq X) (v : iter n (prod nat) Y):
  (forall x y, P x y -> Q x y) ->
  f_lst_hypo x0 P lst v -> f_lst_sound f Q lst v.
Proof.
  move => HPQ.
  elim : n =>[|n IHn] in lst v *=>/=; first exact : HPQ.
  case /andP => Hsize. move /IHn => IH l0 n0.
  elim : v.1 =>[|k IHk] in lst Hsize IH n0 *.
  - case : n0 =>[|n0 /=]; first by rewrite (set_nth_default (lst_nil x0 n)).
      by case : lst Hsize IH.
  - case : n0 =>[|n0]; case : lst Hsize IH =>[|l lst] =>//=. rewrite eqSS.
    move /IHk => IH. move /IH. exact.
Qed.