std4#183, lemmas about Bool

Stream: mathlib4

[Scott Morrison]

@François G. Dorais, your PR std4#183 has just landed, but unfortunately your mathlib branch with the required patches for it is way out of date. (This is not your fault: the Std queue has been slow.)

Unfortunately this means that I can't bump Mathlib to match Std at 65544c31. Would you be able to do this bump? If so, when? I would very much like to have Mathlib in sync with Std again by the end of the weekend so I can do the next Lean release, either by doing the bump or undoing commits to Std. :-(

(pinging @Joe Hendrix so he can see what's happening)

[Scott Morrison]

Okay, I think I've got this sorted out at #7982.

[Scott Morrison]

@Eric Wieser has some comments here. I'm (hopefully) mostly away from the github over the weekend, which has already started here. If anyone wants to get it over the line that would be great, otherwise I can do it on Monday.

[Eric Wieser]

I can address my own comments

[Eric Wieser]

... not without pushing to master apparently

[Eric Wieser]

#7984 adds two lemmas that will answer the question in your PR

[François G. Dorais]

I have time on Saturday. I was planning to update that PR soon anyway but I didn't expect std4#183 to land this soon. There's a couple of small things that were missing in std4#183 as Eric pointed out. I'll try to do a quick supplemental std4 PR tonight (ping @Joe Hendrix) Since #7984 is already in master, I think we can get this all sorted out this weekend!

[Joe Hendrix]

@François G. Dorais I hope I didn't create more work by merging prematurely. I'm trying to move through merge requests faster, but maybe we should have a more clear process. I can review/approve the patch this weekend if it is there.

[François G. Dorais]

No worries @Joe Hendrix, it's not your fault either. I'm really glad this one got merged! That PR was pretty old and it left my working memory and went into storage, now I just need to bring everything back and fix the things that I forgot along the way...

[François G. Dorais]

The quick update is ready at std4#329, your input is requested @Eric Wieser. Thanks in advance!

I had a long day, so I will work on the Mathlib patch tomorrow. See you then!

[François G. Dorais]

Mathlib patch #8005 now exists. There's a bit of an awkward situation though: it depends on std4#329 which is not yet merged and std4#321 (print prefix) got merged after std4#183 but I don't have a patch for std4#321. So I had to test it on a custom std4 branch that includes std4#329 but removes std4#321 found here https://github.com/fgdorais/std4/tree/bool-test

[Scott Morrison]

@François G. Dorais, I've now made #8008, which brings Mathlib up to using current Std (i.e. including std4#321).

Do you think you could adapt your #8005 to "follow" #8008? We'll try to get them all in the right order, and asap. :-)

[François G. Dorais]

@Scott Morrison Done.