[Merged by Bors] - refactor(order/conditionally_complete_lattice): use order_bot#14568
[Merged by Bors] - refactor(order/conditionally_complete_lattice): use order_bot#14568
order_bot#14568Conversation
Use `order_bot` instead of an explicit `c = ⊥` argument in `well_founded.conditionally_complete_linear_order_with_bot`. Also reuse `linear_order.to_lattice`.
| {γ : Type*} [partial_order γ] | ||
|
|
||
| theorem min_le {x : β} {s : set β} (hx : x ∈ s) (hne : s.nonempty := ⟨x, hx⟩) : | ||
| h.min s hne ≤ x := |
There was a problem hiding this comment.
hne doesn't need to be an argument, due to proof irrelevancy you can just put ⟨x, hx⟩ in the theorem statement and it will work just fine.
There was a problem hiding this comment.
That's why hne is an argument with a default value. AFAIR, it may help if we have h.min s hne with some other proof (though two proofs should be equal by definition, so I'm not sure).
There was a problem hiding this comment.
Yeah, that's why I suggest just inlining the proof. There's no circumstance in which you need to provide both hx and hne.
There was a problem hiding this comment.
I think we've sometimes seen some weirdness where this behaves incorrectly due to simp or rw performing a syntactic match rather than unifying. This is definitely a pattern we've used elsewhere, but I don't think it ever got a library note to explain exactly why it matters.
There was a problem hiding this comment.
I've inlined a bunch of proofs into a bunch of statements, and I've never had any of those problems. I'm interested in seeing an example where Lean attempts to do syntactic matching on a proof.
There was a problem hiding this comment.
I've just met the following scenario. While proving disjoint (s : set α) (t : set α), I did rintro x ⟨hs, ht⟩ and got the goal x ∈ ⊥. Then I tried to write exact (hd : disjoint s' t') ⟨_, _⟩ and got x ∈ s' as the first goal. I can't quickly create an example for this lemma.
There was a problem hiding this comment.
Well, if there's the possibility for breakage, then this auxiliary parameter can't possibly do harm. I might rewrite some of those other lemmas I was mentioning to use this pattern to. A library note would be much appreciated!
There was a problem hiding this comment.
I'd be inclined to declare this out of scope, but maybe create a new issue about documenting this approach or cleaning it up
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
|
bors merge We could certainly still do with the library note in #14568 (comment), but that doesn't need to be in this PR. |
|
Pull request successfully merged into master. Build succeeded: |
order_botorder_bot
Use
order_botinstead of an explicitc = ⊥argument inwell_founded.conditionally_complete_linear_order_with_bot. Alsoreuse
linear_order.to_latticeand addwell_founded.min_le.