Issue on definition expansion from Coq module system

Question

I have defined a couple of modules in Coq to build a Byte type from a Bit type, recursively, as a three of pairs. But I hit an issue defining a Numeral Notation for the Byte type.

Here is the code:

Require Import ZArith.

(* bit sequence abstracted interface *)
Module Type Numeric.
    Parameter T: Set.
    Parameter MAX: T.                          (* sequence of 1...1 = 2^n - 1 *)
    Parameter to: T -> Z.                      (* conversion to Z *)
    Parameter of: Z -> option T.               (* conversion from Z *)
End Numeric.

(* a single bit *)
Module Bit.
    Inductive bit: Set := bit0 | bit1.
    Definition T: Set := bit.
    Definition MAX: T := bit1.
    Definition to (i: T): Z :=
        match i with
        | bit0 => 0%Z
        | bit1 => 1%Z
        end.
    Definition of (n: Z): option T :=
        match n with
        | Z0 => Some bit0
        | Zpos xH => Some bit1
        | _ => None
        end.
End Bit.

(* concatenation of two bit sequences *)
Module ConcatNumeric (m1 m2: Numeric).
    Definition T: Set := m1.T * m2.T.
    Definition MAX: T := (m1.MAX, m2.MAX).
    Definition to (x: T): Z :=
        let (x1, x2) := x in
        let i1 := m1.to x1 in
        let i2 := m2.to x2 in
        let base := (m2.to m2.MAX + 1)%Z in
        (i1 * base + i2)%Z.
    Definition of (i: Z): option T :=
        let base := (m2.to m2.MAX + 1)%Z in
        let i2 := (i mod base)%Z in
        let i1 := (i / base)%Z in
        match m1.of i1, m2.of i2 with
        | Some z1, Some z2 => Some (z1, z2)
        | _, _ => None
        end.
End ConcatNumeric.

(* hierarchy defining a byte from bits *)
Module Crumb: Numeric := ConcatNumeric Bit Bit.
Module Nibble: Numeric := ConcatNumeric Crumb Crumb.
Module Byte: Numeric := ConcatNumeric Nibble Nibble.

(* boxing Byte.T in an inductive type to make Numeral Notation happy *)
Inductive u8: Set := u8_box (x: Byte.T).
Definition u8_unbox := fun x => match x with u8_box x => x end.
Definition u8_of := fun i => option_map u8_box (Byte.of i).
Definition u8_to := fun x => Byte.to (u8_unbox x).

(* defines the scope and the Numeral Notation *)
Declare Scope u8_scope.
Delimit Scope u8_scope with u8.
Numeral Notation u8 u8_of u8_to: u8_scope.

(* testing the code *)    
Open Scope u8_scope.
Definition x: u8 := 1.     (* error here! *)

I am getting this error:

Error: Unexpected non-option term
match Byte.of 1 with
| Some a => Some (u8_box a)
| None => None
end while parsing a numeral notation.

which seems not specific to Numeral Notation but rather a more general issue related to the fact that Byte.of cannot be expanded. Can someone shed some light on what is going on, and if there a way to work around this, which appears to be a limitation?

Coq version 8.11.2

Answer 1

When you write Module Byte: Numeric := Foo, you tell Coq to erase all the definitions from Foo and to keep only the signature of Numeric. This causes Byte.of to lose its body.

In your case, you do not want to restrict the content of Byte to Numeric, but only to document that it is compatible with Numeric. You can do so using Module Byte <: Numeric := Foo.

By the way, instead of putting this documentation on Byte, you could instead move it to ConcatNumeric:

Module ConcatNumeric (m1 m2: Numeric) <: Numeric.
  ...
End ConcatNumeric.
Module Byte := ConcatNumeric Nibble Nibble.