## Stream: Coq users

### Topic: Rewriting computational equivalences in SSReflect

#### 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.

#### 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).
Goal forall n, n + n = n.*2.
move=> n.
``````

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`.

#### 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?

#### 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: :

• `rewrite thm` means `thm` is used to rewrite from left to right.
• `rewrite -thm` means `thm` is used to rewrite from right to left.
• `rewrite /term` means the head constant of `term` is unfolded.
• `rewrite -/term` means `term` is folded .
• `rewrite -[term1]/term2 ` means `term1` is converted into `term2`.

#### Fernando Chu (Apr 02 2023 at 14:10):

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

#### 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.

#### 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)

#### 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.

#### 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 :)

#### 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.

#### 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

#### 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: Jun 16 2024 at 01:42 UTC