Suppressing instances & unfolding structures

Stream: general

[Sigma]

I've defined a ring structure ogf {M : Type} [ring M] : ring ( \N -> M ), but then when I try to multiply the elements it seems like its just taking the multiplication component-wise, rather than the ring multiplication I've defined. Is there some way to keep that other multiplication from arising?

As a different approach, when I try to explicitly use ring.mul a b instead of a*b I can't unfold the ring multiplication. Any of unfold ring.mul, ring, ogf don't work, and I can't rewrite the parts it should be defined in terms of. And it won't let me use ogf.mul or any variation of it. What should I do to break it up, or what should I use in place of ring.mul?

[Yakov Pechersky]

The multiplication you're getting is docs#pi.has_mul. The usual way to deal with this is to work with a type synonym of your nat -> M, and place the ring structure on that.

[Johan Commelin]

@Sigma Which ring structure is this ogf?

[Sigma]

I had wanted to avoid synonyms since I was worried it would take too much time translating trivial things over, but that makes sense.

ogf is just the ring multiplication for if you treated the sequence as its power series, its ordinary generating function, hence ogf. I had been wondering if you could just formulate generating functions as their ring structures on the sequences, rather than moving them over to some new object. Ordinary generating functions and Exponential generating functions are both just power series, where the mapping either does or doesnt normalize the coefficients. But a Dirichlet generating function for example, is a different beast than the other two, with a different multiplication. So I was trying to unify the notions of generating functions just as different ring structures on \N -> M rather than needing to define a whole new middleman class of objects for each one.

[Johan Commelin]

docs#power_series exists. So I think it makes sense to build a ogf constructor for it.

[Sigma]

powerseries has a ring coercion as well at docs#power_series.ring , which should work for ordinary and exponential generating series, but not for any of the rest. The next option I thought of was data.seq.seq, but that includes none which we would need to quotient out. I don't know how to use the setoid stuff so I certainly won't be the one to take that approach.

Using {\N -> M // true} seems like it pretty much works, but its a bit of a pain. You need to be careful, if you ever take a.val * b.val it becomes pi.mul

[Eric Wieser]

What's the definition of mul you're using, if it's not the power_series one?

[Johan Commelin]

Sigma said:

Using {\N -> M // true} seems like it pretty much works, but its a bit of a pain. You need to be careful, if you ever take a.val * b.val it becomes pi.mul

This looks overly complicated.

variables (M : Type*) [ring M]

def ogf := ℕ → M

instance : has_mul (ogf M) := sorry

would probably be easier to setup.

[Johan Commelin]

But before taking that route, I would also like to know why power_series can't be reused.

[Sigma]

defining def ogf := ℕ → M isn't enough to stop the pi.mul instance from taking over.

def ogf := ℕ → M

instance : has_mul (ogf M) := {
  mul := λ a b, λ n, finset.sum (finset.nat.antidiagonal n)
    (λ m : ℕ × ℕ, a m.fst * b m.snd) }

example : ((λ n,  1 : ogf M) * (λ n, 2)) 1 = 4 := begin
  simp,
  sorry,
end

the product simplifies to 2 = 4

I don't want to use power_series since it already has a ring instance just like pi.mul, and it only works for 1 (and a half) kinds of generating functions. So if we ever try to implement dirichlet generating functions or anything besides ordinary and exponential, then it wouldn't have the correct multiplication.
Further, power series aren't fundamental to the concept of generating functions, its just written in that way so we remember how to do the multiplication of the sequence coefficients. I want to emphasize that.

I'm trying to explore the question of "given a sequence with some recursive relationship, what concept of generating function. Rather, what ring multiplication on sequences, gives the most information about the sequence."
With ogf's we can get the relation F n = F n - 2 + F n - 1 into F = x + x^2 F + x F, so the fibonacci sequence becomes the terms of x/(1 - x - x^2)
With egf's this becomes a diff eq instead, which is marginally more difficult to solve, and it can't be simplified at all with a dirichlet generating function.

The shift F n - k becomes x^k F plus some correcting polynomial of order <k for an ogf. It becomes taking derivatives for an exponential generating function. A dirichlet series does not respect shifts, but it does respect multiplicative functions and give the mobius inversion formula. So they have different benefits in different situations.

[Kevin Buzzard]

Try (id (λ n, 1) : ogf M) * .... I think this will work

[Kevin Buzzard]

If I'm right then you've fallen into a gotcha -- your code checks that the type of the function is defeq to ogf M but doesn't actually change the type to ogf M. If the id trick doesn't work then ignore what I'm saying. Maybe it's best that you make an explicit constructor instead of all this defeq reliance

[Sigma]

the id trick seems to work

[Sigma]

i think by explicit constructor you meant, structure ogf (M : Type*) := mk :: (f : ℕ → M), which i got into a ring just by copy and pasting the old definition and making a new extensionality lemma. and it seems to work perfectly fine

example : ((ogf.mk (λ n, (2 : ℤ))) * ogf.mk (λ n, (3 : ℤ))).f 2 = 18 := begin
  simp,
  ring,
end

checks

[Eric Wieser]

Does docs#hahn_series have the structure you desire?

[Eric Wieser]

It seems to have the right multiplication