Stream: Coq users

Topic: A technical question when reading the mathcomp book


view this post on Zulip TX Xia (Aug 02 2022 at 10:21):

Hi,
I was reading chapter 7 of the mathcomp book. And this was the code associated.
When running

  Fail Check forall T n (t : n.-tuple T),
      let LHS := [LHS of size_tuple _] in
      let RDX := size (rev t) in
      [unify LHS with RDX].

The failure message on my computer and on the web version of coq is

The command has indeed failed with message:
In environment
T : Type
n : nat_eqType
t : n .-tuple T
LHS := (fix size (s : seq T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end)
((fix catrev (s1 s2 : seq T) {struct s1} : seq T := match s1 with
| [::] => s2
| x :: s1' => catrev s1' (x :: s2)
end) (let (tval, _) := t in tval) [::])(*...*) :
nat
RDX := size (rev t) : nat
The term "erefl LHS" has type "LHS = LHS"
while it is expected to have type "LHS = RDX" (cannot satisfy
constraint
"(fix size (s : seq ?T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end) ?t" == "(fix size (s : seq T) : nat := match s with
| [::] => 0
| _ :: s' => (size s').+1
end)
((fix catrev (s1 s2 : seq T) {struct s1} : seq T := match s1 with
| [::] => s2
| x :: s1' => catrev s1' (x :: s2)
end) (let (tval, _) := t in tval) [::])").

But according to the book the message should be:

Error:
In environment
T : Type
n : nat
t : n .-tuple T
LHS := size (tval ?94 ?92 ?96) (*...*) : nat
RDX := size (rev (tval n T t))           : nat
The term "erefl ?95" has type "?95 = ?95" while
it is expected to have type "LHS = RDX".

What should I do to make the error message more readable?
Thanks!

view this post on Zulip Enrico Tassi (Aug 02 2022 at 11:24):

Coq decided to unfold the definition of size in the error message, I'm afraid you can't do much


Last updated: Jan 28 2023 at 06:30 UTC