The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

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