У меня есть Class, содержащий как данные, так и аксиомы. Я хочу создать еще один экземпляр в режиме проверки на основе (1) существующего экземпляра и (2) некоторых других входных данных. Я хочу destruct этот второй ввод перед созданием нового экземпляра записи.
Минимальный Class, который работает в качестве примера, уменьшен от одного в jwiegley / category-theory:
Require Import Coq.Unicode.Utf8.
Require Import Coq.Init.Datatypes.
Require Import Coq.Classes.Morphisms.
Require Import Coq.Classes.SetoidDec.
Generalizable All Variables.
Reserved Infix "~>" (at level 90, right associativity).
Reserved Infix "∘" (at level 40, left associativity).
Record Category := {
obj : Type;
uhom := Type : Type;
hom : obj -> obj -> uhom where "a ~> b" := (hom a b);
homset :> ∀ X Y, Setoid (X ~> Y);
compose {x y z} (f: y ~> z) (g : x ~> y) : x ~> z
where "f ∘ g" := (compose f g);
compose_respects x y z :>
Proper (equiv ==> equiv ==> equiv) (@compose x y z);
}.
Предположим, что (2) равно bool:
Definition newCat (C : Category) (b : bool) : Category.
Proof.
destruct b.
- eapply Build_Category.
Unshelve.
На этом этапе obj заменяется на Type:
C : Category
============================
∀ x y z : Type, Proper (equiv ==> equiv ==> equiv) (?compose x y z)
subgoal 2 (ID 18) is:
∀ x y z : Type, (λ _ A : Type, A) y z → (λ _ A : Type, A) x y → (λ _ A : Type, A) x z
Это поведение исчезнет, если я удалю аксиому compose_respects (или использую какой-либо другой вид Record без такого поля). Если я заменю Category на Class, obj будет заполнено как obj из C. Похоже, это как-то связано с разрешением классов типов (тот факт, что equivs имеют неявные аргументы класса типов?).
Есть ли способ предотвратить заполнение этих (или любых!) Переменных с помощью унификации? Оптимальным результатом будет что-то вроде _18 _ + _ 19_, где вообще не генерируются экзистенциальные данные, и я могу заполнить поля записи как подцели по порядку.
