Stream: Coq users

Topic: Rewriting computational equivalences in SSReflect

view this post on Zulip Fernando Chu (Apr 02 2023 at 00:31):

Hello, I'm learning SSReflect and the book Mathematical Component mentioned (pp. 66) that rewrite -[n1]/(0 + n1) would rewrite instances of n1 with 0 + n1. My questions are

  1. Why the -? Testing without the - replaces n1 with (0 + n1)%Nrec, what's Nrec? I'd have expected that the - does nothing.
  2. Why does it rewrite all the appearances of n1? rewrite usually just rewrited the first instance.
    I could not find answers to these in the book or docs so I'd appreciate your help, thanks in advance.

view this post on Zulip Laurent Théry (Apr 02 2023 at 01:34):

In ssreflect, when you do rewrite /def it is to unfold the definition def. For example,

Goal forall n, n <= n.
move=> n.
rewrite /leq.

This will unfold the definition of less or equal. you can also give a term with holes

rewrite /(_ <= _).

or even a full term.

rewrite /(n <= n).

So when you are doing rewrite [n1]//(0 + n1) you just ask Coq to find all occurrences of n1, convert then to (0 + n1) and unfold the definition of addn. In Ssreflect, addn is defined in term of addn_rec .

Check (addn 1 2).
Check (addn_rec 1 2).
Goal forall n, n + n = n.*2.
move=> n.
rewrite /addn.

This is the exact purpose of the - to tell Coq you want to do a conversion and not an unfolding. I hope this explains 1.
For 2, in Ssreflect, all occurences are rewritten by default. If you take

Goal forall n, (n + n) + (n + n) = (n + n) + (n + n).
move=> n.

rewrite addnn will try to find the first pattern that matches the left hand side of addnn and select all the occurrences. If you want to give an explicite pattern, you can rewrite [n + n]addnn. If you want to give only some occurrences of the pattern you can use {occ}. For example rewrite {1}[n+n]addnn.

view this post on Zulip Fernando Chu (Apr 02 2023 at 03:24):

Thank you a lot for the explanations! 2 is very clear now. About 1, I think I understood everything up to "This is the exact purpose...".

I thought - was meant for the direction of the rewriting. The docs say

The optional initial - indicates the direction of the rewriting of r_item: if present, the direction is right-to-left and it is left-to-right otherwise.

I'd expect the (implicit) equation used to rewriting to be 0 + n1 = n1, or does - take this different meaning when applying rewrite to terms?

view this post on Zulip Laurent Théry (Apr 02 2023 at 08:42):

rewrite is really the swiss knife of ssreflect. It is used to do many things :wink: :

view this post on Zulip Fernando Chu (Apr 02 2023 at 14:10):

Thanks a lot for the in depth explanations! I think I got it now.

view this post on Zulip Stefan Monnier (Apr 02 2023 at 20:59):

Reminds me of a question I've had about many of Coq tactics: in the context of a language in the family of the deceptively simple and elegant pure type systems, this seems terribly ad-hoc and unprincipled, so I wonder if I'm just failing to see the underlying elegance and simplicity of those tactics.

view this post on Zulip Paolo Giarrusso (Apr 02 2023 at 23:00):

Defining "-/x" as the inverse of "/x" seems sensible enough, and generally, ssreflect tactics tend to have a coherent design, and work very robustly in the math-comp context. (Unlike non-ssreflect tactics, or sometimes ssreflect tactics used in a different context)

view this post on Zulip Paolo Giarrusso (Apr 02 2023 at 23:08):

If you're interested in an elegant type theory that is usable directly, you should look into the research program represented by Agda and relatives. In some contexts it works rather well! Other times, Coq is more versatile.

view this post on Zulip Meven Lennon-Bertrand (Apr 03 2023 at 08:44):

Maybe this is a question of taste, but with "vanilla" tactics I often end up with scripts that look like this

unfold foo ; cbn ; rewrite H, a_thm ; fold foo.

all work on the goal and change it to one which is equivalent to it, in quite similar ways, but the tactics to do this are wildly different, each having their own modifiers, quirks, and so on. Having all on them unified as variants of a unique tactic, sharing the many elements that you want them to share (eg the very powerful pattern selection), looks as principled as having these many different ad-hoc tactics :)

view this post on Zulip Paolo Giarrusso (Apr 03 2023 at 11:59):

More pragmatically, even if math-comp-style proofs has a definite barrier to entry, they have a better signal-to-noise ratio when I'm interested in reading the proof. There are lots of details encoded in "line noise" (I've compared that to Perl), but those are the details that paper proof would often find distasteful to spell out, and the syntax is pretty comfortable once you've climbed the learning curve.

view this post on Zulip Paolo Giarrusso (Apr 03 2023 at 12:01):

I also agree that standard tactics don't even have consistent syntax for doing the same thing

view this post on Zulip Fernando Chu (Apr 04 2023 at 03:26):

As a completely new user, I think that while the unified syntax of tactic a : b => c is very nice, when I really want to understand the finer detail it is somewhat confusing. For example, in wlog _ : _ / _, I had expected the : to be the discharge tactical, but it's not. Though I guess people usually don't care that much about that.
Still, I indeed ended up really appreciating this mode of proving stuff, definitely way shorter than constructing the proof term by hand, as I used to in Agda.

Last updated: Oct 04 2023 at 19:01 UTC