Coïnduction

Stream: general

[Martin Dvořák]

Has anybody developed an (unofficial) extension for Lean that would allow coïnduction?
I'd need both coïnductive types and a tactic for proofs by coïnduction.

[Henrik Böving]

https://github.com/alexkeizer/QpfTypes

[Henrik Böving]

By @Alex Keizer

[Alex Keizer]

Can you elaborate a bit more about what you need? There is no proof by coinduction tactic yet, but with a concrete use-case in mind I could look to see what is the simplest tactic I could add that would work for your case (and can be generalized to more powerful cases later)

[Alex Keizer]

Also, thanks Henrik for pointing people towards my library! It seems you are better at promoting my work than me :sweat_smile:

[Henrik Böving]

I'm just faster :P

[Martin Dvořák]

Let S be the largest X ⊆ 𝒫({0,1}^ω) such that X ⊆ 01X ∪ 10X.
Prove ∀ x : {0,1}^ω, x is in S ↔ every finite prefix of x of even length has #0 = #1.

[Martin Dvořák]

Our teacher said we need to prove ← by coïnduction on S and prove → by induction on ℕ (length of the prefix).

[Shreyas Srinivas]

Isn't stuff like this proved by transfinite induction if I remember my infinite word automaton correctly?

[Alex Keizer]

Can you elaborate on how you are planning to formalize this, and what exactly you expect the coinduction tactic to do?

[Alex Keizer]

It seems like you also want to have coinductive predicates (at least, that is how I assume you'd want to formalize S), which is definitely beyond what we can currently do with QpfTypes

[Martin Dvořák]

I created an experimental version of the exercise in Lean without the coïnductive extension:
https://github.com/madvorak/fecssk/blob/3bc2218de71a6d341eacdb1758dc66306fec2ee5/Fecssk/Class03.lean#L152
It is untested and, quite frankly, I suspect it might not be solvable as it is.

[Martin Dvořák]

Thanks @Alex Keizer for help!

[Mario Carneiro]

Note that Stream' already has a fairly comprehensive coinduction API, so a coinduction package wouldn't be able to do much better than reproduce what is already there

[Mario Carneiro]

the motivation for a tactic is so that you can define your own coinductive types without going through all the work done for the Stream' type

[Mario Carneiro]

Here's a proof:

-- Prove `∀ x : {0,1}^ω` , `x ∈ S` ↔ every finite prefix of `x` of even length has #`0` = #`1`.

example : ∀ x : Word, x ∈ S ↔ ∀ n : ℕ, (x.take (2*n)).count 0 = (x.take (2*n)).count 1 := by
  intro x
  constructor
  · intro h n
    rcases h with ⟨S, hS, ss⟩
    simp [Set.subset_def] at ss
    induction n generalizing x with
    | zero => simp
    | succ n ih =>
      simp [Nat.mul_succ, Stream'.take]
      rcases ss _ hS with ⟨x, h, rfl⟩ | ⟨x, h, rfl⟩ <;> simp [ih _ h]
  · intro h
    refine ⟨{x | ∀ n : ℕ, (x.take (2*n)).count 0 = (x.take (2*n)).count 1}, h, ?_⟩
    simp [Set.subset_def]
    intro x h
    obtain ⟨a, b, c, rfl⟩ : ∃ a b c, x = Stream'.cons a (Stream'.cons b c) :=
      ⟨x.head, x.tail.head, x.tail.tail, by simp only [Stream'.eta]⟩
    match a, b with
    | 0, 1 => refine .inl ⟨_, fun n => by simpa [Nat.mul_succ] using h (n+1), rfl⟩
    | 1, 0 => refine .inr ⟨_, fun n => by simpa [Nat.mul_succ] using h (n+1), rfl⟩
    | 0, 0 | 1, 1 => simpa using h 1

[Martin Dvořák]

Thanks a lot!!!
What imports did you add to make it work?

[Mario Carneiro]

just

import Mathlib.Data.Stream.Init
import Mathlib.Data.Set.Lattice

[Mario Carneiro]

BTW the step that a coinduction tactic would replace is the refine ⟨{x | ∀ n : ℕ, (x.take (2*n)).count 0 = (x.take (2*n)).count 1}, h, ?_⟩ line

[Martin Dvořák]

FYI, I sent the following message to my colleagues. I hope the attribution is all right.

Thanks to amazing help from Alex Keizer and Mario Carneiro, who both promptly replied to my questions, I am now confident that the 4th homework is solvable in Lean, as it is here:

https://github.com/madvorak/fecssk/blob/main/Fecssk/Class03.lean