<blockquote>
  <p>Can this formulation be trivially extended for each constructor by simply adding a Ci for an additional inductive case?</p>
</blockquote>

<p>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.</p>

<h2>Generating the elimination principle</h2>

<p>Given an inductive type of the form (using Agda syntax):</p>

<pre><code>data Foo : (index_0 : I_0) -&gt; ... (index_N : I_N) -&gt; Set where
  ctor_0 : (field_0 : F_0) -&gt; ... (field_N : F_N) -&gt; ret_0
  ...
  ctor_N : (field_0 : F_0) -&gt; ... (field_N : F_N) -&gt; ret_N
</code></pre>

<p>Its elimination is, generally, in that form:</p>

<pre><code>let Foo_match = 

    -- Index arguments
    (index_0 : I_0) -&gt; ...
    (index_N : I_N) -&gt;

    -- Scrutinee
    (X : Foo index_0 ... index_n) -&gt;

    -- Motive
    (P : 
      (index_0 : I_0) -&gt; ...
      (index_n : I_N) -&gt;
      (witness : Foo I_0 ... I_N) -&gt; 
      Set) -&gt;

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

    -- Result type
    P index_0 ... index_N X
</code></pre>

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

<h2>Example</h2>

<p>If our type is:</p>

<pre><code>data Vect : (A : Set) -&gt; (n : Nat) -&gt; Set where
  cons : (A : Set) -&gt; (n : Nat) -&gt; (x : A) -&gt; (xs : Vect A n) -&gt; Vect A (succ n)
  nil  : (A : Set)                                            -&gt; Vect A zero
</code></pre>

<p>Then we get:</p>

<pre><code>let Vect_match =

    -- Index arguments
    (A : Set) -&gt; ...
    (n : Nat) -&gt;

    -- Scrutinee
    (X : Vect A n) -&gt;

    -- Motive
    (P : (A : Set) -&gt; (n : Nat) -&gt; Vect A n -&gt; Set) -&gt;

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

    -- Result type
    P A n X
</code></pre>

<p>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 <code>Foo_match</code> recursively to sub terms. Problem is I don't remember out of my head its shape, but someone is welcome to edit in.</p>

CC BY-SA 4.0
2018-11-23T22:53:03.180Z
Thanks. I also needed the inductive part, which is the tricky part to formulate. Plus, I was not considering whether predicate Q for the elimination  provides as an output another type for an output, which is mutually recursive with the first one (the output of the elimination is yet another inductive type which is mutually recursive with the other one). I think that Proof Assistants like Coq ore Matita extend Agda's elimination.
jackb
CC BY-SA 4.0
2018-11-23T22:46:23.343Z
2018-11-23T22:46:23.343Z
MaiaVictor
<p>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:</p>

<pre><code>inductive nat : Prop ≝
  O : nat
| S : nat → nat.
</code></pre>

<p>We may provide for them the following definition of an elimination function:</p>

<p><span class="math-container">$\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)
$</span></p>

<p>Can this formulation be trivially extended for each constructor by simply adding a <span class="math-container">$C_i$</span> 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 <span class="math-container">$\lambda Pw$</span>, from Falsehood to Leibniz Equality? I.e., how does a theorem prover generates the elimination for inductive types?</p>

<type-theory><dependent-type><automated-theorem-proving><type-inference>
General Induction Principle
jackb
# General Induction Principle

(Asked by: username_0 on 2018-11-22)

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?

**Tags:** type-theory, dependent-type, automated-theorem-proving, type-inference


---

## 1 answers

### Answer by username_1 on 2018-11-23. Score: 1 | Accepted answer

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.

> **Comments:**
> **username_0**: Thanks. I also needed the inductive part, which is the tricky part to formulate. Plus, I was not considering whether predicate Q for the elimination  provides as an output another type for an output, which is mutually recursive with the first one (the output of the elimination is yet another inductive type which is mutually recursive with the other one). I think that Proof Assistants like Coq ore Matita extend Agda's elimination.  

---

