Извлечение coq типа nat в какой тип ocaml, чтобы я мог иметь сертифицированную программу

Question

В Coq Извлечение из типа nat в int или же big_int не сертифицированы (они эффективны). Как в этих ссылках ниже:

http://coq.inria.fr/V8.3/stdlib/Coq.extraction.ExtrOcamlNatBigInt.html и

http://coq.inria.fr/distrib/8.3/stdlib/Coq.extraction.ExtrOcamlNatInt.html

Обе говорят, что: Отказ от ответственности: попытка получить эффективные сертифицированные программы путем извлечения nat в big_int - не обязательно хорошая идея. Смотрите комментарии в ExtrOcamlNatInt.v.

Если у меня есть coq типы: nat, Z, N, а также positive который ocaml типы я должен выбрать для извлечения типа, что я могу иметь сертифицированную (более безопасную) программу (я могу игнорировать эффективную)?

В настоящее время я решил извлечь все из них в int, А потом внутри ocaml int Я использовал Int64 взломать внутри (получить границу min_int а также max_int, если k < min_int затем min_int и в противном случае), для Z а также positive номер, который я проверяю: если (i:int) < 0 затем вернуть тип неотрицательный int, если i <= 0 тогда это типа positive

Answer 1

Если вы не заботитесь об эффективности, вы не должны пытаться привязать тип Coq к типу Ocaml, просто извлеките их как есть (индуктивные типы), и вы будете в безопасности. Однако, используя вычисления над nat (одинарные числа) будет очень медленно. Например:

Extraction nat.
(*
  type nat =
   | O
   | S of nat
 *)

экстрагирование Z будет немного более многословным.