有限列

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.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
xs: fin_seq A n
fin n -> A
  Proof.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
xs: fin_seq A n
fin n -> A
    induction xs.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
fin 0 -> A
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
xs: fin_seq A n
IHxs: fin n -> A
fin (S n) -> A
    -
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
fin 0 -> A
      intro p.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
p: fin 0
A
      contradict p.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
fin 0 -> False
      apply no_fin0.
    -
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
xs: fin_seq A n
IHxs: fin n -> A
fin (S n) -> A
      intro p.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
xs: fin_seq A n
IHxs: fin n -> A
p: fin (S n)
A
      revert xs.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
IHxs: fin n -> A
p: fin (S n)
fin_seq A n -> A
      set (m := S n).
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
IHxs: fin n -> A
p: fin (S n)
m:= S n: nat
fin_seq A n -> A
      fold (pred (S n)) in IHxs.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
IHxs: fin (Nat.pred (S n)) -> A
p: fin (S n)
m:= S n: nat
fin_seq A n -> A
      fold m in IHxs.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
m:= S n: nat
IHxs: fin (Nat.pred m) -> A
p: fin (S n)
fin_seq A n -> A
      destruct p; intro xs.
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
n0: nat
m:= S n0: nat
IHxs: fin (Nat.pred m) -> A
xs: fin_seq A n
A
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
n0: nat
m:= S n0: nat
IHxs: fin (Nat.pred m) -> A
p: fin n0
xs: fin_seq A n
A
      +
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
n0: nat
m:= S n0: nat
IHxs: fin (Nat.pred m) -> A
xs: fin_seq A n
A
        exact a.
      +
A: Type
projection': forall n : nat, fin_seq A n -> fin n -> A
n: nat
a: A
n0: nat
m:= S n0: nat
IHxs: fin (Nat.pred m) -> A
p: fin n0
xs: fin_seq A n
A
        apply (IHxs p).
  Defined.

  Print projection'.
projection' =
fix projection' (n : nat) (xs : fin_seq A n) {struct n} : fin n -> A :=
  fin_seq_rect (fun (n0 : nat) (_ : fin_seq A n0) => fin n0 -> A)
    (fun p : fin 0 => False_rect A (no_fin0 p))
    (fun (n0 : nat) (a : A) (xs0 : fin_seq A n0) (IHxs : fin n0 -> A)
       (p : fin (S n0)) =>
     (let m := S n0 in
      let n1 := S n0 in
      match
        p in fin n2
        return
          (let m0 := n2 in (fin (Nat.pred m0) -> A) -> fin_seq A n0 -> A)
      with
      | @zero n2 =>
          (fun n3 : nat =>
           let m0 := S n3 in
           fun (_ : fin (Nat.pred m0) -> A) (_ : fin_seq A n0) => a) n2
      | @suc n2 f =>
          (fun (n3 : nat) (p0 : fin n3) =>
           let m0 := S n3 in
           fun (IHxs0 : fin (Nat.pred m0) -> A) (_ : fin_seq A n0) =>
           IHxs0 p0) n2 f
      end IHxs) xs0)
    xs
     : forall {n : nat}, fin_seq A n -> fin n -> A

Arguments projection' {n}%_nat_scope xs _
projection' uses section variable A.

  Lemma projection'_cons_zero
    {n}
    (a : A)
    (xs : fin_seq A n)
    : projection' (cons a xs) zero = a.
A: Type
n: nat
a: A
xs: fin_seq A n
projection' (cons a xs) zero = a
  Proof.
A: Type
n: nat
a: A
xs: fin_seq A n
projection' (cons a xs) zero = a
    simpl.
A: Type
n: nat
a: A
xs: fin_seq A n
a = a
    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.
A: Type
n: nat
a: A
xs: fin_seq A n
p: fin n
projection' (cons a xs) (suc p) = projection' xs p
  Proof.
A: Type
n: nat
a: A
xs: fin_seq A n
p: fin n
projection' (cons a xs) (suc p) = projection' xs p
    destruct xs.
A: Type
a: A
p: fin 0
projection' (cons a nil) (suc p) = projection' nil p
A: Type
a: A
n: nat
a0: A
xs: fin_seq A n
p: fin (S n)
projection' (cons a (cons a0 xs)) (suc p) = projection' (cons a0 xs) p
    -
A: Type
a: A
p: fin 0
projection' (cons a nil) (suc p) = projection' nil p
      simpl.
A: Type
a: A
p: fin 0
False_rect A (no_fin0 p) = False_rect A (no_fin0 p)
      reflexivity.
    -
A: Type
a: A
n: nat
a0: A
xs: fin_seq A n
p: fin (S n)
projection' (cons a (cons a0 xs)) (suc p) = projection' (cons a0 xs) p
      simpl.
A: Type
a: A
n: nat
a0: A
xs: fin_seq A n
p: fin (S n)
match p in fin n0 return (fin (Nat.pred n0) -> A) -> fin_seq A n -> A with
| @zero n0 => fun (_ : fin n0 -> A) (_ : fin_seq A n) => a0
| @suc n0 f => fun (IHxs : fin n0 -> A) (_ : fin_seq A n) => IHxs f
end
  (fin_seq_rect (fun (n0 : nat) (_ : fin_seq A n0) => fin n0 -> A)
     (fun p0 : fin 0 => False_rect A (no_fin0 p0))
     (fun (n0 : nat) (a1 : A) (xs0 : fin_seq A n0) 
        (IHxs : fin n0 -> A) (p0 : fin (S n0)) =>
      match
        p0 in fin n1 return (fin (Nat.pred n1) -> A) -> fin_seq A n0 -> A
      with
      | @zero n1 => fun (_ : fin n1 -> A) (_ : fin_seq A n0) => a1
      | @suc n1 f => fun (IHxs0 : fin n1 -> A) (_ : fin_seq A n0) => IHxs0 f
      end IHxs xs0)
     xs)
  xs =
match p in fin n0 return (fin (Nat.pred n0) -> A) -> fin_seq A n -> A with
| @zero n0 => fun (_ : fin n0 -> A) (_ : fin_seq A n) => a0
| @suc n0 f => fun (IHxs : fin n0 -> A) (_ : fin_seq A n) => IHxs f
end
  (fin_seq_rect (fun (n0 : nat) (_ : fin_seq A n0) => fin n0 -> A)
     (fun p0 : fin 0 => False_rect A (no_fin0 p0))
     (fun (n0 : nat) (a1 : A) (xs0 : fin_seq A n0) 
        (IHxs : fin n0 -> A) (p0 : fin (S n0)) =>
      match
        p0 in fin n1 return (fin (Nat.pred n1) -> A) -> fin_seq A n0 -> A
      with
      | @zero n1 => fun (_ : fin n1 -> A) (_ : fin_seq A n0) => a1
      | @suc n1 f => fun (IHxs0 : fin n1 -> A) (_ : fin_seq A n0) => IHxs0 f
      end IHxs xs0)
     xs)
  xs
      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.
A: Type
n: nat
a: A
xs: fin_seq A n
projection (cons a xs) zero = a
  Proof.
A: Type
n: nat
a: A
xs: fin_seq A n
projection (cons a xs) zero = a
    simpl.
A: Type
n: nat
a: A
xs: fin_seq A n
a = a
    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.
A: Type
n: nat
a: A
xs: fin_seq A n
p: fin n
projection (cons a xs) (suc p) = projection xs p
  Proof.
A: Type
n: nat
a: A
xs: fin_seq A n
p: fin n
projection (cons a xs) (suc p) = projection xs p
    simpl.
A: Type
n: nat
a: A
xs: fin_seq A n
p: fin n
projection xs p = projection xs p
    reflexivity.
  Qed.

  Lemma projection_eq
    {n}
    (xs : fin_seq A n)
    : forall p : fin n,
    projection' xs p = projection xs p.
A: Type
n: nat
xs: fin_seq A n
forall p : fin n, projection' xs p = projection xs p
  Proof.
A: Type
n: nat
xs: fin_seq A n
forall p : fin n, projection' xs p = projection xs p
    induction xs; intro p.
A: Type
p: fin 0
projection' nil p = projection nil p
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
p: fin (S n)
projection' (cons a xs) p = projection (cons a xs) p
    -
A: Type
p: fin 0
projection' nil p = projection nil p
      simpl.
A: Type
p: fin 0
False_rect A (no_fin0 p) = False_rect A (no_fin0 p)
      reflexivity.
    -
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
p: fin (S n)
projection' (cons a xs) p = projection (cons a xs) p
      destruct p using fin_S_case.
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
projection' (cons a xs) zero = projection (cons a xs) zero
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
p: fin n
projection' (cons a xs) (suc p) = projection (cons a xs) (suc p)
      +
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
projection' (cons a xs) zero = projection (cons a xs) zero
        simpl.
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
a = a
        reflexivity.
      +
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
p: fin n
projection' (cons a xs) (suc p) = projection (cons a xs) (suc p)
        rewrite projection'_cons_suc.
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
p: fin n
projection' xs p = projection (cons a xs) (suc p)
        rewrite projection_cons_suc.
A: Type
n: nat
a: A
xs: fin_seq A n
IHxs: forall p : fin n, projection' xs p = projection xs p
p: fin n
projection' xs p = projection xs p
        apply IHxs.
  Qed.
End FinSeq.