Агда-подобное программирование в Coq/Proof General?

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

В частности, я хотел бы:

  • Какой-то эквивалент Агды ? или Хаскелла _где я могу опустить часть функции, пока я пишу ее, и (надеюсь) Coq скажет мне тип, который мне нужно поместить туда
  • Эквивалент Cc Cr в режиме Agda (reify), где вы заполняете ? блок с функцией, и это сделает новый ? блоки для необходимых аргументов
  • Когда я делаю match в функции, когда Coq автоматически записывает, расширяет возможные ветви (например, Cc Ca в Agda-режиме)

Это возможно в CoqIde или Proof General?

Источник

2 ответа

Решение

Как было предложено ejgallego в комментариях, вы можете (почти) сделать это. Существует инструмент company-coq, который работает поверх ProofGeneral.

Позвольте мне продемонстрировать, как map Функция может быть реализована с использованием компании-Coq и refine тактика. Начать с

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.

Введите refine ()., затем поместите курсор в паренсы и наберите Cc Ca RET list RET - он вставит match Выражение в списках с отверстиями, которые вы заполняете вручную (давайте заполним имя списка и базовый случай).

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.
  refine (match xs with
          | nil => nil
          | cons x x0 => cons _ _
          end).

Чтобы закончить это мы переименуем x0 в tl и предоставить рекурсивный случай exact (map A B f tl).:

Fixpoint map {A B} (f : A -> B) (xs : list A) : list B.
  refine (match xs with
          | nil => nil
          | cons x tl => cons _ _
          end).
  exact (f x).
  exact (map A B f tl).
Defined.

Существует также полезное сочетание клавиш Cc Ca Cx, которое помогает извлечь текущую цель в отдельную функцию леммы / помощника.

Источник

Позвольте мне научить вас одному странному трюку. Возможно, это не ответ на все ваши вопросы, но это может помочь, по крайней мере, концептуально.

Давайте реализуем сложение для натуральных чисел, последнее задается как

Inductive nat : Set :=
  | zero : nat
  | suc : nat -> nat.

Вы можете попытаться написать дополнение по тактике, но это происходит.

Theorem plus' : nat -> nat -> nat.
Proof.
  induction 1.

plus' < 2 subgoals

  ============================
   nat -> nat

subgoal 2 is:
 nat -> nat

ты не видишь, что ты делаешь.

Хитрость в том, чтобы присмотреться к тому, что ты делаешь. Мы можем ввести безвозмездно зависимый тип, клонирование nat,

Inductive PLUS (x y : nat) : Set :=
  | defPLUS : nat -> PLUS x y.

Идея в том, что PLUS x y это тип "способ вычислить plus x y"Нам понадобится проекция, позволяющая нам извлечь результат такого вычисления.

Theorem usePLUS : forall x y, PLUS x y -> nat.
Proof.
  induction 1.
    exact n.
Defined.

Теперь мы готовы программировать, доказывая.

Theorem mkPLUS : forall x y, PLUS x y.
Proof.

mkPLUS < 1 subgoal

  ============================
   forall x y : nat, PLUS x y

Заключение цели показывает нам нашу текущую левую часть и контекст. Аналог C-c C-c в Агде есть...

  induction x.

mkPLUS < 2 subgoals

  ============================
   forall y : nat, PLUS zero y

subgoal 2 is:
 forall y : nat, PLUS (suc x) y

И вы можете видеть, что это сделало разделение случая! Давайте выбьем базовый случай.

    intros y.
      exact (defPLUS zero y    y).

Вызов конструктора PLUS аналогичен написанию уравнения. Представь = подписать перед третьим аргументом. Для случая шага нам нужно сделать рекурсивный вызов.

    intros y.
      eapply (fun h => (defPLUS (suc x) y    (suc (usePLUS x y h)))).

Чтобы сделать рекурсивный вызов, мы вызываем usePLUS с аргументами, которые мы хотим, здесь x а также y, но мы абстрагируемся от третьего аргумента, который объясняет, как на самом деле его вычислить. Нам остается только эта подзадача, фактически проверка завершения.

mkPLUS < 1 subgoal

  x : nat
  IHx : forall y : nat, PLUS x y
  y : nat
  ============================
   PLUS x y

И теперь, вместо того чтобы использовать проверку Coq, вы используете...

        auto.

... который проверяет, что индуктивные гипотезы охватывают рекурсивный вызов. Мы

Defined.

У нас есть рабочий, но нам нужна обертка.

Theorem plus : nat -> nat -> nat.
Proof.
  intros x y.
    exact (usePLUS x y (mkPLUS x y)).
Defined.

И мы готовы к работе.

Eval compute in (plus (suc (suc zero)) (suc (suc zero))).

Coq <      = suc (suc (suc (suc zero)))
     : nat

У вас есть интерактивный инструмент для строительства. Вы можете играть в нее, чтобы показать вам соответствующие детали проблемы, которую вы решаете, делая типы более информативными. Получившийся корректный скрипт...

Theorem mkPLUS : forall x y, PLUS x y.
Proof.
  induction x.
    intros y.
      exact             (defPLUS zero    y    y).
    intros y.
      eapply (fun h =>  (defPLUS (suc x) y    (suc (usePLUS x y h)))).
        auto.
Defined.

... явно о программе, которую он создает. Вы можете видеть, что это определяющее дополнение.

Если вы автоматизируете эту настройку для построения программы, а затем наложите интерфейс, показывающий программу, которую вы строите, и ключевые тактики, упрощающие решение проблем, вы получите забавный маленький язык программирования под названием Epigram 1.

Источник
Другие вопросы по тегам