2017-02-20 23 views
1

у меня есть проблемы, доказывающий типа второй проекции от типа сигмы: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 необходимо из-за способа existTdeclared является: 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*) 

ответ

1

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

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

Definition e (p : {x:X & Phy x}) : Phy (projT1 p). 
    destruct p; simpl; assumption. 
Defined. 
+0

Удивительно, но это работает для принуждения. Зачем? Было ли это, что 2 не взаимозаменяемые 'X'-s нарушили равномерное условие наследования (или есть более простое объяснение)? – jaam

+0

Ну, это всего лишь проекция. В stdlib эта функция называется 'projT2'. –

+0

ОК. Но почему «Определение e {x: X} {h: Phy x}: PhyX -> Phy x: = fun _ => projT2 (existT _ _ h)' нарушило UIC? – jaam