-
Notifications
You must be signed in to change notification settings - Fork 89
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
feat: Bool
lemmas
#183
feat: Bool
lemmas
#183
Conversation
fgdorais
commented
Jul 10, 2023
•
edited
Loading
edited
- Depends on feat: new alias command #200
- Mathlib patch: https://github.com/leanprover-community/mathlib4/tree/fgdorais-bool
2f43344
to
2c3b74d
Compare
Updated to use new alias command from #200 |
instance : LE Bool := leOfOrd | ||
instance : LT Bool := ltOfOrd | ||
instance : Max Bool := maxOfLe | ||
instance : Min Bool := minOfLe |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
These change the defeq of the boolean order (used in mathlib) to be (IMO) worse. Previously, Mathlib had
instance linearOrder : LinearOrder Bool where
le := fun a b ↦ a = false ∨ b = true
max := or
min := and
Was this a deliberate change?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
There was a hope long ago that core would fixup Ord
before this PR landed. Without that fixup, this is indeed a bad choice. My preferred versions are:
le x y := !x || y
lt x y := !x && y
max x y := x || y
min x y := x && y
These lead to the most efficient code in each case. I'm not sure if you really prefer your version for le
? I will submit a small follow-up PR fixing this as soon as I have a chance.
I think this PR still needs changes, but I didn't have time to review it and things are a bit more complicated now. I told Scott to work around this for now for the mathlib bump, and I will try to make a follow up PR when I have the time. |
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
We need `sup` and `max` to be defeq, and `max` is defined in Std. To achieve this, we define one in terms of the other. Until #8105 was merged (which fixed up leanprover-community/batteries#183), they were not defeq: ```lean example : (GeneralizedCoheytingAlgebra.toLattice : Lattice Bool).sup = DistribLattice.toLattice.sup := rfl -- failed ``` This instance in this PR should have been written such that it couldn't silently cause a diamond in the first place, by reusing existing data rather than creating new data.