Skip to main content
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 ...
András Kovács's user avatar
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 ...
pigworker's user avatar
  • 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 ...
Dan Doel's user avatar
  • 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 ...
Li-yao Xia's user avatar
  • 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: ...
András Kovács's user avatar
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 ...
Michael Norrish's user avatar
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 ...
András Kovács's user avatar
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 <...
gallais's user avatar
  • 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 ...
Dan Doel's user avatar
  • 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 ...
Andrej Bauer's user avatar
  • 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 ...
Pierre Courtieu's user avatar
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 ...
Jason Gross's user avatar
  • 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 ...
András Kovács's user avatar
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 ...
gallais's user avatar
  • 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: ...
gallais's user avatar
  • 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 &...
Meven Lennon-Bertrand's user avatar
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 ...
Felipe's user avatar
  • 273
5 votes

Making a finite graph type in Lean - introduction rule

Here is how Lean defines undirected graphs (docs): ...
Jason Rute's user avatar
  • 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 ...
Meven Lennon-Bertrand's user avatar
5 votes
Accepted

Uniqueness of proofs for inductively defined predicates

Here is a short proof: ...
Meven Lennon-Bertrand's user avatar
4 votes
Accepted

How to prove in Lean that sums are distributive?

Likely the most idiomatic option is the equation compiler: ...
It'sNotALie.'s user avatar
  • 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 ...
Trebor's user avatar
  • 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). ...
Jason Rute's user avatar
  • 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 ...
Meven Lennon-Bertrand's user avatar
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
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 ...
Li-yao Xia's user avatar
  • 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 ...
Joshua Gancher's user avatar
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 ...
Meven Lennon-Bertrand's user avatar
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 ...
Pierre-Marie Pédrot's user avatar
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. ...
Cheery's user avatar
  • 731

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