All Questions
Tagged with inductive-type coq
15
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:
...
- 127
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 ...
- 75
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 ...
- 13
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:
...
- 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
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
-2
votes
2
answers
119
views
Help with strong induction
I have the following definition of divisibility by 3.
...
6
votes
4
answers
841
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 ...
- 224
2
votes
1
answer
92
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
237
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 ...
- 2,868
11
votes
2
answers
412
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 ...
- 213