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

Почему следующее не проверяет тип (coq-8.5pl3)? Сопоставление с образцом, кажется, забывает, что u и v имеют один и тот же тип.

Inductive X : Type -> Type :=
| XId : forall a, X a -> X a
| XUnit : X unit.

Fixpoint f {a : Type} (x : X a) (y : X a) : a :=
  match x, y with
  | XId _ u, XId _ v => f u v
  | XUnit, _ => tt
  | _, XUnit => tt
  end.

Сообщение об ошибке:

Error:
In environment
f : forall a : Type, X a -> X a -> a
a : Type
x : X a
y : X a
T : Type
u : X T
y0 : X T
T0 : Type
v : X T0
The term "v" has type "X T0"
while it is expected to have type "X T".

pattern-matching dependent-type coq
person Li-yao Xia    schedule 12.06.2017    source источник
comment
Попробуйте найти шаблон конвоя на SO или в CPDT   -  person Anton Trunov    schedule 13.06.2017
comment
Это то, что я искал. Спасибо!   -  person Li-yao Xia    schedule 13.06.2017

Ответы (1)


arrow_upward
2
arrow_downward

Благодаря подсказке Антона Трунова о "паттерне конвоя" мне удалось сделать версию, которая компилируется.

Fixpoint f {a : Type} (x : X a) : X a -> a :=
  match x in X a return X a -> a with
  | XId b u => fun y => match y in X b return X b -> b with
                        | XId c v => fun u => f u v
                        | XUnit => fun _ => tt
                        end u
  | XUnit => fun _ => tt
  end.
person Li-yao Xia    schedule 12.06.2017