The Coq mailing list

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

Sorry for forgetting to add explanation. Here is some that may help in understanding the proof.

1) the lemma eq_rect2 is better known as "J rule" in intensional type theory. It is a fundamental induction principle for eliminating proofs of equality. Whenever rewrite fails, I try to manually invoke this J rule. It is particularly useful when a computation is stuck at a match on a proof of equality.

2) In the proof of R0, after the initial unfolding, one sees that the computation is stuck at something like:
`match p with ... eq_refl`.
This computation only proceeds when p is in normal form. Fortunately, this is exactly what the J rule provides. Informally, it says that to show a property about an arbitrary proof of equality, it suffices to show it for its normal form, which is eq_refl.
To apply the J rule (`eq_rect2`), often the most difficult task is to come up with its argument P. Generalizing over the equality proof `p` often results in an  ill  typed term. To make it we'll typed, I had to replace `A` with `A'`. The types of `A` and `A'` are not same. But I still have to remember that `A` and `A'` were the same. This is where the `eq_dep` relation comes handy. It can be used to assert equality on members of dependent types whose indices are not definitionally equal. So I add `eq_dep A A' ` as a hypothesis in my instantiation for P.
After invoking eq_rect2 as H and applying H, the proof p gets replaced by eq_refl, and the computation happily proceeds. Also, after applying H, the types of `A` and `A'` become definitionally equal. Because the equality in N is decidable, using a lemma in the library, one can show that `eq_dep A A'` implies `A=A'`.

--Abhishek
http://www.cs.cornell.edu/~aa755/

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