у меня есть проблемы, доказывающий типа второй проекции от типа сигмы: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
более здраво и/или сделать это принуждение?
EDIT: Я полагаю, при условии, свидетель Phy x
необходимо из-за способа existT
declared является: existT (x:A) (_:P x)
. Вот лучший вариант 2 последних строк кода выше (до сих пор не может сделать его принуждением):
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*)
Удивительно, но это работает для принуждения. Зачем? Было ли это, что 2 не взаимозаменяемые 'X'-s нарушили равномерное условие наследования (или есть более простое объяснение)? – jaam
Ну, это всего лишь проекция. В stdlib эта функция называется 'projT2'. –
ОК. Но почему «Определение e {x: X} {h: Phy x}: PhyX -> Phy x: = fun _ => projT2 (existT _ _ h)' нарушило UIC? – jaam