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)
40
questions
2
votes
3
answers
232
views
Uniqueness of proofs for inductively defined predicates
In Init/Peano.v the less-than-or-equal predicate is defined as follows:
...
1
vote
4
answers
206
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
144
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 ...
5
votes
2
answers
124
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:
...
- 5,510
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
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
98
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 ...
- 476
0
votes
1
answer
163
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:
...
- 5,510
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
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
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
4
votes
1
answer
177
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 ...
- 2,022
2
votes
1
answer
179
views
Induction scheme on two arguments for custom type in Coq
I've been working on formalizing a Hilbert deductive system within Coq. I have the following definition for a term in first-order logic:
...
- 195
18
votes
1
answer
1k
views
What are the complex induction patterns supported by Agda?
A question was recently asked on the Coq-club mailing list on Coq rejecting a nastily nested inductive type. We encountered a similar difficulty while trying to port code from Agda to Coq: Agda ...
- 2,077
-2
votes
2
answers
119
views
