The Coq mailing list

[James Wilcox <wilcoxjay AT gmail.com>]

Hello,

This appears to be a bug in Program, but it works correctly in Coq 8.5. So one option would be to upgrade (either to latest git or to one of the beta releases; I confirmed that this works correctly in both 8.5beta1 and 8.5beta2).

Hope this helps,

James

On Tue, May 5, 2015 at 11:00 PM, 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