fix: avoid surprising symmetry inverse on refinement lemma #207
Conversation
| @@ -44,7 +44,7 @@ theorem none_right {x? : Option α} : | |||
| rintro ⟨⟩ | |||
|
|
|||
| theorem some_left {x : α} {y? : Option α} : | |||
| some x ⊑ y? ↔ y? = some x := by | |||
| some x ⊑ y? ↔ some x = y? := by | |||
There was a problem hiding this comment.
I am less sure about this change, we conventionally use variable = expr.
There was a problem hiding this comment.
I would wait for @alexkeizer or @goens to think about whether this is worse for simp.
There was a problem hiding this comment.
I find it surprising that this change flips the direction of the statement. This will require updates of our auto-generated proofs when applies as a simp lemma. We can leave it as it is and drop this PR. I just then know that when we activate this, we need to be careful.
There was a problem hiding this comment.
The flip might be surprising, but it can be desirable. Say we have some x \sqsubseteq y? as an assumption, then simplifying that to y? = some x gives us a good hypothesis to rewrite along (eliminating the y? variable), while some x = y? would be a bad rewrite, losing some information.
There was a problem hiding this comment.
OK, got it. Thank you. I will close this then.
No description provided.