The Coq mailing list

[rouxcody AT loria.fr]

Hello coq cubbers!

  I am confused. In the following code, i have defined a fix point  
induction principle for a type of dependent natural numbers (with size  
information), and have used this to define a function, namely the  
fibbonaci sequence (function). I then evaluate my function on the  
number 5. Whereas i naively expected the number 8, the result was not  
a term of type nat in normal form (in the empty context). I thought  
maybe some opaque definitions were blocking the reduction, but this  
should not be possible when eliminating towards type nat. Right? What  
is happening here? Otherwise I completely agree that programming by  
proof as I have done is quite disadvisable.

Thanks a lot,

Cody




Code begins here:


Set Implicit Arguments.
Require Export Arith.

(*dependently typed natural numbers with size information*)
Record Dnat (n:nat):Type:=mkdnat{
val:nat;
borne:val<=n}.


(*in this section we define the well founded functionnal we
want to use fixpoint on*)
Section Addbis.

Variable n:nat.

Variable fib: forall m,(m<n)->Dnat m->nat.

Definition Fib: Dnat n->nat.
intro m.
elim m; clear m; intro m.
refine (match m as u return u<=n -> nat with
          |0 => fun h:_=>1
          |1 => fun h:_=>1
          |S(S m')=>fun h:_=>
            (@fib (S m') _ (@mkdnat _ (S m') _))
            +(@fib m' _ (@mkdnat _ m' _))
         end); auto with arith.
Defined.


End Addbis.


(*usefull lemma for well founded induction*)
Lemma le_le_eq_dec:forall i j, i<S j->{i<j}+{i=j}.
intros i j.
generalize i.
induction j; intros.
right.
unfold lt in H.
apply le_S_n in H.
auto with arith.
generalize H.
clear H.
case i0;intros; [left; auto with arith|].
assert (n<S j) by auto with arith.
apply (IHj n) in H0.
elim H0; auto with arith.
Defined.

(*well founded induction (eliminates towards Type)*)
Definition wf_fix:forall C,
  (forall n, (forall m,m<n->Dnat m->C)->(Dnat n->C)) ->
forall n,Dnat n->C.
Proof.
intros C H n.
cut ((forall m,m<n->Dnat m->C)*(Dnat n ->C)).
intros.
destruct X.
auto.
induction n; split; intros.
assert (h1: ~ m < 0) by apply lt_n_O;
 elim h1; assumption.
apply (H 0).
intros.
assert (h1: ~ m < 0) by apply lt_n_O;
 elim h1; assumption.
auto.
destruct IHn.
assert ({m<n}+{m=n}) by (apply le_le_eq_dec; auto).
elim H2; intros.
apply (c m); auto.
subst m; auto.
destruct IHn.
apply (H (S n));[|auto].
intros m h.
assert ({m<n}+{m=n}) by (apply le_le_eq_dec; auto).
destruct H1.
apply c; auto with arith.
subst m; auto.
Defined.

(*the dependent number five*)
Definition D5:Dnat 5.
Proof.
apply (@mkdnat 5 5).
auto with arith.
Defined.


(*of type nat!*)
Check (wf_fix Fib D5).

(*should be a S(...(S 0)..) (empty context) right?*)
Eval compute in (wf_fix Fib D5).

(*this works though...*)
Fixpoint fibo (n:nat):=
  match n with
    |0=>1
    |S m=> match m with
             |0=>1
             |S k=>(fibo m)+(fibo k)
           end
end.

Eval vm_compute in (fibo 5).