小编Jia*_*ang的帖子

在问题中Coq中有一套最小的完整策略吗？,提到的答案exact足以证明所有目标.有人可以解释一下吗？例如,A \/ B -> B \/ AA,B作为Prop 的目标如何仅通过一堆来证明exact？如果您有其他更好的例子,请不要犹豫,也请回答.关键是要对这个问题给出一些解释并给出一个非常重要的例子.

在Coq教程 1.3.1和1.3.2节中，有两个elim应用程序：第一个应用程序：

1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\ B
  ============================
   B /\ A

申请后elim H，

Coq < elim H.
1 subgoal

  A : Prop
  B : Prop
  C : Prop
  H : A /\ B
  ============================
   A -> B -> B /\ A

第二个：

1 subgoal

  H : A \/ B
  ============================
   B \/ A

申请后elim H，

Coq < elim H.
2 subgoals

  H …