Skip to main content

# Tag Info

## Hot answers tagged inductive-type

23 votes
Accepted

### What are the complex induction patterns supported by Agda?

I try to write about what's supported in Agda and the semantics that we have (or don't have) for it. Disclaimers: I'm not an expert on the relevant parts of the Agda source code, I mostly write here ...
• 2,077
17 votes

### Expressivity of mutual/nested inductives vs. regular inductives

Adopting Agda-ish notation, the basic strategy is to turn your bunch of mutually defined inductive types into a single inductively defined universe, indexed over its collection of sorts. Let's do the ...
• 771
14 votes
Accepted

### What are well-founded inductive types?

"Well-founded" and "inductive" mean roughly the same thing. I think the reason different terminology tends to get used for W-types is that their definition looks similar to ...
• 982
10 votes

### Expressivity of mutual/nested inductives vs. regular inductives

There is a fairly general way of turning a mutual inductive into a single inductive which is reminiscent of defunctionalization. This can also be extended to handle nested inductives. A different ...
• 2,032
10 votes
Accepted

### Replacing (strict) positivity with monotonicity on propositions

Impredicative strict Prop supports initial F-algebras for all F : Prop → Prop functors. In Coq: ...
• 2,077
10 votes
Accepted

### Construction of inductive types "the hard way"

In the HOLish settings, these types (starting with the natural numbers) are indeed constructed from first principles; they're certainly not axiomatised. Harrison had an early (1995) paper on how to ...
• 1,112
9 votes
Accepted

### Strong eta-rules for functions on sum types

If we have $\eta$ for functions and also your pointwise conversion rule, that implies the full $\eta$ rule for the (finite) domain type. When checking conversion of arbitrary $t,u$, we can abstract ...
• 2,077
8 votes

### Proving uniqueness of an instance of an indexed inductive type

Or, what would a better way to prove s = single_O? I would define a function that, given a nat n, computes the canonical proof <...
• 1,266
8 votes
Accepted

### Is induction over mutually inductive coinductive types possible?

It makes sense to want something like this, but Agda's termination/productivity checker does not actually validate this interpretation of the types. The reasoning behind your induction principle is ...
• 982
8 votes
Accepted

### Are eliminators useful in practice, or are they only useful in the metatheory?

Indeed, there are parallels between definitions by pattern matching and eliminators. A typical eliminator is just a shallow pattern. For example, the simple recursor for natural numbers can be defined ...
• 9,792
7 votes

### Inductive vs. recursive definitions

Defining recursive properties by fixpoint is possible, but it is usually easier to reason on inductively defined ones. Mostly because they come with their own induction principles. If you use fixpoint ...
7 votes
Accepted

### Why do record based inductive types with primitive projections lack an eta law?

Reduction will not terminate if you give W an eta law. Fixpoints only reduce when applied to constructors. However, if you have ...
• 1,547
7 votes
Accepted

### Pragmatic encodings of inductive inductive types

Your example signature is negative recursive in the second field of Sigma so it can't be encoded in total languages. For internal universes, the usual solution is ...
• 2,077
6 votes

### Expressivity of mutual/nested inductives vs. regular inductives

A lot of these topics are covered in Bruno Barras' habilitation thesis (http://www.lsv.fr/~barras/habilitation/) which, I think, is an interesting read for advanced Coq users. See in particular ...
• 1,266
6 votes
Accepted

### Parameterized Datatypes in a Universe à la Tarski?

Arg : (c : Code) -> (El c -> Desc) -> Desc Are you sure this is what you mean? I think the usual constructor is closer to the following: ...
• 1,266
6 votes

### Construction of inductive types "the hard way"

There are a lot of questions in your question, so I don’t think it’s easy to answer all of them at once, but let me still try and give a picture in the dependently typed setting. First you cannot get &...
• 5,530
5 votes
Accepted

### Explain all the arguments to this rec eliminator

I found hints of the answer here The original definition of JSON "falls outside the strict specification of an inductive type" because ...
• 273
5 votes

### Making a finite graph type in Lean - introduction rule

Here is how Lean defines undirected graphs (docs): ...
• 9,160
5 votes
Accepted

### Proving uniqueness of an instance of an indexed inductive type

Rergarding IDProp, this is the pattern-matching compilation of Coq at work. Basically, because you scrutinee has a type that can only correspond to the ...
• 5,530
5 votes
Accepted

### Uniqueness of proofs for inductively defined predicates

Here is a short proof: ...
• 5,530
4 votes
Accepted

### How to prove in Lean that sums are distributive?

Likely the most idiomatic option is the equation compiler: ...
• 1,445
4 votes

### Turning off some sProp checks

AFAIK there is no way to turn it off. It is also worth pointing out that the cost is greater than you expected. data A : Prop where a b : A It is possible to ...
• 4,025
4 votes
Accepted

### (In Lean), why cannot structural recursion on propositions be used?

TL;DR: There is no logical reason I see that Lean can't do this. It just seems like it is not implemented (and possibly it will be implemented in the future as this comment on Zulip suggests). ...
• 9,160
4 votes

### Inductive vs. recursive definitions

Let me just mention a third possibility which is sometimes called "small inversion". This is some kind of middle ground between the two possibilities you present, which gives you some of the ...
• 5,530
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 ...
• 5,530
4 votes

### Formalizing "finite or infinite" in Coq

Since the error you encountered is that you can't deconstruct a proof term whose type's type is Prop to construct the value whose type's type is ...
• 2,032
3 votes
Accepted

### Coq Induction on Hypothesis destroys the Hypothesis

The induction tactic tends to forget about the values of concrete arguments (e.g., nil on ...
3 votes

### Pragmatic encodings of inductive inductive types

To complement András' answer, and especially if you want to stay in Coq, you can also define such an internal universe using indexed inductive types only. Basically, you replace the definitions of ...
• 5,530
3 votes

### Turning off some sProp checks

In Coq, you can probably hack your way around by unsetting the guard condition and writing a fixpoint that is "semantically" guarded but not syntactically so. Something along the lines of ...
• 2,336
3 votes

### Defining Lists and Prove Associativity of Append

Here's a little list module written in Adga. To do this we are going to need cong -rule, and it resides in PropositionalEquality -module. ...
• 731

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