agda
Rename `≤-stepsʳ` functions in `Data.Nat.Properties`?
These proof names don't really match the style of the rest of the library, where unless it's got a concrete special algebraic name, the names tend to just spell out the result. I suggest deprecating these for e.g. m≤n⇒m≤n+o?
Interesting question. The current name describes the action performed on the proof term while you're proposing a name that indeed "just spells out the result". So the former describes what the arrow does while you're suggesting that it be named after what it is a proof of.
Categorically-oriented me prefers the former (i.e. the current name). However, given that UIP holds for ≤, that's kind of moot, since there's essentially a single member of that type.
A very long-winded way to say: I'm fine with this rename, for this case. But there may well be other cases that look like it where I'd prefer the action-related name.
Agree it is an interesting question.
But I can't help thinking that the answer lies not with these proofs in particular, but the one they derive from, namely ≤-step... which should have its named changed as well, for consistency's sake, if nothing else.
As for the 'being/doing' distinction in terms of how one goes about naming things, any proof/function whose name is an implication is surely, under propositions-as-types, a description of its being a transformation from premise(s) to conclusion. I'm not sure that use of the verb 'step(s)' in the name(s) here helps much... if you want to know (the intensional information as to) how the transformation takes place, better to look inside the definition, and leave the name 'abstract'/declarative/extensional? Or am I misunderstanding your point @JacquesCarette ?
Proposal: rename ≤-step to n≤1+n
EDITED: blast! @JacquesCarette is correct, as the obvious lemma with that name follows immediately after ≤-step.
Revised proposal: rename ≤-step to m≤n⇒m≤1+n
If I had to guess, I'd say that ≤-step was named that way because of the one in equality reasoning, which is used to "take a step" in an equational proof (even though it's just a different name for trans).
@jamesmckinna you are not misunderstanding me. I was writing out my thought process "out loud" as it were. In the hopes that others would (eventually?) join in, and we could arrive at a reasonable outcome.
But as far as this case is concerned: +1 for n≤1+n (which might also exist?)
Hmmm. I'm wondering about my (revised) proposal above (thumbs down everyone, at least for the time being ;-)). The lemma name change seems OK, and (even!) well-motivated. But the name suffix -step arises because of the alternative definition _≤′_ of ≤ needed for the streamlined proofs in Data.Nat.Induction. And I don't know what our library policy (?) is about having a name such as m≤′n⇒m≤′1+n as a constructor of _≤′_ (for such would be the name required for the formal correspondence). Maybe that's OK? But I suspect that there are a lot more uses of ≤′-step and ≤-step in the library besides those in Data.Nat.Properties... 27 each it turns out. Grrr.
So maybe @MatthewDaggitt 's more modest proposal is the way to go.
I think we're significantly more liberal in the names we allow as constructors so I don't have a problem keeping ≤′-step as a constructor name while changing the others.
Still to do:
- [ ]
Data.Integer.Properties - [ ]
Data.Rational.Unnormalised.Properties - [ ]
Data.Rational.Properties
Er... OK, I'd commented in the PR to the effect that I wouldn't be doing those this time round... but yes, now I will.
Some (potential) discrepancy in naming... for Integer.Properties, I have used 1+j (rather than suc[j]) and pred[i]. I had some idea that suc[*] syntax was being itself deprecated... as it is, the library now has both i≤suc[i] AND i≤1+i... the first because it falls under properties of suc, the second because it is the new name of the former ≤-step... My instinct is to deprecate the first in favour of the second, but the two had previously coexisted happily (if not, perhaps, intentionally so?), so I decided not to make that change in addition to the other renamings. But thoughts on the matter welcome!
Modulo the above naming considerations, I think we could move to close this issue. And in any case, all that would be required would be an additional deprecation.
Er... OK, I'd commented in the PR to the effect that I wouldn't be doing those this time round... but yes, now I will.
Ah miscommunication. I was going to merge the PR, but I didn't want to close the issue (and open a new issue just for the remaining tasks), so was documenting that these were still do. It wasn't an instruction to do them, sorry! Thank you for doing so anyway :+1:
the two had previously coexisted happily (if not, perhaps, intentionally so?), so I decided not to make that change in addition to the other renamings. But thoughts on the matter welcome!
I think the best thing to do is to open another issue and leave it for now!