The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

Adam Chlipala's book has a trick that he calls the "Convoy pattern" in
the chapter `MoreDep`,

http://adam.chlipala.net/cpdt/html/MoreDep.html

It has been very useful (to me, at least) for tackling this general
problem of needing to carry around these extra proofs with you through
a dependent match.

Kris


On Sat, Feb 7, 2015 at 6:33 PM, Holden Lee 
<holdenlee AT alum.mit.edu>
 wrote:
> 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