The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

Suppose we have an isomorphism between nat and a type N with O' and S'.  I 
would expect that the recursor for nat can be pulled over to N.  In fact, it 
is not difficult to define a function

R : forall f : N -> Type, f O' -> (forall x, f x -> f (S' x)) -> forall x, f 
x.

However, I cannot show the equation

R f A F O' = A

because a rewrite violates dependent type constraints.

I would much appreciate help from a dependent type expert.  Do you think it 
is possible to define R in such a way that the equation can be shown?  Or is 
it known that the equations of dependent recursors cannot be pulled over?  
Coq code is below.

Gert

PS.  It is not difficult to pull over a simply typed recursor (primitive 
recursion) including the equations.

Section N.
  Variables (N : Type) (O' : N) (S' : N -> N).

  Fixpoint E (n : nat) : N :=
    match n with
      | O => O'
      | S n' => S' (E n')
    end.
  
  Variables (P : N -> nat).
  Variable EP : forall x, E (P x) = x.
  Variable PE : forall n, P (E n) = n.

  Lemma PO' :
    P O' = 0.
  Proof.
    now rewrite <- (PE 0).
  Qed.

  Lemma fEP (f : N -> Type) x :
    f (E (P x)) ->  f x.
  Proof.
    intros A. now rewrite <- EP.
  Defined.
  
  Definition R (f : N -> Type) (A : f O') (F: forall x, f x -> f (S' x)) x : 
f x
    := fEP f x (nat_rect (fun n => f (E n)) A (fun n B => F (E n) B) (P x)).
  
  Lemma R0 f A F :
    R f A F O' = A.
  Proof.
    unfold R. pattern (P O’).  FAILS
  
End N.