gistfile1.coq

Require Import Omega.
Require Import Coq.Vectors.Vector.
Require Import Coq.Vectors.VectorDef.
Open Scope vector_scope.
Require Import Bool.
Require Import List.
Require Import Arith.
Require Import Arith.EqNat.
Require Import Program.

CoInductive triangle_t (T : Type) : nat -> Type :=
| triangle : forall (n : nat), Vector.t T n -> triangle_t T (S n) -> triangle_t T n.

Definition nat_cases (n: nat) :
  { n' : nat | n = S n' } + {n = 0} :=
  match n with
  | O => inright _ eq_refl
  | S n' => inleft _ (exist _ n' eq_refl)
  end.

Definition nth_triangle_aux
  : forall T steps_left stop,
    stop >= steps_left -> triangle_t T (stop - steps_left) -> Vector.t T stop.
  refine (fix fn T (steps_left stop : nat)
                   (pf : stop >= steps_left)
                   (tr : triangle_t T (stop - steps_left))
                   : Vector.t T stop :=
    match steps_left as sl return steps_left = sl -> Vector.t T stop with
    | O => fun Z => _
    | S n' => fun NZ => _
    end (eq_refl steps_left)).
  subst. rewrite <- minus_n_O in tr. inversion tr; subst. apply X.
  apply fn with (steps_left := n').
    rewrite NZ in pf. omega.
    rewrite NZ in tr. inversion tr; subst.
      assert (S (stop - S n') = stop - n'). omega.
      rewrite H in X0. apply X0.
Defined.

Definition nth_triangle {T : Type} (idx : nat) (tr : triangle_t T 0) : Vector.t T idx.
  refine (nth_triangle_aux T idx idx _ _).
  auto.
  rewrite minus_diag. apply tr.
Defined.

Fixpoint pt_aux h len (v : Vector.t nat len) : Vector.t nat len :=
  match v with
  | Vector.nil => Vector.nil nat
  | Vector.cons h' _ t' =>
      Vector.cons nat (h + h') _ (pt_aux h' _ t')
  end.