Kazuhiko Sakaguchi (Feb 10 2023 at 16:25): Kazuhiko Sakaguchi (Feb 10 2023 at 16:25):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?
Kazuhiko Sakaguchi (Feb 10 2023 at 16:27):Ah, cbn behaves as I expected (but it has other issues in MathComp).
Janno (Feb 10 2023 at 16:37):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.
Kazuhiko Sakaguchi (Feb 10 2023 at 17:00):Thanks for the pointer!
Paolo Giarrusso (Feb 10 2023 at 17:08):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.
Kazuhiko Sakaguchi (Feb 10 2023 at 17:13):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.
Paolo Giarrusso (Feb 10 2023 at 17:14):Sure I wasn't suggesting that as a fix
Paolo Giarrusso (Feb 10 2023 at 17:15):Rather, as a data point that seems (to me) unexplained by Janno's theory, even if the bug he mentions definitely exists
Janno (Feb 10 2023 at 17:24):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?
Paolo Giarrusso (Feb 10 2023 at 17:32):I was missing this point: so projections can form a match context (maybe even primitive ones)?
Enrico Tassi (Feb 10 2023 at 20:25):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.
Enrico Tassi (Feb 10 2023 at 20:26):I don't recall how the bug interacts with ! , unfortunately.
Enrico Tassi (Feb 10 2023 at 20:26):But this may explain the discrepancy with cbn.
Enrico Tassi (Feb 10 2023 at 20:26):(which should not have this specific bug)
Paolo Giarrusso (Feb 10 2023 at 20:36):Is that bug related to https://github.com/coq/coq/pull/13448, or just a different bug that also involves wrappers?
Paolo Giarrusso (Feb 10 2023 at 20:37):And not sure if you meant to say "constants hiding constants hiding matches" or just one constant is enough
Enrico Tassi (Feb 10 2023 at 22:46):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.
Enrico Tassi (Feb 10 2023 at 22:47):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.
Enrico Tassi (Feb 10 2023 at 22:47):I say it is a bug, but there is no precise spec, so it more of an opinion :+)
Kazuhiko Sakaguchi (Feb 11 2023 at 11:30):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
Paolo Giarrusso (Feb 11 2023 at 13:38):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.
Kazuhiko Sakaguchi (Mar 08 2023 at 10:48):FTR, I opened an issue on GitHub: https://github.com/coq/coq/issues/17356
Last updated: Oct 04 2023 at 19:01 UTC