Coinduction API

Stream: mathlib4

[Vasilii Nesterov]

Hi there!

I am developing the Stream'.Seq API (as a by-product of my tactic #18486 for computing the asymptotics of real functions). Let me define some predicates on sequences:

import Mathlib.Data.Seq.Seq
namespace Stream'.Seq

def All {α : Type u} (s : Seq α) (p : α → Prop) : Prop := ∀ x ∈ s, p x

def Pairwise {α : Type u} (r : α → α → Prop) (li : Seq α) : Prop :=
  ∀ i j x y, i < j → li.get? i = .some x → li.get? j = .some y → r x y

def AtLeastAsLongAs {α : Type u} {β : Type v} (a : Seq α) (b : Seq β) : Prop :=
  ∀ n, a.TerminatedAt n → b.TerminatedAt n

For all these predicates we can prove "coinduction principles", for example:

theorem All.coind {α : Type u} {s : Seq α} {p : α → Prop}
    (motive : Seq α → Prop) (h_base : motive s)
    (h_cons : ∀ hd tl, motive (cons hd tl) → p hd ∧ motive tl)
    : s.All p := sorry

theorem Pairwise.coind {α : Type u} {r : α → α → Prop} [IsTrans _ r] {s : Seq α}
    (motive : Seq α → Prop) (h_base : motive s)
    (h_step : ∀ hd tl, motive (.cons hd tl) → tl.head.elim True (r hd ·) ∧ motive tl)
    : Pairwise r s := sorry

theorem AtLeastAsLong.coind {α : Type u} {β : Type v} {a : Seq α} {b : Seq β}
    (motive : Seq α → Seq β → Prop) (h_base : motive a b)
    (h_step : ∀ a b, motive a b →
      (∀ b_hd b_tl, (b = cons b_hd b_tl) → ∃ a_hd a_tl, a = cons a_hd a_tl ∧ motive a_tl b_tl))
    : a.AtLeastAsLongAs b := sorry

-- we can also state bisimulation principle in this form:
theorem Eq.coind {α : Type u} {a b : Seq α}
    (motive : Seq α → Seq α → Prop)
    (h_base : motive a b)
    (h_step : ∀ a b, motive a b →
      (∀ hd a_tl, (a = cons hd a_tl) → (∃ b_tl, b = cons hd b_tl ∧ motive a_tl b_tl))
    ) : a = b := sorry

I've never studied corecursion in depth, so I wanted to ask: are these forms of coinduction principles considered conventional? If not, how should they be stated?

[Mario Carneiro]

they look good to me

[Mario Carneiro]

Eq.coind looks false though in the case a = [] and b = [0] and motive is always true

[Mario Carneiro]

the coinduction principle you have there looks like a proof of a.IsPrefixOf b

[Vasilii Nesterov]

Mario Carneiro писал/а:

Eq.coind looks false though in the case a = [] and b = [0] and motive is always true

You're right, I actually proved this:

theorem Eq.coind {α : Type u} {a b : Seq α}
    (motive : Seq α → Seq α → Prop)
    (h_base : motive a b)
    (h_step : ∀ a b, motive a b →
      (∃ hd a_tl b_tl, a = cons hd a_tl ∧ b = cons hd b_tl ∧ motive a_tl b_tl) ∨
      (a = nil ∧ b = nil)) : a = b := sorry

and was going to refactor it as above, but now I see they aren't equivalent.

[Violeta Hernández]

Small note, but I don't think All isn't a very good predicate to have, since it's just a trivial wrapper around Forall.

[Violeta Hernández]

Likewise, AtLeastAsLong could be rewritten as a.length ≤ b.length, which gives you stuff like reflexivity and transitivity for free.

[Violeta Hernández]

Pairwise seems good to me.

[François G. Dorais]

Violeta Hernández said:

Likewise, AtLeastAsLong could be rewritten as a.length ≤ b.length, which gives you stuff like reflexivity and transitivity for free.

Not quite since Seq.length.{u} {α : Type u} (s : Seq α) (h : s.Terminates) : ℕ.

[Vasilii Nesterov]

I think Seq.length should actually be ℕ∞ instead of ℕ. This would allow us to define AtLeastAsLong as Violeta suggests.

[François G. Dorais]

Mathlib's ℕ∞ wouldn't work well since Seq.length would not be computable. You would need the better implementation of ℕ∞ as monotone functions Nat -> Bool.

[Vasilii Nesterov]

Violeta Hernández said:

Small note, but I don't think All isn't a very good predicate to have, since it's just a trivial wrapper around Forall.

Maybe. My instinct when working with Seq is always to treat it as a coinductive type and to hide its representation as ℕ → Option α as an implementation detail.

By the way, we do have analogous docs#List.Forall, but it is hardly used anywhere.

[Miyahara Kō]

Vasily Nesterov said:

I think Seq.length should actually be ℕ∞ instead of ℕ. This would allow us to define AtLeastAsLong as Violeta suggests.

PartENat looks more appropriate.

[Violeta Hernández]

Do note that List.Forall is not just a wrapper around ∀ x ∈ l, p x, as it unfolds to an (equivalent) conjunction

[Violeta Hernández]

Such a thing isn't possible with Seq

[François G. Dorais]

Miyahara Kō said:

Vasily Nesterov said:

I think Seq.length should actually be ℕ∞ instead of ℕ. This would allow us to define AtLeastAsLong as Violeta suggests.

PartENat looks more appropriate.

Almost, Part adds more fuzziness than necessary. I have a personal implementation that works pretty well. I'm thinking one day to put it in Batteries since it's the better way to implement Nat.find and other useful stuff.