Stream: Coq users

Topic: Mathematical Components book example problem.

Andrey Klaus (Apr 15 2021 at 14:51):

Hello,

It looks to me like it is some kind of problem in Coq or in its base libraries.

I'm reading Mathematical Components book. There is an example on page 103:

Lemma eqnP {n m : nat} : reflect (n = m) (eqn n m).
Proof.
  apply: (iffP idP).

after the apply: (iffP idP). I have the next goal

n, m : nat
  ============================
  ?Goal -> reflect (n = m) (eqn n m)

while acording to the book I should have this one:

n : nat
m : nat
===================
m = n -> eqn m n

It looks to me like system loses the information.
2 questions:
1) Is there a way to solve the goal?
2) Is this a new behavior of system or some kind of bug?

$ coqc -v
The Coq Proof Assistant, version 8.13.2 (April 2021)
compiled on Apr 15 2021 14:21:12 with OCaml 4.08.1

Enrico Tassi (Apr 15 2021 at 14:59):

You probably have some wrong settings. It is your entire file?

Andrey Klaus (Apr 15 2021 at 15:02):

You are right.

Andrey Klaus (Apr 15 2021 at 15:03):

when placed to dedicated file it works as expected

Andrey Klaus (Apr 15 2021 at 15:04):

thank you :)

Last updated: Oct 03 2023 at 02:34 UTC