Stream: Coq users

Topic: Advice on managing proliferation of terms

Patrick Nicodemus (Nov 25 2021 at 04:35):

Hi;
A problem I am dealing with is that I run a command like "simpl", it begins to unfold everything in sight and my goal (or my hypotheses) become so complex as to become utterly unreadable. There is a more specific problems I would like to address:
Sometimes when I try to capture a term using "set (j:= f(g(_ x...))" or some other expression, it doesn't work, and nothing happens. I think this error is related to coercions in the terms; when I run "simpl in *" it fixes the problem, presumably because everything gets coerced to the same "bottom" type. I would like to avoid running "simpl" or "cbn" if all i need to do is such a command, but I don't know how to deal with these coercion issues in a more direct way.
How can I deal in general with this kind of 'term proliferation'

Michael Soegtrop (Nov 25 2021 at 08:20):

Both simpl and cbn can be given detailed options to specify what simplifications to do. Click on the "reductions" argument here cbn for details. In case you want to reduce let bindings (you wrote set - not sure what this is) and only let bindings, cbn zeta should do the job.

Paolo Giarrusso (Nov 25 2021 at 09:29):

In general, you can use Set Printing All to see the raw terms and find out what mismatch simpl is fixing (I'd advise trying tool support for showing tactic diffs, but how to get it might be a separate question).

Paolo Giarrusso (Nov 25 2021 at 09:31):

Also you might want to limit reduction for the functions in your goal, to stop simpl from reducing too much.

Christian Doczkal (Nov 25 2021 at 10:55):

Another trick is to define an identity function locked : forall T, T -> T, prove forall T (x:T), x = locked x, make locked opaque, and then use rewrite (lock <arg>) on arguments to functions that you don't want to simplify (and rewrite with -lock afterwards).

Christian Doczkal (Nov 25 2021 at 10:57):

If you're using set, you're maybe using ssreflect/mathcomp where locked and lock are already defined.

Ana de Almeida Borges (Nov 25 2021 at 11:56):

If the problem is specifically with coercions, you can Set Printing Coercions instead of Set Printing All, which should be more readable. There are also other flags that disable some but not all of the printing.

Patrick Nicodemus (Nov 25 2021 at 19:59):

Paolo Giarrusso said:

Also you might want to limit reduction for the functions in your goal, to stop simpl from reducing too much.

ok great this sounds like what i want. How do I "limit reduction"

Paolo Giarrusso (Nov 25 2021 at 20:15):

I was thinking of Arguments, especially ... simpl never, Opaque, and of what Christian suggested above.

Patrick Nicodemus (Nov 25 2021 at 21:25):

Christian Doczkal said:

Another trick is to define an identity function locked : forall T, T -> T, prove forall T (x:T), x = locked x, make locked opaque, and then use rewrite (lock <arg>) on arguments to functions that you don't want to simplify (and rewrite with -lock afterwards).

this is a clever trick, thanks

Karl Palmskog (Nov 25 2021 at 21:49):

the sledgehammer/CoqHammer style of proving things avoids arriving at big terms by only letting high-level automation tactics actually unfold definitions, and then in a controlled way, e.g., by passing a list of definition names that are allowed to be unfolded

Karl Palmskog (Nov 25 2021 at 21:51):

so, for example, if you mostly use sauto(https://coqhammer.github.io/#sauto) with various parameters and go forward in your proofs mostly by asserting facts, you don't get the big term problem, and usually don't use simpl/cbn at all.

Last updated: Apr 18 2024 at 15:01 UTC