The Coq mailing list

[Lars Rasmusson <lra 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).

On Wed, May 6, 2015 at 8:00 AM, Vadim Zaliva <vzaliva AT cmu.edu> wrote:

Hi!

Consider this simple definition:

Require Import Coq.Vectors.Vector.
Require Import Omega.
Require Import ArithRing.

Program Definition TestOK (n pad:nat) (v:Vector.t nat n) : Vector.t nat ((S pad)*n) :=
  match n with
    | 0 => Vector.nil nat
    | S p => const 0 ((S pad) + ((S pad)*p))
  end.
Next Obligation.
  ring.
Defined.

Now, I am replacing const in S p case with equivalent concatenation of two consts:

Program Definition TestERR (n pad:nat) (v:Vector.t nat n) : Vector.t nat ((S pad)*n) :=
  match n with
    | 0 => Vector.nil nat
    | S p => append (const 0 (S pad)) (const 0 ((S pad)*p))
  end.
Next Obligation.

It now asks me to prove an obligation:

S pad = S p

Which does not make sense! A quick check of types shows that they indeed match:

Variable p pad : nat.
Check const 0 ((S pad) + ((S pad)*p)).
Check append (const 0 (S pad)) (const 0 ((S pad)*p)).

This is an artificial example which shows simplified case of a problem I am facing as a part of a more complex proof. I am looking for any explanations on why this is happening and how this could be avoided. Thanks!

Sincerely,
Vadim