不能将一个假设应用于另一个假设

Question

我对CoQ非常陌生，并且正在尝试证明，如果两个功能是iNDIVES，则这些功能的组成也是iNjective。 这是我的代码：

Definition compose {A B C} (g: B -> C) (f: A -> B) :=
  fun x : A => g (f x).

Definition injective {A B} (f: A -> B) :=
  forall x1 x2, f x1 = f x2 -> x1 = x2.

(*
Definition surjective {A B} (f: A -> B) :=
  forall y: B, exists x: A, f x = y.
*)

Theorem example {A B C} (g: B -> C) (f: A -> B) :
  injective f /\ injective g -> injective (compose g f).
Proof.
  intros.
  destruct H as (H1,H2).
  cut (forall x1 x2: A, (compose g f) x1 = (compose g f) x2).
  intros.
  unfold compose in H.
  unfold injective in H2.

结果是：

2 goals
A : Type
B : Type
C : Type
g : B -> C
f : A -> B
H1 : injective f
H2 : forall x1 x2 : B, g x1 = g x2 -> x1 = x2
H : forall x1 x2 : A, g (f x1) = g (f x2)
______________________________________(1/2)
injective (compose g f)
______________________________________(2/2)
forall x1 x2 : A, compose g f x1 = compose g f x2

从这个状态中，我尝试在h中应用H2，以证明f（x1）= f（ x2）。我尝试了应用策略以及专业策略，但它们都没有起作用。

这是我关注的实际证明：

编辑： 非常感谢您的帮助！该代码现在可以工作：

Theorem compose_injective {A B C} (g: B -> C) (f: A -> B) :
  injective f /\ injective g -> injective (compose g f).
Proof.
  intros.
  destruct H as (H1,H2).
  unfold injective.
  intros.
  unfold injective in H2.
  apply H2 in H.
  unfold injective in H1.
  apply H1 in H.
  exact H.

Answer 1

而不是剪切，请使用展开的注入式。显示假设compose gfx = compose gf x'。

Answer 2

在H中应用H2说您缺少x1和x2。首先，x1和x2 展开 in Injective 在您的目标中，并使用intros代码>。然后，您可以在H1中应用H2 （带有适当的参数）。