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.

- the Coq'Art book has a chapter on coinduction (chapter 13), you can get the sources+exercises in this repo, specifically here
- in the same repo, there are sources for a tutorial on both inductive and coinductive types
- CPDT has a chapter on coinductive types.
- Leroy and Grall's coinductive programming language semantics is one application that might help

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

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

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.

but *nobody* uses primitive projections to do coinduction currently

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

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

noted thanks everyone!

Karl Palmskog said:

but

nobodyuses 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.

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.

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

Karl Palmskog said:

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

What did you mean by this?

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.

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

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

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

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

Have you got some examples of datatypes in mind?

streams, infinite trees?

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

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

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.

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

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.

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.

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.

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).

the negative declarations look like garbage

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

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

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

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.

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

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.
```

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.

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

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.

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

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

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

also, most don't care about SR breakage

so I think we are still at an impasse

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

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!

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

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.

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"

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 )

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

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

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

The `traceF`

-`trace`

decomposition just tells you that the observations on your coinductive type have inductive structure.

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

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.

how exactly are negative types more constructive than positive ones?

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!

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.

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

Last updated: Oct 03 2023 at 04:02 UTC