Zulip Chat Archive

Stream: PR reviews

Topic: 4574 better `nontriviality`


view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:02):

@Scott Morrison In #4574 I'm trying to make nontriviality tactic extensible. E.g., I want nontriviality α to work if the goal is is_open s, s : set α, and for some other goals.

view this post on Zulip Scott Morrison (Oct 11 2020 at 22:04):

I really like it!

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:07):

I guess my meta code is suboptimal, feel free to improve it.

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:08):

Here are a few things I don't know how to do:

  • make it accept a list of additional simp lemmas;
  • given nontriviality R, make it mark semimodule.subsingleton R as an instance.

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:14):

One more idea: if we have [inhabited α], then add unique α instead of subsingleton α to the context.

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:22):

And I can't make https://github.com/leanprover-community/mathlib/blob/extend-nontriviality/src/analysis/calculus/times_cont_diff.lean#L2375 work with nontriviality.

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:22):

Or let me try...

view this post on Zulip Heather Macbeth (Oct 11 2020 at 22:25):

What about https://github.com/leanprover-community/mathlib/blob/73f119e04c35a4ab10eae68345472d78e5c4f6c7/src/analysis/normed_space/operator_norm.lean#L835 ?

view this post on Zulip Heather Macbeth (Oct 11 2020 at 22:27):

Maybe there's nothing that needs to be done there

view this post on Zulip Heather Macbeth (Oct 11 2020 at 22:28):

But that lemma could be deleted after your tactic comes in, is that the idea?

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:29):

AFAIR, subsingleton E ∨ _ is used as a technical assumption in the proof of the inverse function theorem.

view this post on Zulip Heather Macbeth (Oct 11 2020 at 22:29):

And the lemma's uses, in places like https://github.com/leanprover-community/mathlib/blob/952a407c2ea89c154d718aa1f92fd988f2b5d338/src/analysis/calculus/inverse.lean#L379 , replaced by uses of the tactic?

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:30):

E.g., in https://github.com/leanprover-community/mathlib/blob/952a407c2ea89c154d718aa1f92fd988f2b5d338/src/analysis/calculus/inverse.lean#L158

view this post on Zulip Heather Macbeth (Oct 11 2020 at 22:30):

Snap ... but yes, I meant that in the the inverse function where this lemma is currently used, could you use an improved nontriviality instead?

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:32):

I did not plan to refactor analysis/calculus/inverse.

view this post on Zulip Yury G. Kudryashov (Oct 11 2020 at 22:34):

And I don't see how can we get rid of this this assumption in the first part of the file.


Last updated: May 09 2021 at 12:14 UTC