The Coq mailing list

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

Hi all,

With your help to my last questions, I managed to write a function
that produces an infinite data structure, where in every level I'm
holding a a row of Pascal's triangle. Here's the complete program:

  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 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 (S len) :=
    match v in Vector.t _ len' with
    | Vector.nil as v' => Vector.cons nat 1 0 v'
    | Vector.cons h' _ t' => Vector.cons nat (h + h') _ (pt_aux h' _ t')
    end.

  CoFixpoint pt_aux' len (v : Vector.t nat len) : triangle_t nat len :=
    match v with
    | Vector.nil as v' => triangle nat 0 v' (pt_aux' 1 (Vector.cons nat 1 0 
v'))
    | Vector.cons h' _ t' as v' =>
        let vec := Vector.cons nat 1 _ (pt_aux h' _ t') in
        triangle nat _ v' (pt_aux' _ vec)
    end.

  Definition pascals_triangle : triangle_t nat 0 := pt_aux' 0 (Vector.nil 
nat).

Even though I didn't run extracted OCaml code, I checked it and the
code looked reasonable(except keeping length of vectors and using
nats). But for some reason, if I try to run this program:

  Eval compute in (Vector.nth (nth_triangle 3 pascals_triangle)
                              (Fin.F1)).

It takes almost a minute to end and it produces a very weird term:

  Warning: query commands should not be inserted in scripts
       = (fix nth_fix (m : nat) (v' : Vector.t nat m) (p : Fin.t m)
{struct v'} :
            nat :=
            match p in (Fin.t m') return (Vector.t nat m' -> nat) with
            | Fin.F1 q =>
                fun v : Vector.t nat (S q) =>
                match
                  v as v'0 in (Vector.t _ m0)
                  return
                    (match m0 as m1 return (Vector.t nat m1 -> Type) with
                     | 0 => fun _ : Vector.t nat 0 => False -> True
                     | S n => fun _ : Vector.t nat (S n) => nat
                     end v'0)
                with
                | Vector.nil =>
                    fun devil : False => match devil return True with
                                         end
                | Vector.cons h _ _ => h
                end
... 650 lines of code removed ...
       : nat

I tried using a different strategy to evaluate this term:

  Eval simpl in (Vector.nth (nth_triangle 3 pascals_triangle)
                            (Fin.F1)).

This time it ended fast but resulting term is still equally useless:

  Warning: query commands should not be inserted in scripts
       = Vector.nth (nth_triangle 3 pascals_triangle) Fin.F1
       : nat

Can anyone tell me what's wrong with my code and how can I get a 'nat'
out of simple program? Do I have to run extracted OCaml program for
this?

Thanks.

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