feat: `Bool` lemmas #183

fgdorais · 2023-07-10T20:33:23Z

Depends on feat: new alias command #200
Mathlib patch: https://github.com/leanprover-community/mathlib4/tree/fgdorais-bool

Std/Data/Bool.lean

fgdorais · 2023-07-27T06:59:51Z

Updated to use new alias command from #200

Std/Data/Bool.lean

eric-wieser · 2023-10-27T14:09:43Z

Std/Data/Bool.lean

+instance : LE Bool := leOfOrd
+instance : LT Bool := ltOfOrd
+instance : Max Bool := maxOfLe
+instance : Min Bool := minOfLe


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 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.

digama0 · 2023-10-29T10:39:50Z

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>

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.

fgdorais force-pushed the bool branch 7 times, most recently from 2f43344 to 2c3b74d Compare July 11, 2023 11:48

fgdorais force-pushed the bool branch from 2c3b74d to bded142 Compare July 19, 2023 01:21

fgdorais marked this pull request as ready for review July 22, 2023 00:53

fgdorais commented Jul 22, 2023

View reviewed changes

Std/Data/Bool.lean Outdated Show resolved Hide resolved

fgdorais force-pushed the bool branch from 74c3758 to ff589bc Compare July 25, 2023 08:42

digama0 reviewed Jul 25, 2023

View reviewed changes

Std/Data/Bool.lean Outdated Show resolved Hide resolved

urkud reviewed Jul 26, 2023

View reviewed changes

Std/Data/Bool.lean Outdated Show resolved Hide resolved

fgdorais force-pushed the bool branch from a84fb71 to 4c898d0 Compare July 27, 2023 06:57

fgdorais force-pushed the bool branch from 4c898d0 to b8eb153 Compare July 27, 2023 07:04

fgdorais force-pushed the bool branch from 958e768 to ab658de Compare August 7, 2023 21:31

fgdorais added the awaiting-author Waiting for PR author to address issues label Aug 21, 2023

leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Aug 22, 2023

fgdorais force-pushed the bool branch from ab658de to cc42f9d Compare August 22, 2023 18:15

leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Aug 22, 2023

fgdorais added awaiting-review This PR is ready for review; the author thinks it is ready to be merged. and removed awaiting-author Waiting for PR author to address issues labels Aug 22, 2023

semorrison reviewed Sep 4, 2023

View reviewed changes

Std/Data/Bool.lean Outdated Show resolved Hide resolved

semorrison approved these changes Sep 4, 2023

View reviewed changes

leanprover-community-mathlib4-bot added the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Sep 27, 2023

fgdorais mentioned this pull request Oct 22, 2023

feat: 3 simple lemmas for Bool #315

Closed

1 task

fgdorais added 3 commits October 22, 2023 20:35

feat: Bool lemmas

3f5848b

fix: margins with btt instead of bool_tt

68355aa

feat: add iff versions of and_or_inj_{left|right}

33ad27f

fgdorais added 5 commits October 22, 2023 20:39

feat: use new alias syntax

10d1079

fix: keep xor in root namespace

8332df8

feat: namespaced operator synonyms

413a0d4

fix: use btt

29e4f2c

fix: use decide

1a49494

fgdorais force-pushed the bool branch from efedb51 to 1a49494 Compare October 23, 2023 00:40

fgdorais added 2 commits October 22, 2023 20:47

fix: duplicate lemma

4cbdf15

fix: long line

02769dd

leanprover-community-mathlib4-bot removed the merge-conflict This PR has merge conflicts with the `main` branch which must be resolved by the author. label Oct 23, 2023

FR-vdash-bot mentioned this pull request Oct 23, 2023

chore: xor is just bne leanprover-community/mathlib4#7840

Closed

joehendrix reviewed Oct 26, 2023

View reviewed changes

Std/Data/Bool.lean Show resolved Hide resolved

joehendrix reviewed Oct 26, 2023

View reviewed changes

Std/Data/Bool.lean Show resolved Hide resolved

joehendrix added awaiting-author Waiting for PR author to address issues and removed awaiting-review This PR is ready for review; the author thinks it is ready to be merged. labels Oct 26, 2023

joehendrix suggested changes Oct 26, 2023

View reviewed changes

Std/Data/Bool.lean Show resolved Hide resolved

Std/Data/Bool.lean Outdated Show resolved Hide resolved

fix: naming convention and style

5c4f443

joehendrix approved these changes Oct 26, 2023

View reviewed changes

joehendrix merged commit 65544c3 into leanprover-community:main Oct 27, 2023
1 check passed

semorrison added a commit to leanprover-community/mathlib4 that referenced this pull request Oct 27, 2023

chore: update Mathlib for leanprover-community/batteries#183

1b00a6e

eric-wieser reviewed Oct 27, 2023

View reviewed changes

joehendrix removed the awaiting-author Waiting for PR author to address issues label Oct 27, 2023

digama0 mentioned this pull request Oct 29, 2023

[Merged by Bors] - chore: update Mathlib for leanprover/std4#183 leanprover-community/mathlib4#7982

Closed

bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Oct 29, 2023

chore: update Mathlib for leanprover-community/batteries#183 (#7982)

3a9b57c

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

grunweg pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 1, 2023

chore: update Mathlib for leanprover-community/batteries#183 (#7982)

90c0cab

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

fgdorais pushed a commit to leanprover-community/mathlib4 that referenced this pull request Nov 1, 2023

chore: update Mathlib for leanprover-community/batteries#183 (#7982)

9e9b0e8

Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser mentioned this pull request Nov 1, 2023

[Merged by Bors] - chore(Order/BooleanAlgebra): reduce risk of instance diamonds leanprover-community/mathlib4#8099

Closed

This was referenced Jan 4, 2024

chore: fix nightly testing to work with 2024-01-03 leanprover-community/mathlib4#9438

Merged

[Merged by Bors] - chore: CI: improve comment created on lean PRs leanprover-community/mathlib4#9585

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: `Bool` lemmas #183

feat: `Bool` lemmas #183

fgdorais commented Jul 10, 2023 •

edited

Loading

fgdorais commented Jul 27, 2023

eric-wieser Oct 27, 2023 •

edited

Loading

fgdorais Oct 27, 2023

digama0 commented Oct 29, 2023

feat: Bool lemmas #183

feat: Bool lemmas #183

Conversation

fgdorais commented Jul 10, 2023 • edited Loading

fgdorais commented Jul 27, 2023

eric-wieser Oct 27, 2023 • edited Loading

Choose a reason for hiding this comment

fgdorais Oct 27, 2023

Choose a reason for hiding this comment

digama0 commented Oct 29, 2023

feat: `Bool` lemmas #183

feat: `Bool` lemmas #183

fgdorais commented Jul 10, 2023 •

edited

Loading

eric-wieser Oct 27, 2023 •

edited

Loading