The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Thanks. That is better but does not completely solve the problem:

Require Import ZArith.
Axiom n:nat.
Arguments Nat.modulo !x !y/: simpl nomatch.
Eval simpl in (Nat.modulo (S n) 3).
(*
     = S n mod 3
     : nat
*)
Eval simpl in (Nat.modulo 5 3).
(*
2
*)

However, I want this to not simplify, but it does:

Eval simpl in (Nat.modulo (S n) (S n)).

(*
     = n -
       snd
         match n with
         | 0 => Nat.divmod n n 1 n
         | S u' => Nat.divmod n n 0 u'
         end
     : nat
*)

Similarly, I want the following to not simplify, but it does:

Arguments Z.of_nat !n: simpl nomatch.
Eval simpl in (Z.of_nat (S n)).

(*

     = Z.pos (Pos.of_succ_nat n)
     : Z

*)

Thanks

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Thu, Dec 19, 2019 at 1:55 PM Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net> wrote:

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/