[WIP] added basic machinery for defining coinductive types

[cipher1024]

No description provided.

[cipher1024]

I took the example from
https://github.com/leanprover/lean/wiki/Coinductive-Types

It defines a possibly infinite tree as:

-- coinductive l_two_tree (A : Type) : Type :=
-- | nil {}      : l_two_tree A
-- | cons        : A → l_two_tree A → l_two_tree A
-- | cons₂       : A → l_two_tree → l_two_tree A → l_two_tree A

It can be constructed using cofix and two additional types: a node type (which contains the A information but nothing on the children trees) and a view type which offer more straightforward constructors than the sigma types specified by the cofix interface. With that machinery I managed to make the following code do what we would expect it to do:

def mk_tree : ℕ → l_two_tree ℕ :=
l_two_tree.corec $ λ z n mk_tree,
if n % 10 = 0 then
  l_two_tree'.cons n (mk_tree $ n+1)
else if n % 10 = 7 then
  l_two_tree'.nil
else
  l_two_tree'.cons₂ n (mk_tree $ n+1) (mk_tree $ n+2)

The parameter z is a bit of visual noise but otherwise, it looks just like a recursive program that we could write in Haskell.

[gebner]

This import is not needed, right?

[gebner]

AFAIK, the abbreviation command is not intended for general usage. Its only purpose is to define id_rhs. The difference compared to def is that it sets a special reducibility hint for the kernel type-checker.

[cipher1024]

Thanks for the note! I thought I read a comment from Leo about abbreviation removing the need to ever use reducible but I can't find it anymore. In any case, this definition works even without reducible so I'll just make it plain.

[gebner]

I won't complain about coding style. https://github.com/leanprover/mathlib/blob/master/docs/style.md

[cipher1024]

I think the naming is good but the spacing probably needs work. The proofs I think need a lot of work. A lot are far too long. I'll be addressing both as I whip the package into shape

[gebner]

def mk_tree : ℕ → l_two_tree ℕ :=
l_two_tree.corec $ λ z n mk_tree,

This seems to work pretty nicely in practice. Is it possible to change the internal l_two_tree' type so that it can store more than one "layer" of the tree? That is, so that you can produce more than one node by writing l_two_tree'.cons n (l_two_tree'.cons n (mk_tree $ n+1)) in mk_tree.

[cipher1024]

I have a few ideas on how to do that. I think ultimately, the best will be to have a different keyword than def (e.g. cofix) so that we don't have to set up our types to make it look like a recursive function. It would also allow us to support more fancy situations like mutually co-recursive definitions.

I can address your example with an ad hoc contraption as follows:

def l_two_tree.corec' {A} {X : Sort*}
  (f : Π z, X → (X → z) → l_two_tree' A (l_two_tree' A z))
  (s₀ : X)
: l_two_tree A :=
of_intl $
  cofix.corec
  (λ s : X ⊕ l_two_tree' A X,
        match s with
         | (sum.inl s') :=
           match f X s' id with
            | l_two_tree'.nil := ⟨ l_two_tree_node.nil, empty.elim ⟩
            | (l_two_tree'.cons x t) := ⟨ l_two_tree_node.cons x, λ _, sum.inr t ⟩
            | (l_two_tree'.cons₂ x t₀ t₁) := ⟨ l_two_tree_node.cons₂ x, λ b : bool, sum.inr (if b then t₀ else t₁) ⟩
           end
         | (sum.inr s) :=
           match s with
            | l_two_tree'.nil := ⟨ l_two_tree_node.nil, empty.elim ⟩
            | (l_two_tree'.cons x t) := ⟨ l_two_tree_node.cons x, λ _, sum.inl t ⟩
            | (l_two_tree'.cons₂ x t₀ t₁) := ⟨ l_two_tree_node.cons₂ x, λ b : bool, sum.inl (if b then t₀ else t₁) ⟩
           end
        end )
  (sum.inl s₀ : X ⊕ l_two_tree' A X)

def mk_tree' : ℕ → l_two_tree ℕ :=
l_two_tree.corec' $ λ z n mk_tree,
l_two_tree'.cons₂ n (l_two_tree'.cons (n+1) (mk_tree $ n+1)) (l_two_tree'.cons (n+2) (mk_tree $ n+2))

Notice that l_two_tree.corec' accepts exactly two nested constructors, no more, no less. I think I could make l_two_tree' recursive so as to make l_two_tree.corec more general.

[cipher1024]

I should add: thanks for asking this question, I could really use that kind of device in my pipes library and I was about to dive head first in an implementation of unbounded recursion to handle my problem. What you asked about is much better.

[cipher1024]

By changing l_two_tree' from:

inductive l_two_tree' (A X : Type) : Type
| nil {}      : l_two_tree'
| cons        : A → X → l_two_tree'
| cons₂       : A → X → X → l_two_tree'

to

mutual inductive l_two_tree', l_leaf' (A X : Type)
with l_two_tree' : Type
| nil {}      : l_two_tree'
| cons        : A → l_leaf' → l_two_tree'
| cons₂       : A → l_leaf' → l_leaf' → l_two_tree'
with l_leaf' : Type
| hole {} : X → l_leaf'
| more : l_two_tree' → l_leaf'

I managed to write a corecursor that accommodates arbitrary (non-null) number of nested constructors:

def mk_tree : ℕ → l_two_tree ℕ :=
l_two_tree.corec $ λ z n mk_tree,
l_two_tree'.cons₂ n (mk_tree $ n+1) (mk_tree $ n+2)

def mk_tree' : ℕ → l_two_tree ℕ :=
l_two_tree.corec $ λ z n mk_tree,
l_two_tree'.cons₂ n (more $ l_two_tree'.cons (n+1) (mk_tree $ n+1))
                    (more $ l_two_tree'.cons (n+2) (mk_tree $ n+2))

It has one new quirk: the necessity of calling more if you are nesting constructors.

[cipher1024]

Here are a few ideas for where this project might go:

• nested constructors
• coinductive type families
• mutual coinductive types
• mutual corecursive functions
• syntax
• in coinductive type declaration, nesting of recursive call inside of other inductive / coinductive types
• vm support?

[cipher1024]

Looking at how I enabled nested constructors, I'm wondering if we could have a more relaxed guardedness criterion than Coq and allow code like this:

coinductive stream a 
| cons : a -> stream a -> stream a

def weak_guardedness : nat -> list nat -> stream (list nat) 
| n (x :: xs) := weak_guardedness (n + x) xs
| n [] := cons n (weak_guardedness n [1 .. n])

Basically, one of the branches is not guarded (according to Coq) but the list argument decreases until we use a constructor of stream.

[cipher1024]

My motivating example for this feature is a Lean port of the Haskell pipes library for composing streaming programs: https://hackage.haskell.org/package/pipes. As an aside, it is also beautifully documented.

Mine is https://github.com/cipher1024/lean-pipes. I started developing it again to see how far the current feature set takes me. This package finally enabled me to write the map :: (a -> b) -> Pipe a b m r program which basically forever waits for input, transforms, yields it and starts over.

I'm now exploring how I need to adapt bisimulation for practical proofs of equality.

[robertylewis]

@cipher1024 What is the status of this? Is this still WIP, or dead? Should we close this PR?

[cipher1024]

I have moved this development to mathlib-nursery because it will probably be long winded and also useful before it gets pretty.

[johoelzl]

Fare well