seq equality inductively

Stream: new members

[Marcus Rossel]

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]

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

[Eric Wieser]

Can you provide a #mwe?

[Marcus Rossel]

@[ext]
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' :=
begin
  ext1,
  apply seq.ext,
  intro n,
  induction n,
    { sorry },
    { sorry }
end

[Marcus Rossel]

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

[Adam Topaz]

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

import data.seq.seq

@[ext]
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' :=
begin
  ext1,
  apply seq.ext,
  intro n,
  induction n with n hn,
    { change e.nums.head = e'.nums.head,
      rw [e.head, e'.head] },
    { rw [e.next, e'.next, hn]  }
end

[Marcus Rossel]

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

[Adam Topaz]

We have docs#seq.coinduction

[Adam Topaz]

(seq is a "coinductive" type)

[Mario Carneiro]

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]

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]

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]

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

[Damiano Testa]

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]

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]

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]

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]

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