Questions tagged [coinductive-type]

Use with coinductive types.

Filter by
Sorted by
Tagged with
8 votes
3 answers
188 views

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

I have defined the conatural numbers, bisimulation (extensional equality?) and addition as follows, ...
  • 101
4 votes
2 answers
157 views

Why do coinductive types require bisimilarity relations?

I was messing around with induction stuff again and some stuff seems to require bisimilarity relations instead of just equality when dualizing for coinductive types. ...
4 votes
2 answers
115 views

What is a non-canonical term?

I've heard the phrase used in relation to comparing proof assistants, but I don't understand what it means. For example, for introducing an instance of coinductive types, Agda uses destructors and ...
12 votes
0 answers
124 views

Rules for mutual inductive/coinductive types

Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
  • 2,215
11 votes
1 answer
256 views

Is induction over mutually inductive coinductive types possible?

You can encode ordinals in Coq as Inductive ord := O | S (n: ord) | Lim (s: nat -> ord). Suppose you use the following encoding instead ...
9 votes
2 answers
212 views

Comparison between proof assistants for coinductive structures and proofs

I have a quite vague and naïve question: what are the differences between the different proof assistants regarding coinduction? My motivation is that I'd like to formalize some proofs, basically about ...
19 votes
1 answer
322 views

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

Ever since the work by Gimenez for his PhD thesis, Coq has supported positive coinductive types. For example, the type of always-infinite streams containing elements of type ...
  • 195
8 votes
1 answer
106 views

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

In Agda with --guardedness, we can define productive definitions using copatterns like the following ...
  • 4,740
18 votes
1 answer
174 views

When to use coinductive types?

One could define streams in the following manner ...