The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

 I don't know it it answers really to your original question, but I 
found it simpler
to consider separately your type Bounded from the Prefix computation. I 
suppose that
the code can be much simplified using Program Fixpoint, but I didn't try 
it yet.

Regards,

Pierre




Samuel E. Moelius III a écrit :
> Adam,
>
> For the meantime, I would like to let my original question stand.  

Require Import Bvector.
Require Import Program.

Definition prefix'(A:Type) : forall (m : nat) (i : nat), i<= m ->
        vector A m -> vector A i. 

induction m.
destruct i.
constructor.
intros;elimtype False.
inversion H.
intro i; case i.
constructor.
intros n H X; refine (Vcons _ (Vhead _ _ X) _ (IHm n _ (Vtail _ _ X))).
auto with arith.
Defined.


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


 
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
.


Lemma Bounded_lt : forall n (i:Bounded n), Bounded_to_nat n i < n.
induction i;simpl;auto with arith.
Qed.


Implicit Arguments Succ [n].
Implicit Arguments Zero [n]. 
Implicit Arguments Bounded_to_nat [n]. 

 Definition prefix(A:Type) : forall (m : nat) (i : Bounded (S m)) ,
        vector A m -> vector A (Bounded_to_nat i). 
Proof.
 intros A m i v.
 refine  (prefix' A m (Bounded_to_nat i) _ v).
 generalize (Bounded_lt _ i); auto with arith. 
 Defined.

 


Implicit Arguments Vcons [A n].
Implicit Arguments prefix [A m].
Definition v := Vcons 4 (Vcons 7 (Vcons 8 (Vnil _))).



Eval compute in (prefix Zero v). 

Eval compute in (prefix  (Succ Zero) v). 

Eval compute in (prefix  (Succ(Succ Zero)) v). 

Eval compute in (prefix  (Succ(Succ(Succ Zero))) v).


(*

Eval compute in (prefix  (Succ (Succ(Succ(Succ Zero)))) v).

Toplevel input, characters 110-111:
Error: The term "v" has type "vector nat 3" while it is expected to have type
 "vector ?122 (S (S (S (S ?128))))".
*)