Zulip Chat Archive

Stream: new members

Topic: seq equality inductively

Marcus Rossel (Jun 02 2021 at 10:56):

Is there a way to prove that two seqs are equal by using an inductive approach?
I have two sequences s and s' of which I know that s.head = s'.head, and I know that each element is determined by its predecessor alone.
I don't know how to show s = s' from this though.

Marcus Rossel (Jun 02 2021 at 10:59):

I think using seq.ext and then performing induction on the index might work.

Eric Wieser (Jun 02 2021 at 12:44):

Can you provide a #mwe?

Marcus Rossel (Jun 02 2021 at 16:14):

structure evens :=
  (nums : seq )
  (head : nums.head = some 0)
  (next :  i, nums.nth (i + 1) = (nums.nth i).map (nat.add 2))

example (e e' : evens) : e = e' :=
  apply seq.ext,
  intro n,
  induction n,
    { sorry },
    { sorry }

Marcus Rossel (Jun 02 2021 at 16:14):

The proof at the bottom is to demonstrate my current approach.

Adam Topaz (Jun 02 2021 at 16:41):

This approach works, but you need to use what you know about e and e'.

Marcus Rossel (Jun 02 2021 at 16:46):

I guess what I'm wondering is whether there exists a nice lemma that wraps up this induction approach?

Adam Topaz (Jun 02 2021 at 16:51):

We have docs#seq.coinduction

Adam Topaz (Jun 02 2021 at 16:52):

(seq is a "coinductive" type)

Mario Carneiro (Jun 02 2021 at 17:16):

it might not be obvious but eq_of_bisim is the general coinduction principle (seq.coinduction only applies when you have an appropriate function fr)

Mario Carneiro (Jun 02 2021 at 17:18):

well, actually for this theorem you probably want to use induction on the index since you have defined things in terms of nth instead of using the destructors head and tail

Marcus Rossel (Jun 03 2021 at 06:35):

Adam Topaz said:

(seq is a "coinductive" type)

What does that mean (for non-mathematicians)/how does it manifest in Lean?
I looked it up, but didn't understand the difference to inductive types.

Kevin Buzzard (Jun 03 2021 at 06:46):

Trust me, mathematicians don't know anything about conductive types

Damiano Testa (Jun 03 2021 at 06:47):

I was secretly hoping that the expected explanation from Adam would have been for mathematicians, to get an idea of what they are... :upside_down:

Mario Carneiro (Jun 03 2021 at 07:39):

Kevin Buzzard said:

Trust me, mathematicians don't know anything about conductive types

I can't tell if the misspelling here is a joke...

Adam Topaz (Jun 03 2021 at 15:13):

My flawed intuition is that inductive types are like colimits while coinductive types are like limits (in the categorical sense). There is a formal definition in terms of a terminal object which you can find on the nlab, which is probably even less helpful.

In less categorical terms, the defining property of an inductive type is the rule that tells you how to map out of it, while the defining property of a coinductive type tells you how to map into it… I don’t know if that’s helpful at all 😕

Adam Topaz (Jun 03 2021 at 15:19):

And of course this is the point of view of a mathematician who doesn’t care about computations. A computer scientist will give you some other description in terms of infinite data and lazy evaluation or something 😉

Horatiu Cheval (Jun 03 2021 at 18:24):

My naive mental picture always was that inductive means "the smallest type closed under these rules of construction", while coinductive means "the largest one". I don't know if that's entirely right

Last updated: Dec 20 2023 at 11:08 UTC