The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2015-02-08 0:33 GMT+01:00 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'?

​That is dependent pattern matching.

First of all, generalize over n: the type of "F" probably contains references to "n" and you want it to either depend on "O", or depend on "S n'"

The default behavior is:​

​

​

Definition nat_to_bin : (nat -> bin) :=

strong_rec (fun _

​​

=> bin) (fun n => 

  match n

 ​

with 

    | O =>

​fun (F : forall m, (m<O) 

->

​ bin​

) 

​

=>

 ​

O'

    | S n' =>

​

      ​

​fun (F : forall m, (m<S n') 

->

​ bin​

) 

​

=>

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

​

At this point, it is possible that Coq complains about branches having different types. If this is the case, simply use some extended match construction.

​​

​

Definition nat_to_bin : (nat -> bin) :=

strong_rec (fun _ 

​​

=> bin) (fun n => 

  match n

 ​as x return (forall m, m<x -> bin) -> bin 

with 

    | O => 

​fun (F : forall m, (m<O) 

->

​ bin​

) 

​

=>

 ​

O'

    | S n' =>

​

      ​

​fun (F : forall m, (m<S n') 

->

​ bin​

) 

​

=>

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

​

​With that Coq has enough type information.​

 

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