Eugene Kirpichov (antilamer) wrote,
Eugene Kirpichov
antilamer

«Program Definition» в последних версиях Coq — это ацкая силища.

В двух словах, они позволяют писать сертифицированные программы как обычные, т.е. как будто бы доказательный компонент отсутствует (например, использовать {x:nat | even x} как будто это просто nat), а затем автоматически пытается решить все оставшиеся «обязательства»; те, что не решились — можно дорешать самому. Большинство простых случаев решается автоматически.
Продуктивность вырастает на порядок, уж не говоря вовсе о краткости и понятности кода.


Definition pos_nat := {x:nat | x > 0}.
(* Хинт: выполнять destruct над гипотезами типа pos_nat *)
Hint Extern 5 => match goal with | n:pos_nat |- _ => destruct n end.

Obligation Tactic := auto with arith.

(* Пример 1: Program Definition *)

Program Definition sum_pos : pos_nat -> pos_nat -> pos_nat := fun n1 n2 => n1 + n2.

(* Пример 2: явное определение *)

Definition sum_pos' : pos_nat -> pos_nat -> pos_nat.
  refine (fun p1 p2 => match p1,p2 with
  | exist n1 p1, exist n2 p2 => exist _ (n1+n2) _
  end); auto with arith.
Defined.

(* Пример 3: определение с помощью тактик *)

Definition sum_pos'' : pos_nat -> pos_nat -> pos_nat.
  intros [n1 pn1] [n2 pn2]; exists (n1+n2); auto with arith.
Defined.



Планируется поддержка импорта кода на Haskell, OCaml, Scheme.
Tags: programming
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 25 comments