All Questions
Tagged with inductive-type coq
15
questions
2
votes
3
answers
247
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
214
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 ...
- 248
2
votes
4
answers
146
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 ...
1
vote
0
answers
46
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
99
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
169
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,530
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
2
votes
1
answer
182
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
-2
votes
2
answers
119
views
6
votes
4
answers
849
views
Inductive vs. recursive definitions
In Coq there are two ways to define a new type on an inductive type: Using Inductive and using Fixpoint. What are pros and cons ...
- 146
2
votes
1
answer
93
views
Coq Induction on Hypothesis destroys the Hypothesis
I'm trying to prove something in coq
I have and Inductive prop type named in_order_merge which is a relation between three lists that shows third one is in_order merge of first two, here is the ...
3
votes
1
answer
239
views
Why do record based inductive types with primitive projections lack an eta law?
In Coq there is ongoing work to shore up some weaknesses in subject reduction and coinductive types. Primitive projections are part of that effort for better behaviour.
I get why there might be ...
- 1,547
11
votes
2
answers
415
views
Proving uniqueness of an instance of an indexed inductive type
Consider the simple indexed inductive type
Inductive Single : nat -> Set :=
| single_O : Single O
| single_S {n} : Single n -> Single (S n).
Intuitively, I ...
- 5,530