Сопоставление с образцом

Выражение match разбирает значение индуктивного типа, объявленного командой #data, по одной ветви на конструктор. Это нотация для порождённых элиминаторов, в духе дисциплины Epigram¹, недавно возрождённой проектом Pterodactyl²: при проверке типов каждое match элаборируется в применение ind-<имя> (или rec-<имя>, если цель не зависит от разбираемого значения), поэтому вычисление и завершимость устроены в точности как у элиминаторов.

#lang rzk-1
#data nat := zero | suc (n : nat)

Ветвь называет конструктор и связывает по одной переменной на каждый аргумент метода: поля конструктора, затем по одной индуктивной гипотезе на каждое рекурсивное поле, по порядку. Стрелка ветви — ⇒ (ASCII =>).

#define plus
  ( n m : nat)
  : nat
  := match n
      ( zero ⇒ m
      | suc k ih ⇒ suc ih)

Здесь ih обозначает plus k m, результат рекурсии по k. Рекурсия возможна только через индуктивные гипотезы, поэтому всякое match завершается по построению. Вычисление дефинициональное:

#define plus-two-two
  : plus (suc (suc zero)) (suc (suc zero)) =_{nat} suc (suc (suc (suc zero)))
  := refl

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

Модальное сопоставление

Форма match μ x (...) проверяет разбираемое выражение x под модальностью μ и использует элиминатор, сгенерированный для этой модальности. Тип D без конструкторов путей порождает ind-D и rec-D для тождественной модальности, а также ind-op-D/rec-op-D и ind-b-D/rec-b-D. Это принципы «чёткой» (crisp) индукции, верные для левых сопряжённых ᵒᵖ и ♭. Для ♯ их нет: как правый сопряжённый, ♯ не сохраняет копроизведения и рекурсию, поэтому match _# x (...) отвергается.

#data Nat := zero | suc (pred : Nat)

#define modal-predecessor (n :_b Nat) : _b Nat
  := match _b n
       (zero => mod _b zero
       | suc pred _ => mod _b pred)

Если поле конструктора объявлено под модальностью ν, его биндер в модальном элиминаторе и соответствующая переменная ветви получают μ · ν. Сгенерированные индуктивные гипотезы остаются обычными; _ в примере — такая неиспользуемая гипотеза. Параметры типа данных, индексы, shape-поля и их guards также наследуют μ.

Форма с явным мотивом записывается match μ x into motive (...). Для неиндексированного типа D мотив имеет тип (z :_μ D) → U. Для индексированного типа каждая связывающая переменная телескопа мотива наследует μ, поэтому для одного обычного индекса мотив имеет тип (i :_μ I) → (z :_μ D i) → U. Высшие индуктивные типы пока порождают только ind-D и rec-D; модальное сопоставление по ним отклоняется, поскольку для него нужна модальная индукция по путям.

Поскольку модальность сразу после match выбирает эту форму, для обычного match по выражению с модальным префиксом нужны скобки: match (mod ♭ x) (...).

Мотив

match в позиции проверки берёт мотив из ожидаемого типа: если разбираемое выражение — переменная, она абстрагируется из цели, и ветви видят цель на каждом конструкторе. Так получается зависимое сопоставление через подстановку:

#define plus-zero
  ( n : nat)
  : plus zero n =_{nat} n
  := refl

#define zero-plus
  ( n : nat)
  : plus n zero =_{nat} n
  := match n
      ( zero ⇒ refl
      | suc k ih ⇒
          idJ
            ( nat , plus k zero
            , \ z q → suc (plus k zero) =_{nat} suc z
            , refl , k , ih))

В ветви suc цель — plus (suc k) zero =_{nat} suc k, и доступна гипотеза ih : plus k zero =_{nat} k; индукция по путям над ih даёт конгруэнтность для suc, завершающую доказательство.

Если разбираемое выражение — не переменная, мотив постоянен: цель не должна от него зависеть. Наконец, явный мотив записывается после into. Это семейство, в которое ведёт сопоставление, применяемое к индексам и разбираемому значению:

#define plus'
  ( n m : nat)
  : nat
  := match n into (\ _ → nat)
      ( zero ⇒ m
      | suc k ih ⇒ suc ih)

match без into принимается только там, где его тип уже известен. В позиции вывода (например, под #compute) мотив нужно указать явно.

Приём «конвой»

Чтобы ветвь могла использовать гипотезу при уточнённом разбираемом значении, сделайте мотив функциональным типом и примените match к гипотезе снаружи (приём «конвой» из фольклора Coq³). Например, при

#data bool := false | true

#define not
  ( b : bool)
  : bool
  := match b
      ( false ⇒ true
      | true ⇒ false)

доказательство C (not (not b)) из h : C b нельзя получить прямым разбором b: в ветви true цель становится C (not (not true)), но h по-прежнему имеет тип C b для неуточнённого b. Протаскивание h через мотив уточняет обе стороны сразу:

#define convoy
  ( C : bool → U)
  ( b : bool)
  ( h : C b)
  : C (not (not b))
  := (match b into (\ b' → C b' → C (not (not b')))
        ( false ⇒ \ h' → h'
        | true ⇒ \ h' → h')) h

В каждой ветви аргумент h' имеет тип C на конструкторе, а C (not (not true)) вычисляется в C true, так что достаточно тождественной функции.

Индексированные семейства

Разбор значения индексированного семейства устроен так же. Мотив после into абстрагирует индексы перед разбираемым значением:

#data vec
  ( A : U)
  : nat → U
  :=
    nil : vec A zero
  | cons (n : nat) (x : A) (xs : vec A n) : vec A (suc n)

#define vlen
  ( A : U)
  ( n : nat)
  ( xs : vec A n)
  : nat
  := match xs
      ( nil ⇒ zero
      | cons k x tail ih ⇒ suc ih)

Мотив может использовать индексы. Например, безопасная голова на vec A (suc n) вычисляет свой мотив вложенным разбором индекса, так что ветвь nil должна дать Unit, а ветвь cons — элемент A:

#define vhead
  ( A : U)
  ( n : nat)
  ( xs : vec A (suc n))
  : A
  := match xs into (\ k v → match k (zero ⇒ Unit | suc j jh ⇒ A))
      ( nil ⇒ unit
      | cons k x tail ih ⇒ x)

Если цель зависит от индексов переменной, по которой идёт разбор, построенный мотив оставляет индексы фиксированными, что для индукции обычно не годится. В этом случае запишите зависимый мотив через into.

Высшие индуктивные типы

match распространяется на конструкторы путей без изменений, как нотация для элиминаторов. Ветвь конструктора пути проверяется против соответствующего типа метода, который зависит от ветвей конструкторов точек. Если цель не упоминает разбираемое значение, match разворачивается через rec, поэтому ветвь loop ниже проверяется против base = base — уравнения, которое определяет ветвь base:

#data S¹
  :=
    base
  | loop : base =_{S¹} base

#define S¹-id
  ( x : S¹)
  : S¹
  := match x (base ⇒ base | loop ⇒ loop)

На конструкторе пути ничего не вычисляется дефиниционально; пропозициональная замена — порождённые правила compute- (см. #data).

---

1. Conor McBride and James McKinna. The view from the left. Journal of Functional Programming 14(1), pp. 69–111, 2004. https://doi.org/10.1017/S0956796803004829 ↩

2. Jon Sterling. Is it time for a new proof assistant? Talk at the Homotopy Type Theory Electronic Seminar Talks (HoTTEST), 25 September 2025. https://www.youtube.com/watch?v=7oBkEbKJvnE ↩

3. Adam Chlipala. Certified Programming with Dependent Types. MIT Press, 2013. http://adam.chlipala.net/cpdt/ — приём «конвой» назван в §8.4 (Dependently Typed Red-Black Trees) главы 8, More Dependent Types, http://adam.chlipala.net/cpdt/html/MoreDep.html. ↩