The Coq mailing list

[Lars Rasmusson <Lars.Rasmusson AT sics.se>]

As the others have said, it seems to be a problem with "Program".

I tried to rewrite TestERR without using Program.

I use the "Convoy Pattern" idea to not lose the info that n=0 in the first case and n=S n' in the second case.

I had to convince the type checker that 

* when n=0 then t nat 0  actually is equal  t nat ((S pad)*n, and

* when n=S n; then  t nat (S pad + (S pad * n')) -> t nat ((S pad)*n)

To do that, I defined two functions, f1 and f2 that took a term of the first type and returned the second type.

My question is:  is there a more elegant way to do this, without having to introduce the "dummy type coersion functions"?

Here is my development:

Definition f1 (pad n:nat) : n = 0 -> t nat 0 -> t nat ((S pad)*n).

  intros. subst. rewrite mult_0_r. auto. Qed.

Definition f2 (pad n n':nat) : n = S n' -> t nat (S pad + (S pad * n')) -> t nat ((S pad)*n).

  intros H H0. replace (S pad + S pad * n') with (S pad * S n') in H0 by ring.

  subst; auto.

Qed.

Definition TestERR (n pad:nat) (v:Vector.t nat n) : Vector.t nat ((S pad)*n) :=

  match n as m return n=m -> Vector.t nat ((S pad)*n) with

    | 0 => fun H => f1 _ _ H (Vector.nil nat)

    | S p => fun H => f2 _ _ _ H (append (const 0 (S pad)) (const 0 ((S pad)*p)))

  end

    (eq_refl n).