В этой задаче мы реализуем алгоритм Евклида для нахождения наибольшего общего делителя (GCD) в типе Z. В файле EuclidZ_2025_task.v приведены подсказки — формулировки основных лемм и определений.
Определяются понятия делимости и свойства "быть наибольшим общим делителем":
Definition div (x y : Z) := exists z : Z, x = y*z. Definition isGCD (a b d : Z) := div a d /\ div b d /\ forall d2 : Z, (div a d2 /\ div b d2 -> div d d2).Далее формулируется сама задача — построить функцию из a и b в d с условием isGCD a b d:
Definition GCD : forall a b : Z, { d : Z | isGCD a b d }.
Это "определение" GCD нужно доказать как теорему средствами Rocq. Фактически, конструктивно доказывается утверждение ∀a,b ∃d isGCD(a,b,d), однако делается это в универсуме Set, а не Prop. После завершения доказательства оказывается определён терм GCD в типе-зависимом произведении forall a b : Z, { d : Z | isGCD a b d }. В частности, внутри этого терма содержится искомая функция из a, b в d, т.е. код алгоритма, вычисляющего GCD. Эту функцию мы будем извлекать стандартными средствами Rocq, которые удаляют всё, чьи типы лежат в универсуме Prop (доказательства), оставляя только то, что лежит в Set (вычисления).
Прежде, чем извлекать код, однако, мы преобразуем тип входных и выходных данных из внутреннего типа Z в машинный тип int. Для этого подключим модуль Coq.extraction.ExtrOcamlIntConv, в котором определены преобразователи z_of_int и int_of_z. К сожалению, равенство z_of_int (int_of_z x) = x в общем случае неверно: число x может выйти за предельный размер типа int и будет "обрезано". Мы постулируем это равенство при условии, что наше число достаточно маленькое (а именно, не больше некоторого числа вида z_of_int n, заведомо не превосходящего предельный размер для int:
Axiom zz' : forall b : Z, forall n : int, Z.abs b <= Z.abs (z_of_int n) -> z_of_int (int_of_z b) = b.(Отметим, что доказать zz' средствами Rocq невозможно, поскольку это утверждение оперирует внешним по отношению к Rocq типом int.) При помощи zz' сформулируем и докажем определение GCD в типе int:
Definition GCDint : forall a b : int,
{ d : int | isGCD (z_of_int a) (z_of_int b) (z_of_int d) }.
Наконец, мы готовы извлечь программный код:
Extraction "/tmp/gcd.ml" GCDint.В файле gcd.ml содержится код вычисления GCD на языке OCaml. Его можно запустить в интерпретаторе:
$ ocaml OCaml version 4.14.1 Enter #help;; for help. # #use "/tmp/gcd.ml";; [....] # gCDint 36 24;; - : int = 12