Переписывание сетоидов с просьбой о тривиальном морфизме? - PullRequest
Новая
       21

Переписывание сетоидов с просьбой о тривиальном морфизме?

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

Я получаю следующую ошибку, когда звоню setoid_rewrite (kron_1_r U) по цели U == U ⊗ I 1 (где == равно mat_equiv, а ⊗ равно kron): 

Ltac call to "setoid_rewrite (orient) (glob_constr_with_bindings)" failed.
setoid rewrite failed: Unable to satisfy the following constraints:
In environment:
W : WType
u : Unitary W
ρ : Square (2 ^ ⟦ W ⟧)
H : Mixed_State ρ
U : Square (2 ^ ⟦ W ⟧)
HeqU : U = denote_unitary u
do_subrelation := Morphisms.do_subrelation : Morphisms.apply_subrelation

?p : "Morphisms.Proper (mat_equiv ==> flip impl) (mat_equiv U)"

Я попытался доказать, что Morphisms.Proper (mat_equiv ==> flip impl) (mat_equiv U), и это тривиально - это следует из mat_equiv, являющегося отношением эквивалентности (которое я уже объявил).

Есть идеи, что может происходить и как я могу это разрешить?

(Соответствующие объявленные морфизмы - это kron от == и == до == и Mixed_State от == до iff. Последнее здесь не явно, но я использовал его ранее в доказательстве и обычно могу переписать.)

...