Apparently, the `!`

flag in the `Arguments`

command does not let (at least) the `simpl`

tactic to determine whether the corresponding argument reduces to a constructor application *by simpl itself*, and I have the following issue:

```
Structure eqType := EqType {
eq_sort : Type;
eq_op : eq_sort -> eq_sort -> bool;
}.
Structure ordType := OrdType {
ord_sort : Type;
ord_eq_op : ord_sort -> ord_sort -> bool;
le_op : ord_sort -> ord_sort -> bool;
}.
(* The subtyping function from [ordType] to [eqType]. *)
Canonical ord_eqType (O : ordType) :=
{| eq_sort := ord_sort O; eq_op := ord_eq_op O |}.
(* Two [Arguments] directives that are crucial in the following example. *)
Arguments eq_op {!T} x y : rename.
Arguments ord_eqType !O.
Canonical nat_eqType := {| eq_sort := nat; eq_op := Nat.eqb |}.
Canonical nat_ordType :=
{| ord_sort := nat; ord_eq_op := Nat.eqb; le_op := Nat.leb |}.
Goal forall (n : nat), eq_op n n = true.
(* In this case, I want [simpl] to reduce [eq_op] to [Nat.eqb] because it *)
(* comes from a concrete instance of [eqType], namely, [nat_eqType]. *)
Proof.
simpl. (* Expected behavior. *)
Abort.
Goal forall (O : ordType) (x : ord_sort O), eq_op x x = true.
(* In this case, I want [simpl] not to reduce [eq_op] to [ord_eq_op], because *)
(* it comes from an abstract instance of [ordType] and I want to keep [eq_op] *)
(* as the canonical comparison function for *abstract* [eqType] instances. *)
Proof.
simpl. (* Unexpected behavior. *)
Abort.
```

Since I instructed Coq to unfold `eq_op`

and `ord_eqType`

only when the given structure instance reduces to a constructor application, I expected `@eq_op (ord_eqType O)`

to unfold only when `O`

is (or reduces to) a constructor application, which means `O`

is a concrete instance. Is there any workaround for this issue?

Ah, `cbn`

behaves as I expected (but it has other issues in MathComp).

This is a known issue. `simpl`

will do this even when you add `Arguments ord_eqType : simpl never`

. See https://github.com/coq/coq/issues/15768 for some discussion and pointers related to this.

Thanks for the pointer!

I knew about that bug but something seems missing: `Arguments eq_op : simpl never.`

changes the result, while the bug appears with no simplification tweaks or with the original Arguments. And yet, `eq_op`

's argument doesn't seem to reduce to a constructor, _and_ `eq_op`

is not appearing in a match context — which is the exception to `simpl never`

IIUC this comment.

But `simpl never`

breaks the first example `Goal forall (n : nat), eq_op n n = true`

. As I expressed in the comment, I want `eq_op`

to unfold only when the instance given as its first argument is concrete.

Sure I wasn't suggesting that as a fix

Rather, as a data point that seems (to me) unexplained by Janno's theory, even if the bug he mentions definitely exists

I think it is the attempt of simplifying `eq_op`

that leads `simpl`

to be tempted by `ord_eqType`

. `eq_op`

gets unfolded to a `match`

statement and then `ord_eqType`

is no longer off limits. Or am I missing something?

I was missing this point: so projections can form a match context (maybe even primitive ones)?

IIRC simpl has a big when it comes to constants hinding a constand hiding a match. In this case it gets confused, and does not reduce. This is why there is surprisingly no simpl directive for these projections in mathcomp.

I don't recall how the bug interacts with ! , unfortunately.

But this may explain the discrepancy with cbn.

(which should not have this specific bug)

Is that bug related to https://github.com/coq/coq/pull/13448, or just a different bug that also involves wrappers?

And not sure if you meant to say "constants hiding constants hiding matches" or just one constant is enough

You need two IIRC. simpl tries to understand if a delta would expose a iota. If the match is not there, but only behind a second delta, it gets confused.

Paolo Giarrusso said:

Is that bug related to https://github.com/coq/coq/pull/13448, or just a different bug that also involves wrappers?

No, it was there even before simpl never was added.

I say it is a bug, but there is no precise spec, so it more of an opinion :+)

For me, fixing `cbn`

so that we can replace `simpl`

with `cbn`

in MathComp is another potential solution. In this direction, the first issues I hit are that refolding in `cbn`

does not seem to work very well and `SimplIsCbn`

seems somewhat broken. https://github.com/coq/coq/issues/17251

That seems new, but the bug tracker already has quite a few bugs on simpl vs cbn... My 2 cents as an outsider: there's enough that I'd estimate the problem as PhD-thesis-sized, except that the last PhD thesis on the topic, while adding cbn, hasn't been able to supersede simpl...

Specifying simplification as a backtracking-free rewrite system seems more attractive (I and Enrico have agreed on this) and matches more closely other systems like Agda and Lean, but it seems invasive.

FTR, I opened an issue on GitHub: https://github.com/coq/coq/issues/17356

Last updated: Jun 24 2024 at 12:02 UTC