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 

Answer 1

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.