The Coq mailing list

[Jiten Pathy <jpathy AT fssrv.net>]

Hello,
I just started learning Coq. And currently facing difficulty solving
the following theorem(bin_conv) using induction. Anybody could help me
out with this? I am having difficulty with the normalize fixpoint
where i am using recursive pattern matching.

Inductive bin : Type :=
    | O' : bin
    | T : bin -> bin
    | T' : bin -> bin.

Fixpoint normalize (b :bin) : bin :=
    match b with
    | O' => O'
    | T n' =>
            match normalize n' with
            | O' => O'
            | _ => T (normalize n')
            end
    | T' n' => T' (normalize n')
    end.

The full file to run with Coq.
https://gist.github.com/anonymous/082c9f17c3d9dc2b5263