Специализация аргумента модуля в Coq - PullRequest
Новая
       6

Специализация аргумента модуля в Coq

0 голосов
/ 15 февраля 2019

У меня есть модуль, и мне нужно специализировать один из его аргументов.Я хочу использовать натуральные числа вместо произвольного UsualDecidableTypeFull.Как я могу получить такое поведение в Coq?

Я определил некоторый модуль: 

Module PRO2PRE_mod
(SetVars FuncSymb PredSymb PropSymb: UsualDecidableTypeFull).
(* ... *)
End PRO2PRE_mod.

Затем я специализировал последний из аргументов PropSymb. 

Require Import Arith.PeanoNat.
Module m2 : UsualDecidableTypeFull.
Definition t:=nat.
Definition eq := @eq nat.
Definition eq_refl:=@eq_refl nat.
Definition eq_sym:=@eq_sym nat.
Definition eq_trans:=@eq_trans nat.
Definition eq_equiv:Equivalence eq := Nat.eq_equiv.
Definition eq_dec := Nat.eq_dec.
Definition eqb:=Nat.eqb.
Definition eqb_eq:=Nat.eqb_eq.
End m2.

Этот модульнужна специализация PropVars: 

Module SWAP_mod
(SetVars FuncSymb PredSymb : UsualDecidableTypeFull).

Module PRE := PRO2PRE_mod SetVars FuncSymb PredSymb m2.
Import PRE.

Theorem test : m2.t.
try exact 0. (* ERROR HERE! *)
Abort.
End SWAP_mod.

Как использовать теоремы о натуральных числах внутри последнего модуля?(Я думаю, что не понимаю что-то об использовании модулей ... Может быть, нам нужно как-то привести тип 'm2.t' к типу 'nat'?)

1 Ответ

0 голосов
/ 15 февраля 2019

Действительно, использование : UsualDecidableTypeFull в определении m2 полностью скрывает детали реализации m2.Снаружи m2.t - неизвестный тип.

Иногда это именно то, что вы хотите.Например, вы можете абстрагироваться от типа, определенного в модуле, чтобы пользователи не могли манипулировать значениями этого типа без использования функций, которые вы им дали в модуле.Таким образом, вы можете быть уверены, что они не сломают некоторые инварианты.

Однако, в вашем случае вы должны помнить, что m2.t на самом деле nat, у вас есть по крайней мере эти две опции:

  • Сделайте интерфейс прозрачным с помощью Module m2 <: UsualDecidableTypeFull.При использовании этого Coq просто проверяет соответствие определения модуля подписи, но не скрывает содержимое модуля.

  • Если вы все еще хотите скрыть часть модуляВы также можете использовать 

    Module m2 : UsualDecidableTypeFull with Definition t := nat.

    В этом случае извне m2.t известно как nat, но другие поля m замаскированы.Например, тело m2.eqb скрыто.

...