Stream: Coq users

Topic: Where to learn about co induction


view this post on Zulip walker (Feb 12 2022 at 15:19):

Not strictly related to coq, but I am learning it in coq context.. Does any one knows good place to learn about coinductive types and coinduction in I am struggling to see the difference between inductive types and co-inductive types in coq.

view this post on Zulip Karl Palmskog (Feb 12 2022 at 15:41):

view this post on Zulip Alexander Gryzlov (Feb 12 2022 at 15:44):

https://plv.mpi-sws.org/paco/ might be also useful

view this post on Zulip walker (Feb 12 2022 at 15:49):

Thanks a lot every, probably I would start by the tutorial, and decide what to do next from there!

view this post on Zulip Ali Caglayan (Feb 12 2022 at 15:55):

Don't forget about the Coq reference manual. There is an important caveat that you should keep in mind. Many of the older sources linked above will treat coinductive types in a "positive" manner, using constructors and pattern matching.

This can be argued to be a historical mistake, and is known to break important properties of Coq. The alternative is the "negative" presentation of coinductive types, which essentially look like records whose fields can reference the record type.

view this post on Zulip Karl Palmskog (Feb 12 2022 at 15:57):

but nobody uses primitive projections to do coinduction currently

view this post on Zulip Karl Palmskog (Feb 12 2022 at 15:57):

and I would strongly advise not to do that, since syntax and semantics is terrible

view this post on Zulip Karl Palmskog (Feb 12 2022 at 16:04):

in contrast, Pierre-Marie's proposal for fixing of "breaking of important properties" looks bearable and will not kill off coinduction in the Coq ecosystem, like mandating primitive projections will: https://github.com/coq/coq/pull/10764

view this post on Zulip walker (Feb 12 2022 at 16:35):

noted thanks everyone!

view this post on Zulip Yannick Zakowski (Feb 12 2022 at 17:08):

Karl Palmskog said:

but nobody uses primitive projections to do coinduction currently

I don't know if that's true. We do in the Interaction Trees library and other experimental projects related: https://github.com/DeepSpec/InteractionTrees/
And fwiw so does paco in its internals, though it's not visible from the user side.

view this post on Zulip Yannick Zakowski (Feb 12 2022 at 17:10):

And more generally on the topic of coinduction in Coq, I strongly recommend Pous's library as a potential alternative to paco: https://github.com/damien-pous/coinduction
I tend to find it more accessible as it builds on a cleaner foundation.

view this post on Zulip Arpan Agrawal (Feb 14 2022 at 10:10):

According to http://flint.cs.yale.edu/cs428/coq/doc/faq.html, Eduardo Gimenez' thesis (Reference number 8 on the page) is a good resource

view this post on Zulip Ali Caglayan (Feb 28 2022 at 17:35):

Karl Palmskog said:

and I would strongly advise not to do that, since syntax and semantics is terrible

What did you mean by this?

view this post on Zulip Ali Caglayan (Feb 28 2022 at 17:36):

I am very confused since I was under the impression that negative coinductive types had a semantics that made sense, whereas for positive coinductive types that is not the case.

view this post on Zulip Ali Caglayan (Feb 28 2022 at 17:37):

Have you got any information on the semantics of positive coinductive types?

view this post on Zulip Karl Palmskog (Feb 28 2022 at 17:56):

@Ali Caglayan please see the Q&A I had with PMP here: https://proofassistants.stackexchange.com/questions/583/what-is-the-state-of-coinductive-types-and-reasoning-in-coq

There is a reason that primitive projections are unpopular. In my view, the connection between records and coinductive types should be nonexistent. PMP's positive types would at least make sense.

view this post on Zulip Ali Caglayan (Feb 28 2022 at 18:01):

Can you expand on why there should be no connection between records and coinductive types?

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:02):

I want to express a coinductive datatype or relation, I don't want to declare some weird record that can't be accessed. This is not hard

view this post on Zulip Ali Caglayan (Feb 28 2022 at 18:03):

Have you got some examples of datatypes in mind?

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:04):

streams, infinite trees?

view this post on Zulip Ali Caglayan (Feb 28 2022 at 18:05):

For streams you have a one constructor coinductive type, isn't a record precisely what having one constructor means (in the non-indexed case)?

view this post on Zulip Ali Caglayan (Feb 28 2022 at 18:07):

And could you elaborate on "weird record that can't be accessed"?

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:08):

Paulin introduced inductive datatype declarations into Coq, and Gimenez mirrored her syntax for coinductive types. Why would I want to use anything else? The burden is basically on you to show convincingly why switching to primitive projections everywhere only for coinductive declarations is a good idea.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:10):

you can see similar reasoning here: https://github.com/coq/coq/pull/10764#issuecomment-532771463

view this post on Zulip Ali Caglayan (Feb 28 2022 at 18:12):

I'm trying to understand why people are using positive coinductive types in Coq, and so far the only convincing reason I've found is that "negative coinductive types weren't around then". I'm looking to understand what people expect when they do coinduction.

Gimenez "mirroring syntax" doesn't seem quite correct to me. Inductive datatypes are typically thought of as the least fixed point of something. Being the least, they have to somehow map into every other fixed point hence you get an elimination principle. Coinductive datatypes are typically thought of as the greatest fixed point of something. Being the greatest you have to map other fixed into them. This is why I don't expect to see (multiple) constructors when talking about coinductive types.

view this post on Zulip Ali Caglayan (Feb 28 2022 at 18:14):

Karl Palmskog said:

you can see similar reasoning here: https://github.com/coq/coq/pull/10764#issuecomment-532771463

This thread is also very confusing, but it seems that the quarrel is rather with PMP's "complicated" syntactic criterion rather than anything concrete about negative coinductive types.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:18):

What exactly is confusing about this quote from Xavier:

Coq's positive coinduction leads to awkward proofs (manual unrollings, nothing computes, etc) but the specifications are quite nice. You can take Capretta's PhD thesis, or the Leroy-Grall paper on coinductive natural semantics, and transcribe the mathematical descriptions as coinductive types and predicates that look like the maths.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 18:18):

Paulin introduced inductive datatype declarations into Coq, and Gimenez mirrored her syntax for coinductive types. Why would I want to use anything else?

Because codata is _dual_ to data. Coinduction with negative types works in Agda and makes lots of sense (at least ignoring sized types).

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:19):

the negative declarations look like garbage

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 18:22):

apologies for mistaking this for a discussion, but I don't care enough for coinduction to deal with this much emotion.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:27):

but what exactly is your argument then? Rewrite tens of thousands of lines of Coq proofs because it makes sense in Agda?

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:29):

I'm fine with primitive projections being available, but if the only argument is: it works in Agda and the previous syntax seems incorrect - why would anyone want to port code? The best solution is probably just to get https://github.com/coq/coq/pull/10764 merged

view this post on Zulip Ali Caglayan (Feb 28 2022 at 18:33):

Let's remove Agda from the discussion, since that should have zero weight here. What I'm simply trying to understand is are there any semantics for positive coinductive types? The semantic picture which gets discussed when talking about coinduction which I outlined above seems to indicate that we expect to see negative coinductive types.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:36):

have you read Gimenez's thesis and papers? I already link to https://link.springer.com/chapter/10.1007/3-540-60579-7_3 in the StackExchange post

view this post on Zulip Karl Palmskog (Feb 28 2022 at 18:56):

if the defining feature of negative types are a single constructor, does this mean you have to use option to get anything close to possibly-infinite/lazy lists? For example:

CoInductive trace : Type :=
| Tnil : A -> trace
| Tcons : A -> B -> trace -> trace.

view this post on Zulip Li-yao (Feb 28 2022 at 19:01):

You can convert any positive coinductive into a negative by first breaking the recursion into a non-recursive functor and then wrap it in a single-field coinductive. And I agree it looks silly.

view this post on Zulip Li-yao (Feb 28 2022 at 19:02):

Inductive traceF (X : Type) : Type := Tnil : A -> traceF X | Tcons : A -> B -> X -> traceF X.
CoInductive trace := { untrace : traceF trace }.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:04):

oh gods.. the only way I can see this being used [the positive version] is by compilation akin to Equations. That is, one would write everything as positive types first and then convert them to negative.

view this post on Zulip Ali Caglayan (Feb 28 2022 at 19:06):

Right, but the semantics of that thing are well understood, so if Coq compiled "positive" coinductive definitions in the background, would anybody care?

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:07):

as also discussed on the StackExchange, you have to also introduce axioms

view this post on Zulip Ali Caglayan (Feb 28 2022 at 19:08):

Right, but also discussed is the fact that funext is a thing, and few people seem to mind.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:09):

also, most don't care about SR breakage

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:09):

so I think we are still at an impasse

view this post on Zulip Li-yao (Feb 28 2022 at 19:12):

Wouldn't people who don't care about SR be just as happy with adding the eta rule as an axiom?

view this post on Zulip Ali Caglayan (Feb 28 2022 at 19:15):

I don't really care that people like to write their coinductive types in a positive way, Li-yao already demonstrated how that can be overcome using a "compilation". SR breakage isn't a deal breaker for me but rather a symptom of a bigger problem which is that there are no good semantics for positive coinductive types AFAICT. If there are, please tell me!

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:15):

OK, define first what you mean by "good semantics"

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:16):

then the next step might be to demonstrate why Gimenez's semantics / the current positive types implementation is not "good" according to the definition and why the proposal in PR 10764 is not "good" either. In the second case, it may be better to take the discussion to the PR.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:23):

I at least read PMP's answer on the StackExchange as that SR is the basic issue, which in my view makes it boil down to: "nice definitions + SR breakage" or "non-nice definitions + axioms + no SR breakage"

view this post on Zulip Li-yao (Feb 28 2022 at 19:30):

Just as a comment, IIRC Gimenez does not really address the SR problem, instead he moves the goalposts by proving a weaker SR-like theorem (thesis p48 (p60 of the PDF): http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.16.9849&rep=rep1&type=pdf )

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:33):

yeah, from what I know Gimenez was aware of the SR breakage, but Ali said the SR breakage itself wasn't the deal breaker.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 19:39):

FWIW, "backwards compatibility" is one concern (and a valid one), "negative records are bad" is a different one.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 19:40):

And looking from here, I'm not sure why you're blaming negative coinductives when people mix inductives and coinductives without realizing.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 19:43):

The traceF-trace decomposition just tells you that the observations on your coinductive type have inductive structure.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 19:44):

Having said that, I don't know if negative coinductives are "the right" concept, but they certainly have a claim to that position.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 19:45):

The resulting maths looks certainly different; but constructive maths looks unusual to a classical mathematician, and I don't think we'd appreciate if they talked about "garbage" for those definitions.

view this post on Zulip Karl Palmskog (Feb 28 2022 at 19:57):

how exactly are negative types more constructive than positive ones?

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 19:58):

I didn't say "more constructive", I made an analogy: Some would argue they're "more principled" since they support SR more elegantly — which of course is subjective!

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 19:59):

Either way, Coq supports both classical logic and definitional proof irrelevance (and nobody plans to drop either), so it could just as well keep supporting positive inductives (either as-is, or with PMP's restriction). If people want SR by default, you could just restrict positive inductives by default.

view this post on Zulip Paolo Giarrusso (Feb 28 2022 at 20:00):

But I'm anyway a pluralist who doesn't see Lean's choices as sinful.


Last updated: Feb 08 2023 at 23:03 UTC