[TYPES] Implementing induction principles

[Dan Licata]

Hi Patty,

Here's an Agda development of the induction principle along the lines
you suggest:

 http://www.cs.cmu.edu/~drl/code/Ind.agda

Regarding your questions at the end, I think the reason that my
development works is that uniqueness of the iterator is (more or
less--see below) true up to propositional (but not definitional)
equality.

For example, if I defined induction more simply like this:

 natrec : (P : Nat -> Set) (base : (P Z)) (step : ((n : Nat) -> P n -> P (S n))) 
        -> (n : Nat) -> P n
 natrec P base step Z = base
 natrec P base step (S n) = step n (natrec P base step n)

then I can easily prove that any function that behaves like base on zero
and behaves like (step o itself) on successor behaves like
natrec(base,step) on all numbers:

 unique : (P : Nat -> Set) (base : (P Z)) (step : ((n : Nat) -> P n -> P (S n))) 
          (f : (n : Nat) -> P n)
          (id0 : Id (f Z) base) 
          (id1 : (n : Nat) -> Id (f (S n)) (step n (f n)))
          (n : Nat) -> Id (f n) (natrec P base step n)

(This doesn't prove that Id f (natrec P base step)---I don't think this
holds, because proposotional equality defined by Id does not treat
functions extensionally.)

Similarly, to develop 'ind' along the lines you suggested, you need to
prove the lemma that

 itlemma : (n : Nat) -> Id (fst (iterate n)) n

which you do by induction.  

-Dan

On Jun22, Patricia Johann wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 
> Dear Types,
> 
> I'm trying to implement the induction principle for the natural numbers.
> 
> Briefly, given P: Nat -> * and
> 
> u: P(0)
> v: forall n:Nat. Pn -> P(n+1)
> 
> I can bundle these together to form a 1+_-algebra on the type Sigma n:Nat. 
> P n, i.e., a function
> 
> my_algebra  : (1 + Sigma n:Nat. P n) -> Sigma n:Nat. P n
> my_algebra = [ (0,u), \(n,p) -> (n+1, v n p)]
> 
> Then I can write
> 
> ind P :: forall n:Nat. P n
> ind P n = p where (m,p) = iterate my_algebra n
> 
> To show that this is correct, I need to show that n=m. This is easily done 
> using the uniqueness of the iteration operator.
> 
> Here are my questions:
> 
> 1. Can I implement ind in a programming language, theorem prover or 
> intensional type theory where the uniqueness of the iteration operator is 
> not available? Maybe this can be done because I only need to know that 
> projection after a specific iterator is the identity. Or maybe there is a 
> different approach to implementing ind?
> 
> 2. Is there a programming language or theorem prover where the uniqueness 
> of the iteration operator can be used?
> 
> 3. Or are there theoretical reasons (perhaps due to undecidability of type 
> checking) why this is not possible?
> 
> Thanks very much in advance,
> -patty
>