类型类解析和自动重写

Question

我有重写引理的基础。其中一些由类型类参数化。当应用引理时，重要的是当 Coq 无法自动解析类型类时重写会​​失败。我发现获得这种行为的唯一方法是隐式声明大多数参数。

Class T (t:Type) : Type.
Instance T1 : T nat.
Instance T2 : forall {A1 A2:Type} {t1:T A1} {t2:T A2}, T (A1*A2).

Definition f {A:Type} (x:A) := x.

Lemma f_eq : forall {A:Type} (t:T A) (x:A), f x = x.
Proof.
  reflexivity.
Qed.

Lemma test1 : f (0,1) = (0,1).
Proof.
  rewrite f_eq.
  (* a subgoal T (nat * nat) is generated,
     which should have been resolved directly *)
Abort.

Lemma test2 : f (0,true) = (0,true).
Proof.
  rewrite f_eq.
  (* a subgoal T (nat * bool) is generated,
     while it should have failed *)
Abort.

Arguments f_eq {_ _} _.

Lemma test1 : f (0,1) = (0,1).
Proof.
  rewrite f_eq.
  reflexivity. (* OK *)
Qed.

Lemma test2 : f (0,true) = (0,true).
Proof.
  Fail rewrite f_eq. (* fails as expected *)
Abort.

然后我想将我的引理添加到重写数据库中，但是添加到数据库中的引理已经是专门化的。

提示重写 f_eq : my_db.

打印重写 HintDb my_db。
(* 数据库 my_db
   重写 -> forall x 类型的 f_eq : nat , fx = x *)

如何将我的引理添加到重写数据库并在其参数的类型类解析方面获得正确的行为？

编辑：有一个选项Set Typeclass Resolution After Apply.似乎可以实现我期望的行为，但仅限于apply，而不是rewrite。相应的commit给出了以下描述：

添加一个选项来解决由 apply 生成的类型类目标，否则由于 evar 和元之间的差异而无法捕获该目标。

Answer 1

一种可能的解决方案是使用 ssreflect 的重写（这将解决问题的第一部分）并用多重重写规则替换提示数据库。也就是说：

From mathcomp Require Import ssreflect.

Class T (t:Type) : Type.
Instance T1 : T nat.
Instance T2 : forall {A1 A2:Type} {t1:T A1} {t2:T A2}, T (A1*A2).

Definition f {A:Type} (x:A) := x.

Lemma f_eq : forall {A:Type} (t : T A) (x:A), f x = x.
Proof. by []. Qed.

(* Add more lemmas as needed *)
Definition my_db A := (@f_eq A, @f_eq A).

Lemma test1 : f (0,1) = (0,1).
Proof. by rewrite my_db. Qed.

Lemma test2 : f (0,true) = (0,true).
Proof.
Fail rewrite f_eq.
Abort.