The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

On Mon, May 9, 2016 at 5:38 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

My guess would be you need "Obligation Tactic := program_simpl; ring."
 That would have it perform the same simplifications that "Next
Obligation." performs before showing you the problem.

Thanks! I did not realize that "Next Obligation" performs simplification.

Your suggestion solved the problem. However I am stumbled at another one, illustrated by the following example:

Require Coq.Program.Tactics.

Record Matrix (m n : nat).

Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q):

  Matrix (m*p) (n*q). Admitted.

Program Fact kp_assoc

        (xr xc yr yc zr zc: nat)

        (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc):

  kp x (kp y z) = kp (kp x y) z.

Under Coq-8.4 it generates obligations which I could try to solve. However under Coq-8.5 it just gives me the following error:

Error: Cannot infer this placeholder of type

"xr * yr * zr = xr * (yr * zr)" in environment:

xr, xc, yr, yc, zr, zc : nat

x : Matrix xr xc

y : Matrix yr yc

z : Matrix zr zc

Any suggestions?

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060