coinductive datatypes

Stream: new members

[Utensil Song]

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.

Reference: http://isabelle.in.tum.de/dist/doc/datatypes.pdf

[Mario Carneiro]

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

[Mario Carneiro]

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

[Utensil Song]

https://github.com/avigad/qpf/

[Utensil Song]

Looks promising

[Mario Carneiro]

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

[Utensil Song]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

Depending on your use case this may be sufficient

[Mario Carneiro]

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]

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

[Utensil Song]

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)

instantiation mvec :: ab_group_add
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
by intro_classes (simp_all add: mvec_eq_iff)
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]

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]

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

[Mario Carneiro]

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]

@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]

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]

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.

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

3. 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]

This can all be done with no difficulty

[Mario Carneiro]

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

[Mario Carneiro]

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.