The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

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.