Require Import Coq.Arith.Lt.

(**************)
(* 論理的な表現 *)
(**************)


Section remove'_lst_section.
  
  Inductive remove'_lst {A} : list A -> nat -> list A -> Prop :=
  | is_remove_at_i_O : forall l a, remove'_lst (cons a l) O l
  | is_remove_at_i_S : forall l1 l2 a i, remove'_lst l1 i l2 -> remove'_lst (cons a l1) (S i) (cons a l2)
  .

  Lemma remove'_lst_O_inv :
    forall {A} (l1 l2 : list A),
      remove'_lst l1 0 l2 ->
      exists a, l1 = cons a l2.
  Proof.
    intros A l1 l2 rlH.
    inversion rlH; subst.
    exists a.
    reflexivity.
  Qed.

  Lemma remove'_lst_S_inv :
    forall {A} (a1 a2 : A) l1 l2 i,
      remove'_lst (cons a1 l1) (S i) (cons a2 l2) ->
      a1 = a2 /\ remove'_lst l1 i l2.
  Proof.
    intros A a1 a2 l1 l2 i rmH.
    inversion rmH; subst.
    split.
    reflexivity.
    assumption.
  Qed.
  
  Lemma remove'_lst_length :
    forall {A} (l1 l2 : list A) i,
      remove'_lst l1 i l2 ->
      length l1 = S (length l2).
  Proof.
    fix Ind 5.
    intros A l1 l2 i rlH.
    destruct rlH as [l a | l1' l2' a i rlH'].
    reflexivity.
    simpl.
    apply Coq.Arith.PeanoNat.Nat.succ_inj_wd.
    exact (Ind _ _ _ _ rlH').
  Qed.

  Lemma exist_remove'_lst : forall {A} (l : list A) i, i < length l -> exists l', remove'_lst l i l'.
  Proof.
    fix Ind 2.
    intros A l i p.
    destruct l.
    {
      simpl in p.
      now apply Coq.Arith.PeanoNat.Nat.nlt_0_r in p.
    }
    destruct i.
    exists l.
    apply is_remove_at_i_O.
    simpl in p.
    apply Coq.Arith.PeanoNat.Nat.succ_lt_mono in p.
    destruct (Ind _ l i p) as [l' isH].
    exists (cons a l').
    apply is_remove_at_i_S.
    exact isH.
  Qed.

  Theorem unq_remove'_lst : forall {A} (l : list A) i, i < length l -> forall l1 l2, remove'_lst l i l1 -> remove'_lst l i l2 -> l1 = l2.
  Proof.
    fix Ind 2.
    intros A l i p l1 l2 rlH1 rlH2.
    destruct l.
    inversion rlH1.
    destruct i as [| i'].
    {
      inversion rlH1; subst.
      inversion rlH2; subst.
      reflexivity.
    } {
      destruct l1 as [| a1 l1'].
      inversion rlH1.
      apply remove'_lst_S_inv in rlH1.
      destruct rlH1 as [eqa1 rmH1'].
      destruct l2 as [| a2 l2'].
      inversion rlH2.
      apply remove'_lst_S_inv in rlH2.
      destruct rlH2 as [eqa2 rmH2'].
      rewrite <- eqa1.
      rewrite <- eqa2.
      cut (l1' = l2').
      {
        intro eql.
        rewrite eql.
        reflexivity.
      }
      simpl in p.
      apply Coq.Arith.PeanoNat.Nat.succ_lt_mono in p.
      exact (Ind _ _ _ p _ _ rmH1' rmH2').
    }
  Qed.        
      
End remove'_lst_section.


Section nth_section.

  Inductive nth {A} : list A -> nat -> A -> Prop :=
  | nth_O : forall l a, nth (cons a l) O a
  | nth_S : forall l a n x, nth l n a -> nth (cons x l) (S n) a
  .
  
  Lemma nth_eq_O : forall {A} (l : list A) a1 a2, nth (cons a1 l) 0 a2 -> a1 = a2.
  Proof.
    intros A l a1 a2 nthH.
    now inversion nthH; subst.
  Qed.
  
  Lemma nth_S_rev : forall {A} (l : list A) a n x, nth (cons x l) (S n) a -> nth l n a.
  Proof.
    intros A l a n x nthH.
    inversion nthH; subst.
    exact H3.
  Qed.

  Lemma nth_unq : forall {A} (l : list A) i a1 a2, nth l i a1 -> nth l i a2 -> a1 = a2.
  Proof.
    fix Ind 2.
    intros A l i a1 a2.
    intros nth1 nth2.
    destruct l as [|a l'].
    {
      inversion nth1.
    } {
      destruct i as [|i'].
      {
        apply nth_eq_O in nth1.
        apply nth_eq_O in nth2.
        rewrite <- nth1.
        rewrite <- nth2.
        reflexivity.
      } {
        apply nth_S_rev in nth1.
        apply nth_S_rev in nth2.
        exact (Ind _ l' i' _ _ nth1 nth2).
      }
    }
  Qed.        
  
End nth_section.



Inductive remove_lst {A} : list (list A) -> nat -> nat -> list (list A) -> Prop :=
  | remove_lst_O : forall j l1 l2, remove'_lst l1 j l2 -> forall ll, remove_lst (cons l1 ll) O j (cons l2 ll)
  | remove_lst_S : forall ll1 ll2 l i j, remove_lst ll1 i j ll2 -> remove_lst (cons l ll1) (S i) j (cons l ll2)
.

Lemma remove_lst_O_inv :
  forall {A} (l : list A) ll' ll j,
    remove_lst (cons l ll') 0 j ll ->
    exists l',
      remove'_lst l j l' /\ ll = cons l' ll'.
Proof.  
  intros A l ll' ll j rmH.
  inversion rmH; subst.
  exists l2.
  split.
  assumption.
  reflexivity.
Qed.  

Lemma remove_lst_S_inv :
  forall {A} (l : list A) ll' mm i j,
    remove_lst (cons l ll') (S i) j mm ->
    exists mm',
      remove_lst ll' i j mm' /\ mm = cons l mm'.
Proof.
  intros A l ll mm i j rlH.
  inversion rlH; subst.
  exists ll2.
  split.
  assumption.
  reflexivity.
Qed.

Lemma remove_lst_O_rev :
  forall {A} (l1 l2 : list A) ll j,
    remove_lst (cons l1 ll) 0 j (cons l2 ll) ->
    remove'_lst l1 j l2.
Proof.
  intros A l1 l2 ll j rlH.
  inversion rlH; subst.
  assumption.
Qed.  


(* i 番目のリストについては、その j 番目の 要素を取り除く *)
Theorem is_remove_lst_i_j :
  forall {A} (ll1 ll2 : list (list A)) i j,
    remove_lst ll1 i j ll2 ->
    forall (l1 l2 : list A),
      nth ll1 i l1 -> nth ll2 i l2 ->
      remove'_lst l1 j l2.
Proof.
  fix Ind 6.
  intros A ll1 ll2 i j rlH l1 l2 nth1 nth2.
  destruct rlH as [i l1' l2' rlH ll | ll1 ll2 l i j rlH].
  {
    apply nth_eq_O in nth1.
    apply nth_eq_O in nth2.
    rewrite <- nth1.
    rewrite <- nth2.
    assumption.
  } {
    apply nth_S_rev in nth1.
    apply nth_S_rev in nth2.
    exact(Ind _ _ _ _ _ rlH _ _ nth1 nth2).
  }
Qed.

(* それ以外のリストについては、もとのまま *)
Theorem is_remove_lst_i_i'_j :
  forall {A} (ll1 ll2 : list (list A)) i j,
    remove_lst ll1 i j ll2 ->
    forall i',
      ~i = i' ->
      forall (l1 l2 : list A),
        nth ll1 i' l1 -> nth ll2 i' l2 ->
        l1 = l2.
Proof.
  fix Ind 6.
  intros A ll1 ll2 i j rlH i' neqi l1 l2 nth1 nth2.
  destruct rlH as [i l1' l2' rlH ll | ll1 ll2 l i j rlH].
  {
    destruct i' as [| i'].
    tauto.
    apply nth_S_rev in nth1.
    apply nth_S_rev in nth2.
    apply (nth_unq _ _ _ _ nth1 nth2).
  } {
    destruct i' as [| i'].
    {
      apply nth_eq_O in nth1.
      apply nth_eq_O in nth2.
      rewrite <- nth1.
      rewrite <- nth2.
      reflexivity.
    } {
      apply nth_S_rev in nth1.
      apply nth_S_rev in nth2.
      assert(neqi' : i <> i').
      {
        intro eqi.
        apply neqi.
        rewrite eqi.
        reflexivity.
      }
      exact (Ind _ _ _ _ _ rlH _ neqi' _ _ nth1 nth2).
    }
  }
Qed.

(* i 番目のリストについては、もとのリストより 1 短くなっている *)
Theorem remove_lst_length :
  forall {A} (ll1 ll2 : list (list A)) i j,
    remove_lst ll1 i j ll2 ->
    forall l1 l2,
      nth ll1 i l1 -> nth ll2 i l2 ->
      length l1 = S (length l2).
Proof.
  intros A ll1 ll2 i j rlH l1 l2 nth1 nth2.
  apply (remove'_lst_length _ _ j).
  exact (is_remove_lst_i_j _ _ _ _ rlH _ _ nth1 nth2).
Qed.

(* それ以外については、もとのリストと同じ *)
Theorem remove_lst_length_eq :
  forall {A} (ll1 ll2 : list (list A)) i j,
    remove_lst ll1 i j ll2 ->
    forall i',
      ~ i = i' ->
      forall l1 l2,
        nth ll1 i' l1 -> nth ll2 i' l2 ->
        length l1 = length l2.
Proof.
  intros A ll1 ll2 i j rlH i' neqi l1 l2 nth1 nth2.
  cut (l1 = l2).
  {
    intro eql.
    rewrite eql.
    reflexivity.
  }
  exact (is_remove_lst_i_i'_j _ _ _ _ rlH _ neqi _ _ nth1 nth2).
Qed.


(* i 番目のリストの j 番目の 要素を取ったリストが存在 *)
Theorem exists_remove_lst :
  forall {A} (ll : list (list A)) i,
    i < length ll ->
    forall li,
      nth ll i li ->
      forall j,
        j < length li ->
        exists ll', remove_lst ll i j ll'.
Proof.
  fix Ind 2.
  intros A ll i prf_i li nthH j prf_j.
  destruct ll as [| l ll'].
  inversion nthH.
  destruct i as [| i'].
  {
    apply nth_eq_O in nthH.
    rewrite <- nthH in prf_j.
    generalize (exist_remove'_lst _ _ prf_j).
    intros exsH.
    destruct exsH as [lr rlH].
    exists (cons lr ll').
    apply remove_lst_O.
    assumption.
  } {
    simpl in prf_i.
    apply Coq.Arith.PeanoNat.Nat.succ_lt_mono in prf_i.
    apply nth_S_rev in nthH.
    generalize (Ind _ _ _ prf_i _ nthH _ prf_j).
    intros exsH.
    destruct exsH as [ll'r rlH].
    exists (cons l ll'r).
    apply remove_lst_S.
    assumption.
  }
Qed.

(* i 番目のリストの j 番目の 要素を取ったリストは高々１つ *)
Theorem unq_remove_lst :
  forall {A} (ll : list (list A)) i,
    i < length ll ->
    forall li,
      nth ll i li ->
      forall j,
        j < length li ->
        forall ll1 ll2,
          remove_lst ll i j ll1 -> remove_lst ll i j ll2 ->
          ll1 = ll2.
Proof.
  fix Ind 2.
  intros A ll i prf_i li nthH j j_prf ll1 ll2 rlH1 rlH2.
  destruct ll as [| l ll'].
  inversion prf_i.
  destruct i as [| i'].
  {
    apply nth_eq_O in nthH.
    rewrite <- nthH in j_prf.
    apply remove_lst_O_inv in rlH1.
    destruct rlH1 as [l1 [rlH1' eq1]].
    apply remove_lst_O_inv in rlH2.
    destruct rlH2 as [l2 [rlH2' eq2]].
    rewrite eq1.
    rewrite eq2.
    cut (l1 = l2).
    {
      intro eql.
      rewrite eql.
      reflexivity.
    }
    exact (unq_remove'_lst _ _ j_prf _ _ rlH1' rlH2').
  } {
    simpl in prf_i.
    apply Coq.Arith.PeanoNat.Nat.succ_lt_mono in prf_i.
    apply nth_S_rev in nthH.
    apply remove_lst_S_inv in rlH1.
    destruct rlH1 as [mm1 [rmH1' eq1]].
    apply remove_lst_S_inv in rlH2.
    destruct rlH2 as [mm2 [rmH2' eq2]].
    rewrite eq1.
    rewrite eq2.
    cut (mm1 = mm2).
    {
      intro eqm.
      rewrite eqm.
      reflexivity.
    }
    exact (Ind _ _ _ prf_i _ nthH _ j_prf _ _ rmH1' rmH2').
  }
Qed.