Coq 使用具有双向含义的细化答案

【问题标题】：Coq use refine with bi-implicationCoq 使用具有双向含义的细化
【发布时间】：2020-03-04 19:43:03
【问题描述】：

我不知道如何表达我的问题，因为我是 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 并以更简单的方式获得它的子目标吗？

谢谢

【问题讨论】：

在这种情况下，你可以apply t2。
是的，但我正在尝试使用更复杂的定理，只是想发布一个简单的示例。
如果您执行destruct (t2 A).，您将在上下文中获得H: B->C 和H1: C->B。然后您可以使用H 来解决您的目标。不能使用refine (t2 _ _) 的原因是t2 是A->(B<->C) 类型，注意括号。
对我有用
我希望有一些聪明的策略能够使用 BC 来证明 B->C 并以某种方式使用它来改进

标签： coq coq-tactic

【解决方案1】：

A <-> B 定义为(A -> B) /\ (B -> A)，因此您可以使用proj1、proj2 进行投影：

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

【讨论】：

完美，正是我的想象