2

我有两个假设，我想使用前向推理来应用一个同时使用它们的定理。

我的具体我有假设

H0 : a + b = c + d
H1 : e + f = g + h

我想应用标准库中的定理：

f_equal2_mult
     : forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2

现在我知道我可以手动给出 x1、y1、x2、y2 的值​​，但我希望 Coq 在与H0和统一时自动确定这些值H1。我发现我可以让它像这样工作：

eapply f_equal2_mult in H0; try exact H1.

但这感觉就像一个 hack，对称性被破坏，try. 我真的很想能够说apply f_equals2_mult in H0, H1清楚或类似的东西。有没有这样的方法？

4

1 回答 1

2

您可以使用pose proof在上下文中引入引理，并将specialize其应用于其他假设。

Lemma f (a b c d : nat) : a = b -> c = d -> False.
intros H1 H2.
pose proof f_equal2_mult as pp.
specialize pp with (1 := H1).
specialize pp with (1 := H2).

(* or *)
specialize pp with (1 := H1) (2 := H2).
于 2018-11-04T13:06:49.253 回答