Zulip Chat Archive
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.
Reference: http://isabelle.in.tum.de/dist/doc/datatypes.pdf
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
Utensil Song (Jun 09 2020 at 08:56):
https://github.com/avigad/qpf/
Utensil Song (Jun 09 2020 at 08:57):
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/leanprovercommunity/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/CoinductiveTypes , 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)
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 (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 nonbuiltin 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:
 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.

we need to generalize to n dimensions not only 3 dimensions

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