Skip to main content

Questions tagged [inductive-type]

In terms of categorical semantics, an inductive type is a type whose interpretation is given by an initial algebra of an endofunctor. (from nLab)

Filter by
Sorted by
Tagged with
22 votes
0 answers
563 views

Categorical semantics of Agda

I would like to know the state of the art regarding the categorical semantics of the type theory implemented by Agda — or at least some approximation of that type theory that is amenable to ...
Mike Shulman's user avatar
  • 3,060
16 votes
3 answers
243 views

Expressivity of mutual/nested inductives vs. regular inductives

This question is from @TaliaRinger: Are mutually inductive types and plain old inductive types equally expressive? (Say, in Coq.) I assume yes, but the motive for induction will be a huge mess. But ...
ionchy's user avatar
  • 1,026
16 votes
1 answer
1k views

What are the complex induction patterns supported by Agda?

A question was recently asked on the Coq-club mailing list on Coq rejecting a nastily nested inductive type. We encountered a similar difficulty while trying to port code from Agda to Coq: Agda ...
Meven Lennon-Bertrand's user avatar
12 votes
1 answer
471 views

Is induction over mutually inductive coinductive types possible?

You can encode ordinals in Coq as Inductive ord := O | S (n: ord) | Lim (s: nat -> ord). Suppose you use the following encoding instead ...
Ms. Molly Stewart-Gallus's user avatar
12 votes
0 answers
167 views

Rules for mutual inductive/coinductive types

Some proof assistants, like Agda and maybe Coq, allow families of mutually defined types, or nested definitions of types, in which some are inductive and others are coinductive. I have no idea what ...
Mike Shulman's user avatar
  • 3,060
11 votes
2 answers
409 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 ...
L. F.'s user avatar
  • 213
10 votes
1 answer
585 views

What are well-founded inductive types?

W-types are said to be "a well-founded inductive type" that is parameterized over arities and constructors, similar to a "tree of possible constructions". On nlab, it is said that ...
ice1000's user avatar
  • 6,186
10 votes
2 answers
541 views

Replacing (strict) positivity with monotonicity on propositions

When defining an inductive type, there is a famous "positivity" restriction on the constructor types. For example, an inductive type $\mathsf D$ has constructor $\mathsf c : F(\mathsf D) \to ...
Trebor's user avatar
  • 3,967
10 votes
2 answers
213 views

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

We can derive eliminators (as functions) for inductive types and translate (structurally) recursive functions into invocations of eliminators. However, eliminators seem to be essentially recursive ...
ice1000's user avatar
  • 6,186
9 votes
2 answers
813 views

Construction of inductive types "the hard way"

Most theorem provers simply axiomize inductive types (or equivalently W types) in the abstract which is fine. But I'm curious about explicit constructions of inductive types within the theory. I ...
Ms. Molly Stewart-Gallus's user avatar
9 votes
1 answer
311 views

Strong eta-rules for functions on sum types

I am wondering whether a rule like the following is consistent with decidable conversion and type-checking for dependent type theory: $$ \frac{f\, g : (x:\mathsf{bool}) \to C~x\quad f~\mathsf{tt} \...
Mike Shulman's user avatar
  • 3,060
6 votes
4 answers
792 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 ...
8bc3 457f's user avatar
  • 224
6 votes
2 answers
265 views

How to prove in Lean that sums are distributive?

Assume we are given three types in Lean. constants A B C : Type There is a canonical map of the following form. ...
Nico's user avatar
  • 722
6 votes
1 answer
250 views

Parameterized Datatypes in a Universe à la Tarski?

I'm wondering, is there a way to make a Universe à la Tarski that models all of the types in an open type theory, where there can be user defined parameterized inductive types? For context, I'm trying ...
Joey Eremondi's user avatar
5 votes
1 answer
147 views

Explain all the arguments to this rec eliminator

I defined this inductive type for representing JSON elements ...
Felipe's user avatar
  • 273
5 votes
2 answers
120 views

Comparing indexed induction to recursion

Many indexed inductive families can be "equivalently" defined by recursion over their indices. For instance, the type family of vectors: ...
Mike Shulman's user avatar
  • 3,060
4 votes
2 answers
152 views

Pragmatic encodings of inductive inductive types

What's the most pragmatic encoding for inductive-inductive types such as for a universe of types? In pseudo Coq syntax. ...
Ms. Molly Stewart-Gallus's user avatar
4 votes
2 answers
179 views

Turning off some sProp checks

In Definitional Proof Irrelevance Without K, inductives in sProp need to satisfy three conditions to allow large elimination: (1) Every non-forced argument must be in sProp. (2) The return types of ...
ionchy's user avatar
  • 1,026
4 votes
1 answer
209 views

Making a finite graph type in Lean - introduction rule

I'm making a finite directed graph type in Lean. I know type theory from an abstract point of view, but I'm struggling to find the way Lean would produce a type playing the role of a "finite set&...
Ronald J. Zallman's user avatar
4 votes
1 answer
176 views

Co-induction principle

It's known that Nat-ind = Nat-rec ⨯ Nat-initiality Has someone figured out how to define a suitable Conat-coind such that ...
Russoul's user avatar
  • 345
3 votes
1 answer
222 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 ...
Ms. Molly Stewart-Gallus's user avatar
3 votes
1 answer
115 views

Can you remove strict positivity from mere propositions?

You can encode induction impredicatively. Some minimalist theories dispense entirely with inductive/coinductive types for proof irrelevant impredicative sorts. But in a practical theorem prover it's ...
Ms. Molly Stewart-Gallus's user avatar
2 votes
4 answers
132 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 ...
Glyn Webster's user avatar
2 votes
1 answer
759 views

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

Update: this has been fixed and the fix is available in the latest nightly release of Lean 4. In Lean 4, structural recursion on functions on types is no issue. ...
Jozef Mikušinec's user avatar
2 votes
2 answers
208 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 ...
paulotorrens's user avatar
2 votes
1 answer
172 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: ...
Circuit Craft's user avatar
2 votes
1 answer
89 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 ...
asha soroushpoor's user avatar
2 votes
1 answer
174 views

Defining Lists and Prove Associativity of Append [closed]

When I saw this question asking what is the "Hello, World!" for proof assistants I immediately thought of that exercise. Not a long time after this answer by Couchy was proposed. Therefore, ...
Wno-all's user avatar
  • 1,108
2 votes
0 answers
61 views

Elimination rules of inductive types

Why does the elimination rule of inductive types sometimes allow the target type to depend on the inductive type and sometimes not? I am confused by that. Is it correct that it makes no difference in ...
Nico's user avatar
  • 722
1 vote
1 answer
92 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 ...
smithers's user avatar
1 vote
1 answer
107 views

Inductive types associated to instances of a structure in Lean

I am using the Lean computer proof assistant. I am using the combinatorial structure of a graph with an abelian operation on its edges as a learning example. In it I have a structure Graph. I want to ...
Ronald J. Zallman's user avatar
1 vote
0 answers
64 views

Heterogeneous lists, large indices

Recently I had cause to define a type of heterogeneous lists in Lean, and wrote ...
Brendan Murphy's user avatar
1 vote
0 answers
44 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(...
noCrayCray's user avatar
1 vote
0 answers
60 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 ...
Kyle Lin's user avatar
  • 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 ...
Kyle Lin's user avatar
  • 143
1 vote
0 answers
179 views

Descriptions of heterogenous datatypes

When attempting to describe the datatype as appearing in my previous question, using indexed descriptions in style of The Gentle Art of Levitation to describe this datatype (using Agda for examples): <...
Ilk's user avatar
  • 547
0 votes
1 answer
157 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: ...
Tiago Campos's user avatar
-2 votes
2 answers
114 views

Help with strong induction

I have the following definition of divisibility by 3. ...
deleted_user0972's user avatar