Получение ограничений из GADT для обеспечения исчерпания соответствия шаблонов в Coq - PullRequest
Новая
       77

Получение ограничений из GADT для обеспечения исчерпания соответствия шаблонов в Coq

1 голос
/ 10 июня 2019

Давайте определим два вспомогательных типа: 

Inductive AB : Set := A | B.
Inductive XY : Set := X | Y.

Затем два других типа, которые зависят от XY и AB

Inductive Wrapped : AB -> XY -> Set :=
| W : forall (ab : AB) (xy : XY), Wrapped ab xy
| WW : forall (ab : AB), Wrapped ab (match ab with A => X | B => Y end)
.

Inductive Wrapper : XY -> Set :=
  WrapW : forall (xy : XY), Wrapped A xy -> Wrapper xy.

Обратите внимание на конструктор WW - он можетбыть только значениями типов Wrapped A X и Wrapped B Y.

Теперь я хотел бы сопоставить шаблон с Wrapper Y: 

Definition test (wr : Wrapper Y): nat :=
  match wr with
  | WrapW Y w =>
    match w with
    | W A Y => 27
    end
  end.

, но я получаю ошибку 

Error: Non exhaustive pattern-matching: no clause found for pattern WW _

Почему это происходит?Силами Wrapper, содержащими Wrapped в версии A, конструкторы сигнатур типов Y и WW запрещают быть одновременно A и Y.Я не понимаю, почему этот случай даже рассматривается, хотя я вынужден проверить, что кажется невозможным.

Как обойти эту ситуацию?

Ответы [ 2 ]

3 голосов
/ 10 июня 2019

Давайте упростим: 

Inductive MyTy : Set -> Type :=
  MkMyTy : forall (A : Set), A -> MyTy A.

Definition extract (m : MyTy nat) : nat :=
  match m with MkMyTy _ x => S x end.

Это не удалось: 

The term "x" has type "S" while it is expected to have type "nat".

ваты.

Это потому что я сказал 

Inductive MyTy : Set -> Type

Это сделал первый аргумент MyTy индексом MyTy, в отличие от параметра. Индуктивный тип с параметром может выглядеть так: 

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

Параметры именуются слева от : и не являются forall -d в определении каждого конструктора. (Они по-прежнему присутствуют в типах конструкторов вне определения: cons : forall (A : Type), A -> list A -> list A.) Если я сделаю Set параметром MyTy, то можно определить extract: 

Inductive MyTy (A : Set) : Type :=
  MkMyTy : A -> MyTy A.

Definition extract (m : MyTy nat) : nat :=
  match m with MkMyTy _ x => S x end.

Причина этого в том, что внутри match игнорирует все, что вы знаете об индексах проверяемого извне. (Или, скорее, базовое выражение match в Gallina игнорирует индексы. Когда вы пишете match в исходном коде, Coq пытается преобразовать его в примитивную форму, в то же время включая информацию из индексов, но это часто не удается. ) То, что m : MyTy nat в первой версии extract просто не имело значения. Вместо этого совпадение дало мне S : Set (имя было автоматически выбрано Coq) и x : S, согласно конструктору MkMyTy, без упоминания nat. Между тем, поскольку у MyTy есть параметр во второй версии, я на самом деле получаю x : nat. На этот раз _ действительно заполнитель; его обязательно нужно записать как _, потому что нечего сопоставлять, и вы можете Set Asymmetric Patterns, чтобы он исчез.

Причина, по которой мы различаем параметры и индексы, заключается в том, что параметры имеют множество ограничений - особенно, если I является индуктивным типом с параметрами, тогда параметры должны появляться как переменные в типе возврата каждого конструктора: 

Inductive F (A : Set) : Set := MkF : list A -> F (list A).
                                            (* ^--------^ BAD: must appear as F A *)

В вашей задаче мы должны указать параметры там, где можем. Например. бит match wr with Wrap Y w => _ end неверен, поскольку аргумент XY для Wrapper является индексом, поэтому тот факт, что wr : Wrapper Y игнорируется; вам также нужно будет заняться делом Wrap X w. Coq не удосужился сказать вам это. 

Inductive Wrapped (ab : AB) : XY -> Set :=
| W : forall (xy : XY), Wrapped ab xy
| WW : Wrapped ab (match ab with A => X | B => Y end).

Inductive Wrapper (xy : XY) : Set := WrapW : Wrapped A xy -> Wrapper xy.

А теперь ваш test компилирует (почти): 

Definition test (wr : Wrapper Y): nat :=
  match wr with
  | WrapW _ w => (* mandatory _ *)
    match w with
    | W _ Y => 27 (* mandatory _ *)
    end
  end.

, поскольку наличие параметров дает Coq достаточно информации для его match -разработки, чтобы использовать информацию из индекса Wrapped. Если вы введете Print test., вы увидите, что есть небольшой скачок для передачи информации об индексе Y через примитив match s, который в противном случае игнорировал бы его. См. Справочное руководство для получения дополнительной информации.

2 голосов
/ 10 июня 2019

Решение оказалось простым, но хитрым: 

Definition test (wr : Wrapper Y): nat.
  refine (match wr with
  | WrapW Y w =>
    match w in Wrapped ab xy return ab = A -> xy = Y -> nat with
    | W A Y => fun _ _ => 27
    | _ => fun _ _ => _
    end eq_refl eq_refl
  end);
[ | |destruct a]; congruence.
Defined.

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

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

  • ab очевидно A
  • xy очевидно Y

Я рассмотрел реальные случаи, игнорируя эти предположения, и я отложил «плохие» случаипозже будет доказано, что это оказалось тривиальным.Я был вынужден передать eq_refl s вручную, но это сработало и выглядит не так уж плохо.

...