The Coq mailing list

[Andreas Ames <andreas.ames AT gmx.de>]

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

-- 
"I don't want to belong to any club that will have me as a member." G. Marx