Inductively Defined Propositions

Inductive Type Definition

• Inductive nat is defined as:

  • zero

  • succ nat

• Introduces type nat with specific constructors.

• Elements are distinct and fully defined by constructors.

Set vs Prop vs Type

• Set: Default for data types (computational).

• Prop: For logical propositions.

• Type: When a compiler requires universe levels.

Inductive Syntax

• Defined as Inductive nat : Set := | zero : nat | succ : nat -> nat.
• Constructors map into the defined type.
• Allows for arbitrary arguments and GADTs.

Dependent Types Hierarchy

• Types and terms can depend on:
  • Terms (using λ-abstraction).
  • Types (via polymorphism).
  • Other terms (dependent types).
• Possible, but rare, for terms to depend on types.

Dependent Types Power

• Enable precise specifications (e.g., vectors with lengths in type).
• Very powerful, yet complex.
• Foundational in Rocq/Coq.

Inductive Type Properties

• Terms exist solely as themselves.
• Pairwise disjoint from other types.
• Defined exclusively by constructors.

Barendregt's λ-cube

• Framework classifying type systems by:
  • Terms depending on types (polymorphism).
  • Types depending on types (type operators).
  • Types depending on terms (dependent types).
• Rocq is positioned near the top.

GADTs (Generalized Algebraic Data Types)

• Haskell extension allowing constructors to return specific type instances.
• Rocq inductive types support similar functionality through dependent types.