Coq使用带二次蕴涵的精炼

Question

我不确定如何措辞我的问题，因为我不熟悉coq。我想对包含双向蕴涵的一个定理使用优化。示例代码：

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是我要精炼的定理。 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 _) _).