coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] autorewrite neglects sub-patterns?

From: Kevin Hamlen <hamlen AT utdallas.edu>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] autorewrite neglects sub-patterns?
Date: Thu, 7 Jun 2018 13:02:03 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=hamlen AT utdallas.edu; spf=Pass smtp.mailfrom=hamlen AT utdallas.edu; spf=None smtp.helo=postmaster AT esa4.hc50-71.r1.ces.cisco.com
Ironport-phdr: 9a23:x++G3xwVzJYR46LXCy+O+j09IxM/srCxBDY+r6Qd1OwSIJqq85mqBkHD//Il1AaPAd2Graocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HTbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRH2iCkJKj03/m/ZhcN/kK1VrxOhqgdjw4PXeoyZKOZyc63fcN4cWGFPXtxRVytEAo6kaoUAEfQBPeder4LgpVUBtx6+BQ2yC+Pp1zRFgX/20rc/0+QlDw7G2hctH88SsHvJttr1MKMSXvquzKXS0zrMcu5W1C775YPVcR4huemBULJufcbLxkQiFxnJgkuQpID4JT+Zy+cAvmiD4+Z9Se6jkXMrpgJvrjS1xMoglpPFip8bx1zY7Sl13Zg5KNmiREJmfNKoDIFcuz+VOodoWM8uXm5ltSU8x7Ybo5C0ZjIKx44ixxPHa/yIbYyI4hX7WemPOjd3nn1odKi/hxmu8UWs1vTwW8up3FpQtCpJj8PAuWwT2BzI8MSIVvp9/ly91jaIzQzc9uZEIUUsmaraLZ4u3KIwm4ITvEjdBCP7l0X7gLWIekgk5+Sk8fnrb7bmq5OEMo97kAD+MqAgmsylBuQ4NxADX2iB9uS50L3s40v5Ta5Xjv0qj6bWqpTaJcABqa6iGQNazJss6wunAze8zNsYhWUHLE5CeB+fk4fpPEjOLOnkAve7nlSjiyxmx+vGP73kGpXCNGLPkLbnfbZn6k5T0hA/zd5F58EcNrZUdPn0Qwr6sMHSJh4/KQ29hej9XoZTzIQbDEGCHK6feIPbtFuF4Kp7I+CJYIITkCvhJ/Eh4/f1y3I1hAlOLuGSwZILZSXgTbxdKEKDbC+024ZTISIxpgM7CdfSphiHWD9XaWy1WvtgtCwnBIuiCY7YAI2hne7YhXvpLthtfmlDT2u0PzLwbYzdB6URdC6bJstoiXoJWaXzE9Z8hyHrjxfzzv9cFsSR+iAcssm6htVu7rGVlRpvrXkrVoKHiieGQnoylWITTDhw16d68xRw

Dear Coq users,

I'm finding that "autorewrite" fails to consider rewriting opportunities within patterns that match a hint but fail it. Is this behavior intentional? Here's an example:

Require Import NArith.
Open Scope N.

Hint Rewrite N.mod_small using assumption : mydb.

Goal forall x y z, x < y -> (x mod y) mod z = x mod z.
intros.
Fail progress (autorewrite with mydb).
(* This unfortunately fails to progress even though it could successfully rewrite "x mod y" to "x". It fails because it first tries rewriting "(x mod y) mod z" to "x mod y" and is unsuccessful, and then never looks for rewrite opportunities within the matched pattern. *)

(* If I manually strip the "_ mod z" part, it finds the pattern and rewrites it: *)
apply (f_equal (fun n => n mod z)).
progress (autorewrite with mydb).
reflexivity.
Qed.

Is there any work-around? This behavior unfortunately makes autorewrite useless for most of my patterns, forcing me to resort to much slower Ltacs.

Cheers,
Kevin

[Coq-Club] autorewrite neglects sub-patterns?, Kevin Hamlen, 06/07/2018
- Re: [Coq-Club] autorewrite neglects sub-patterns?, Matthieu Sozeau, 06/07/2018
  - Re: [Coq-Club] autorewrite neglects sub-patterns?, Kevin Hamlen, 06/08/2018
    - Re: [Coq-Club] autorewrite neglects sub-patterns?, Matthieu Sozeau, 06/12/2018
- Re: [Coq-Club] autorewrite neglects sub-patterns?, Samuel Gruetter, 06/12/2018