From mathcomp Require Import ssreflect.

Module My01.

  Inductive bool : Type :=
  | true
  | false.

  Check false : bool.
false : bool
     : bool
  Check false.
false
     : bool

  Check (bool -> bool) : Type.
bool -> bool : Type
     : Type

  Check (fun b : bool => b).
id
     : bool -> bool

  Check fun b => b.
id
     : ?T -> ?T
where
?T : [ |- Type]

  Check (fun b => b) true.
id true
     : bool

  Check fun (f : bool -> bool) => f true.
@^~ true
     : (bool -> bool) -> bool

  Compute (fun b => b) true.
= true
: bool

Определения и функции

Поехали дальше. Можно определять всякие штуки, вот так:

  Definition idb := fun b : bool => b.

С этими "определениями" можно делать те же операции, что и с термами: чекать тип, вычислять и т.д.

  Check idb.
idb
     : bool -> bool
  Check (fun (f : bool -> bool) => f true) idb.
(@^~ true) idb
     : bool
  Compute idb false.
= false
: bool

Команда Fail используется, когда хочется "ожидать ошибку". Пример:

  Fail Check (fun (f : bool -> bool) => f true) false.
The command has indeed failed with message:
The term "false" has type "bool"
while it is expected to have type "bool -> bool".

Мы применяем функцию высшего порядка к терму типа bool, а она хочет тип bool -> bool. Кстати, можно даже писать Fail Fail..., чтобы проверить что "ошибка НЕ произошла (как и ожидалось)".

Паттерн матчинг. Элиминация. Редукции. Eval

Определим функцию отрицания:

  Definition negb :=
    fun (b : bool) =>
      match b with
      | true => false
      | false => true
      end.

  Check negb.
negb
     : bool -> bool
  Compute (negb true).
= false
: bool
  Compute (negb false).
= true
: bool

Результат negb true можно пошагово разложить на последовательность редукций:

negb true

\(\rightsquigarrow \delta\)

(fun (b : bool) => match b with | true => false | false => true end) true

\(\rightsquigarrow \beta\)

match true with | true => false | false => true end

\(\rightsquigarrow \iota \)

false

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

• \(\delta\) (дельта-редукция) — разворачивает определение
• \(\beta\) (бета-редукция) — подставляет значения аргумента в тело определения
• \(\iota\) (ёпта-редукция) — выполняет паттерн-матчинг

Можно управлять степенью раскрытия через команду Eval — она может применять разные стратегии редукции.

  Eval cbv delta in negb true.
= (fun b : bool =>
   match b with
   | true => false
   | false => true
   end) true
: bool
  Eval cbv beta delta in negb true.
= match true with
  | true => false
  | false => true
  end
: bool
  Eval cbv beta delta iota in negb true.
= false
: bool

Порядок тут не важен.

Символические вычисления / вычисления с переменными

В новых версиях Coq просит помещать Variable или Hypothesis внутрь секий.

  Section MySymbolic.

Теперь можно объявить какую-то переменную.

    Variable c : bool.

С переменными можно производить вычисления. Ниже видно как переменная c останавливает цепочку редукций на шаге паттерн матчинга (\(\iota\) — ёпта-редукции).

    Compute idb c.
= c
: bool
    Compute negb c.
= match c with
  | true => false
  | false => true
  end
: bool

Вот два варианта \(\land\) для bool.

    Definition andb (n m : bool) :=
      match n with
      | false => false
      | true => m
      end.

    Definition andb' (n m : bool) :=
      match m with
      | false => false |
        true => n
      end.

Экстенсионально эти функции равны, в том смысле, что: \(\forall b\ c.\ andb\ b\ c = andb'\ b\ c\).

Но если использовать символьный аргумент, то видно, что их поведение чуть разное, просто потому что andb разбирает первый аргумент, ну а andb' — второй.

    Compute andb c true.
= match c with
  | true => true
  | false => false
  end
: bool
    Compute andb c false.
= match c with
  | true | _ => false
  end
: bool

    Compute andb' c true.
= c
: bool
    Compute andb' c false.
= false
: bool

Пока закроем эту секцию.

  End MySymbolic.

Индуктивные типы и рекурсивные функции

В какую психушку? Вы чё, угараете?

Определим новый индуктивный тип для чисел Пеано.

  Inductive nat : Type :=
  | O
  | S of nat.

Напечатем определение.

  Print nat.
Inductive nat : Set :=  O : nat | S : nat -> nat.

Проверим тип.

  Check nat.
nat
     : Set

Посмотрим на типы значений.

  Check O.
O
     : nat
  Check S O.
S O
     : nat
  Check S (S O).
S (S O)
     : nat
  Check S (S (S O)).
S (S (S O))
     : nat

Унарная запись неудобна для вычислений, но суперудобна для доказательств. Поэтому унарные числа часто встречаются в доказательствах и для них есть специальная нотация — можно просто писать 0, 1, 2, 3 и так далее вместо вот этих термов типа S (S (S O)). Чтобы можно было просто писать числа, нужно закрыть наш этот модуль My01 и тогда будет использоваться стандартное определение nat и станут доступны соответствующие нотации.

Определим пару арифметических операций с этими нашими числами.

  Definition succn := S.

Тотальность

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

Definition predn (n : nat) : nat :=
  match n with
  | S x => x
  | O => _ (* А тут что? *)
  end.

Coq — язык тотальный, то есть хрен там, а не исключение можно кинуть. Нам надо реально вернуть что-то типа nat. Прикинем вообще, какие есть способы написать эту функцию:

• pred : nat -> nat — просто возвращаем что-то по умолчанию (0 самое логичное, чо уж там)
• pred : nat -> option nat — возвращаемый тип можно сделать option
• pred : forall n : nat, (n <> 0) -> nat — потребовать n <> 0, чтобы гарантировать, что функцию не вызовут с нулём.

На практике используется, как правило, первый вариант.

  Definition predn (n : nat) : nat :=
    match n with
    | S x => x
    | O => O
    end.

То же самое и с делением — если делим на ноль, просто возвращаем ноль и не ебём мозги. Казалось бы будто так можно всю логику сломать, но ничего подобного. Просто местами придётся добавить парочку предусловий в леммы.

Рекурсия

Классика: сложение двух чисел. Это рекурсивная функция, поэтому надо использовать команду Fixpoint вместо Definition.

  Fixpoint addn (n m : nat) {struct n} : nat :=
    match n with
    | O => m
    | S n' => S (addn n' m)
    end.

Кусок {struct n} указывает по какому параметру идёт рекурсивный вызов — тут это n. Мы как будто подсказываем Coq'у какой терм структурно уменьшается. Конкретно для addn не обязательно было это указывать, так как Coq по умолчанию предполагает, что это будет первый аргумент. Дальше мы увидим, что бывают случаи когда это необходимо.

\(2 + 2 = 4\)

  Compute addn (S (S O)) (S (S O)).
= S (S (S (S O)))
: nat

Как это можно записать более идиоматично.

  Fixpoint addn_idiomatic (n m : nat) : nat :=
    if n is S n' then S (addn_idiomatic n' m) else m.

Посмотрим что там внутри.

  Print addn_idiomatic.
addn_idiomatic =
fix addn_idiomatic (n m : nat) {struct n} : nat :=
  match n with
  | O => m
  | S n' => S (addn_idiomatic n' m)
  end
     : nat -> nat -> nat

Arguments addn_idiomatic n m

Имя после fix используется для рекурсивных вызовов и оно не обязано совпадать с настоящим именем функции, хоть хуем назови, т.е. можно было бы и так:

  Definition addn_no_sugar :=
    fix hooy (n m : nat) {struct n} : nat :=
      match n with
      | O => m
      | S n' => S (hooy n' m)
      end.

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

  Fixpoint addn' (n m : nat) {struct m} :=
    if m is (S m') then S (addn' n m') else n.

Щас снова будем работать с символьными вычислениями, поэтому нужно делать это внутри секции. Да, секции можно "переоткрывать".

  Section MySymbolic.

    Variable z : nat.

    Compute addn O z.
= z
: nat
    Compute addn' O z.
= (fix Ffix (x x0 : nat) {struct x0} : nat :=
     match x0 with
     | O => x
     | S x1 => S (Ffix x x1)
     end) O z
: nat

  End MySymbolic.

Допустим мы сделали ошибку и ебанули рекурсию не по структурно меньшему m', а снова по m. В таком случае тоталити чекер скажет нам "ты чо творишь ёбаный рот, ты сказал, что шаришь в этой теме".

  Fail Fixpoint addn_loop (n m : nat) {struct n} : nat :=
    if n is S _
    then S (addn_loop n m)
    else m.
The command has indeed failed with message:
Recursive definition of addn_loop is ill-formed.
In environment
addn_loop : nat -> nat -> nat
n : nat
m : nat
n0 : nat
Recursive call to addn_loop has principal argument
equal to "n" instead of "n0".
Recursive definition is:
"fun n m : nat =>
 match n with
 | O => m
 | S _ => S (addn_loop n m)
 end".

Видно, что он прям синтаксис проверяет, чтобы находить такие косяки.

Взаимная рекурсия

  Fixpoint is_even (n : nat) : bool :=
    if n is S n' then is_odd n' else true
  with is_odd n :=
    if n is S n' then is_even n' else false.

Обе эти взаимно-рекурсивные функции — is_even и is_odd — теперь доступны для использования.

  Compute is_even (S (S (S O))). (* 3 *)
= false
: bool
  Compute is_even (S (S O)). (* 2 *)
= true
: bool
  Compute is_odd (S (S (S O))). (* 3 *)
= true
: bool
  Compute is_odd (S (S O)). (* 2 *)
= false
: bool

Закроем наш корневой модуль.

End My01.

Теперь все его определения получат префикс имени модуля.

Check My01.nat.
My01.nat
     : Set
Check My01.addn.
My01.addn
     : My01.nat -> My01.nat -> My01.nat

Дальше мы забиваем на свои самописные версии и переключаемся на готовые реализации из MathComp.

From mathcomp Require Import ssrnat ssrbool.

После импорта Coq предупреждает: "некоторые стандартные нотации перекрыты". Нам вообще похую. Эти ворнинги можно отключить вот так:

Set Warnings "-notation-overridden".

Теперь над доступны функции для работы с bool и nat из библиотеки mathcomp.

Module My02.

Вот, например, \(a \oplus b\). Это операция XOR или другими словами "сложение по модулю 2".

  Print addb.
addb =
fun b : bool => if b then negb else id
     : bool -> bool -> bool

Arguments addb (b b)%bool_scope

С помощью команды About можно узнать чуть больше инфы, чем сообщает Check.

  About nat.
nat : Set

nat is not universe polymorphic
Expands to: Inductive Coq.Init.Datatypes.nat
  About S.
S : nat -> nat

S is not universe polymorphic
Arguments S _%nat_scope
Expands to: Constructor Coq.Init.Datatypes.S

А вот и упомятый выше сахар для натуральных чисел Пеано.

  Check S (S (S O)).
3
     : nat
  Check 42.
42
     : nat

Отключение/включение синтаксического сахара.

  Set Printing All. Check 5 + 4.
addn (S (S (S (S (S O))))) (S (S (S (S O))))
     : nat
  Unset Printing All.

Как выяснить значения непонятных нотаций.

  Locate ".+1".
Notation "n .+1" := (S n) : nat_scope
  (default interpretation)

Хотя, иногда бывает сложно понять, что является частью нотации, а что нет.

  Locate ".+".
Unknown notation

  Section MySymbolic.

    Variable x : nat.

    Check x.+1.
x.+1
     : nat

  End MySymbolic.

Короче, нотации это просто удобные текстовые сокращения, их можно свободно менять. А определения это фундаментальные объекты в теории: они влияют на всё.

End My02.

Практика

Теперь немного практики — сделаем домашку из курса. Я это уже всё решал лет 5 назад, но всё к забыл. Решу всё ещё разок, заново.

Module My03.

Продолжаем работать с нашими собственными определениями булевых значений и натуральных чисел.

  Inductive bool :=
  | true
  | false.

  Definition negb :=
    fun (b : bool) =>
      match b with
      | true => false
      | false => true
      end.

Упражнение 1: Булевы функции.

1a. Определите функцию orb, реализующую дизъюнкцию (логическое "или") для булевых значений, и тщательно протестируйте её при помощи команды Compute.

  Definition orb (b c : bool) : bool :=
    match b, c with
    | false, false => false
    | _, _ => true
    end.

  Compute orb true true.
= true
: bool
  Compute orb true false.
= true
: bool
  Compute orb false true.
= true
: bool
  Compute orb false false.
= false
: bool

1b. Определите функцию addb, реализующую XOR (\(a \oplus b\)). Попробуйте придумать более одного способа реализации (не просто поменять местами аргументы) и исследуйте, как ведёт себя редукция функции при наличии символических переменных.

  Section MySymbolic.

Для наглядности распишем все кейсы.

    Definition addb0 (b c : bool) : bool :=
      match b, c with
      | true, true => false
      | true, false => true
      | false, true => true
      | false, false => false
      end.

    Variable x : bool.

    Compute addb0 true x.
= match x with
  | true => false
  | false => true
  end
: bool
    Compute addb0 x true.
= match x with
  | true => false
  | false => true
  end
: bool

Попробуем теперь использовать анонимные функции.

    Definition addb1 :=
      fun (b : bool) =>
      fun (c : bool ) =>
        match b, c with
        | true, true => false
        | false, false => false
        | _, _ => true
        end.

    Compute addb1 true x.
= match x with
  | true => false
  | false => true
  end
: bool
    Compute addb1 x true.
= match x with
  | true => false
  | false => true
  end
: bool

Ну символически-вычисленные термы одинаковы. А что будет, если сравнить цепочки редукций?

    Eval cbv delta in addb0 true x.
= (fun b c : bool =>
   match b with
   | true =>
       match c with
       | true => false
       | false => true
       end
   | false =>
       match c with
       | true => true
       | false => false
       end
   end) true x
: bool
    Eval cbv delta in addb1 true x.
= (fun b c : bool =>
   match b with
   | true =>
       match c with
       | true => false
       | false => true
       end
   | false =>
       match c with
       | true => true
       | false => false
       end
   end) true x
: bool

    Eval cbv delta beta in addb0 true x.
= match true with
  | true =>
      match x with
      | true => false
      | false => true
      end
  | false =>
      match x with
      | true => true
      | false => false
      end
  end
: bool
    Eval cbv delta beta in addb1 true x.
= match true with
  | true =>
      match x with
      | true => false
      | false => true
      end
  | false =>
      match x with
      | true => true
      | false => false
      end
  end
: bool

    Eval cbv delta beta iota in addb0 true x.
= match x with
  | true => false
  | false => true
  end
: bool
    Eval cbv delta beta iota in addb1 true x.
= match x with
  | true => false
  | false => true
  end
: bool

Ну очевидно, что оно всё одинаковое. Но пока у нас разница между addn0 и addn1 только в том, используем ли мы анонимные функции или нет. Похоже это вообще никак не влияет на цепочку редукций и в задаче требовалось проверить какое-то другое различие.

А что, если добавить какую-нибудь комбинацию \(\land\), \(\lor\) или \(\lnot\) в тело функции, но так, чтобы это не повлияло не результат? Ну типа сделать эти две функции экстенсионально одинаковыми, но интенсионально различными?

    Definition addb2 (b c : bool) : bool :=
      orb (negb (orb (negb b) c)) (negb (orb b (negb c))).

    Compute addb2 true false.
= true
: bool
    Compute addb2 false true.
= true
: bool
    Compute addb2 true true.
= false
: bool
    Compute addb2 false false.
= false
: bool

    Compute addb2 true x.
= match
    match
      match x with
      | true => true
      | false => false
      end
    with
    | true => false
    | false => true
    end
  with
  | true => true
  | false => false
  end
: bool
    Compute addb2 x true.
= match
    match
      match
        match x with
        | true => false
        | false => true
        end
      with
      | true | _ => true
      end
    with
    | true => false
    | false => true
    end
  with
  | true => true
  | false =>
      match
        match
          match x with
          | true => true
          | false => false
          end
        with
        | true => false
        | false => true
        end
      with
      | true => true
      | false => false
      end
  end
: bool

Сравним теперь цепочки редукций.

    Eval cbv delta beta in addb0 true x.
= match true with
  | true =>
      match x with
      | true => false
      | false => true
      end
  | false =>
      match x with
      | true => true
      | false => false
      end
  end
: bool
    Eval cbv delta beta in addb2 true x.
= match
    match
      match
        match true with
        | true => false
        | false => true
        end
      with
      | true => true
      | false =>
          match x with
          | true => true
          | false => false
          end
      end
    with
    | true => false
    | false => true
    end
  with
  | true => true
  | false =>
      match
        match
          match true with
          | true => true
          | false =>
              match
                match x with
                | true => false
                | false => true
                end
              with
              | true => true
              | false => false
              end
          end
        with
        | true => false
        | false => true
        end
      with
      | true => true
      | false => false
      end
  end
: bool
    Eval cbv delta beta iota in addb0 true x.
= match x with
  | true => false
  | false => true
  end
: bool
    Eval cbv delta beta iota in addb2 true x.
= match
    match
      match x with
      | true => true
      | false => false
      end
    with
    | true => false
    | false => true
    end
  with
  | true => true
  | false => false
  end
: bool

  End MySymbolic.

1c. Определите функцию eqb, реализующую проверку равенства на булевых значениях, то есть eqb b c должно возвращать true тогда и только тогда, когда b и c равны. Добавьте юнит-тесты. Под юнит-тестами тут и дальше имеется ввиду, что надо просто сделать Compute и убедиться в корретности результата.

  Definition eqb (b c : bool) :=
    negb (addb0 b c).

  Compute eqb true false.
= false
: bool
  Compute eqb false true.
= false
: bool
  Compute eqb true true.
= true
: bool
  Compute eqb false false.
= true
: bool

Упражнение 2: Арифметика.

  Inductive nat : Type :=
  | O
  | S of nat.

2a. Определите функцию dec2 типа nat -> nat, которая уменьшает натуральное число на 2. Например, для числа 5 должно вернуться 3. Напишите несколько юнит-тестов для dec2. Что функция должна возвращать для 1 и 0?

Будем O возвращать, практичности и удобства ради.

  Definition dec2 (n : nat) :=
    if n is (S (S n')) then n' else O.

  Compute dec2 (S (S (S (S (S O))))).
= S (S (S O))
: nat
  Compute dec2 (S O).
= O
: nat
  Compute dec2 O.
= O
: nat

2b. Определите функцию subn типа nat -> nat -> nat, которая принимает два натуральных числа m и n и возвращает результат вычитания n из m. Например, subn 5 3 должно возвращать 2. Напишите юнит-тесты.

  Fixpoint subn0 (m n : nat) : nat :=
    match m, n with
    | O, _ => O
    | _, O => m
    | S m', S n' => subn0 m' n'
    end.

Или вот более идиоматичное определение вычитания.

  Fixpoint subn1 (m n : nat) {struct m} :=
    if m is S m'
    then
      if n is S n'
      then m' - n'
      else m
    else m
  where "m - n" := (subn1 m n) : nat_scope.

  Compute (S (S (S (S (S O))))) - (S (S (S O))).
= S (S O)
: nat
  Compute (S (S O)) - O.
= S (S O)
: nat
  Compute (S (S (S O))) - (S O).
= S (S O)
: nat
  Compute (S (S (S O))) - (S (S O)).
= S O
: nat
  Compute (S (S (S O))) - (S (S (S O))).
= O
: nat
  Compute (S O) - (S (S (S O))).
= O
: nat

2c. Определите функцию muln типа nat -> nat -> nat, которая принимает два натуральных числа m и n и возвращает результат их умножения. Напишите юнит-тесты.

Умножение это как будто сокращённое сложение: \(a * 3 \equiv a + a + a\). Поэтому определим сначала операцию сложения для наших чисел.

  Fixpoint addn (m n : nat) {struct n} : nat :=
    if n is S n'
    then S (addn m n')
    else m
  where "m + n" := (addn m n) : nat_scope.

Проверим, что это вообще работает как мы ожидаем.

  Compute (S (S O)) + (S (S (S O))).
= S (S (S (S (S O))))
: nat

  Compute O + (S O).
= S O
: nat

  Compute O + (S (S O)).
= S (S O)
: nat

  Compute (S (S O)) + O.
= S (S O)
: nat

Теперь определим:

\(m * n \equiv m + \dots + m\).

  Fixpoint muln (m n : nat) {struct n} : nat :=
    if n is S n'
    then m + (m * n')
    else O
  where "m * n" := (muln m n) : nat_scope.

  Compute (S (S O)) * (S (S (S O))). (* 2 * 3 = 5 *)
= S (S (S (S (S (S O)))))
: nat
  Compute O * (S O). (* 0 * 1 = 0 *)
= O
: nat
  Compute (S O) * (S (S O)). (* 1 * 2 = 2 *)
= S (S O)
: nat
  Compute (S (S O)) * O. (* 2 * 0 = 0 *)
= O
: nat
  Compute (S (S O)) * (S O). (* 2 * 1 = 2 *)
= S (S O)
: nat

2d. Реализуйте функцию сравнения на равенство eqn для натуральных чисел типа nat -> nat -> bool. Она должна возвращать true тогда и только тогда, когда числа равны.

  Fixpoint eqn (m n : nat) : bool :=
    match m, n with
    | O, O => true
    | S m', O => false
    | O, S n' => false
    | S m', S n' => m' = n'
    end
  where
    "m = n" := (eqn m n) : nat_scope and
    "m <> n" := (negb (m = n)) : nat_scope.

  Compute (S O) <> O.
= true
: bool
  Compute (S (S O)) = (S (S O)).
= true
: bool
  Compute (S (S (S O))) <> (S (S O)).
= true
: bool
  Compute (S (S (S O))) = (S (S (S O))).
= true
: bool

2e. Реализуйте функцию сравнения "меньше или равно" leq для натуральных чисел типа nat -> nat -> bool. Выражение leq m n должно возвращать true тогда и только тогда, когда \(m \leq n\). Решение не должно использовать рекурсию, но можно переиспользовать ранее определённые функции.

  Definition leq (m n : nat) : bool :=
    (n - m) <> O.

В этот раз ради прикола отдельно определим нотацию \(\leq\) для функции leq.

  Notation "m <= n" := (leq m n) : nat_scope.

  Compute (S O) <= O.
= false
: bool
  Compute (S (S O)) <= (S O).
= false
: bool
  Compute (S (S O)) <= (S (S (S O))).
= true
: bool
  Compute O <= O.
= false
: bool
  Compute (S O) <= (S O).
= false
: bool

Дополнительное. Реализуйте деление divn на этих ваших натуральных числах и напишите несколько юнит-тестов для него.

Аналогично тому, что умножение это фактически сокращённая запись сложения. Деление должно как-то получаться из серии вычитаний.

Возьмём, например число \(12 : 3 = 4\). Попробуем вычитать из \(12\) его делитель \(3\), пока оно не обратится в \(0\). Cколько раз это можно сделать?

\(12 - 3 - 3 - 3 - 3 = 0\).

Всего \(4\) раза — это и есть частное.

А тут хуяк и допустим мы забыли чо такое этот минус: subn0 или subn1?

  Locate "_ - _".
Notation "m - n" := (Nat.sub m n) : coq_nat_scope
Notation "m - n" := (subn1 m n) : nat_scope
  (default interpretation)

О, это subn1. Ну короче искать мы умеем.

  Fixpoint divn (m n : nat) : nat :=
    if n is S n'
    then
      if m - n' is S m'
      then S (m' / n)
      else O
    else O
  where "m / n" := (divn m n) : nat_scope.

  Compute (S (S (S (S O)))) / (S (S O)). (* 4 / 2 = 2 *)
= S (S O)
: nat
  Compute (S (S (S O))) / (S (S (S O))). (* 3 / 3 = 1 *)
= S O
: nat
  Compute (S (S (S (S (S (S (S (S O)))))))) / (S (S O)). (* 8 / 2 = 4 *)
= S (S (S (S O)))
: nat
  Compute (S (S (S (S (S O))))) / (S (S O)). (* 5 / 2 = 2 *)
= S (S O)
: nat
  Compute (S O) / O. (* 1 / 0 = 0 *)
= O
: nat
  Compute O / O. (* 0 / 0 = 0 *)
= O
: nat

У меня 10 тыщ пенсия. Я хуй без соли доедаю.
Ёлочка мне нравится? Елочка блять мне нравится.

Теперь вспомним что там были за задачки на семинаре.

End My03.

Module My04.

Семинар

Упражнение 1: Реализуй функции с указанными типами.

  Definition prodA {A B C : Type} :
    (A * B) * C -> A * (B * C) :=
    fun abc =>
      match abc with
      | ((a, b), c) => (a, (b, c))
      end.

  Compute prodA ((true, 1), 2).
= (true, (1, 2))
: bool * (nat * nat)

  Definition sumA' {A B C : Type} :
    (A + B) + C -> A + (B + C)
  :=
    fun abc =>
      match abc with
      | inl ab =>
          match ab with
          | inl a => inl a
          | inr b => inr (inl b)
          end
      | inr c => inr (inr c)
      end.

  Compute @sumA' nat bool nat (inl (inr true)).
= inr (inl true)
: nat + (bool + nat)
  Compute @sumA' bool nat bool (inr false).
= inr (inr false)
: bool + (nat + bool)

Другая возможная реализация с ипользованием вложенного паттерн-матчинга - так даже более идиоматично:

  Definition sumA (A B C : Type) :
    (A + B) + C -> A + (B + C)
  :=
    fun abc =>
      match abc with
      | inl (inl a) => inl a
      | inl (inr b) => inr (inl b)
      | inr c => inr (inr c)
      end.

  Compute sumA nat bool nat (inl (inr true)).
= inr (inl true)
: nat + (bool + nat)
  Compute sumA bool nat bool (inr false).
= inr (inr false)
: bool + (nat + bool)

  Check sumA nat nat bool.
sumA nat nat bool
     : nat + nat + bool -> nat + (nat + bool)
  Compute sumA nat nat bool (inl (inl 1)).
= inl 1
: nat + (nat + bool)

  Definition prod_sumD (A B C : Type) :
    A * (B + C) -> (A * B) + (A * C)
  := fun '(a, bc) =>
      match bc with
      | inl b => inl (a, b)
      | inr c => inr (a, c)
      end.                

  Check prod_sumD bool nat bool.
prod_sumD bool nat bool
     : bool * (nat + bool) -> bool * nat + bool * bool
  Compute prod_sumD bool nat bool (true, inr true).
= inr (true, true)
: bool * nat + bool * bool
  Check prod_sumD nat bool nat.
prod_sumD nat bool nat
     : nat * (bool + nat) -> nat * bool + nat * nat
  Compute prod_sumD bool bool nat (false, inl false).
= inl (false, false)
: bool * bool + bool * nat

  Definition sum_prodD (A B C : Type) :
    A + (B * C) -> (A + B) * (A + C)
  := fun a_bc =>
      match a_bc with
      | inl a => (inl a, inl a)
      | inr (b, c) => (inr b, inr c)
      end.

  Compute sum_prodD nat nat bool (inr (5, false)).
= (inr 5, inr false)
: (nat + nat) * (nat + bool)
  Compute sum_prodD bool bool nat (inl true).
= (inl true, inl true)
: (bool + bool) * (bool + nat)

Упражнение 2: Композиция функций.

  Definition comp A B C (f : B -> A) (g : C -> B) : C -> A
    := fun x => f (g x).

  Compute comp nat nat nat id (fun x => x * 2) 3.
= 6
: nat

Введи нотацию, чтобы можно было использовать композицию вот так: \(f \circ g\). Возможно, тебе придётся немного подправить настройку неявных аргументов у comp.

  Arguments comp [A B C] _ _ _.

В ssrfun есть уже нотация для композии функций, можно использовать её.

  Locate "_ \o _".
Notation "f1 \o f2" := (ssrfun.comp f1 f2)
  : function_scope (default interpretation)

Но если б её не было, ты мог бы её определить вот так:

Notation "f \o g" := (comp f g) (at level 70).

  Compute ((fun x => x + 1) \o (fun x => x * 2)) 3.
= 7
: nat

Введём пустой тип.

  Inductive void : Type := .
Automatically putting void in Prop even though it was
declared with Type.
Unset Automatic Proposition Inductives to prevent this
(it will become the default in a future version).
If you instead put void explicitly in Prop, set
Dependent Proposition Eliminators around the
declaration for full backwards compatibility.
[automatic-prop-lowering,deprecated-since-8.20,deprecated,default]

Тут получаем предупреждение, тк мы объявили тип void во вселенной типов (Type), но петушара автоматически понизил его до Prop (логических утверждений). Такое автоматическое поведение с понижением до Prop — устаревшее и скоро станет невозможным.

• Coq различает два главных юниверса: Type (обычные типы: множества, структуры) и Prop (логические утверждения — истинные или ложные).​
• В старых версиях Coq, если ты объявляешь void как тип в Type, но используешь его там, где ожидается Prop, Coq автоматически переводит его в Prop (это называется "prop lowering").​
• Текущий warning говорит: "Я объявлен в Type, но меня используют как Prop → делаю автоматическое понижение". Это скоро перестанет делаться автоматически, чтоб избежать неявного поведения.

Из пустоты (неконструируемого) можно получить всё, но сначала предъяви пустоту (неконструироемое).

  Definition void_terminal (A : Type) :
    void -> A
  :=
    fun x => match x with end.

Введём тип unit — это тип, у которого ровно одно значение (каноническая форма).

  Inductive unit : Type := tt.
Automatically putting unit in Prop even though it was
declared with Type.
Unset Automatic Proposition Inductives to prevent this
(it will become the default in a future version).
If you instead put unit explicitly in Prop, set
Dependent Proposition Eliminators around the
declaration for full backwards compatibility.
[automatic-prop-lowering,deprecated-since-8.20,deprecated,default]

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

  Definition unit_initial (A : Type) :
    A -> unit
  :=
    fun _ => tt.

  Compute unit_initial nat 1.
= tt
: unit

Подумай над другими сигнатурами типов, использующими void, unit, sum и prod:

1. (void + unit) * unit -> unit

Check (fun _ => tt): (void + unit) * unit -> unit.
(fun=> tt) : (void + unit) * unit -> unit
     : (void + unit) * unit -> unit

2. void -> void + void

Check (fun x => inr x): void -> void + void.
[eta inr] : void -> void + void
     : void -> void + void

3. void * unit + void -> void * unit

Check
  (fun vu_or_v =>
     match vu_or_v with
     | inl (v, u) => (v, u)
     | inr v => (v, tt)
     end
  ): void * unit + void -> void * unit.
(fun vu_or_v : void * unit + void =>
 match vu_or_v with
 | inl (v, u) => (v, u)
 | inr v => (v, tt)
 end)
:
void * unit + void -> void * unit
     : void * unit + void -> void * unit

End My04.

Module My05.

Полиморфные функции и зависимые функции

Была у нас такая функция:

Definition id := fun (b : bool) => b.

Теперь мы хотим такую же, но только чтобы она работала на всех типах, а не только на bool. То есть нам нужна функция не типа bool -> bool, а типа \(\alpha \rightarrow \alpha\). Функции такого типа называются параметрически полиморфными. Но почему-то следующий код не работает:

  Fail Definition id : A -> A := fun (x : A) => a.
The command has indeed failed with message:
The reference A was not found in the current
environment.

Проблема примера выше в том, что Coq не знает, что такое A: она нигде не определена и не связана. Нам нужно явно это указать. Иными словами, мы щас попытались использовать параметрический полиморфизм в неявной форме, а Coq поддерживает его только в явной форме. По сути, мы хотим сказать что-то вроде id : (A : Type) -> A -> A. Однако это выражение в Coq не означает то, что мы имеем в виду.

Правильный синтаксис в Coq таков:

forall ident : term, term,

где в нашем случае под term следует понимать тип.

Ну короче:

  Definition id :
    forall A : Type, A -> A := fun A : Type => fun x : A => x.

Пример использования:

  Compute id bool true.
= true
: bool
  Compute id nat 42.
= 42
: nat

Теперь функция получает два аргумента — сначала тип, затем значение. Чтобы применить id к данным вроде true или 42, нужно явно указывать тип. Позже мы научимся, как обходиться без явного указания типа.

Ну и мы только что познакомились с зависимыми типами, потому что по факту тип результата функции id зависит от её первого аргумента.

  Check id bool : bool -> bool.
id bool : bool -> bool
     : bool -> bool
  Check id nat : nat -> nat.
id nat : nat -> nat
     : nat -> nat

В теории типов это называется \(\pi\)-типы ("пи"-типы). Можно попробовать почитать в вики про пи-типы, но как по мне, если ты заранее не знаешь о чём речь и не знаком с теорией, то вкуривание той вики-странички будет напряжно.

Типы в Coq — это такие же термы, как и любые другие. Они являются "объектами первого класса" (на русском это странно звучит, вообще термин звучит как "first-class citizen"). Это означает, что в Coq типы можно хранить их в структурах, передавать и возвращать из функций.

В Coq нет какого-то особого стрелочного типа ->. Все функции — зависимо типизированные, а -> — это просто нотация. Проверим:

  Locate "->".
Notation "A -> B" := (forall _ : A, B) : type_scope
  (default interpretation)

Петушара показывает, что это тоже зависимая функция, просто в ней параметр не используется (поэтому подчёркивание). Таким образом, обычный тип A -> B — частный случай зависимого типа.

Coq не запрещает явно именовать параметры, даже если они не используются:

  Definition id' :
    forall A : Type ,  forall x : A ,  A
  :=
      fun A : Type =>    fun x : A => x.

Ну короче, если хочется погрузиться и начать шарить в этой теме, то можно почитать Introduction to the Calculus of Inductive Constructions, а пока нас это ебать не должно.

Тип-произведение

Каррирование позволяет работать с функциями любой арности (любого количества аргументов). Например, сложение имеет тип nat -> nat -> nat, что тоже самое, что и nat -> (nat -> nat). Но что если функция возвращает несколько результатов, как, например, при целочисленном делении нужно вернуть частное и остаток?

  Inductive prodn : Type := | pairn of nat & nat.

pairn of nat & nat означает, что конструктор pairn содержит 2 натуральных числа.

  Print prodn.
Inductive prodn : Set :=  pairn : nat -> nat -> prodn.

Arguments pairn (_ _)%nat_scope

Это назвается и тип-произведение, потому что по смыслу это тоже самое, что и прямое (декартово) произведение, только на типах, а не на множествах.

Теперь мы могли бы реализовать, например, деление: divmod : nat -> nat -> prodn, но тут появляется проблема — пришлось бы создавать свой "тип-произведение" под каждую комбинацию типов: nat*bool, bool*nat, и т.д.

Параметризованные индуктивные типы

Вместо этого мы можем использовать параметризованный индуктивный тип:

  Inductive prod (A B : Type) : Type := pair of A & B.

Важно понимать, что prod это не тип, а конструктор типа. Проверим:

  Fail Check prod : Type.
The command has indeed failed with message:
The term "prod" has type "Type -> Type -> Type"
while it is expected to have type "Type".

Видимо потому, что выговаривать "конструктор типа" каждый раз долго, люди часто всё равно называют их просто "типами". В общем, чтобы получить именно тип, нужно применить его к аргументам A, B:

  Check prod nat bool : Type.
prod nat bool : Type
     : Type

Предлагается ещё помедитировать над этим:

  Check pair.
pair
     : forall A B : Type, A -> B -> prod A B
  Check pair nat bool 42 true.
pair nat bool 42 true
     : prod nat bool

Неявные аргументы

Всё время явно указывать типы запаришься. Особенно когда сам Coq прекрасно может догадаться, что ты имел в виду. Например, он ведь точно знает, что у числа 42 тип nat, а у true тип bool. Значит, он вполне может вывести это сам. К счастью петушок умеет выводить их автоматически через неявные аргументы. Давай включим их для id и pair:

  Arguments id [A] _.
  Arguments pair [A B] _ _.

Строка Arguments id [A] _. сообщает коку следующее: параметр типа A теперь будет выводиться автоматически, поэтому нам больше не нужно его указывать вручную. Для pair та же фигня, только Coq тут выведет сразу оба типа — A и B. Теперь можно писать так:

  Check id 42.
id 42
     : nat
  Check id true.
id true
     : bool
  Check pair 42 true.
pair 42 true
     : prod nat bool

Кстати, вызов pair nat bool 42 true (с явной передачей аргументов типа) теперь зафейлится — nat и bool стали неявными, и Coq сам должен их вычислить.

  Fail Check pair nat bool 42 true : prod nat bool.
The command has indeed failed with message:
Illegal application (Non-functional construction): 
The expression "pair nat bool" of type "prod Set Set"
cannot be applied to the term
 "42" : "nat"

Это не значит, что мы поменяли сам тип pair. Нет, внутри всё осталось как раньше — Coq просто как бы добавил сверху такой удобный слой, чтобы нам не приходилось писать много руками. Такой прикол часто используют в ML‑подобных языках, откуда вдохновлялись видимо разработчики кока.

Если вдруг нужно, наоборот, отключить неявное определение и заставить Coq требовать все аргументы явно, используется @. Это такое "локальное отключение вывода аргументов".

  Check @pair nat bool 42 true : prod nat bool.
pair 42 true : prod nat bool
     : prod nat bool

Претти-принтер учитывает, какие аргументы сделаны неявными, и по умолчанию их не показывает — даже если ты сам их написал руками. Иногда это мешает, например, когда надо точно понять, что именно Coq подставил под капотом. Чтобы увидеть всё "как есть", включаем специальный режим:

  Set Printing Implicit.
  Check pair 42 true : prod nat bool.
@pair nat bool 42 true : prod nat bool
     : prod nat bool
  Unset Printing Implicit.

Для сравнения:

  Check pair 42 true : prod nat bool.
pair 42 true : prod nat bool
     : prod nat bool

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

Да, каждое новое определение или тип прописывать с Arguments вручную немного напрягает. Чтобы Coq сам решал, какие параметры можно сделать неявными, есть глобальная команда:

  Set Implicit Arguments.

С этого момента и до конца файла (или пока не встретится Unset Implicit Arguments) Coq сам будет пытаться выяснить, какие аргументы можно брать неявно. Можно сказать, у него включается режим "я шарю в этой теме".

Нотации

Работать с парами через prod и pair напрямую неудобно и громоздко. Все обычно пользуются более привычными обозначениями вроде A * B для типа произведения и (a, b) для конкретной пары.

К счастью, Coq позволяет вводить свои собственные нотации — по сути, добавлять новые правила для парсера прямо "на лету". Вообще система нотаций в Coq довольно хитрая и многослойная, но сейчас мы глянем только основное.

Вот пример нотации для типа произведения (prod). Дальше ниже разберём, что здесь происходит.

  Notation "A * B" :=
    (prod A B)
    (at level 40, left associativity)
    : type_scope.
Setting B constr at next level
to match previous notation with longest common prefix:
"_ * _".

Заметь, Coq выдаст предупреждение, что нотация уже переопределяется — это потому что стандартная библиотека уже содержит аналог.

А теперь разберём по пунктам, что всё это значит:

• Notation говорит Coq, что мы сейчас добавим новую синтаксическую конструкцию
• Определяемая нотация берётся в двойные кавычки (чтобы показать точный вид, включая пробелы и символы)
• Идентификаторы вроде A и B автоматически становятся связанными переменными внутри тела после :=
• Само тело нотации (prod A B) обязательно помещается в скобки — это то, во что Coq будет реально разворачивать запись при парсинге
• Далее задаётся грамматическая информация, например уровень приоритета (at level 40) и ассоциативность (left associativity). Чем level ниже, тем сильнее нотация "сцепляется" с другими операторами
• После этого указывают область видимости — здесь это type_scope, то есть нотация будет применяться, когда Coq ожидает тип
• При желании можно ещё добавить правила для pretty-printer'а. В этом примере это не показано

Теперь, когда мы напишем A * B, петушара сам поймёт, что имеется в виду prod A B. Как только Coq встречает подобную запись, то он добавляет соотвествующее правило в некоторую свою таблицу грамматических правил.

Области нотаций

Один и тот же символ можно использовать для разных вещей. В нашем случае мы уже переиспользовали * — теперь это не умножение, а тип произведения. Но по умолчанию * вообще-то означает именно умножение для натуральных чисел.

  Locate "*".
Notation "m * n" := (Nat.mul m n) : coq_nat_scope
Notation "m * n" := (muln m n) : nat_scope
  (default interpretation)
Notation "A * B" := (prod A B) : type_scope

В выводе команды Locate можно увидеть, что у символа есть "default interpretation". Это значит, что если Coq не понимает, в каком смысле ты используешь *, он воспримет его как умножение. Поэтому следующая проверка не сработает:

  Fail Check nat * bool.
The command has indeed failed with message:
The term "nat" has type "Set"
while it is expected to have type "nat".

Нужно подсказать Coq'у, что это не оператор умножения, а тип произведения двух других типов. Чтобы объяснить Coq, что здесь подразумевается тип произведения, надо указать "область нотации" — с помощью %type:

  Check (nat * bool)%type.
(nat * bool)%type
     : Set

Альтернативный способ сделать тоже самое:

  Check (nat * bool) : Type.
nat * bool : Type
     : Type

В этом случае Coq понимает, что в скобках написан тип, а не терм (житель/значение типа), и значит * — это нотация не для Nat.muln, а для prod.

Ещё один способ поменять значение символа по умолчанию — это открыть соответствующую область - Open Scope. В Coq области (scopes) ведут себя как стек: последняя открытая становится текущей.

  Open Scope type_scope.
  Locate "*".
Notation "m * n" := (Nat.mul m n) : coq_nat_scope
Notation "m * n" := (muln m n) : nat_scope
Notation "A * B" := (prod A B) : type_scope
  (default interpretation)

Опа, дефолтная интерпретацию нотации "*" изменилась.

  Check (nat * nat).
nat * nat
     : Set

Когда открытая область больше не нужна, её можно закрыть — это "вытолкнет" её со стека и вернёт старое поведение.

  Close Scope type_scope.
  Locate "*".
Notation "m * n" := (Nat.mul m n) : coq_nat_scope
Notation "m * n" := (muln m n) : nat_scope
  (default interpretation)
Notation "A * B" := (prod A B) : type_scope
  Fail Check (nat * nat).
The command has indeed failed with message:
The term "nat" has type "Set"
while it is expected to have type "nat".

Кстати, про left associativity, которое мы указали в определении нотации A * B. Это нужно для того, чтобы можно было писать кортежи без дополнительных скобок. Например, тройку из типов nat, bool и nat можно описать так:

  Check ((nat * bool) * nat)%type.
(nat * bool * nat)%type
     : Set

Из-за ассоциативности влево можно спокойно опустить скобки.

  Check (nat * bool * nat)%type.
(nat * bool * nat)%type
     : Set

А если наоборот, получится другой, хоть и изоморфный, тип.

  Check (nat * (bool * nat))%type.
(nat * (bool * nat))%type
     : Set

Раз уж мы завели удобную нотацию для prod, сделаем то же самое для pair, чтобы можно было писать (42, true) вместо pair 42 true.

Первая наивная попытка сделать эту нотацию могла бы быть такой:

  Notation "( p ; q )" := (pair p q).
Setting notation at level 0
to match previous notation with longest common prefix:
"( _ , _ , .. , _ )".

  Check (1; false).
(1; false)
     : nat * bool

Кстати, пробелы после открывающей и до закрывающей скобки обязательны.

Это работает, но только для пар, а вот так уже не получится:

Check (1; false; 2).

А мы ведь хотим писать тройки, четвёрки и т.д. Для этого есть рекурсивные нотации:

  Notation "( p , q , .. , r )" :=
    (pair .. (pair p q) .. r) : core_scope.

Здесь мы указываем core_scope для нашей нотации, ибо pair в отличии от prod это конструктор значения, а не конструктор типа.

  Check (1, false) : nat * bool.
(1, false) : nat * bool
     : nat * bool
  Check (1, false, true) : nat * bool * bool.
(1, false, true) : nat * bool * bool
     : nat * bool * bool
  Check (1, false, 2, true) : nat * bool * nat * bool.
(1, false, 2, true) : nat * bool * nat * bool
     : nat * bool * nat * bool

Теперь можно, наконец, использовать всё это добро для простых функций с парами. Например, напишем проекции — fst и snd.

  Definition fst {A B : Type} : A * B -> A :=
    fun p =>
      match p with
      | (a, _) => a
      end.

Пока что будем думать что {A B : Type} и [A B : Type] - одно и тоже. В том смысле, что A и B объявлены как неявные параметры.

Если не очень понятно что именно какая-то нотация развернётся, то можно попросить петушка вывести полную форму без всяких сокращений:

  Print fst.
fst =
fun (A B : Type) (p : A * B) =>
match p with
| (a, _) => a
end
     : forall {A B : Type}, A * B -> A

Arguments fst {A B}%type_scope _
  Unset Printing Notations.
  Print fst.
fst =
fun (A B : Type) (p : prod A B) =>
match p with
| pair a _ => a
end
     : forall {A B : Type} (_ : prod A B), A

Arguments fst {A B}%type_scope _
  Set Printing Notations.

Теперь пишем вторую проекцию, тут всё то же самое:

  Definition snd {A B : Type} : A * B -> B :=
  fun p =>
    match p with
    | pair _ b => b
    end.

В ssreflect есть привычная нотация для этих проекций — её тоже сделаем:

  Notation "p .1" := (fst p).
  Notation "p .2" := (snd p).

  Compute (true, 39).1.
= true
: bool
  Compute (true, 39).2.
= 39
: nat

А вот функция, которая меняет местами компоненты пары:

  Definition swap {A B : Type} : A * B -> B * A :=
    fun p =>
      match p with
      | (a, b) => (b, a)
      end.

  Compute swap (false, 40).
= (40, false)
: nat * bool

Тип-сумма

  Inductive sum (A B : Type) :=
    | inl of A
    | inr of B.

  Notation "A + B" :=
    (sum A B)
    (at level 50, left associativity)
    : type_scope.
Setting B constr at next level
to match previous notation with longest common prefix:
"_ + _".

Аналогичные типы это:

• Result.t в OCaml
• Either в Haskell

Наш этот тип sum можно использовать для тех же целей, для которых используются его аналоги. Например, какой-то парсер может иметь тип: String -> AST + Error. То есть он либо попарсил успешно и вернул AST, либо не смог и вернул Error.

- Это смысл нашей передачи - наваливать кринге.
- Ты правда веришь, что у меня Лилит в первом доме и я устраиваю кринж?
- Конечно, моя луна подсвечивает твоё солнце, а это значит, что ты настоящий бунтарь.

А теперь задачки.

End My05.

Нам нужно будет работать со списками, поэтому сразу импортируем seq.

From mathcomp Require Import seq.

Module My06.

Практика: Язык арифметических выражений

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

  Inductive expr : Type :=
  | Const of nat
  | Plus of expr & expr
  | Minus of expr & expr
  | Mult of expr & expr.

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

  Declare Custom Entry expr.

Вот это вот выше означает, что мы объявляем expr идентификатором для нотации.

Сообщаем парсеру, что expr связан с двойными скобками. Это значит, что внутри двойных скобок парсер будет использовать нотации, связанные с нашим expr.

  Notation "'[[' e ']]'" :=
    e (e custom expr at level 0).

Делаем так, чтобы числа можно было использовать без обёртки в конструктор Const.

  Notation "x" :=
    (Const x)
      (in custom expr at level 0, x bigint).

  Notation "( x )" :=
    x (in custom expr, x at level 2).

  Notation "x + y" :=
    (Plus x y)
      (in custom expr at level 2, left associativity).

Упражнение 1: Определить нотации для вычитания и умножения.

Подсказки:

• меньший уровень означает более высокий приоритет
• нотации должны начинаться с in custom expr как выше

  Notation "x - y" :=
    (Minus x y)
      (in custom expr at level 2, left associativity).

  Notation "x * y" :=
    (Mult x y)
      (in custom expr at level 1, left associativity).

Вот как записывается Plus (Const 0) (Plus (Const 1) (Const 2)):

  Check [[0 + (1 + 2)]].
[[(0 + (1 + 2))]]
     : expr

А вот так Plus (Plus (Const 0) (Const 1)) (Const 2):

  Check [[(0 + 1) + 2]].
[[(0 + 1 + 2)]]
     : expr

Упражнение 2: Убедитесь, что следующие строки парсятся как ожидается. Какой запрос можно использовать для этого?

Можно выключить претти-принтинг нотаций и посмотреть глазами что именно там скрывается под ними.

  Unset Printing Notations.

  Check [[((0 + 1) + 2) + 3]].
Plus (Plus (Plus (Const 0) (Const 1)) (Const 2))
  (Const 3)
     : expr
  Check [[0 + (1 + (2 + 3))]].
Plus (Const 0)
  (Plus (Const 1) (Plus (Const 2) (Const 3)))
     : expr
  Check [[0 + 1 * 2]].
Plus (Const 0) (Mult (Const 1) (Const 2))
     : expr

  Set Printing Notations.

Вот тут ещё есть хороший пример работы с нотациями и я мб ниже ещё накину пару своих чуть более детальных примерчиков (если не забуду).

Упражнение 3: Напишите вычислитель для языка выражений, который определяет семантику. Семантика языка выражений должна совпадать с соответствующими функциями: addn, subn, muln.

Напишем:

  Fixpoint eval (e : expr) : nat :=
    match e with
    | Const n => n
    | Plus e1 e2 => eval e1 + eval e2
    | Minus e1 e2 => eval e1 - eval e2
    | Mult e1 e2 => eval e1 * eval e2
    end.

Тесты для eval.

Check erefl : eval [[ 0 - 4 ]] = 0.
erefl : eval [[(0 - 4)]] = 0
     : eval [[(0 - 4)]] = 0
Check erefl : eval [[ 0 + (2 - 1) ]] = 1.
erefl : eval [[(0 + (2 - 1))]] = 1
     : eval [[(0 + (2 - 1))]] = 1
Check erefl : eval [[ (0 + 1) + 2 ]] = 3.
erefl : eval [[(0 + 1 + 2)]] = 3
     : eval [[(0 + 1 + 2)]] = 3
Check erefl : eval [[ 2 + 2 * 2 ]] = 6.
erefl : eval [[(2 + 2 * 2)]] = 6
     : eval [[(2 + 2 * 2)]] = 6
Check erefl : eval [[ (2 + 2) * 2 ]] = 8.
erefl : eval [[((2 + 2) * 2)]] = 8
     : eval [[((2 + 2) * 2)]] = 8

Практика: Компиляция арифметических выражений в стековый язык

Брат, всегда сдавайся, не иди до конца.

Вот "низкоуровневый" стековый язык, который может служить целевым языком для компилятора из языка арифметических выражений выше:

  Inductive instr :=
  | Push (n : nat)
  | Add
  | Sub
  | Mul.

Программа на этом языке — список инструкций, каждая из которых манипулирует стеком натуральных чисел. Есть инструкции для помещения констант в стек, а также для сложения/вычитания/умножения двух верхних элементов стека, снятия их со стека и помещения результата обратно в стек.

Можно определить собственные нотации для операций со стеком, чтобы удобнее писать тесты. Сделаем их такими милыми кошечками, с ушками:

  Notation " <^ n ^> " :=
    (Push n) (at level 0, n constr).

  Notation "<^+^>" := Add (at level 1).
  Notation "<^-^>" := Sub (at level 1).
  Notation "<^*^>" := Mul (at level 1).

  Check <^5^> : instr.
<^ 5 ^> : instr
     : instr
  Unset Printing Notations.
  Check <^39^>.
Push 39
     : instr
  Check <^+^>.
Add
     : instr
  Check <^-^>.
Sub
     : instr
  Check <^*^>.
Mul
     : instr
  Set Printing Notations.

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

Кстати, seq — это просто нотация для стандартного типа list.

  Print seq.
Notation seq := list

Inductive list (A : Type) : Type :=
    nil : seq A | cons : A -> seq A -> seq A.

Arguments list A%type_scope
Arguments nil {T}%type_scope
  (where some original arguments have been renamed)
Arguments cons {T}%type_scope x s%seq_scope
  (where some original arguments have been renamed)
  Print list.
Inductive list (A : Type) : Type :=
    nil : seq A | cons : A -> seq A -> seq A.

Arguments list A%type_scope
Arguments nil {T}%type_scope
  (where some original arguments have been renamed)
Arguments cons {T}%type_scope x s%seq_scope
  (where some original arguments have been renamed)

^ Сильно вникать не надо, там дофига чего написано, надо просто посмотреть на первую строчку.

Можно создавать списки так:

• [::] — нотация для конструктора nil
• x :: xs — нотация для конструктора cons
• [:: 1; 2; 3] — последовательность из трёх элементов 1, 2 и 3

Вот пример:

Ну короче, используя seq, определим тип "прога" вот так:

  Definition prog := seq instr.

Пример проги (5 + 4) * 2 - 9:

  Check [:: <^5^>; <^4^>; <^+^>; <^2^>; <^*^>; <^9^>; <^-^>] : prog.
[:: <^ 5 ^>; <^ 4 ^>; <^+^>; <^ 2 ^>; <^*^>; <^ 9 ^>;
    <^-^>]
:
prog
     : prog

А тип "стек" так:

  Definition stack := seq nat.

  Compute [:: 1; 2; 3] ++ [::] : stack.
= [:: 1; 2; 3]
: stack

  Locate "++".
Notation "x ++ y" := (app x y) : list_scope
Notation "x ++ y" := (cat x y) : seq_scope
  (default interpretation)
  Print cat.
cat =
fun T : Type =>
fix cat (s1 s2 : seq T) {struct s1} : seq T :=
  match s1 with
  | [::] => s2
  | x :: s1' => x :: cat s1' s2
  end
     : forall {T : Type}, seq T -> seq T -> seq T

Arguments cat {T}%type_scope (s1 s2)%seq_scope

Упражнение 4: Реализовать функцию run - интерпретатор нашего стекового языка. Она принимает программу (список инструкций) и текущий стек, и исполняет программу пошагово, возвращая итоговый стек.

Я сделаю отдельно функцию "шага", мне так будет проще написать run.

  Fixpoint step (i : instr) (s : stack) : stack :=
    match i, s with
    | Push x, s' => x :: s'
    | Add, x :: y :: s' => (y + x) :: s'
    | Sub, x :: y :: s' => (y - x) :: s'
    | Mul, x :: y :: s' => (y * x) :: s'
    | _, s' => s'
    end.
Not a truly recursive fixpoint.
[non-recursive,fixpoints,default]

Тесты:

  Compute step <^+^> [:: 5; 4].
= [:: 9]
: stack
  Compute step <^+^> (step <^4^> (step <^5^> [::])).
= [:: 9]
: stack

  Compute step <^*^> [:: 9; 2].
= [:: 18]
: stack
  Compute step <^-^> [:: 18; 1].
= [:: 0]
: stack

  Fixpoint run (p : prog) (s : stack) : stack :=
    if p is i :: p'
    then run p' (step i s)
    else s.

Тесты:

  Compute run [:: <^1^>; <^2^>; <^+^>] [::].
= [:: 3]
: stack

  Compute run
    [::
       <^5^>; <^4^>; <^+^>;
       <^2^>; <^*^>;
       <^1^>; <^-^>
    ] [::].
= [:: 17]
: stack

  Check erefl :
    run
      [::
         <^5^>; <^4^>; <^+^>;
         <^2^>; <^*^>;
         <^1^>; <^-^>
      ] [::] = [:: 17].
erefl
:
run
  [:: <^ 5 ^>; <^ 4 ^>; <^+^>; <^ 2 ^>; <^*^>;
      <^ 1 ^>; <^-^>] [::] = [:: 17]
     : run
         [:: <^ 5 ^>; <^ 4 ^>; <^+^>; <^ 2 ^>; <^*^>;
             <^ 1 ^>; <^-^>] [::] = [:: 17]

Упражнение 5: Реализовать функцию compile - компилятор из "высокоуровневых" выражений в "низкоуровневые" стековые программы и написать несколько тестов.

Идеи для тестов:

• Проверить, что run (compile e) [::] = [:: eval e], где e — произвольное выражение
• Проверить, что compile — инъективная функция

  Fixpoint compile (e : expr) : prog :=
    match e with
    | Const x => [:: <^x^>]
    | Plus x y => compile x ++ compile y ++ [:: <^+^>]
    | Minus x y => compile x ++ compile y ++ [:: <^-^>]
    | Mult x y => compile x ++ compile y ++ [:: <^*^>]
    end.

Тесты:

  Unset Printing Notations.
  Check compile [[ (5 + 4) * 2 - 9 ]].
compile
  (Minus (Mult (Plus (Const 5) (Const 4)) (Const 2))
     (Const 9))
     : prog
  Set Printing Notations.

То, что надо.

  Check erefl :
    compile [[ (5 + 4) * 2 - 9 ]] =
      [:: <^5^>; <^4^>; <^+^>; <^2^>; <^*^>; <^9^>; <^-^>].
erefl
:
compile [[((5 + 4) * 2 - 9)]] =
[:: <^ 5 ^>; <^ 4 ^>; <^+^>; <^ 2 ^>; <^*^>; <^ 9 ^>;
    <^-^>]
     : compile [[((5 + 4) * 2 - 9)]] =
       [:: <^ 5 ^>; <^ 4 ^>; <^+^>; <^ 2 ^>; <^*^>;
           <^ 9 ^>; <^-^>]

Теперь проверим, что run (compile e) [::] = [:: eval e].

  Check erefl :
    run (compile [[ (5 + 4) * 2 - 9 ]]) [::] =
      [:: eval [[ (5 + 4) * 2 - 9 ]]].
erefl
:
run (compile [[((5 + 4) * 2 - 9)]]) [::] =
[:: eval [[((5 + 4) * 2 - 9)]]]
     : run (compile [[((5 + 4) * 2 - 9)]]) [::] =
       [:: eval [[((5 + 4) * 2 - 9)]]]

Убедимся, что compile - инъективная функция. По определению инъективности это означает, что нам хочется проверить вот такое свойство \(f(x_1) = f(x_2) \Rightarrow x_1 = x_2\). Хм, опробуем понять что это может значить в нашем случае для compile:

compile(e1) = compile(e2) => e1 = e2

Ну, наверное, от нас хотят рассуждения вроде таких:

• eval(e1) = eval(e2) => e1 = e2
• run(is1) = run(is2) => is1 = is2
• run(compile(e1)) = run(compile(e2)) => eval(e1) = eval(e2) => e1 = e2

Фиг знает.

Упражнение 5: Реализуйте декомпилятор, преобразующий стековую программу prog обратно в выражение expr.

Подсказка: Возможно, стоит ввести рекурсивный вспомогательный метод decompile' для переиспользования в decompile.

Тут задача сводится к преобразованию списка инструкций в дерево выражений.

  Fixpoint decompile' (p : prog) (s : seq expr) : option (seq expr) :=
    match p with
    | [::] => Some s
    | i :: p' =>
      match i with
      | Push x => decompile' p' (Const x :: s)
      | Add =>
        match s with
        | e2 :: e1 :: es => decompile' p' (Plus e1 e2 :: es)
        | _ => None
        end
      | Sub =>
        match s with
        | e2 :: e1 :: es => decompile' p' (Minus e1 e2 :: es)
        | _ => None
        end
      | Mul =>
        match s with
        | e2 :: e1 :: es => decompile' p' (Mult e1 e2 :: es)
        | _ => None
        end
      end
    end.

  Compute decompile' [:: <^5^>; <^4^>; <^+^>; <^2^>; <^*^>].
= fun s : seq expr =>
  Some ([[((5 + 4) * 2)]] :: s)
: seq expr -> option (seq expr)

  Definition decompile (p : prog) : option expr :=
    match decompile' p [::] with
    | Some [:: e] => Some e
    | _ => None
    end.

  Check erefl :
    decompile [:: <^5^>; <^4^>; <^+^>; <^2^>; <^*^>; <^1^>; <^-^>] =
      Some [[ (5 + 4) * 2 - 1 ]].
erefl
:
decompile
  [:: <^ 5 ^>; <^ 4 ^>; <^+^>; <^ 2 ^>; <^*^>;
      <^ 1 ^>; <^-^>] = Some [[((5 + 4) * 2 - 1)]]
     : decompile
         [:: <^ 5 ^>; <^ 4 ^>; <^+^>; <^ 2 ^>; <^*^>;
             <^ 1 ^>; <^-^>] =
       Some [[((5 + 4) * 2 - 1)]]

End My06.

From mathcomp Require Import ssreflect ssrfun.
Set Implicit Arguments.

Module My07.

Импликация

Импликация соответствует типу функции. Доказательство утверждения "A влечет B" — это просто функция типа A -> B, которая преобразует доказательство A в доказательство B.

Вот доказательство того, что из A следует A:

  Definition a_implies_a (A : Prop) :
    A -> A
  :=
    fun proof_of_a : A => proof_of_a.

Это просто тождественная функция, как мы уже видели ранее и её можно понимать как лемму под названием a_implies_a.

Мы используем вселенную Prop — это примитив Coq, о котором будет рассказано чуть ниже. Сейчас достаточно знать, что A : Prop значит "A — это высказывание".

Еще один пример:

  Definition A_implies_B_implies_A (A B : Prop) :
    A -> B -> A
  :=
    fun proof_a => fun proof_b => proof_a.

Это соответствует функции const.

А modus ponens - это просто применение функции:

  Definition modus_ponens (A B : Prop) :
    A -> (A -> B) -> B
  :=
    fun p_a p_a_impl_b => p_a_impl_b p_a.

Конъюнкция

Конструктивное доказательство конъюнкции \(A \land B\) — это пара доказательств A и B:

   Inductive and (A B : Prop) : Prop :=
   | conj of A & B.

   Notation "A /\ B" := (and A B) : type_scope.

Заметь, насколько and похож на prod:

Inductive prod (A B : Type) : Type :=
  | pair of A & B.

Докажем, что конъюнкция коммутативна.

  Definition andC (A B : Prop) :
    A /\ B -> B /\ A
  :=
    fun p_a_and_b =>
      match p_a_and_b with
      | conj p_a p_b => conj p_b p_a
      end.

Это доказательство выглядит точь‑в‑точь как функция, переставляющая местами компоненты пары.

Дизъюнкция

Конструктивное доказательство дизъюнкции \(A \lor B\) — это либо доказательство A, либо доказательство B, плюс "тэг/метка", показывающая, какое именно из высказываний доказано. Короче, определение дизъюнкции выглядит так:

  Inductive or (A B : Prop) : Prop :=
  | or_introl of A
  | or_intror of B.

  Notation "A \/ B" := (or A B) : type_scope.

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

  Arguments or_introl [A] B _, [A B] _.
  Arguments or_intror [A] B _, [A B] _.

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

В примере выше у нас 2 варианта:

Вариант [A] B _

Используется в случае применения конструктора or_introl (or_intror) к двум аргументам и означает, что:

• Первый аргумент [A] может быть выведен неявно
• Второго аргумент B нужно подставить самому (явно)
• _ это само доказательство A, ну т.е. это or_introl of A

[A] можно вывести неявно потому, что доказательство or_introl of A уже имеет тип A. Ну просто потому что все конструкторы наследуют параметры самого индуктивного типа, который они конструируют:

  Check or_introl.
or_introl
     : forall A B : Prop, A -> A \/ B

Вариант [A B] _

Иногда B может быть выведен из контекста (ниже будет пример такого случая). Так вот в варианте [A B] _ мы говорим, что если or_introl применён к всего лишь одному аргументу, то нужно вывести из контекста оба утверждения: A и B (если не получится это сделать, то будет ошибка).

И снова — полное сходство с sum:

Inductive sum (A B : Type) : Type :=
| inl of A
| inr of B.

Разница лишь в том, что or живёт во вселенной Prop, а sum — в Type.

А вот так будет выглядеть конструктивной логике доказательство дистрибутивности конъюнкции (логического "и") над дизъюнкцией (логическим "или")

\((A \lor B) \land C \to (A \land C) \lor (B \land C)\)

  Definition and_or_distr (A B C : Prop) :
    (A \/ B) /\ C -> (A /\ C) \/ (B /\ C)
  :=
    fun '(conj p_a_or_b p_c) =>
      match p_a_or_b with
      | or_introl p_a => or_introl (conj p_a p_c)
      | or_intror p_b => or_intror (conj p_b p_c)
      end.

Ну смысл понятен, да? Мы просто конструируем штуки всякие. Поэтому и логика такая называется "конструктивная". А как мы их конструируем? - Мы пишем функции.

Истинное высказывание

Тривиально истинное высказывание не несет никакой информации, и его доказательство тоже должно быть тривиальным. Поэтому истинное высказывание — это, по сути, юнит-тип во вселенной Prop. У него ровно один конструктор с историческим именем I.

  Inductive True : Prop :=
  | I.

Истина всегда остаётся истиной, вне зависимости от любых посылок.

  Definition anything_implies_true (A : Prop) :
    A -> True
  :=
    fun _ => I.

  Definition true_and_true :
    True /\ True
  :=
    conj I I.

Ложь

Ложь это пустой тип во вселенной Prop, у него нет конструкторов.

  Inductive False : Prop := .

Так как у False нет конструкторов, его нельзя доказать без дополнительных предположений — то есть в пустом контексте, если только в самом Coq нет критических багов (а они иногда бывают). Команда разработчиков даже держит список таких багов.

Поскольку у False нет конструкторов, выражение сопоставления с образцом для него имеет интересную форму: ветвей нет, а значит, можно построить терм любого типа, потому что ничего определять не нужно. Это известный принцип взрыва (ex falso quodlibet) — из лжи следует всё. Вот пример:

  Definition exfalso_quodlibet {A : Prop} :
    False -> A
  :=
    fun (p_f : False) => match p_f with end.

Ещё простой пример:

  Definition a_or_false_implies_a (A : Prop) :
    A \/ False -> A
  :=
    fun p_a_or_f =>
      match p_a_or_f with
      | or_introl p_a => p_a
      | or_intror p_f => exfalso_quodlibet p_f
      end.

Отрицание

Под not A (или ~ A) понимают короткую запись для A -> False.

  Definition not (A : Prop) := A -> False.
  Notation "~ A" := (not A) : type_scope.

Чтобы доказать A -> ~~A, нужно помнить, что это значит:

A -> (A -> False) -> False:

  Definition dni (A : Prop) : (* double negation introduction *)
    A -> ~ ~A
  :=
    fun (p_a : A) => fun p_not_a => p_not_a p_a.

Логика, построенная таким образом, называется интуиционистской. В ней, как известно, нельзя в общем случае доказать классический принцип устранения двойного отрицания (DNE - double negation elimination), то есть нельзя построить терм типа ~~A -> A для произвольного A:

  Fail Definition dne (A : Prop) :
    ~ ~ A -> A
  :=
    fun not_not_a => _.
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
  (fun (A : Prop) (not_not_a : ~ ~ A) => ?a)
More precisely: 
- ?a: Cannot infer this placeholder of type "A" in
  environment:
  A : Prop
  not_not_a : ~ ~ A

Всё что у нас есть это терм вот такого типа not_not_a: (A -> False) -> False. Это ф-ция, но мы её "вызвать" не можем, тк у нас нет ни A ни (A -> False).

Тоже самое и с законом исключённого третьего (LEM - law of excluded middle):

  Fail Definition lem (A : Prop) :
    A \/ ~ ~ A := _.
The command has indeed failed with message:
The following term contains unresolved implicit arguments:
  (fun A : Prop => ?o)
More precisely: 
- ?o: Cannot infer this placeholder of type
  "A \/ ~ ~ A" in environment:
  A : Prop

Без сахара это A \/ (A -> False). Чтобы доказать дизъюнкцию нам нужно доказать правый либо левый дизъюнкт, а мы не можем ни то ни другое сконструировать.

Логическая эквивалентность (двойная импликация)

Как и отрицание, логическая эквивалентность не является first-class коннектором в Coq. Вместо этого есть определение iff, которое означает конъюнкцию двух импликаций + нотация <->.

  Definition iff (A B : Prop) := (A -> B) /\ (B -> A).
  Notation "A <-> B" := (iff A B) : type_scope.

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

Квантор всеобщности

Доказательство высказывания \(\forall x. P(x)\) — это функция, которая принимает какой-то конкретный \(x\) и возвращает доказательство \(P(x)\) и тип вот этого доказательства зависит от x.

Ну то есть у нас есть некий \(x\) и утверждение \(P(x)\), тип которого меняется в зависимости от \(x\). Это значит, что \(P(x_1)\) и \(P(x_2)\) имеют разные типы. Ну а это ровно то, чем является зависимая функция в теории типов.

Здесь мы не можем сами определить этот тип зависимых функций (квантор \(\forall\)), потому что это примитив Coq.

Короче вот то, что описано выше словами:

forall x : T, P x, где P : T -> Prop

это предикат (функция из типа в Prop).

Пример:

  Definition forall_andD (A : Type) (P Q : A -> Prop) :
    (forall x, P x /\ Q x) -> (forall x, P x) /\ (forall x, Q x)
  :=
    fun all_p_and_q =>
      conj
        (fun x => match all_p_and_q x with | conj px _ => px end)
        (fun x => match all_p_and_q x with | conj _ qx => qx end).

В этом примере:

• all_p_and_q : (x : T) -> P x /\ Q x
• forall x, P x : (x : T) -> P x
• forall x, Q x : (x : T) -> Q x

Квантор существования

Вот как это выглядит:

  Inductive ex (A : Type) (P : A -> Prop) : Prop :=
  | ex_intro (x : A) (proof : P x).

Получаем тип, обобщающий конъюнкцию (\(\land\)), только теперь тип второго компонента зависит от значения первого.

Упрощённая нотация, для одной переменной:

Notation "'exists' x : A , P" :=
  (ex (fun (x : A) => P))
    (at level 200, right associativity).

Общая нотация:

  Notation "'exists' x .. y , p" :=
    (ex (fun x => .. (ex (fun y => p)) ..))
    (at level 200, x binder, right associativity,
    format "'[' 'exists'  '/  ' x  ..  y ,  '/  ' p ']'")
    : type_scope.

Сложная нотация. Разберёмся что тут вообще происходит.

1. Нотация exists x y, p — это сокращённо от ex (fun x => ex (fun y => p)), т.е. вложенное существование: \(\exists x\), \(\exists y\), и при этом \(p\) истинно.

2. Команда binder x — позволяет коку понять, что x это переменная-байндер. Так он сможет распарсить такой список переменных подряд: x .. y не просто как список символов, а как цепочку связанных переменных.

3. format — отвечает за претти-принтинг. Позволяет нам напечатать выражение exists x y, p вот так:

[ exists
  x y,
  p
]

То есть символы '[' и ']' это просто визуальное оформление, / — перевод строки с отступом, а сама запись становится читабельнее в доказательствах.

Пример рассуждения с квантором существования:

  Definition exists_p_x_impl_not_all_not_p_x A (P : A -> Prop) :
    (exists x, P x) -> ~ (forall x, ~ P x)
  :=
    fun (ex_p_x : exists x, P x) =>
      fun (not_all_not_p_x : forall x, ~ P x) =>
        match ex_p_x with
        | ex_intro x p_x => not_all_not_p_x x p_x
        end.

Чтобы легко парсить в голове утверждения, в которых присутствует ложь, важно помнить чем является ложь в конструктивной логике:

~ A \(\equiv\) A -> False

поэтому

not_all_not_p_x : ~ (forall x, ~ P x)

есть просто

not_all_not_p_x : (forall x, P x -> False) -> False

и поэтому

not_all_not_p_x x p_x : False

Мы ему дали конкретный \(x\) для которого выполняется \(P(x)\) и само \(P\).

Каррирование для зависимых пар:

  Definition curry_dep A (P : A -> Prop) Q :
    ((exists x, P x) -> Q) -> (forall x, P x -> Q)
  :=
    fun f : (exists x, P x) -> Q =>
      fun x : A =>
        fun px : P x =>
          f (ex_intro _ x px).

• A - это тип, поэтому его явно не надо передавать, кок его выведет
• P является зависимым предикатом (функцией из элементов типа A в Prop), и его можно явно передавать в ex_into, либо использовать _, чтобы кок его вывел за нас

Равенства

Одна из центральных тем теории типов. Там существует целая иерархия понятий равенства или эквивалентности.

Равенство по определению

Не известно корректный ли термин, но в оригинале это definitional equality.

На мета-уровне существует встроенное понятие равенства между термами. Оно утверждает, что любые два терма равны, если можно свести один к другому вычислениями (т.е. если они "конвертируемы"). Такое равенство нельзя доказать, такие равенства - внутренняя механика кока. То есть, насколько я понял, кок просто запускает вычисление, смотрит на редуцированную пару термов и заключает "равны" они или нет.

Пропозициональное равенство

Мы можем ввести равенство по определению внутрь языка с помощью вот такого идуктивного типа eq:

  Inductive eq (A : Type) (x : A) : A -> Prop :=
  | eq_refl : eq x x.

Это и называется пропозициональное равенство. Единственное свойство, заложенное в этом равенстве — рефлексивность.

Это первая встреча с индексированными типами и надо бы разобраться.

В этом определении тип A после двоеточия называется индексом, а x — параметром. Параметры должны быть одинаковыми для всех конструкторов, а индексы могут меняться. В данном случае конструктор один, поэтому вариантов нет. Но именно благодаря такому механизму паттерн-матчинг позволяет симулировать равенство между термами.

End My07.