Questions tagged [coinductive-type]

Use with coinductive types.

Filter by
Sorted by
Tagged with
1 vote
1 answer
52 views

Using coIH as an argument to the transitivity of Bisimilarity (cofix and pcofix)

It might be a very silly question for the logic gurus but less so for me. First I generally describe the issue, than I provide a proper example with code. Assume three streams of nats: xs, ys, zs. ...
Uladzimir Treihis's user avatar
3 votes
2 answers
88 views

Defining and using bisimilarity for negatively-defined conatural numbers

Since positive coinductive types in Coq are evil and break subject reduction, I am trying to develop the theory of the conatural numbers using the following negative formulation (within a module ...
Ian Maxwell's user avatar
1 vote
1 answer
82 views

Proof of Constant folding in Coq for IMP using Interaction Trees

Hello Stack Exchange Community, I'm currently working on my thesis which involves using Interaction Trees to define big-step operational semantics for programming languages, particularly the IMP ...
Andrea Tirelli's user avatar
2 votes
2 answers
208 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 ...
paulotorrens's user avatar
4 votes
1 answer
175 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 ...
Russoul's user avatar
  • 345
2 votes
1 answer
102 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 ...
Russoul's user avatar
  • 345
6 votes
2 answers
222 views

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

Consider the following program in Haskell: ...
Sebastian Graf's user avatar
1 vote
0 answers
65 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 ...
Alex Byard's user avatar
1 vote
3 answers
126 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 ...
matteo_c's user avatar
  • 131
0 votes
2 answers
64 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: ...
matteo_c's user avatar
  • 131
21 votes
0 answers
550 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 ...
Mike Shulman's user avatar
  • 3,040
8 votes
1 answer
299 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(...
aradarbel10's user avatar
8 votes
3 answers
391 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, ...
Daigo's user avatar
  • 101
4 votes
2 answers
227 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. ...
Molly Stewart-Gallus's user avatar
3 votes
2 answers
168 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 ...
Robert Watson's user avatar
12 votes
0 answers
167 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 ...
Mike Shulman's user avatar
  • 3,040
12 votes
1 answer
454 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 ...
Molly Stewart-Gallus's user avatar
9 votes
2 answers
406 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 ...
sparusaurata's user avatar
22 votes
1 answer
915 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 ...
palmskog's user avatar
  • 395
8 votes
1 answer
153 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 ...
ice1000's user avatar
  • 6,144
18 votes
1 answer
298 views

When to use coinductive types?

One could define streams in the following manner ...
Agnishom Chattopadhyay's user avatar