replace trivial rcases with have
#200
Conversation
| rcases h₁ with ⟨hl₁, h₁⟩ ; subst hl₁ | ||
| rcases h₂ with ⟨hl₂, h₂⟩ ; subst hl₂ | ||
| rcases (Values.lt_trans h₁ h₂) with h₃ | ||
| have ⟨hl₁, h₃⟩ := h₁ ; subst hl₁ |
There was a problem hiding this comment.
I think we should use rcases in all cases that requires deconstructing the output, like this one.
There was a problem hiding this comment.
what's your rationale?
There was a problem hiding this comment.
I think rcases looks better in this case, and it makes the code style more consistent.
We clearly can't replace rcases with have everywhere, because it's a more powerful tactic. So, I'd prefer a simple rule for when to use one versus the other: use rcases when you need to deconstruct, and use have otherwise.
Using rcases also makes it possible / easier to apply a more advanced deconstruction pattern if that becomes necessary in the future as proofs change.
There was a problem hiding this comment.
I've thought about this more, and I propose a different simple rule for one versus the other: rcases for patterns involving |, and have in all other cases.
The reason I think this is sensible is that it reserves rcases for the times when we're actually splitting goals into separate cases, hence the name. When we destructure an and with ⟨_, _⟩, we're not casing on anything. Lean splits our goal into 1 subcase called "intro", which is not helpful or elegant.
I'm skeptical that we will often be refactoring in a way that changes a term from a non-| pattern to a | pattern or vice versa. And realistically, if we do need to refactor in that way, that will involve more invasive changes to the remainder of the proof (as we now have multiple cases to consider, or no longer have multiple cases to consider, respectively), so it's not a huge burden to change between rcases and have during that refactor.
There was a problem hiding this comment.
Personally I think have looks nicer than rcases for ⟨_, _⟩ expressions. The syntax looks sort of like a let, which makes it easier for me to remember.
There was a problem hiding this comment.
Ok, the rule works.
But I still find having the matching pattern on the LHS really counterintuitive. At least for all the languages I'm used to, the pattern-matching happens on the right.
I see why have is more appealing for binding a single name (a regular let). But for deconstruction,rcases still looks better to me because it reads as match.
Curious: is there any observable effect on proof performance (e.g., faster with have)?
Or we just have to settle this based on the aesthetics? 😄
There was a problem hiding this comment.
CI took 2min 38sec to build the Lean for this PR, vs 2min 41sec to build the Lean in #199 (the previous change). Could be noise, or could be that have is a small improvement vs rcases. (I have to imagine that have is if anything faster, because since it is less powerful, it is doing less. It's also not creating new subgoals like rcases is, even for trivial matches.)
There was a problem hiding this comment.
Yeah, I was hoping that have would be much faster (because it's doing less), so that would be a good justification to go with have even for those who find it less intuitive 🙂
I don't love it but I'll take the 3 seconds!
There was a problem hiding this comment.
Sounds like just a matter of preference then 🤷♀️ I usually reach for let over match because it avoids the extra indentation. (Which is not applicable in this case -- that's just why I like let)
There was a problem hiding this comment.
Agree, just a matter of preference. And we have 2 vs 1 votes for pattern-matching on the left, so I'm disagreeing and committing on this one :)
| rcases h₂ with ⟨h₂, _⟩ | ||
| rcases h₂ with ⟨hl₂, hr₂⟩ ; subst hl₂ hr₂ | ||
| have ⟨⟨hl₂, hr₂⟩, _⟩ := h₂ | ||
| subst hl₂ hr₂ |
There was a problem hiding this comment.
here's an example of compound deconstruction with have. (Replacing rcases code that wasn't even doing the compound deconstruction 😂 )
This PR is pure refactoring, no functional change.
Replaces (almost) all of our use of
rcaseswith a trivial pattern (no destructuring, or just destructuring a conjunction) with an equivalenthave.Some side effects:
rcases/haveto shadow a previous binding, as inhave ⟨_, h₁⟩ := h₁. I believe the shadowed (but still present) binding is put in a different order byrcasesvshave, which may affect any subsequent renaming operations. I've made the necessary adjustments in this PR; they are minor. In many of these cases I just removed the shadowing for clarity.By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.