The Coq mailing list

[Holden Lee <holdenlee AT alum.mit.edu>]

I define "strong" recursion for natural numbers:

Definition strong_rec (P: nat -> Type) : 

  (forall n: nat, 

    (forall m: nat, (m<n) -> P m) -> P n) -> (forall m: nat, P m).

Now I try to define a function to convert from unary to binary: 

Definition nat_to_bin : (nat -> bin) :=

strong_rec (fun _ => bin) (fun n => (fun F => 

  match n with 

    | O => O'

    | S n' => 

      match (div2rem n) with

        | (x, O) => T (F (fst (div2rem (S n'))) (div2smaller n'))

        | (x, S y) => ST (F (fst (div2rem (S n'))) (div2smaller n'))

      end

  end)).

Basically I define nat_to_bin n in terms of nat_to_bin (n/2)

Here div2smaller n' is a proof that (S n')/2<S n' so that we can use strong_rec.

Lemma div2smaller:

  forall n, fst (div2rem (S n))<S n.

However this gives the error

Error:

In environment

n : nat

F : forall m : nat, m < n -> bin

n' : nat

x : nat

n0 : nat

The term "div2smaller n'" has type "fst (div2rem (S n')) < S n'"

 while it is expected to have type "fst (div2rem (S n')) < n".

How can I tell Coq that n=S n'?

For reference here is the definition for bin:

Inductive bin : Type :=

   | O' : bin

   | T : bin -> bin (*twice*)

   | ST: bin -> bin. (*one more than twice*)

Thanks,

Holden