The Coq mailing list

[Jiten Pathy <jpathy AT fssrv.net>]

Thanks Daniel for clear IHn'. I was actually confused because of the
IHn' suddenly came as a condition.

On Sat, Dec 13, 2014 at 8:25 AM, Daniel Schepler 
<dschepler AT gmail.com>
 wrote:
> 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
>