The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sat, Dec 13, 2014 at 5:48 AM, Jiten Pathy <jpathy AT fssrv.net> wrote:

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

First off, I found it useful to insert "clear IHn'" between "rewrite <- IHn'" and the induction.  Otherwise, IHn' came along as a condition which couldn't be satisfied in the inductive hypothesis.

Then, a bit more simplification of S m' + S m' got it to the point where I could use the inductive hypothesis, then do another destruct of a term:

    rewrite <- plus_n_Sm. simpl.

    rewrite IHm'. destruct (un2bin m').

    SSCase "un2bin m' = 0".

    reflexivity.

    SSCase "un2bin m' = T b".

    reflexivity.

    SSCase "un2bin m' = T' b".

    reflexivity.

-- 

Daniel Schepler