Questions tagged [coinductive-type]
Use with coinductive types.
18
questions
2
votes
2
answers
194
views
How to reason about and extract code for inductive types with negative occurrences in Coq?
I'm interested in proving correctness of the interpreter of Appel's compiler (appendix B), and compare it to the machine semantics given by Kennedy on his paper. The interpreter acts as a denotational ...
- 123
4
votes
1
answer
163
views
Co-induction principle
It's known that Nat-ind = Nat-rec ⨯ Nat-initiality
Has someone figured out how to define a suitable Conat-coind
such that ...
- 345
2
votes
1
answer
89
views
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?
Suppose we work inside MLTT with equality reflection (extensional MLTT).
Assume I postulate existence of Streams as final co-algebra for the suitable functor.
Is that enough to prove the bisimulation ...
- 345
6
votes
2
answers
199
views
Is there a formalism of "coinductive" data types with negative occurrences?
Consider the following program in Haskell:
...
1
vote
0
answers
58
views
Can you help me lay out the different variations of CoC and their generalizations?
I am learning the typed lambda-calculus and looking into the Calculus of Constructions. It was going well until I was slapped in the face with variations, and now I'm confused about the layout of all ...
- 342
1
vote
3
answers
77
views
Two-step induction of inductive predicate on Streams
If I want to have an induction principle for nats from n to n+2, I can define and prove this ...
- 131
0
votes
2
answers
55
views
Stream of all finite prefixes of a stream
If I want to construct of list of all (obviously finite) prefixes of a list, I can define this function:
...
- 131
22
votes
0
answers
490
views
Categorical semantics of Agda
I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
- 2,902
7
votes
1
answer
181
views
What are the differences and similarities between records, coinductive records, and codatatypes?
Record types are a common feature in most paradigms.
Agda also allows defining records with the coinductive keyword.
Lastly there are the seemingly more exotic co(...
- 289
8
votes
3
answers
297
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
190
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.
...
- 2,748
3
votes
2
answers
142
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
152
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,902
12
votes
1
answer
378
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
...
- 2,748
9
votes
2
answers
306
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 ...
- 111
21
votes
1
answer
663
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 ...
- 315
8
votes
1
answer
127
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
...
- 5,792
18
votes
1
answer
252
views