Лемма как тип записи

То, что вы пишете, не имеет смысла, потому что обозначение _ ==> _ должно связывать два логических значения. Но CA имеет тип A m, который сам по себе является типом, а не логическим значением.

Одной из возможностей продвижения вперед было бы создание логической функции CA, которая могла бы представлять предикат A.

Еще одна трудность с вашей гипотетической записью заключается в том, что мы не знаем, каковы типы ввода для A и B, поэтому я предполагаю, что мы живем в окружающем типе T, по которому появляются количественные оценки. Итак, вот вариант:

Record test (T : Type) (A : T -> Prop) (B : T * T -> bool) :=
{
  CA : T -> bool;
  CA_A : forall m, CA m = true -> A m;
  CB : forall a b m, (CA m ==> B(a, b)) = true
}.

Этот пример заставляет вас понять, что в этом логическом языке есть два разных понятия: bool значения и Prop значения. Они представляют разные вещи, которые иногда могут быть объединены, но вам нужно четко уяснить различие в своей голове, чтобы выйти из категории новичок.

Для вашего последнего предложения «что значит иметь квантифицированную лемму как тип» здесь есть другое объяснение.

При программировании на обычном языке программирования вы можете возвращать массивы целых чисел. Однако вы не можете быть явным и сказать, что вы хотите вернуть массив целых чисел конкретная длина. В Gallina (базовый язык программирования Coq) можно определить тип массивов длины 10. Предположим, что такой тип будет записан array n. Таким образом, array 10 и array 11 будут двумя разными типами. Функция, которая принимает на вход число n и возвращает на выходе массив длины n, будет иметь следующий тип:

forall n, array n

Таким образом, объект, тип которого имеет количественную формулу, просто является функцией.

С логической точки зрения утверждение forall n, array n обычно читается как для каждого n существует массив size n. Это утверждение, вероятно, не стало для вас сюрпризом.

Таким образом, тип массива зависит от индекса. Теперь мы можем подумать о другом типе, например, тип доказательства того, что n простое число. Предположим, что этот тип пишется prime n. Конечно, есть числа, которые не являются простыми, поэтому, например, тип prime 4 вообще не должен содержать никакого доказательства. Теперь я могу написать функцию с именем test_prime : nat -> bool со свойством, что когда она возвращает true, у меня есть гарантия, что ввод является простым. Это будет написано так:

forall n, test_prime n = true -> prime n

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

Record certified_prime_test :=
  {
     test_prime : nat -> bool;
     certificate : forall n, test_prime n = true -> prime nat
  }.

Таким образом, записи, содержащие универсальные квантифицированные формулы, могут относиться к одной из этих двух категорий: либо один компонент является одной из этих функций, выходные данные которой различаются для нескольких типов одного и того же семейства (как в примере array), либо один из компонентов на самом деле приносит больше логическая информация о другом компоненте, который является функцией. В примере certified_prime_test компонент certificate содержит больше информации о функции test_prime.