(*|
有限列
======
|*)

Require Import finite.

Set Implicit Arguments.

Inductive fin_seq (A : Type) : nat -> Type :=
  | nil      : fin_seq A O
  | cons {n} : A -> fin_seq A n -> fin_seq A (S n).

Scheme All for fin_seq.

Arguments nil {A}.

Section FinSeq.
  Context {A : Type}.

  Fixpoint projection'
    {n}
    (xs : fin_seq A n)
    : fin n -> A.
  Proof.
    induction xs.
    -
      intro p.
      contradict p.
      apply no_fin0.
    -
      intro p.
      revert xs.
      set (m := S n).
      fold (pred (S n)) in IHxs.
      fold m in IHxs.
      destruct p; intro xs.
      +
        exact a.
      +
        apply (IHxs p).
  Defined.

  Print projection'.

  Lemma projection'_cons_zero
    {n}
    (a : A)
    (xs : fin_seq A n)
    : projection' (cons a xs) zero = a.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Lemma projection'_cons_suc
    {n}
    (a : A)
    (xs : fin_seq A n)
    (p : fin n)
    : projection' (cons a xs) (suc p) = projection' xs p.
  Proof.
    destruct xs.
    -
      simpl.
      reflexivity.
    -
      simpl.
      reflexivity.
  Qed.

  Fixpoint projection
    {n}
    (xs : fin_seq A n)
    : fin n -> A :=
    match xs with
    | nil       => fun p => False_rect A (no_fin0 p)
    | cons x ys => fun p => (
          match p in fin m return fin_seq A (pred m) -> A with
          | zero  => fun _  => x
          | suc q => fun zs => projection zs q
          end
        ) ys
    end.

  Lemma projection_cons_zero
    {n}
    (a : A)
    (xs : fin_seq A n)
    : projection (cons a xs) zero = a.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Lemma projection_cons_suc
    {n}
    (a : A)
    (xs : fin_seq A n)
    (p : fin n)
    : projection (cons a xs) (suc p) = projection xs p.
  Proof.
    simpl.
    reflexivity.
  Qed.

  Lemma projection_eq
    {n}
    (xs : fin_seq A n)
    : forall p : fin n,
    projection' xs p = projection xs p.
  Proof.
    induction xs; intro p.
    -
      simpl.
      reflexivity.
    -
      destruct p using fin_S_case.
      +
        simpl.
        reflexivity.
      +
        rewrite projection'_cons_suc.
        rewrite projection_cons_suc.
        apply IHxs.
  Qed.
End FinSeq.