The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Ralf,

Coq 8.5 has a new replacement for simpl, called cbn. The manual says "The cbn 
tactic is claimed to be a more principled, faster and more predictable 
replacement for simpl". The cbn tactic can be fine tuned using the Arguments 
command and with a few options. I made good experiences with cbn. I think it 
would solve your problem as well.

Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Ralf Jung
Sent: Friday, May 29, 2015 1:47 PM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] "simpl" control

Hi all,

I am currently struggling a lot with the simplification of Coq often going 
way too far, and unfolding terms so deep that the result is huge, and 
unusable.

In particular, to control simplification of "equiv" (the general extensional 
equality, type: forall T, Setoid T -> T -> T -> Prop) I now have the 
following "Arguments":
  Arguments equiv {_ _} !_ !_ /.
Lots of times, that does what I want: When I have an equality of two 
(explicitly written down) pairs, that reduces to the conjunct of the two 
inner equalities. Same for option types. However, unfortunately, the check 
for constructors being in argument position is "too clever": It reduces even 
if there is a function call that results in ultimately a constructor being in 
head position. For example, if I have

  Definition unit t := (foo, t).
  Goal: unit somet == (fooz, barz). simpl
  (* "==" is infix for "equiv" *)

then this will simplify. But I don't want that to happen! This often goes way 
too far, and I'd rather explicitly "unfold unit; simpl" in the few cases that 
I actually want a reduction to happen. Currently, I am using ssreflect's 
"locked" mechanism to work around that in a few places. But that's not always 
possible, sometimes I really need the terms to remain convertible, or else 
things will be really painful.

So, in decreasing order of preference, I wonder whether any of the following 
is possible:
* Can I do something with unit that's a bit like "locked" in that
  it prevents Coq from recognizing constructors "through" unit,
  but retains convertibility? I tried

  Arguments unit t : simpl never.

  But that does not stop Coq from simplifying unit in this case.
  Is there a "simpl never and I mean it"? I also tried "nosimpl"
  from ssreflect, to no avail.
* If the above is not possible, is there something I can do to the
  "Arguments" of equiv such that it only reduces if a constructor
  is present *syntactically* in argument position, *not* considering
  delta reduction?
* And as a last stop, is there some way to make the reduction on equiv
  dependent on the first argument? Say, generally I do not want equiv
  to reduce, but if the first argument is a "T * S" or an "option T",
  I want it to reduce if there is a constructor in both argument
  positions. (That wouldn't help above, but most of the cases where
  annoying simplification happens are with new types I define myself,
  where I am okay with things never simplifying. Plus, this may help
  with some other trouble I am having, which I did not understand well
  enough yet to even ask specific questions.)

So far, I tried Coq 8.4 only. Have there been noticeable changes to 
simplification in Coq 8.5?

Any help would be appreciated.
Kind regards,
Ralf