Coq use refine with bi-implication

Question

我不知道如何表达我的问题，因为我是coq的新手。我想用包含双向蕴涵的定理来使用refine。示例代码：

Parameters A B C : Prop.

Theorem t1:
  A -> B -> C.
Admitted.

Theorem t2:
  A -> B <-> C.
Admitted.

Theorem test1:
  A -> B -> C.
Proof.
  intros.
  refine (t1 _ _).
  assumption.
  assumption.
Qed.

Theorem test2:
  A -> B -> C.
Proof.
  intros A B.
  refine (t2 _ _).

t1和t2是我想在refine中使用的定理。t1按照我所期望的方式工作(如test1所示)。但我对t2有个问题。我得到的错误是：

Ltac call to "refine (uconstr)" failed.
Error: Illegal application (Non-functional construction): 
The expression "t2 ?a" of type "Top.B <-> C"
cannot be applied to the term
 "?y" : "?T"
Not in proof mode.

我试过的东西是这样的：

Theorem test3:
  A -> B -> C.
Proof.
  intros.
  cut (B <-> C).
  firstorder.
  refine (t2 _).
  assumption.
Qed.

但是随着更长的道具和证据，它变得有点混乱。(我还必须自己证明这一点)。我可以使用t2并以一种更简单的方式获得它的子目标吗？

谢谢

Answer 1

A <-> B被定义为(A -> B) /\ (B -> A)，因此您可以使用proj1、proj2

Theorem test2:
  A -> B -> C.
Proof.
  intros A B.
  refine (proj1 (t2 _) _).