dependent finsupp

Stream: general

[Kenny Lau]

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

[Johannes Hölzl]

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

[Kenny Lau]

@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]

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]

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

[Kenny Lau]

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

[Johannes Hölzl]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

should I work on that?

[Johannes Hölzl]

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.

[Kenny Lau]

yes, ok, thanks

[Kenny Lau]

@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]

I would go for the latter.

[Johan Commelin]

Alternatively, provide both...

[Kevin Buzzard]

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

[Johan Commelin]

Constructive direct sums, I think

[Kevin Buzzard]

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

[Johannes Hölzl]

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]

@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]

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

[Kenny Lau]

Should I make a new typeclass for that? decidable_zero

[Mario Carneiro]

decidable_pred (eq 0) works

[Kenny Lau]

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

[Simon Hudon]

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]

well, option has decidable "none"

[Kenny Lau]

with_zero has decidable zero

[Simon Hudon]

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

I think so

[Kenny Lau]

oh I don't even need to prove it!

[Kenny Lau]

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

[Kenny Lau]

Lean is smart

[Kenny Lau]

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

[Kenny Lau]

I can't believe this, something must be wrong

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

yeah the second one is wrong

[Kenny Lau]

Lean interpreted 0 as natural

[Simon Hudon]

So how does Lean prove the instances for you?

[Kenny Lau]

I proved the second one now

[Kenny Lau]

the first one is just solve by elim

[Simon Hudon]

Why does that work?

[Simon Hudon]

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

[Kenny Lau]

@Johannes Hölzl commited to the PR

[Kenny Lau]

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

[Kevin Buzzard]

People being busy?

[Kevin Buzzard]

You'll understand, one day :-)

[Kenny Lau]

Are there any problems with my PR? @Mario Carneiro

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kenny Lau]

ok no problem