## Stream: new members

### Topic: coinductive datatypes

#### Utensil Song (Jun 09 2020 at 02:27):

Is there coinductive datatypes in Lean or a way to mimic it? It's called codatatype in Isabelle/HOL. I kind of need to port something defined by codatatype in Isabelle/HOL to Lean.

#### Mario Carneiro (Jun 09 2020 at 04:56):

There is no built in support, but a few ways to mimic it

#### Mario Carneiro (Jun 09 2020 at 04:57):

The QPF package being developed by @Simon Hudon is the nearest hope to a general facility for this in lean, but in specific cases you can make do with ad hoc encodings

Looks promising

#### Mario Carneiro (Jun 09 2020 at 08:58):

I think that version is fixed for the lean together meeting. I'm pretty sure it's been developed since then

#### Utensil Song (Jun 10 2020 at 14:48):

I'm a little bit confused. It seems that coinductive was once in Lean and removed since v3.4.2 (18 Jan 2019) with comment "To be moved to mathlib instead." And mathlib has https://github.com/leanprover-community/mathlib/blob/master/src/meta/coinductive_predicates.lean and some smoke tests show that it basically works. By there's no built in support, do you mean the implementation so far is not complete or not general enough?

#### Utensil Song (Jun 10 2020 at 15:03):

A friend found https://github.com/leanprover/lean/wiki/Coinductive-Types , which provides a historical perspective.

#### Mario Carneiro (Jun 10 2020 at 15:04):

There are two different things here: coinductive predicates and coinductive types

#### Mario Carneiro (Jun 10 2020 at 15:05):

Coinductive predicates were originally in lean core and were moved to mathlib a while ago, and although they haven't gotten any love in the past few years the implementation works as far as I am aware

#### Mario Carneiro (Jun 10 2020 at 15:05):

Depending on your use case this may be sufficient

#### Mario Carneiro (Jun 10 2020 at 15:07):

These are propositions though, and can be defined fairly easily by using impredicativity of Prop. This construction does not cover coinductive datatypes, which live in Type

#### Mario Carneiro (Jun 10 2020 at 15:07):

Do you have any specific examples you are trying to encode? You linked to a book

#### Utensil Song (Jun 10 2020 at 16:06):

The motivating example:

We first define concrete data structures. We define a type mvec of a multivector as a codatatype in Isabelle. We could have used a datatype but by defining this notion coalgebraically, we can formalize the various multivector operations more elegantly by considering their grades separately.

codatatype mvec = Mvec (Scalar: real) (Vec: "real^3") (Bivec: "real^3") (Trivec: real)

begin
primcorec zero_mvec where
"Scalar 0 = 0"
| "Vec 0 = 0"
| "Bivec 0 = 0"
| "Trivec 0 = 0"

primcorec plus_mvec where
"Scalar (x + y) = Scalar x + Scalar y"
| "Vec (x + y) = Vec x + Vec y"
| "Bivec (x + y) = Bivec x + Bivec y"
| "Trivec (x + y) = Trivec x + Trivec y"

primcorec uminus_mvec where
"Scalar (-x) = - Scalar x"
| "Vec (-x) = - Vec x"
| "Bivec (-x) = - Bivec x"
| "Trivec (-x) = - Trivec x"

primcorec minus_mvec where
"Scalar (x - y) = Scalar x - Scalar y"
| "Vec (x - y) = Vec x - Vec y"
| "Bivec (x - y) = Bivec x - Bivec y"
| "Trivec (x - y) = Trivec x - Trivec y"
instance
end


(More code omitted, it's from A New Formalization of Origami in Geometric Algebra by Tetsuo Ida, Jacques Fleuriot, and Fadoua Ghourabi )

#### Utensil Song (Jun 10 2020 at 16:08):

Mario Carneiro said:

These are propositions though, and can be defined fairly easily by using impredicativity of Prop. This construction does not cover coinductive datatypes, which live in Type

Ah, I need to read more to tell the difference...They look very similar (not only by name but also by use cases)

#### Mario Carneiro (Jun 10 2020 at 17:03):

What? This is not even a recursive structure, so it makes no difference if it is inductive or coinductive

#### Mario Carneiro (Jun 10 2020 at 17:04):

I believe that the comments about codatatype over datatype have more to do with details of the datatype package implementation in isabelle than any mathematical notion

#### Mario Carneiro (Jun 10 2020 at 17:11):

@Utensil Song Here's a rendering of that code snippet in lean:

import data.real.basic algebra.pi_instances

structure mvec :=
(scalar : ℝ)
(vec : fin 3 → ℝ)
(bivec : fin 3 → ℝ)
(trivec : ℝ)

instance : has_zero mvec := ⟨⟨0, 0, 0, 0⟩⟩
instance : has_add mvec := ⟨λ x y,
⟨x.scalar + y.scalar, x.vec + y.vec, x.bivec + y.bivec, x.trivec + y.trivec⟩⟩
instance : has_neg mvec := ⟨λ x, ⟨-x.scalar, -x.vec, -x.bivec, -x.trivec⟩⟩


#### Mario Carneiro (Jun 10 2020 at 17:14):

I think the quote is saying that the use of codatatype allows them to define the various components of the operations by specifying all of its projections separately rather than making a constructor which puts them all in one expression. I think this is a minor gain, and in the context of lean certainly not worth the hassle of using a non-builtin datatype with worse defeq. Instead you can use attributes like @[simps] to automatically generate the projection theorems that isabelle's primcorec is creating

#### Utensil Song (Jun 12 2020 at 03:53):

Thanks for the tips and sorry for the late reply. Yes, the trivial addition case failed to demonstrate the necessity of coinductive types, but we need more general cases:

1. for multiplication, it would need something like
instantiation mvec :: monoid_mult
begin
primcorec times_mvec where
"Scalar (x * y) = Scalar x * Scalar y + (Vec x · Vec y) - (Bivec x · Bivec y) - Trivec x * Trivec y"
| "Vec (x * y) = ..."
| "Bivec (x * y) = ..."
| "Trivec (x * y) = ..."
end


and yes, this is still something that can be solved by plain structures.

1. we need to generalize to n dimensions not only 3 dimensions

2. there's an infinite dimension version along the way, from it obtain all finite dimensional geometric algebras as subalgebras.

I'm still looking into the possibilities of implementing the above in Lean or Agda. And I'm also learning more about the whole coninductive, corecursive, coinduction thing and its applicability/necessity to my problem.

I also checked out @[simps] which doesn't seem to solve the multiplication case and is very limited for the addition case.

I'll get back here when I have a more clear picture of what I'm trying to do here.

#### Mario Carneiro (Jun 12 2020 at 04:32):

This can all be done with no difficulty

#### Mario Carneiro (Jun 12 2020 at 04:32):

there is no argument for coinductive types here besides some trivial syntax

#### Mario Carneiro (Jun 12 2020 at 04:38):

import analysis.normed_space.real_inner_product

structure mvec :=
(scalar : ℝ)
(vec : euclidean_space (fin 3))
(bivec : euclidean_space (fin 3))
(trivec : ℝ)

instance : has_zero mvec := ⟨⟨0, 0, 0, 0⟩⟩

instance : has_add mvec := ⟨λ x y,
⟨x.scalar + y.scalar, x.vec + y.vec, x.bivec + y.bivec, x.trivec + y.trivec⟩⟩

instance : has_neg mvec := ⟨λ x, ⟨-x.scalar, -x.vec, -x.bivec, -x.trivec⟩⟩

noncomputable instance : has_mul mvec := ⟨λ x y,
{ scalar := x.scalar * y.scalar + inner x.vec y.vec - inner x.bivec y.bivec - x.trivec * y.trivec,
vec := sorry,
bivec := sorry,
trivec := sorry }⟩


Note that I don't actually know the maths here, I'm just following your indications. There is some complexity in defining the infinite dimensional version but as long as you can give it an inner product structure you can do the same as above.

Last updated: May 12 2021 at 05:19 UTC