基于forall证明较弱的存在

Question

Lemma one_bigger' : forall n h, 
   n = S (double h) -> (exists k, S n = double k).
Proof.
  intros n h H.  rewrite H. exists (S h). reflexivity.
Qed.

Lemma one_bigger : forall n, 
   (exists k, n = S (double k)) -> (exists k, S n = double k).
Admitted.

在我看来，考虑到第一个引理，第二个引理应该是可以轻易证明的，但我似乎无法理解如何使用第一个引理来证明第二个引理。

Answer 1

case H 似乎是我找不到的魔法：

Lemma one_bigger : forall n, 
   (exists k, n = S (double k)) -> (exists k, S n = double k).
Proof.
  intros n H. case H. apply one_bigger'.
Qed.

Answer 2

事实上，你的例子是一个等价的实例（引理L）

Section S1.
  Variable (A :Type).
  Variables (P : A -> Prop) (Q:  Prop).
  
  Lemma L : (forall x , P x  -> Q ) <-> ((exists x, P x) -> Q). 
   Proof.
    split.
    - intros H [x Hx]; now apply (H x).
    - intros H x Hx; apply H. now exists x.
  Qed.
End S1.

Lemma one_bigger'' : forall n, 
    (exists k, n = S (double k)) -> (exists k, S n = double k).
Proof. 
  intros n .
  rewrite <- L . 
  apply one_bigger'. 
Qed. 

Answer 3

如果您使用 SSReflect，您可以按如下方式编写证明。

From mathcomp Require Import all_ssreflect.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Lemma one_bigger' : forall n h, 
   n = S (double h) -> (exists k, S n = double k).
Proof.
  intros n h H.  rewrite H. exists (S h). reflexivity.
Qed.

Lemma one_bigger : forall n, 
   (exists k, n = S (double k)) -> (exists k, S n = double k).
Proof. by move=> n [k /one_bigger']. Qed.

move 构造与 intros 相同，只是您的 H 在这里直接解构为见证人 k ，以及存在性平等的证明。最后一个证明通过 / 表示法直接传递给 one_bigger'，从而产生预期的结果。

另一个更明确的证明是

Proof. move=> n [k eqn]. exists k.+1. by rewrite eqn doubleS. Qed.