18 votes

When to use coinductive types?

First a note: you are using the syntax for so-called "positive" coinductive types, which makes them look like inductive types, defined by "constructors". This has various problems:...
Mike Shulman's user avatar
  • 3,040
18 votes
Accepted

What is the state of coinductive types and reasoning in Coq?

Intuition of the problem A good rule of thumb is to consider that in intensional type theory, coinductive types and function types share a lot of properties. In particular, equality over streams is ...
Pierre-Marie Pédrot's user avatar
9 votes
Accepted

Is it possible to define `fib` coinductive stream w/o sized types?

I recommend the state machine definition that we'd use for looping over Fibonacci numbers: ...
András Kovács's user avatar
8 votes
Accepted

Is induction over mutually inductive coinductive types possible?

It makes sense to want something like this, but Agda's termination/productivity checker does not actually validate this interpretation of the types. The reasoning behind your induction principle is ...
Dan Doel's user avatar
  • 942
7 votes

Comparison between proof assistants for coinductive structures and proofs

Here's my quick and dirty overview. I don't know Lean, so anyone who does is free to edit the answer to add it, but my impression is that co-induction isn't natively supported there yet. Coq: ...
Joey Eremondi's user avatar
6 votes
Accepted

Defining and using bisimilarity for negatively-defined conatural numbers

You must recognize that you really have two mutually defined types here: conat and option conat. (In general, you should think ...
HTNW's user avatar
  • 533
6 votes

How to prove that addition is commutative for conatural numbers in Coq

You just have to be a bit smarter about the definition of coadd so that it consumes both arguments. ...
Andrej Bauer's user avatar
  • 8,969
5 votes

Why do coinductive types require bisimilarity relations?

Semantically, bisimulation just is the correct notion of equality for coinductive types. A nice intuition for it comes from parametricity. The Church encoding of a coinductive stream type $\nu a.\,(\...
Neel Krishnaswami's user avatar
4 votes
Accepted

What are the differences and similarities between records, coinductive records, and codatatypes?

By reading your question, I believe that you are not looking for a very technical answer, but general ideas instead. If you would like to dig deeper, you can search with the keyword 'polarity' and '...
ice1000's user avatar
  • 6,124
4 votes

What is a non-canonical term?

Your claim that Agda has element which Idris doesn't have is not true. Here's an Idris-equivalent I came up with: ...
ice1000's user avatar
  • 6,124
4 votes
Accepted

Why do coinductive types require bisimilarity relations?

Coinductive types "require bisimilarity instead of =" for the same reason function types "require ...
HTNW's user avatar
  • 533
3 votes
Accepted

How to reason about and extract code for inductive types with negative occurrences in Coq?

Building on Cody's suggestion, the following might work for you. I will consider a simpler type that still captures the essence of the problem. Define a structure which, given a type ...
Andrej Bauer's user avatar
  • 8,969
3 votes

Comparison between proof assistants for coinductive structures and proofs

I do not know much about other proof assistants, but as for Coq I can say that there are quite some resources around that you might benefit from. Here is a starting point. However, the current ...
Meven Lennon-Bertrand's user avatar
3 votes

Is existence of Stream as final co-algebra for the suitable functor enough to write functions into equality of streams by co-induction in ExtMLTT?

The universal property of final coalgebras can be formalized as unique-ana : ∀ (f : A → B × A) (g : A → Stream B) → unfold ∘ g ≡ map₂ g ∘ f → g ≡ ana f where <...
Li-yao Xia's user avatar
  • 1,727
3 votes
Accepted

Is there a formalism of "coinductive" data types with negative occurrences?

I found my answer in Guarded Domain Theory and its implementation in Guarded Cubical Agda (implementing Ticked Cubical Type Theory). The following program type-checks ...
Sebastian Graf's user avatar
2 votes

How to prove that addition is commutative for conatural numbers in Coq

Andrej Bauer has introduced a smarter definition of coadd and has proven that it is commutative. However, I would like to show that we can prove commutativity ...
Daigo's user avatar
  • 101
2 votes

How to prove that addition is commutative for conatural numbers in Coq

You could try to use the techniques described in Nils Anders Danielsson's Beating the Productivity Checker Using Embedded Languages. I've used them in the Agda standard library and successfully ...
gallais's user avatar
  • 1,126
2 votes

Stream of all finite prefixes of a stream

If you do not care about algorithmic efficiency, the simplest way to do this is to thread an accumulator in your cofixpoint: ...
Pierre-Marie Pédrot's user avatar
1 vote

Defining and using bisimilarity for negatively-defined conatural numbers

This is not really an answer, but in case you decide not to use coinductive types at all, you can have a look at how the Brown-Pradic result is formalized in Martín Escardó's ...
Andrej Bauer's user avatar
  • 8,969
1 vote

Co-induction principle

It it a plausible thing to do? I could just be lacking imagination, but this doesn't seem like a plausible thing to do. This seems to be a misguided attempt at understanding coinduction by duality ...
Li-yao Xia's user avatar
  • 1,727
1 vote

Is there a formalism of "coinductive" data types with negative occurrences?

Your datatype is a variant of the domain equation for the untyped lambda calculus. Verifying that an arbitrary untyped lambda term is normalizing is an undecidable problem, but there are undecidable ...
Max New's user avatar
  • 304
1 vote

Two-step induction of inductive predicate on Streams

Do you mean the induction principle generated by the following definition ? ...
Pierre Castéran's user avatar
1 vote

What is a non-canonical term?

The notion of a canonical term is an additional structure on type theory which must be specified. Informally speaking, it means something like "special nice form that we like very much". ...
Andrej Bauer's user avatar
  • 8,969

Only top scored, non community-wiki answers of a minimum length are eligible