The Coq mailing list

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

Dear Abhishek, many thanks for your impressive proof.  I’ll try to digest and 
do the proof for S’.  Gert

> On 17 Dec 2015, at 22:07, Abhishek Anand 
> <abhishek.anand.iitg AT gmail.com>
>  wrote:
> 
> I have reduced your proof to showing that equality on N is decidable, which 
> should be easy.
> 
> Require Import  Coq.Unicode.Utf8.
> Require Import Coq.Logic.EqdepFacts.
> Require Import Coq.Logic.Eqdep_dec.
> 
> Lemma eq_rect2
>      : forall (T : Type) (x : T) (P : ∀ t : T, eq x t → Type),
>        P x (eq_refl x) → ∀ (y : T) (e : eq x y), P y e.
> Proof.
>   intros.
>   rewrite <-e. assumption.
> Qed.
> 
> Lemma NDec: ∀ x y : N, {x = y} + {x ≠ y}.
> Admitted.
> 
>   Lemma R0 f A F :
>     R f A F O' = A.
>   Proof.
>     unfold R, fEP, eq_rect.
>     remember 
>     (fun (z:N) (p:(E (P O'))=z) => forall A',
>     eq_dep _ _ _ A _ A' ->
>     match p in (_ = y) return (f y) with
>   | eq_refl =>
>     nat_rect (fun n : nat => f (E n)) A
>       (fun (n : nat) (B : f (E n)) => F (E n) B) 
>       (P O')
> end = A'
> ) as PP.
>   pose proof (fun pp => @eq_rect2 N  _ PP pp) as H.
>   subst PP.
>   apply H; auto.
>   rewrite PO'. simpl.
>   intro.  apply eq_dep_eq_dec.
>   exact NDec.
> Qed.
> 
> Print Assumptions R0.
> 
> (*
> Section Variables: 
> ....
> Axioms:
> NDec : ∀ x y : N, {x = y} + {x ≠ y}
> *)
> 
> 
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
> 
> On Thu, Dec 17, 2015 at 1:10 PM, Gert Smolka 
> <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.
>