Require Import Coq.Arith.Lt.

(****************************)
(* 依存型プログラミング的な表現 *)
(****************************)

Definition explosion A : False -> A :=
  fun f => match f with end.

Lemma nleinil {A} : forall i, ~i < @length A nil.
Proof.
  exact Coq.Arith.PeanoNat.Nat.nlt_0_r.
Qed.

Lemma pre_length {A} : forall i (a : A) (l : @list A), S i < length (cons a l) -> i < length l.
Proof.
  intros i a l leH.
  simpl in leH.
  exact (lt_S_n _ _ leH).
Qed.

Lemma fun_eq {A B} : forall (f : A -> B) (a1 a2 : A), a1 = a2 -> f a1 = f a2.
  intros.
  rewrite H.
  tauto.
Qed.


Section nth_section.
  
  Fixpoint nth {A} (l : list A) (i : nat) (le : i < length l) : A :=
    match l as l0 return (i < length l0) -> A with
      | nil => fun p => explosion _ (nleinil _ p)
      | cons a l' => fun p =>
                       match i as i0 return (i0 < length (cons a l')) -> A with
                         | O => fun q => a
                         | S i' => fun q => nth l' i' (pre_length _ _ _ q)
                       end p
    end le.
  
  Lemma nth_0 {A} : forall (a : A) p, nth (cons a nil) 0 p = a.
    reflexivity.
  Qed.
  
  Lemma nth_n {A} : forall (a : A) (l : list A) i p, nth (cons a l) (S i) p = nth l i (pre_length _ _ _ p).
    reflexivity.
  Qed.

  Lemma nth_proof_irrelevance {A} :
    forall (l : list A) (i : nat),
    forall (le1 le2 : i < length l),
      nth l i le1 = nth l i le2.
  Proof.
    fix Ind 1.
    intros l i le1 le2.
    destruct l as [|a l'].
    exact (explosion _ (nleinil _ le1)).
    destruct i as [| i'].
    simpl.
    reflexivity.
    simpl.
    apply Ind.
  Qed.
  
End nth_section.

Section remove'_lst_section.
  
  Fixpoint remove'_lst {A} (l : list A) (i : nat) (le : i < length l) : list A :=
    match l as l0 return (i < length l0) -> list A with
      | nil => fun p => explosion _ (nleinil _ p)
      | cons a l' => fun p => 
                       (match i as i0 return (i0 < length (cons a l')) -> list A with
                          | O => fun p => l'
                          | S i' => fun p => cons a (remove'_lst _ _ (pre_length _ _ _ p))
                        end p)
    end le.
  
  Lemma remove'_lst_length {A} :
    forall (l : list A) i (le : i < length l),
      S (length (remove'_lst l i le)) = length l.
  Proof.
    fix Ind 1.
    intros l i le.
    destruct l as [| a l'].
    exact (explosion _ (nleinil _ le)).
    destruct i as [| i'].
    {
      simpl.
      reflexivity.
    } {
      simpl.
      simpl in le.
      apply Coq.Arith.PeanoNat.Nat.succ_inj_wd.
      exact (Ind l' _ _).
    }
  Qed.

  Lemma remove'_lst_proof_irrelevance {A} :
    forall (l1 l2 : list A) i1 i2 (le1 : i1 < length l1) (le2 : i2 < length l2),
      l1 = l2 -> i1 = i2 ->
      remove'_lst l1 i1 le1 = remove'_lst l2 i2 le2.
  Proof.
    fix Ind 1.
    intros l1 l2 i1 i2 le1 le2 eql eqi.
    destruct l1 as [|a1 l1'].
    exact (explosion _ (nleinil _ le1)).
    subst.
    destruct i2 as [| i2'].
    simpl.
    reflexivity.
    simpl.
    apply (fun_eq (fun x => cons a1 x)).
    apply (Ind l1' _ _ _ _ _); reflexivity.
  Qed.
    
End remove'_lst_section.


Fixpoint remove_lst {A} (ll : list (list A)) i (i_prf : i < length ll) j (j_prf : j < length (nth ll i i_prf)) : list (list A) :=
  match ll as ll0 return forall (ip : i < length ll0), (j < length (nth ll0 i ip)) -> list (list A) with
    | nil => fun pi pj => explosion _ (nleinil _ pi)
    | cons l ll' => fun pi pj =>
                      match i as i0 return forall (ip : i0 < length (cons l ll')), (j < length (nth (cons l ll') i0 ip)) -> list (list A) with
                        | O => fun qi qj => cons (remove'_lst l j qj) ll'
                        | S i' => fun qi qj => cons l (remove_lst ll' i' (pre_length _ _ _ qi) j (eq_ind _ (fun x => j < length x) qj _ (nth_n _ _ i' qi)))
                      end pi pj
  end i_prf j_prf.

Lemma remove_lst_proof_irrelevance {A} :
  forall (ll1 ll2 : list (list A)) i1 i2 (i1_prf : i1 < length ll1) (i2_prf : i2 < length ll2) j1 j2 (j1_prf : j1 < length (nth ll1 i1 i1_prf)) (j2_prf : j2 < length (nth ll2 i2 i2_prf)),
    ll1 = ll2 -> i1 = i2 -> j1 = j2 ->
    remove_lst ll1 i1 i1_prf j1 j1_prf = remove_lst ll2 i2 i2_prf j2 j2_prf.
Proof.
  fix Ind 1.
  intros ll1 ll2 i1 i2 i1_prf i2_prf j1 j2 j1_prf j2_prf eql eqi eqj.
  destruct ll1 as [| l1 ll1'].
  exact (explosion _ (nleinil _ i1_prf)).
  subst.
  destruct i2 as [| i2'].
  {
    simpl.
    apply (fun_eq (fun x => cons x ll1')).
    apply remove'_lst_proof_irrelevance; reflexivity.
  } {
    assert(i1_prf' : i2' < length ll1').
    {
      generalize i1_prf.
      apply Coq.Arith.PeanoNat.Nat.succ_lt_mono.
    }
    assert(j1_prf' : j2 < length (nth ll1' i2' i1_prf')).
    {
      cut (nth (cons l1 ll1') (S i2') i1_prf = nth ll1' i2' i1_prf').
      {
        intro relH.
        rewrite <- relH.
        assumption.
      }
      simpl.
      apply nth_proof_irrelevance.
    }
    transitivity (cons l1 (remove_lst ll1' i2' i1_prf' j2 j1_prf')).
    {
      simpl.
      apply (fun_eq (fun x => cons l1 x)).
      apply Ind; reflexivity.
    }
    simpl.
    apply (fun_eq (fun x => cons l1 x)).
    apply Ind; reflexivity.
  }
Qed.