Definition Structure: It defines a type and its constructors simultaneously.
Example (Natural Numbers): Inductive nat : Set := | O : nat | S : nat -> nat.
Recursive References: Constructors can reference the type being defined (e.g., S takes nat as an argument).
Induction Principle Generation: The command automatically generates induction principles (nat_ind, nat_rect, etc.) based on the structure of the definition, allowing for proofs by induction.
Positivity Condition: To ensure soundness, constructors must satisfy a strict positivity condition, meaning the type being defined cannot appear on the left side of an arrow in the argument types of constructors.
Parameterized vs. Indexed: Inductive definitions can be parameterized (e.g., list A) or indexed (e.g., even : nat -> Prop).
Mutually Inductive Types: The with keyword allows for defining mutually recursive types (e.g., trees and forests).
Software Foundations
Software Foundations
+4
Related Commands
CoInductive: Used for infinite data structures (streams).
Variant: Similar to Inductive but does not allow recursive references.
Scheme: Used to generate advanced or specialized induction principles.
Fixpoint: Used to define functions that recurse over Inductive types.
Site Title 