The Coq mailing list

[Ömer Sinan Ağacan <omeragacan AT gmail.com>]

Hi all,

I've been playing with CoInductive definitions and corecursive
functions but and I'm stuck with one problem that I wanted to solve
for learning purposes.

But before that I also want to ask about another problem I'm having
with this simple definition:

  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.

  Definition admit {T: Type} : T.  Admitted.

  CoInductive colst (T : Type) : Type :=
  | ccons : T -> colst T -> colst T.

  CoFixpoint nats_iter (n : nat) : colst nat :=
    ccons nat n (nats_iter (n + 1)).

  Definition nats : colst nat := nats_iter 0.

  Fixpoint take {T : Type} (n : nat) (lst : colst T) : list T :=
    match n with
    | 0 => nil
    | S n' =>
        match lst with
        | ccons h t => h :: take n' t
        end
    end.

  CoFixpoint facs_iter (n : nat) (r : nat) : colst nat :=
    let r' := r * n in
    ccons nat r' (facs_iter (n + 1) r').

  Definition facs : colst nat := facs_iter 1 1.

  Eval compute in (take 9 facs).

This eval command fails with stack overflow. It works fine when n is
8. I was wondering what am I doing wrong, in most other languages same
function works for n > 500 without problems. Or is this because Coq's
default stack depth is very low?

Now my main question, I have this CoInductive definition:

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

What this represents is a data structure that in every level holds a
vector of length `level`. e.g. level 0 has an empty vector, level one
has a vector with one element etc. In data constructor, first argument
is the vector that holds elements, second argument is like 'link' part
of a linked list, it points to rest of the structure.

Now as you may have guessed, I'm trying to implement pascal triangle
using this type. As a first step I tried to implement this generic
index function:

  Fixpoint nth_triangle_aux {T : Type} (idx stop : nat) (tr :
triangle_t T idx) : Vector.t T stop :=
    if beq_nat idx stop then
      match tr with triangle _ _ v _ => v end
    else
      match tr with triangle _ _ _ tr' => nth_triangle_aux (S idx) stop tr' 
end.

  Definition nth_triangle {T : Type} (idx : nat) (tr : triangle_t T 0)
: Vector.t T idx :=
    nth_triangle_aux 0 idx tr.

But Coq gives this error:

  Error:
  In environment
  nth_triangle_aux : forall (T : Type) (idx stop : nat),
                     triangle_t T idx -> Vector.t T stop
  T : Type
  idx : nat
  stop : nat
  tr : triangle_t T idx
  T0 : Type
  n : nat
  v : Vector.t T0 n
  t : triangle_t T0 (S n)
  The term "v" has type "Vector.t T0 n" while it is expected to have type
   "Vector.t ?23 stop".

Error location is first part of if conditional in fixpoint definition.
The problem here is that Coq can't infer that n = idx and idx = stop,
so n = stop. How can I tell that to Coq? Do I need to switch to proof
mode somehow?

Once I got this working, I want to gradually encode more properties of
Pascal's triangle in type level and make sure implementation is
correct, if such a thing is possible.

Thanks.

---
Ömer Sinan Ağacan
http://osa1.net