The Coq mailing list

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

Indeed, that also occurred to me after I sent my post.

Thorsten

From: <coq-club-request AT inria.fr> on behalf of Jason Gross <jasongross9 AT gmail.com>
Reply-To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Friday, 18 December 2015 16:57
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Dependent Type Problem

You should be able to do it for other (non-hset) types by "adjusting" the isomorphism into a good notion of equivalence, and using that instead, right?

-Jason

On Dec 18, 2015 11:02 AM, "Thorsten Altenkirch" <Thorsten.Altenkirch AT nottingham.ac.uk> wrote:

Actually, you do need that Nat is a set otherwise you would need to add a
condition to the isomorphism.

Hence Abhishek is right to use decidability - I just realized this.

If we assume extensionality it will also hold for types whose equality is
stable, eg datatypes with infinitary constructors.

Thorsten

On 18/12/2015 15:18, "Altenkirch Thorsten"
<psztxa AT exmail.nottingham.ac.uk> wrote:

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

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.