Fernando Chu (Apr 02 2023 at 00:31): 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
-? Testing without the - replaces n1 with (0 + n1)%Nrec, what's Nrec? I'd have expected that the - does nothing.n1? rewrite usually just rewrited the first instance. 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.
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: Oct 13 2024 at 01:02 UTC