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

Question

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

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

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

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

Answer 1

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

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

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

типа в refine()., затем поместите курсор внутри скобок и введите Cc Ca список RET 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, который помогает с извлечением текущей цели в отдельную лемму/вспомогательную функцию.

Answer 2

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

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

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 в Agda является ...

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 

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

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. 

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

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