Questions tagged [inductive-type]
In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor. (from nLab)
11
questions
2
votes
3
answers
160
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
- 127
1
vote
4
answers
205
views
Formalizing "finite or infinite" in Coq
In Coq, I am trying to formalize the notion of a finite or infinite sequence, e.g. of natural numbers: call it a run, and call ...
- 249
2
votes
4
answers
142
views
How do I define an induction principle for a type with a nested list of tuples?
I want to define an inductive type that describes records. The records are lists of elements, each element has a name and type. This requires nested recursion, so I've had to define an induction ...
- 75
1
vote
0
answers
69
views
Heterogeneous lists, large indices
Recently I had cause to define a type of heterogeneous lists in Lean, and wrote
...
- 111
5
votes
2
answers
123
views
Comparing indexed induction to recursion
Many indexed inductive families can be "equivalently" defined by recursion over their indices. For instance, the type family of vectors:
...
- 3,190
1
vote
0
answers
45
views
how to inductively define paths from paths using unimath
I'd like to define a type of graph where given a set of edges, we can define another graph that has everything from graph 1 but extends the set of edges by adding higher level edges to parallel edges(...
- 71
1
vote
1
answer
97
views
How to apply constructor injectivity in the goal
Suppose I have a goal
Goal forall m n, S m = S n -> m = n.
intros m n H.
1 goal
m, n : nat
H : S m = S n
============================
m = n
I know ...
- 13
0
votes
1
answer
162
views
Why inductive types (or variants) are so rigid in terms of the set of constructors
An inductive type definition normally carries a set of constructors C, but I am not so sure why the set of constructors C is always once-for-all statically defined.
For instance:
...
- 125
1
vote
0
answers
63
views
Why does Coq not allow constructor argument types to be strictly positive mutual inductive types?
Note: Apologies for the wicked mouthful of a title. I'm still getting acquainted with Coq terminology, so I might not have chosen the best words. If you have a better title suggestion, edits are more ...
- 143
1
vote
0
answers
48
views
Can you always replace mutually recursive references with parameters?
This is a follow up to a question someone else previously posted: Expressivity of mutual/nested inductives vs. regular inductives.
pigworker answered that
Adopting Agda-ish notation, the basic ...
- 143
2
votes
2
answers
211
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 ...
- 133