The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

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