coq - coq 中的通用平等提升

Question

是否有任何策略或事实或其他东西将相等性提升为归纳和反向的构造函数，将归纳构造函数的相等性提升为构造函数参数的相等性，即：

forall T: Type, forall t1 t2: T, Some t1 = Some t2 -> t1 = t2 
forall T: Type, forall t1 t2: T, t1 = t2 -> Some t1 = Some t2 

标签： coq

Answer 1

第一个原则通常被称为构造函数的注入性，并且有多种策略可以使用它。一种选择是injection策略：

Goal forall T: Type, forall t1 t2: T, Some t1 = Some t2 -> t1 = t2.
intros T t1 t2 H. injection H as H. apply H.
Qed.

另一个原则适用于任何函数，而不仅仅是构造函数。您可以使用以下f_equal策略：

Goal forall T: Type, forall t1 t2: T, t1 = t2 -> Some t1 = Some t2.
intros T t1 t2 H. f_equal. exact H.
Qed.

请注意，在这种情况下，简单地用等式重写通常更容易，因为当您有一个多参数函数时，它可以避免生成多个目标：

Goal forall T: Type, forall t1 t2: T, t1 = t2 -> Some t1 = Some t2.
intros T t1 t2 H. rewrite H. trivial.
Qed.