Проблема с расширением определения из модульной системы Coq - PullRequest
Новая
       61

Проблема с расширением определения из модульной системы Coq

1 голос
/ 09 июля 2020

Я определил пару модулей в Coq для создания типа Byte из типа Bit, рекурсивно, как тройку пар. Но я столкнулся с проблемой, определяющей Numeral Notation для типа Byte.

Вот код: 

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! *)

Я получаю эту ошибку: 

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

который кажется не конкретным от c до Numeral Notation, а скорее более общей проблемой, связанной с тем, что Byte.of не может быть расширен. Может ли кто-нибудь пролить свет на то, что происходит, и есть ли способ обойти это, что, похоже, является ограничением?

Coq version 8.11.2

1 Ответ

3 голосов
/ 10 июля 2020

Когда вы пишете Module Byte: Numeric := Foo, вы говорите Coq стереть все определения из Foo и оставить только подпись Numeric. Это приводит к тому, что Byte.of теряет свое тело.

В вашем случае вы не хотите ограничивать содержимое Byte до Numeric, а только документировать, что оно совместимо с Numeric. Вы можете сделать это, используя Module Byte <: Numeric := Foo.

Кстати, вместо того, чтобы помещать эту документацию на Byte, вы могли бы вместо этого переместить его в ConcatNumeric: 

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