The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

Hi Gert,

it should be certainly provable because it follows from the fact that
initiality implies the existence of a recursor and that initiality is
closed under isomorphism. Both are provable in type theory and do not
require the use of UIP. Hence it should be provable in coq and it should
not depend on the assumption that it equality is decidable.

I realize that my answer isn¹t very constructive :-)

Thorsten

On 17/12/2015 18:10, 
"coq-club-request AT inria.fr
 on behalf of Gert Smolka"
<coq-club-request AT inria.fr
 on behalf of 
smolka AT ps.uni-saarland.de>
 wrote:

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





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.