Stream: Coq users

Topic: How can I make ssreflect stop unfolding all my Fixpoints?


view this post on Zulip Tiara Sinlo (Jan 27 2024 at 13:29):

SSReflect somehow always tries to unfold any Fixpoint it gets its hands on, even if there is nothing to apply:

  T : Type
  x, h : T
  t : list T
  ============================
  In x (h :: t)  True

case; [admit|].

  T : Type
  x, h : T
  t : list T
  ============================
  (fix In (a : T) (l : list T) {struct l} : Prop :=
     match l with
     | [] => False
     | b :: m => b = a  In a m
     end) x t  True

while destruct doesn't do this:

move=>H; destruct H; move: H; [admit|].

  T : Type
  x, h : T
  t : list T
  ============================
  In x t  True

Can I change some setting in ssreflect to stop this behaviour? This also happens sometimes in implicit arguments that aren't printed, which produces some annoying unification failures.

view this post on Zulip Paolo Giarrusso (Jan 27 2024 at 14:20):

Does simplifying first stop this?

view this post on Zulip Paolo Giarrusso (Jan 27 2024 at 14:21):

Your In term has a redex, and destruct and case must unfold the redex to proceed

view this post on Zulip Paolo Giarrusso (Jan 27 2024 at 14:25):

simpl does something more, that is refold your fixpoint. Your example suggests that destruct does that too, but I don't think that's part of destruct's spec?

view this post on Zulip Paolo Giarrusso (Jan 27 2024 at 14:27):

so, I'm confused about "there is nothing to apply" part.

view this post on Zulip Paolo Giarrusso (Jan 27 2024 at 14:36):

About this happening in implicit arguments, it might be good to see an actual example, even not minimized.

view this post on Zulip Tiara Sinlo (Jan 27 2024 at 16:14):

Yes, simpl first stops it. I'm still learning all of this, so I'm not up to speed with terminology, but "there is nothing to apply" should be "not beta-reducible", I think. As in, why do ssreflect tactics do unfold->fix-reduction->beta-reduction but then leave the (non beta-reducible) fixes produced by fix-reduction unfolded? (unlike, apparently, destruct)

This is more a general feeling but "vanilla" coq usually "cleans up" after fix-reduction whereas ssreflect tends to dump fix everywhere

view this post on Zulip Tiara Sinlo (Jan 27 2024 at 16:16):

As to the implicit argument part, that turned out to be a different problem (that I also don't understand) after I tried minimizing it. I made a gist here

view this post on Zulip Cyril Cohen (Jan 29 2024 at 07:46):

CC @Enrico Tassi

view this post on Zulip Enrico Tassi (Jan 29 2024 at 12:08):

The automatic-refolding code post-dates SSR. In your case you have to rewrite -/(In x t) in order to clean up the mess.
Said that, many of these unfoldings can be prevented by using lemmas, eg mem x (h :: tl) = x == y || mem x tl (we have these for mem in bool of course). After the rewrite you would case on x == y, which is less problematic.

view this post on Zulip Tiara Sinlo (Jan 29 2024 at 12:27):

Very interesting, thank you! Would SSR accept a contribution to add automatic refolding and is this something that can be done without a PhD in a reasonable timeframe?

view this post on Zulip Enrico Tassi (Jan 29 2024 at 12:35):

It should be about calling a function/passing a flag. I even think that they tried (to always refold), but there was a visible performance problem. Refolding, IIRC, tries to unify goal sub-terms with folded candidates, without too much of a "strategy".

view this post on Zulip Tiara Sinlo (Jan 29 2024 at 12:39):

Would it be possible/help to remember which fixes were produced by fix-reduction and only attempt refolding these? (refolding these should never fail I think?)

view this post on Zulip Enrico Tassi (Jan 29 2024 at 12:41):

This goes beyond my knowledge. The PhD that worked on refolding is not active anymore, but his advisor is. @Hugo Herbelin do you recall how it works? Do you have a pointer to the thesis?

view this post on Zulip Hugo Herbelin (Jan 29 2024 at 21:07):

The PhD student @Enrico Tassi is talking about is Pierre Boutillier and he's the author of the refolding abstract machine used in cbn. Beforehand, there was already a refolding machinery in simpl and hnf, which destruct was using. The relevant functions used by destruct are Tacred.reduce_to_atomic_ref and Tacred.reduce_to_quantified_ref. I guess it would be enough that ssreflect case calls them, the same way as destruct calls them.

I think it would be valuable for users to have more convergence between ssreflect tactics and vanilla tactics.

view this post on Zulip Enrico Tassi (Jan 30 2024 at 12:10):

Well, it calls Tacred.reduced_to_quantified_ind https://github.com/coq/coq/blob/a6d226f4074da9e2be6a735ce38142acebfbee12/plugins/ssr/ssrelim.ml#L203

view this post on Zulip walker (Jan 30 2024 at 12:39):

Not exactly using pure ssreflect, but if you are the one creating the fixpoint function. It possible to create it with coq equations. Then nothing gets simplified automatically. To simplify everything there is a special auto-rewrite based tactic (simp). or you can use on of the custom (but automatically generated) rewriting lemmas that give you fine control on how simplification happens.

view this post on Zulip Hugo Herbelin (Jan 30 2024 at 18:37):

Enrico Tassi said:

Well, it calls Tacred.reduced_to_quantified_ind https://github.com/coq/coq/blob/a6d226f4074da9e2be6a735ce38142acebfbee12/plugins/ssr/ssrelim.ml#L203

Ok, I see. Then, apparently, the conclusion of the unfolded_c_ty there is discarded. I don't know well what saturate does. Is it important that it restarts from c_ty rather than from unfolded_c_ty?


Last updated: Jun 13 2024 at 19:02 UTC