General Induction Principle

Question

Let us suppose that we want to provide for each inductive type an axiom describing the associated elimination/induction principle. For example, given a definition for the naturals:

inductive nat : Prop ≝
  O : nat
| S : nat → nat.

We may provide for them the following definition of an elimination function:

$\texttt{let rec nat_ind(x) := }\\ \quad\forall Q:nat\to Prop. \\ \quad\forall C_1: (Q\; O). \\ \quad\forall C_2: (\forall x:nat. Q x \to Q (S x).\\ \quad\quad (\texttt{x}\equiv O\Rightarrow C_1) \\ \quad\quad \vee (\exists y:nat. x\equiv S y \Rightarrow \Big(C_2\; y\; (\texttt{nat_ind(}y\texttt{)}\;Q\;C_1\;C_2)\Big) $

Can this formulation be trivially extended for each constructor by simply adding a $C_i$ for an additional inductive case? If not, where can I look for a general definition of the elimination axiom that can be applied to any inductive type expressible ine a CoC/CIC dependent type system extending $\lambda Pw$, from Falsehood to Leibniz Equality? I.e., how does a theorem prover generates the elimination for inductive types?

Answer 1

Can this formulation be trivially extended for each constructor by simply adding a Ci for an additional inductive case?

Yes. I can't provide a general nor a technical answer, but a while ago I was trying to solve a similar problem and someone helped me by providing a visualization of the general procedure. This helped me a lot, so I'll reproduce it here in the case it helps you too.

Generating the elimination principle

Given an inductive type of the form (using Agda syntax):

data Foo : (index_0 : I_0) -> ... (index_N : I_N) -> Set where
  ctor_0 : (field_0 : F_0) -> ... (field_N : F_N) -> ret_0
  ...
  ctor_N : (field_0 : F_0) -> ... (field_N : F_N) -> ret_N

Its elimination is, generally, in that form:

let Foo_match = 

    -- Index arguments
    (index_0 : I_0) -> ...
    (index_N : I_N) ->

    -- Scrutinee
    (X : Foo index_0 ... index_n) ->

    -- Motive
    (P : 
      (index_0 : I_0) -> ...
      (index_n : I_N) ->
      (witness : Foo I_0 ... I_N) -> 
      Set) ->

    -- Constructor arguments
    (ctor_0 : 
        (field_0 : F_0) -> ...
        (field_N : F_N) -> 
        ret_0[Foo/P] (ctor_0 field_0 ... field_N)) ->
    (ctor_N :
        (field_0 : F_0) -> ...
        (field_N : F_N) -> 
        ret_N[Foo/P] (ctor_N field_0 ... field_N)) ->

    -- Result type
    P index_0 ... index_N X

Where [Foo/P] means we replace the constructor type by the variable P in ret_N.

Example

If our type is:

data Vect : (A : Set) -> (n : Nat) -> Set where
  cons : (A : Set) -> (n : Nat) -> (x : A) -> (xs : Vect A n) -> Vect A (succ n)
  nil  : (A : Set)                                            -> Vect A zero

Then we get:

let Vect_match =

    -- Index arguments
    (A : Set) -> ...
    (n : Nat) ->

    -- Scrutinee
    (X : Vect A n) ->

    -- Motive
    (P : (A : Set) -> (n : Nat) -> Vect A n -> Set) ->

    -- Constructor arguments
    (cons : 
        (A  : Set) ->
        (n  : Nat) -> 
        (x  : A) ->
        (xs : Vect A n) ->
        P A (succ n) (cons A n x xs)) ->
    (nil :
        P A zero nil) ->

    -- Result type
    P A n X

Note: I've not included parameters, but they're trivial. They work like indices, except they're not included on the constructors. I've also not included the inductive argument, so this is not actually the elimination principle, just total pattern-matching. You can get induction by applying Foo_match recursively to sub terms. Problem is I don't remember out of my head its shape, but someone is welcome to edit in.