coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] simpl (unfold definition) only if the argument is in fully normal form

From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] simpl (unfold definition) only if the argument is in fully normal form
Date: Thu, 19 Dec 2019 22:55:41 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay5-d.mail.gandi.net
Ironport-phdr: 9a23:6fBHGRwKQ699FYrXCy+O+j09IxM/srCxBDY+r6Qd2+kRIJqq85mqBkHD//Il1AaPAdyAragd0qGP7vmocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmTSwbalsIBmrsAndudQajIt/Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lL9VrgyvpxJ/wIDabo+aO/V8cazBct0XXnZBU8VLWiBdHo+xYYkCAuwcNuhYtYn9oF4OoAO/Cwa2GOTv1iVHhnnu0qM70uQhFRrJ0xI6H9ISrX/Zq9r1O70MXuCp1qbIyy/Pb/xX2Tf584fHbAohoe2XULJrcsrQyVIvFwDEjlWVrIzqISmV2v4Ls2eF8+ptTOSigHMppQF2pzig3MYsio/Ri40JzVDE7yN5z5gxJd28UkJ0f8OrEIZWuiqHNIV2WtsvT391tCs40LELu4K3cDIXxJkkyRPTceGLfoyK7x77SuqdPDl1iGh4dL+/mRq+61Wsx+zhWsWu31tGsixImcTWuH8XzRzc8M2HR+N9/ki/3TaP0Bje6vtaLkAwj6XaK54szqctmZYJtETMBC72mEHsgK+ZbEok/PWn6+X9brXguJCcK5d4igD4MqswhsyyGfo0PhUMUmSB++mwyKfv8VD6TbhElPE6j63UvZLCKcQevKG5AgtV0og56xa4CjeryNsYkmMZI1JZYh2HiZLlO17PIPD8FviwnU6skCtwyvDdPb3gAo7NLnvCkLfkeLZy9VRcxBA1zd9B+5JYEqsBL+7rWk/tqNzYCQc0PBCzw+b+EdlyyoceWX+UDaKCK6PTsVqI5vo1LOWWZY8Vviz9K/k/6PL0g385gwxVQa781pwOLXu8A/5OIkODYHOqjM1SP30Nu18RRW/2gVu1fj9XbXuoQ+po6Tg2FIugS4jCQoqgmqCpxySqBZ5XY2VLEBaKHGu+JNbMYOsFdC/HepwpqTcDT7X0E9ZwhyHrjxfzzv9cFsSR/yQZsZz5090sub/IlgAp9j1xCsmHlWeAUzMtxz9ad3oNxKl65HdF5BKby6Eh3a5DFs1I5PJMVwogc5jR074iUo2gakf6Zt6MDW2ebJCmDDU2FI9j2dIKalcgXtnkixnC22ylCrkZlvqNCYBmqq8=

add ": simpl nomatch" at the end of the Arguments command?

Gaëtan Gilbert

On 19/12/2019 22:51, Abhishek Anand wrote:

Currently, I can use the Arguments command to tell simpl to unfold a definition iff its arguments are in head normal form. In many cases when the argument are not in fully normal form, `simpl` then only makes the term less "simple":

Require Import ZArith.
Axiom n:nat.
Arguments Nat.modulo !x !y/.
Eval simpl in (Nat.modulo (S n) 3).
(*
= match snd (Nat.divmod n 2 0 1) with
| 0 => 2
| 1 => 1
| S (S _) => 0
end
: nat
*)

Nevertheless, we usually do want to unfold such definitions when the argument is in fully normal form:
Eval simpl in (Nat.modulo 5 3).

Is there a way to tell `simpl` to unfold a definition only when some chosen arguments are in fully normal form?

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/

[Coq-Club] simpl (unfold definition) only if the argument is in fully normal form, Abhishek Anand, 12/19/2019
- Re: [Coq-Club] simpl (unfold definition) only if the argument is in fully normal form, Gaëtan Gilbert, 12/19/2019
  - Re: [Coq-Club] simpl (unfold definition) only if the argument is in fully normal form, Abhishek Anand, 12/19/2019
    - Re: [Coq-Club] simpl (unfold definition) only if the argument is in fully normal form, Jason Gross, 12/20/2019