The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Quick warning: it's great that you're interested in learning about Coq, 
but Software Foundations asks students not to share publicly any details 
of their solutions to its exercises, and I think your question already 
breaks that rule, since it includes details of a first attempt.  A 
public reply answering your question would go even further against the 
spirit of the rule.

On 07/09/2017 12:04 PM, Andreas Ames wrote:
> Hi all,
>
> I am ridiculously new to Coq, proof assistants in genral etc.  My
> primary interest is formal verification of real-world programs,
> currently with frama-c.  Therefore I am working through Software
> Foundations, which seems to be exactly what I need to learn something
> about Coq.
>
> Unfortunately I am currently stuck at the end of the second chapter
> about induction, where I would like to normalise the inductive type
> "bin":
>
> Inductive bin : Type :=
> | B0 : bin                      (* binary zero *)
> | BEV : bin -> bin              (* even binary: 2*x *)
> | BOD : bin -> bin.             (* odd binary: 2*x+1 *)
>
> The task is to make the notation of binary numbers unambiguous by
> providing a normalisation for such numbers, because "BEV B0 = B0".
>
> My idea to achieve this is to have a helper "normalize'" replacing a
> single "BEV B0" with "B0" and call that from "normalize" as often as
> needed.  If normalize' returns its argument, ecursion has to stop.
> Otherwise normalize has to recurse.
>
> Fixpoint normalize' (b : bin) : bin :=
>    match b with
>    | B0 => B0
>    | BEV B0 => B0
>    | BEV b' => BEV (normalize' b')
>    | BOD b' => BOD (normalize' b')
>    end.
>
> Unfortunately I am lacking the syntactic abilities to do so and the Coq
> reference of "match" is still beyond my reach.  I have tried things like
> the following to no avail:
>
> Fixpoint normalize (b : bin) : bin :=
>    match (normalize' b) with
>    | b => b
>    | _ => normalize _
>    end.
>
> Could you please provide me some hint how to write normalize in a way
> aceptable to Coq?
>
>
> TIA,
>
> Andreas