Coq: определение функции от сигма-типа до ее второй проекции (и превращение ее в приведение)

У меня возникли проблемы с доказательством типа второй проекции из сигма-типа:

Variable X:Type.
Variable Phy: X -> Type.
Definition e {x:X}: {x:X & Phy x} -> Phy x. 
intro. Fail exact (@projT2 _ _ X0).
(*The term "projT2 X0" has type "Phy (projT1 X0)"
while it is expected to have type "Phy x" (cannot unify
"(fun x : X => Phy x) (projT1 X0)" and "Phy x").*)

Является ли свидетельство {x:X & Phy x} (или {x:X | Phy x}) недостаточным для получения свидетельства Phy x через проекции? В любом случае, я мог бы определить e (более глупо), приняв свидетелей. Кроме того, я хочу сделать это принуждением (но не удается):

Reset e.
Definition PhyX := {x:X & Phy x}.
Definition e {x:X} {z:Phy x} {y:PhyX}: PhyX -> Phy x := fun y => z.
Coercion e: PhyX >-> Funclass. (*e does not respect the uniform inheritance condition*)

Теперь к вопросу: Могу ли я определить e более разумно и/или сделать его принуждением?

РЕДАКТИРОВАТЬ: я предполагаю, что свидетельство Phy x необходимо из-за того, как existT объявлен: existT (x:A) (_:P x). Вот лучшая версия двух последних строк кода выше (все еще не удалось сделать это принуждением):

Definition e {x:X} {h:Phy x}: PhyX -> Phy x := fun _ => projT2 (existT _ _ h).
Coercion e: PhyX >-> Phy. (*e does not respect the uniform inheritance condition*)

types subtype coercion coq proof
person jaam    schedule 20.02.2017    source источник

Ответы (1)


arrow_upward
1
arrow_downward

В вашем определении есть два значения X: одно указано в качестве аргумента с {x:X}, а другое скрыто в сигме. Эти два не взаимозаменяемы.

Что вы можете сделать, так это:

Definition e (p : {x:X & Phy x}) : Phy (projT1 p).
  destruct p; simpl; assumption.
Defined.
person John Wiegley    schedule 22.02.2017
comment
Удивительно, но это работает для принуждения. Почему? Было ли это тем, что 2 невзаимозаменяемых X нарушили условие равномерного наследования (или есть более простое объяснение)? - person jaam; 23.02.2017
comment
Ну это просто проекция. В стандартной библиотеке эта функция называется projT2. - person John Wiegley; 24.02.2017
comment
ХОРОШО. Но почему Definition e {x:X} {h:Phy x}: PhyX -> Phy x := fun _ => projT2 (existT _ _ h) нарушил UIC? - person jaam; 25.02.2017
comment
Я не уверен, что вы подразумеваете под нарушением UIC? Это определение типа проверяет. - person John Wiegley; 26.02.2017
comment
Условие равномерного наследования. Это связано с приведением - person jaam; 28.02.2017