Skip to main content
4 votes
Accepted

Why inductive types (or variants) are so rigid in terms of the set of constructors

There are two components to your question. The first, corresponds to the idea of constructor subtyping (actually, non-empty lists are the first example of the paper). I don't think there are any hard ...
Meven Lennon-Bertrand's user avatar
3 votes
Accepted

Induction scheme on two arguments for custom type in Coq

Coq complains with reason: there is a priori no reason why the number of arguments of the two functions you are comparing have to be the same. And, indeed, you lemma is false! ...
Meven Lennon-Bertrand's user avatar
3 votes
Accepted

How to reason about and extract code for inductive types with negative occurrences in Coq?

Building on Cody's suggestion, the following might work for you. I will consider a simpler type that still captures the essence of the problem. Define a structure which, given a type ...
Andrej Bauer's user avatar
  • 9,194
3 votes

How do I define an induction principle for a type with a nested list of tuples?

The question of recursors for types nested with lists, aka rose trees, is popping up quite often these days. I did develop a Coq library specifically for the purpose of dealing with these data ...
Dominique Larchey-Wendling's user avatar
2 votes

How do I define an induction principle for a type with a nested list of tuples?

...
Li-yao Xia's user avatar
  • 1,757
1 vote
Accepted

How do I define an induction principle for a type with a nested list of tuples?

Concerning your question in a comment about Equal : _ -> _ -> Prop, this is how I would proceed, using an inductive predicate: ...
Dominique Larchey-Wendling's user avatar
1 vote

How do I define an induction principle for a type with a nested list of tuples?

Allow me to give a “these are not the droids you're looking for” answer. A record is a mapping from field labels to corresponding values. A list of pairs, such as the one you are using, is not a ...
Andrej Bauer's user avatar
  • 9,194
1 vote

Co-induction principle

It it a plausible thing to do? I could just be lacking imagination, but this doesn't seem like a plausible thing to do. This seems to be a misguided attempt at understanding coinduction by duality ...
Li-yao Xia's user avatar
  • 1,757
1 vote

Comparing indexed induction to recursion

As you conjecture in the comments, I also think the two presentations are isomorphic in the "nice enough" case, so I would say this is a question of usage. The exact definitional behaviour ...
Meven Lennon-Bertrand's user avatar
1 vote

Comparing indexed induction to recursion

Since I am familiar with Coq, so I talk about some experiences when I did both in Coq. In most cases, the indexed inductive type would be a greater option. The recursive fashion may require less ...
Hiroki Chen's user avatar
1 vote
Accepted

How to apply constructor injectivity in the goal

You can write an ad-hoc tactic ...
Lolo's user avatar
  • 476

Only top scored, non community-wiki answers of a minimum length are eligible