你如何确定在 coq 中调用 intros 的术语答案

【问题标题】：How do you determine which terms to call intros on in coq你如何确定在 coq 中调用 intros 的术语
【发布时间】：2014-04-08 05:49:02
【问题描述】：

我是 coq 的初学者，所以这可能是一个微不足道的问题。在编写定理时，有时我无法弄清楚我需要调用哪些术语。一个简单的例子，

Theorem silly1 : forall (n m o p : nat),
  n = m  ->
  [n;o] = [n;p] ->
  [n;o] = [m;p].
Proof.
  intros n m o p eq1 eq2.
  rewrite <- eq1.
  apply eq2.  Qed.

我知道基于目标，我可能需要在 (n m o p) 上调用 intros，但为什么我需要在 eq1 和 eq2 上使用它。

此外，在其他一些定理中，您可能需要对类型参数、假设或归纳假设使用介绍。示例

Theorem trans_eq : forall (X:Type) (n m o : X),
  n = m -> m = o -> n = o.
Proof.
  intros X n m o eq1 eq2. rewrite -> eq1. rewrite -> eq2. 
  reflexivity.  Qed.

Theorem silly3' : forall (n : nat),
  (beq_nat n 5 = true -> beq_nat (S (S n)) 7 = true) ->
  true = beq_nat n 5  ->
  true = beq_nat (S (S n)) 7.
Proof.
  intros n eq H.
  symmetry in H. apply eq in H. symmetry in H. 
  apply H.  Qed.

所以我想我要问的是......当我开始证明一个定理时，我应该如何通过目标进行推理，以确定我需要调用哪些术语？

【问题讨论】：

如果引入太多参数，最坏的情况是生成的证明项是eta-expanded。没有问题。

标签： coq

【解决方案1】：

gallais 所指的一个例子就是这个。

Theorem example_1 : forall A B, (A -> B) -> A -> B.
Proof. intros ? ? H1. apply H1. Qed.

Theorem example_2 : forall A B, (A -> B) -> A -> B.
Proof. intros ? ? H1 H2. apply H1. apply H2. Qed.

Print example_1.
Print example_2.

另一个可能出现问题的例子是在使用归纳之前使用介绍。这使得归纳假设有所不同。

Fixpoint reverse_helper {A : Type} (l1 l2 : list A) : list A :=
  match l1 with
  | nil => l2
  | cons x l1 => reverse_helper l1 (cons x l2)
  end.

Theorem example_3 : forall A (l1 l2 : list A), reverse_helper l1 l2 = app (reverse_helper l1 nil) l2.
Proof. intros. induction l1. simpl. reflexivity. simpl. try rewrite IHl1. Abort.

Theorem example_4 : forall A (l1 l2 : list A), reverse_helper l1 l2 = app (reverse_helper l1 nil) l2.
Proof. induction l1. intros. simpl. reflexivity. intros. simpl. rewrite (IHl1 (cons a l2)). rewrite (IHl1 (cons a nil)). Admitted.

否则，您应该尽可能使用介绍。在你这样做之前，你将无法使用任何被量化的内容或暗示的前因。

顺便说一句

H1 : A1
...
Hn : An
___
B

等价于

H1: A1, ..., Hn: An ⊢ B.

当您以交互方式证明某事时，您是在使用从结论开始的连续演算，然后再回到假设。

【讨论】：