The Coq mailing list

["Samuel E. Moelius III" <moelius AT cis.udel.edu>]

In the code below, I would like that when I enter

    Eval compute in (test (Zero 0)).

I get back

    Vnil nat

As things currently stand, this is not the case.

Question 1: Am I correct that this is due to the use of opaque constants 
such as eq_add_S and UIP_refl?

Question 2: Were I to redefine these constants so that they were 
transparent, and then use the new constants, I still would not get what 
I want because UIP_refl is proven using the axiom eq_rect_eq, correct?

Question 3: Is there a way to get what I want using Bounded_elim as I 
have defined it, or am I on the wrong track?

Any help would be greatly appreciated.  Thanks in advance.

Sam

(*====================================================================*)

Require Import Bvector.
Require Import Eqdep.

Inductive Bounded : nat -> Set :=
    |   Zero : forall (n : nat), Bounded (S n)
    |   Succ : forall (n : nat), Bounded n -> Bounded (S n)
.

Definition Bounded_elim : forall (m : nat) (i : Bounded (S m))
        (A : Type),
    (forall (n : nat) (p : S n = S m),
        i = eq_rect (S n) Bounded (Zero n) (S m) p -> A) ->
    (forall (n : nat) (p : S n = S m) (j : Bounded n),
        i = eq_rect (S n) Bounded (Succ n j) (S m) p -> A) -> A.
    intros.
    remember i as j.
    destruct i.
    (* Case "Zero" *)
        apply (X n (refl_equal (S n))).
        simpl.
        apply Heqj.
    (* Case "Succ ..." *)
        apply (X0 n (refl_equal (S n)) i).
        simpl.
        apply Heqj.
Defined.

Fixpoint Bounded_to_nat (n : nat) (i : Bounded n) {struct i} : nat :=
    match i with
    |   Zero _     => 0
    |   Succ n0 i0 => S (Bounded_to_nat n0 i0)
    end
.

Definition test : forall (i : Bounded 1),
        vector nat (Bounded_to_nat 1 i).
    intros.
    apply (Bounded_elim 0 i).
    intros.
    rewrite H; clear H.
    assert (n = 0). apply (eq_add_S n 0 p).
    revert p. rewrite H. intro.
    assert (p = refl_equal 1).
    apply (UIP_refl nat 1).
    rewrite H0.
    simpl.
    apply (Vnil nat).
    intros.
    rewrite H; clear H.
    assert (n = 0). apply (eq_add_S n 0 p).
    revert j p.
    rewrite H.
    intro.
    inversion j.
Defined.

Eval compute in (test (Zero 0)).