Stream: Coq users

Topic: Advice on managing proliferation of terms


view this post on Zulip 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'

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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"

view this post on Zulip Paolo Giarrusso (Nov 25 2021 at 20:15):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Feb 06 2023 at 11:03 UTC