## Stream: general

### Topic: dependent finsupp

#### 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?

#### Johannes Hölzl (Sep 04 2018 at 08:27):

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

#### 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?

#### 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)].

#### Kenny Lau (Sep 04 2018 at 19:04):

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

#### Kenny Lau (Sep 05 2018 at 13:37):

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

#### Johannes Hölzl (Sep 05 2018 at 13:38):

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

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

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

#### Kenny Lau (Sep 05 2018 at 13:53):

should I work on that?

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

yes, ok, thanks

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

#### Johan Commelin (Sep 06 2018 at 18:06):

I would go for the latter.

#### Johan Commelin (Sep 06 2018 at 18:07):

Alternatively, provide both...

#### Kevin Buzzard (Sep 06 2018 at 18:07):

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

#### Johan Commelin (Sep 06 2018 at 18:08):

Constructive direct sums, I think

#### Kevin Buzzard (Sep 06 2018 at 18:08):

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

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

#### 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?

#### Simon Hudon (Sep 07 2018 at 06:58):

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

#### Kenny Lau (Sep 07 2018 at 06:59):

Should I make a new typeclass for that? decidable_zero

#### Mario Carneiro (Sep 07 2018 at 06:59):

decidable_pred (eq 0) works

#### 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?

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

#### Kenny Lau (Sep 07 2018 at 07:01):

well, option has decidable "none"

#### Kenny Lau (Sep 07 2018 at 07:01):

with_zero has decidable zero

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

#### Kenny Lau (Sep 07 2018 at 07:03):

oh I don't even need to prove it!

#### Kenny Lau (Sep 07 2018 at 07:03):

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


Lean is smart

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


#### Kenny Lau (Sep 07 2018 at 07:04):

I can't believe this, something must be wrong

#### Mario Carneiro (Sep 07 2018 at 07:04):

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

#### Mario Carneiro (Sep 07 2018 at 07:04):

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

#### Kenny Lau (Sep 07 2018 at 07:05):

yeah the second one is wrong

#### Kenny Lau (Sep 07 2018 at 07:05):

Lean interpreted 0 as natural

#### Simon Hudon (Sep 07 2018 at 07:08):

So how does Lean prove the instances for you?

#### Kenny Lau (Sep 07 2018 at 07:11):

I proved the second one now

#### Kenny Lau (Sep 07 2018 at 07:11):

the first one is just solve by elim

#### Simon Hudon (Sep 07 2018 at 07:12):

Why does that work?

#### Simon Hudon (Sep 07 2018 at 07:12):

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

#### Kenny Lau (Sep 08 2018 at 23:04):

@Johannes Hölzl commited to the PR

#### Kenny Lau (Oct 06 2018 at 20:47):

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

#### Kevin Buzzard (Oct 06 2018 at 20:52):

People being busy?

#### Kevin Buzzard (Oct 06 2018 at 20:52):

You'll understand, one day :-)

#### Kenny Lau (Oct 06 2018 at 21:14):

Are there any problems with my PR? @Mario Carneiro

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

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

#### Kenny Lau (Oct 07 2018 at 07:57):

ok no problem

Last updated: Dec 20 2023 at 11:08 UTC