[Merged by Bors] - feat(algebra/category/*): get rid of the local reducible hack #3354

semorrison · 2020-07-10T07:08:21Z

I thought I did this back in April, but apparently never made the PR.

We currently use a strange hack when setting up concrete categories, making them locally reducible. There's a library note about this, which ends:

TODO: Probably @[derive] should be able to create instances of the	
required form (without `id`), and then we could use that instead of	
this obscure `local attribute [reducible]` method.

This PR makes the small change required to delta_instance to make this happen, and then stops using the hack in setting up concrete categories (and deletes the library note explaining this hack).

gebner · 2020-07-10T08:33:10Z

Looks good to me. This is definitely the way to go. Why is the PR closed?

semorrison · 2020-07-10T10:55:34Z

I ran into trouble in analysis/analytic/basic.lean, where the definition of the order on ennreal is unfolding weirdly and breaking a proof. I closed, hoping that I could fix it, but I'm struggling. Help appreciated!

semorrison · 2020-07-10T11:09:28Z

It used to be that the line by_cases h : p.radius ≤ nnnorm x, introduced the perfectly sensible hypothesis h : p.radius ≤ ↑(nnnorm x).

Now, however we get the sick h : ∀ (a : nnreal), a ∈ ↑(nnnorm x) → (λ (a : nnreal), ∃ (b : nnreal) (H : b ∈ p.radius), b ≤ a) a.

The problem is surely connected to where we use @[derive] handlers to build the order instances for ennreal. Somehow the change I've made to delta_instance messes this up, but so far I'm not understanding how or why.

semorrison · 2020-07-10T11:27:20Z

Okay, that's awesome, @gebner, thank you! I was beginning to suspect that it was by_cases at fault, rather than my change ...

gebner · 2020-07-10T11:31:12Z

Somehow the change I've made to delta_instance messes this up, but so far I'm not understanding how or why.

No, you made exactly the right change to the derive handler. Before:

@[instance]
protected noncomputable def ennreal.complete_linear_order : complete_linear_order ennreal :=
id with_top.complete_linear_order

After:

@[instance]
protected noncomputable def ennreal.complete_linear_order : complete_linear_order ennreal :=
with_top.complete_linear_order

Notice the missing id? We've wanted to change this for a long time now.

The built-in by_cases is buggy here, it shouldn't unfold the proposition at all.

gebner · 2020-07-10T11:31:59Z

src/tactic/fix_by_cases.lean

+dec_e ← mk_app ``decidable [e] <|> fail "by_cases tactic failed, type is not a proposition",
+inst ← mk_instance dec_e <|> pure `(classical.prop_decidable %%e),
+let inst := `(id %%inst : decidable %%e),
+cases inst [h, h],


Does anybody use by_cases in term-mode and expect the result to be a dite?

Apparently @b-mehta's fintype_hom instance did, so I've changed it (back) to produce a dite term.

Is this something I can fix? Was it one of the things in wide_pullbacks?

No, I've already changed by_cases so that it produces a dite. I don't have a strong opinion one way or another. The cases tactic (which produces decidable.rec) was just easier to use than to construct a dite term by hand.

And yes, it was wide_pullbacks.

The only thing missing on this PR now are the linting errors (inhabited instances & docstrings).

gebner · 2020-07-10T14:34:48Z

It is surprisingly hard to write a robust by_cases. For example you can't use refine if the goal contains metavariables. Why? Because to_expr sees the (existing) metavariables in the proof, and believes that they need to be turned into new goals...

bryangingechen · 2020-07-10T14:43:42Z

src/tactic/fix_by_cases.lean

+ - It only works if the proposition is decidable.
+ - It sometimes unfolds the proposition.
+
+We override the `by_cases` tactic with a correct implementation here.


Why not fix this in core?

I'll move it to core once it works in mathlib. But seeing the problems (and unforeseen issues) that I encountered while "improving" the tactic, it is absolutely necessary to test this on mathlib first.

b-mehta · 2020-07-10T18:21:00Z

Oh hah just the other day I saw this local reducible trick and thought it was clever and copied you! Now I know :)

gebner · 2020-07-11T07:59:20Z

bors r+

I thought I did this back in April, but apparently never made the PR. We currently use a strange hack when setting up concrete categories, making them locally reducible. There's a library note about this, which ends: ``` TODO: Probably @[derive] should be able to create instances of the required form (without `id`), and then we could use that instead of this obscure `local attribute [reducible]` method. ``` This PR makes the small change required to `delta_instance` to make this happen, and then stops using the hack in setting up concrete categories (and deletes the library note explaining this hack). Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org>

bors · 2020-07-11T10:10:58Z

Pull request successfully merged into master.

Build succeeded:

`by_cases` was changed to use classical reasoning (#3354, leanprover-community/lean#409), but the documentation hasn't been updated yet. I leave `by_contra` alone as it still uses `decidable`.

…over-community#3354) I thought I did this back in April, but apparently never made the PR. We currently use a strange hack when setting up concrete categories, making them locally reducible. There's a library note about this, which ends: ``` TODO: Probably @[derive] should be able to create instances of the required form (without `id`), and then we could use that instead of this obscure `local attribute [reducible]` method. ``` This PR makes the small change required to `delta_instance` to make this happen, and then stops using the hack in setting up concrete categories (and deletes the library note explaining this hack). Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Gabriel Ebner <gebner@gebner.org>

semorrison added 17 commits April 20, 2020 11:29

chore(tactic/simp_result): forgot to import in tactic.basic

ef85b35

Merge remote-tracking branch 'origin/master' into import_simp_result

5020ecf

fix(tactic/delta_instance): handle universe metavariables

8099abe

Merge branch 'import_simp_result' into local_reducible

34472b9

gah

55f2fca

gah

14dc696

fix

bab3ace

merge

980d0c3

fix

bffa0c3

missing instance on Meas

bbb43e9

.

970a872

merge

c3cc297

fix

d5a8a14

fixes

bcd871b

fixes

06cfd75

revert weird changes

3dfc0eb

make things more uniform

e9523a0

semorrison closed this Jul 10, 2020

semorrison reopened this Jul 10, 2020

gebner added enhancement help-wanted The author needs attention to resolve issues WIP Work in progress labels Jul 10, 2020

Fix analytic/basic

11e8bd4

semorrison changed the title ~~Local reducible~~ feat(algebra/category/*): get rid of the local reducible hack Jul 10, 2020

More principled fix.

d15cfaa

semorrison removed the WIP Work in progress label Jul 10, 2020

semorrison removed the help-wanted The author needs attention to resolve issues label Jul 10, 2020

gebner reviewed Jul 10, 2020

View reviewed changes

gebner added 5 commits July 10, 2020 13:53

Fix by_cases fallout.

3001d07

by_cases': produce dite-terms

5d5f41f

Fix linear_algebra/finsupp

b0ca9a7

Fix computability/halting

cd77205

Even more robust by_cases..

d597c23

bryangingechen reviewed Jul 10, 2020

View reviewed changes

linting

6733689

semorrison added the awaiting-review The author would like community review of the PR label Jul 11, 2020

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jul 11, 2020

bors bot changed the title ~~feat(algebra/category/*): get rid of the local reducible hack~~ [Merged by Bors] - feat(algebra/category/*): get rid of the local reducible hack Jul 11, 2020

bors bot closed this Jul 11, 2020

bors bot deleted the local_reducible branch July 11, 2020 10:11

lambda-fairy mentioned this pull request Aug 7, 2020

[Merged by Bors] - doc(tactic/lean_core_docs): by_cases is classical #3718

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(algebra/category/*): get rid of the local reducible hack #3354

[Merged by Bors] - feat(algebra/category/*): get rid of the local reducible hack #3354

semorrison commented Jul 10, 2020

gebner commented Jul 10, 2020

semorrison commented Jul 10, 2020 •

edited

semorrison commented Jul 10, 2020

semorrison commented Jul 10, 2020

gebner commented Jul 10, 2020

gebner Jul 10, 2020

gebner Jul 10, 2020

b-mehta Jul 10, 2020

gebner Jul 10, 2020

gebner commented Jul 10, 2020

bryangingechen Jul 10, 2020

gebner Jul 10, 2020

b-mehta commented Jul 10, 2020

gebner commented Jul 11, 2020

bors bot commented Jul 11, 2020

[Merged by Bors] - feat(algebra/category/*): get rid of the local reducible hack #3354

[Merged by Bors] - feat(algebra/category/*): get rid of the local reducible hack #3354

Conversation

semorrison commented Jul 10, 2020

gebner commented Jul 10, 2020

semorrison commented Jul 10, 2020 • edited

semorrison commented Jul 10, 2020

semorrison commented Jul 10, 2020

gebner commented Jul 10, 2020

gebner Jul 10, 2020

Choose a reason for hiding this comment

gebner Jul 10, 2020

Choose a reason for hiding this comment

b-mehta Jul 10, 2020

Choose a reason for hiding this comment

gebner Jul 10, 2020

Choose a reason for hiding this comment

gebner commented Jul 10, 2020

bryangingechen Jul 10, 2020

Choose a reason for hiding this comment

gebner Jul 10, 2020

Choose a reason for hiding this comment

b-mehta commented Jul 10, 2020

gebner commented Jul 11, 2020

bors bot commented Jul 11, 2020

semorrison commented Jul 10, 2020 •

edited