Coq - понимание синтаксиса forall`

Question

Я изучаю Coq, читая книгу «Сертифицированное программирование с зависимыми типами», и у меня возникают проблемы с синтаксисом forall.

В качестве примера давайте подумаем это взаимно индуктивного типа данных: (код из книги)

Inductive even_list : Set := 
| ENil : even_list 
| ECons : nat -> odd_list -> even_list 

with odd_list : Set := 
| OCons : nat -> even_list -> odd_list. 

и это взаимно рекурсивные определения функций:

Fixpoint elength (el : even_list) : nat := 
    match el with 
    | ENil => O 
    | ECons _ ol => S (olength ol) 
    end 

with olength (ol : odd_list) : nat := 
    match ol with 
    | OCons _ el => S (elength el) 
    end. 

Fixpoint eapp (el1 el2 : even_list) : even_list := 
    match el1 with 
    | ENil => el2 
    | ECons n ol => ECons n (oapp ol el2) 
    end 

with oapp (ol : odd_list) (el : even_list) : odd_list := 
    match ol with 
    | OCons n el' => OCons n (eapp el' el) 
    end. 

и мы имеем индукционные схемы генерироваться:

Scheme even_list_mut := Induction for even_list Sort Prop 
with odd_list_mut := Induction for odd_list Sort Prop. 

---

Теперь то, что я не понимаю, от типа even_list_mut я могу увидеть его принимает 3 аргумента:

even_list_mut 
    : forall (P : even_list -> Prop) (P0 : odd_list -> Prop), 
     P ENil -> 
     (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> 
     (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> 
     forall e : even_list, P e 

Но для того, чтобы применить его, мы должны предоставить ему два параметра, и он заменяет цель с 3 помещениями (для P ENil, forall (n : nat) (o : odd_list), P0 o -> P (ECons n o) и forall (n : nat) (e : even_list), P e -> P0 (OCons n e)).

Так что, как это на самом деле получает 5 параметров, а не 3.

Но тогда эта идея терпит неудачу, когда мы думаем, что этого типа:

fun el1 : even_list => 
    forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2 
     : even_list -> Prop 

и

fun el1 el2 : even_list => elength (eapp el1 el2) = elength el1 + elength el2 
    : even_list -> even_list -> Prop 

---

Может ли кто-нибудь объяснить, как работает синтаксис forall?

Спасибо,

Answer 1

На самом деле, even_list_mut принимает 6 аргументов:

even_list_mut 
: forall 
    (P : even_list -> Prop)          (* 1 *) 
    (P0 : odd_list -> Prop),          (* 2 *) 
    P ENil ->             (* 3 *) 
    (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> (* 4 *) 
    (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> (* 5 *) 
    forall e : even_list,          (* 6 *) 
    P e 

Вы можете думать стрелки, как только синтаксический сахар:

A -> B 
=== 
forall _ : A, B 

Таким образом, вы могли бы переписать even_list_mut этот путь :

even_list_mut 
: forall 
    (P : even_list -> Prop) 
    (P0 : odd_list -> Prop) 
    (_ : P ENil) 
    (_ : forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) 
    (_ : forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) 
    (e : even_list), 
    P e 

Иногда, когда вы применяете такой термин, некоторые аргументы могут быть выведены путем унификации (сравнивая тип возвращаемого выражения с вашей целью), поэтому эти аргументы не становятся целями, потому что Coq выяснил это. Например, скажем, у меня есть:

div_not_zero : 
    forall (a b : Z) (Anot0 : a <> 0), a/b <> 0 

И я применяю его к цели 42/23 <> 0. Coq может выяснить, что a должно быть 42 и b должно быть 23. Остается только доказать, что 42 <> 0. Но действительно, Coq неявно передает 42 и 23 в качестве аргументов div_not_zero.

Надеюсь, это поможет.

---

EDIT 1:

Отвечая на ваш дополнительный вопрос:

fun (el1 : even_list) => 
    forall (el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2 
: even_list -> Prop 

является функцией одного аргумента, el1 : even_list, который возвращает тип forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2. Неофициально, учитывая список el1, он строит заявление for every list el2, the length of appending it to el1 is the sum of its length and el1's length.

fun (el1 el2 : even_list) => 
    elength (eapp el1 el2) = elength el1 + elength el2 
: even_list -> even_list -> Prop 

является функцией двух аргументов el1 : even_list и el2 : even_list, который возвращает тип elength (eapp el1 el2) = elength el1 + elength el2. Неофициально, учитывая два списка, он строит заявление for these particular two lists, the length of appending them is the sum of their length.

Обратите внимание на две вещи: - сначала я сказал «построить утверждение», что сильно отличается от «построения доказательства утверждения». Эти две функции просто возвращают типы/предложения/утверждения, которые могут быть истинными или ложными, могут быть доказуемыми или недоказуемыми. - первый, однажды подавший некоторый список el1, возвращает довольно интересный тип. Если у вас есть доказательство этого утверждения, вы бы знали, что для любого выбора el2 длина добавления его к el1 является суммой длин.

На самом деле, здесь есть еще один тип/заявление для рассмотрения:

forall (el1 el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2 
: Prop 

Это утверждение говорит, что для любых двух списков, длиной добавляющего является суммой длин.

---

Одна вещь, которая может ввести в заблуждение вас тоже, что это происходит:

fun (el1 el2 : even_list) => 
    (* some proof of elength (eapp el1 el2) = elength el1 + elength el2 *) 

термин, тип которого является

forall (el1 el2 : even_list), 
    elength (eapp el1 el2) = elength el1 + elength el2 

который является заявление, тип которого является

Prop 

Итак, вы видите, что fun и forall - это две вещи связанные, но очень разные. Фактически, все формы fun (t : T) => p t - это термин, тип которого forall (t : T), P t, при условии, что p t имеет тип P t.

Таким образом, возникает путаница, когда вы пишете:

fun (t : T) => forall (q : Q), foo 
       ^^^^^^^^^^^^^^^^^^^ 
       this has type Prop 

, потому что это имеет тип:

forall (t : T), Prop (* just apply the rule *) 

Так forall действительно может появиться в двух контекстах, потому что это исчисление может вычислять типы. Таким образом, вы можете увидеть forall в вычислении (который намекает на то, что это вычисление по типу), или вы можете увидеть его в типе (который обычно вы видите). Но это то же самое forall для всех целей и задач. С другой стороны, fun появляется только в вычислениях.