Проверить теоремы coq в скрипте сборки?

Я использую coq для изучения метатеории языка программирования.

Составление и проверка теорем в интерактивном режиме в среде IDE — это хорошо, но мне нужно автоматизировать (повторную) проверку. Я вижу справочные страницы, но нигде не вижу описанного варианта использования.

Как включить проверку coq в сценарий сборки?


command-line automation coq
person phs    schedule 10.05.2014    source источник
comment
Вы изучали coqc и coqchk?   -  person gallais    schedule 10.05.2014
comment
Я их вижу, но простого примера, показывающего их совместное использование, не было. Я также не беспокоюсь (пока) о производительности проверки, поскольку теория все еще мала; интерпретированное решение подходит лучше на данный момент.   -  person phs    schedule 10.05.2014

Ответы (1)


arrow_upward
1
arrow_downward

Если у нас есть это metatheory/hello_world.v:

$ cat metatheory/hello_world.v
Theorem hello_world : forall a b:Prop, a /\ b -> b /\ a.
intros a b H.
split.
destruct H as [H1 H2].
exact H1. (* A bug: We actually need H2 here. *)
intuition.

Затем мы можем увидеть ошибку (с ошибкой кода выхода) с:

$ coqtop -batch -silent -l metatheory/hello_world.v
Error while reading metatheory/hello_world.v:
File "/vagrant/metatheory/hello_world.v", line 5, characters 6-8:
Error: In environment
a : Prop
b : Prop
H1 : a
H2 : b
The term "H1" has type "a" while it is expected to have type
"b".

Если мы решим проблему:

$ coqtop -batch -silent -l metatheory/hello_world.v

..с успешным кодом выхода.

person phs    schedule 10.05.2014