Zulip Chat Archive

Stream: general

Topic: dependent finsupp


view this post on Zulip Kenny Lau (Sep 04 2018 at 08:17):

I want to make finsupp dependent, and then build the current finsupp as a special case. Is this a good idea?

view this post on Zulip Johannes Hölzl (Sep 04 2018 at 08:27):

I thought to suggest this as part of the direct sum PR :-)

view this post on Zulip Kenny Lau (Sep 04 2018 at 11:04):

@Johannes Hölzl I'm not sure what to do with this. finsupp is widely used. should I make a separate file?

view this post on Zulip Johannes Hölzl (Sep 04 2018 at 11:09):

Yes. Start with a separate file where you generalize from direct sum to dfinsupp, i.e. from [Π i, module R (β i)] to [Π i, has_zero (β i)].

view this post on Zulip Kenny Lau (Sep 04 2018 at 19:04):

problem. the simp lemmas now require higher order unification, rendering them useless

view this post on Zulip Kenny Lau (Sep 05 2018 at 13:37):

@Johannes Hölzl should I make finsupp dependent on dfinsupp?

view this post on Zulip Johannes Hölzl (Sep 05 2018 at 13:38):

Yes, I think so. But let's first add dfinsupp and then see.

view this post on Zulip Kenny Lau (Sep 05 2018 at 13:52):

@Johannes Hölzl there's one thing though. now for finsupp from A to B, we need decidable equality on B

view this post on Zulip Kenny Lau (Sep 05 2018 at 13:52):

I suspect that if we define finsupp differently, then we won't need decidbale equlaity on B

view this post on Zulip Kenny Lau (Sep 05 2018 at 13:53):

should I work on that?

view this post on Zulip Johannes Hölzl (Sep 05 2018 at 13:54):

I guess this is your quotient construction, the one you use in your direct sums construction? If you want to use it, that's fine for me.

view this post on Zulip Kenny Lau (Sep 05 2018 at 13:54):

yes, ok, thanks

view this post on Zulip Kenny Lau (Sep 06 2018 at 18:00):

@Johannes Hölzl I'm in a dilemma: I can either define dfinsupp.sum with the same arguments, but it would require decidable equality on the codomains; or I can define dfinsupp.sum without decidable equality on the codomains, but it would require me to provide an extra argument that the input function maps 0 to 0.

view this post on Zulip Johan Commelin (Sep 06 2018 at 18:06):

I would go for the latter.

view this post on Zulip Johan Commelin (Sep 06 2018 at 18:07):

Alternatively, provide both...

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 18:07):

What's your motivation for defining dfinsupp? Is there some application you have in mind?

view this post on Zulip Johan Commelin (Sep 06 2018 at 18:08):

Constructive direct sums, I think

view this post on Zulip Kevin Buzzard (Sep 06 2018 at 18:08):

oh that would make sense, Kenny was talking to me about direct sums recently.

view this post on Zulip Johannes Hölzl (Sep 06 2018 at 19:19):

Since the types are usually fixed and it's super annoying to always attach the f 0 = 0 proof: assume decidability of the codomain for sum.

view this post on Zulip Kenny Lau (Sep 07 2018 at 06:56):

@Johannes Hölzl sometimes we don't actually need decidable equality in general, we just need to determine if something is zero. What should I do in that case?

view this post on Zulip Simon Hudon (Sep 07 2018 at 06:58):

you can say that (x = 0) and (0 = x) are decidable.

view this post on Zulip Kenny Lau (Sep 07 2018 at 06:59):

Should I make a new typeclass for that? decidable_zero

view this post on Zulip Mario Carneiro (Sep 07 2018 at 06:59):

decidable_pred (eq 0) works

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:00):

if I prove that decidable_eq \to decidable_pred (eq 0), will Lean be able to use it?

view this post on Zulip Simon Hudon (Sep 07 2018 at 07:00):

If you look at decidable_eq, decidable_pred and decidable_rel, they are simply definitions on top of decidable. You only need to do the same for 0 if it's pervasive enough

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:01):

well, option has decidable "none"

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:01):

with_zero has decidable zero

view this post on Zulip Simon Hudon (Sep 07 2018 at 07:01):

if I prove that decidable_eq \to decidable_pred (eq 0), will Lean be able to use it?

I think so

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:03):

oh I don't even need to prove it!

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:03):

instance {γ : Type w} [has_zero γ] [decidable_eq γ] : decidable_pred (eq (0 : γ)) :=
by apply_instance

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:03):

Lean is smart

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:04):

instance {γ : Type w} [has_zero γ] [decidable_pred (eq (0 : γ))] : decidable_pred (λ x, x = 0) :=
by apply_instance

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:04):

I can't believe this, something must be wrong

view this post on Zulip Mario Carneiro (Sep 07 2018 at 07:04):

eq 0 is \lam x, eq 0 x which is \lam x, 0 = x

view this post on Zulip Mario Carneiro (Sep 07 2018 at 07:04):

the other one is (= 0) which is \lam x, x = 0

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:05):

yeah the second one is wrong

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:05):

Lean interpreted 0 as natural

view this post on Zulip Simon Hudon (Sep 07 2018 at 07:08):

So how does Lean prove the instances for you?

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:11):

I proved the second one now

view this post on Zulip Kenny Lau (Sep 07 2018 at 07:11):

the first one is just solve by elim

view this post on Zulip Simon Hudon (Sep 07 2018 at 07:12):

Why does that work?

view this post on Zulip Simon Hudon (Sep 07 2018 at 07:12):

Oh, ok, it's proving less than I thought

view this post on Zulip Kenny Lau (Sep 08 2018 at 23:04):

@Johannes Hölzl commited to the PR

view this post on Zulip Kenny Lau (Oct 06 2018 at 20:47):

What is preventing this 22-day-old pull request from being merged?

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:52):

People being busy?

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 20:52):

You'll understand, one day :-)

view this post on Zulip Kenny Lau (Oct 06 2018 at 21:14):

Are there any problems with my PR? @Mario Carneiro

view this post on Zulip Mario Carneiro (Oct 06 2018 at 23:27):

It conflicts with the module refactor, so don't expect this to be merged until after that

view this post on Zulip Kevin Buzzard (Oct 06 2018 at 23:35):

But after the module refactor Kenny will be too busy working on algebraic closure to be able to fix up this PR.

view this post on Zulip Kenny Lau (Oct 07 2018 at 07:57):

ok no problem


Last updated: May 12 2021 at 23:13 UTC