coq - 将假设中的 ~exists 转换为 forall

Question

我陷入了假设的境地 ~ (exists k, k <= n+1 /\ f k = f (n+2))并希望将其转换为等效的(我希望如此)假设forall k, k <= n+1 -> f k <> f (n+2) .

这是一个小例子:

Require Import Coq.Logic.Classical_Pred_Type.
Require Import Omega.

Section x.
  Variable n : nat.
  Variable f : nat -> nat.
  Hypothesis Hf : forall i, f i <= n+1.
  Variable i : nat.
  Hypothesis Hi : i <= n+1.
  Hypothesis Hfi: f i = n+1.
  Hypothesis H_nex : ~ (exists k, k <= n+1 /\ f k = f (n+2)).
  Goal (f (n+2) <= n).

我尝试使用not_ex_all_not来自Coq.Logic.Classical_Pred_Type .

Check not_ex_all_not.
not_ex_all_not
     : forall (U : Type) (P : U -> Prop),
       ~ (exists n : U, P n) -> forall n : U, ~ P n

apply not_ex_all_not in H_nex.
Error: Unable to find an instance for the variable n.

我不明白这个错误意味着什么，所以作为随机猜测，我尝试了这个:

apply not_ex_all_not with (n := n) in H_nex.

它成功了，但是 H_nex现在完全是废话:

H_nex : ~ (n <= n+1 /\ f n = f (n + 2))

另一方面，如果 H_nex 就很容易实现我的目标表示为forall :

  Hypothesis H_nex : forall k, k <= n+1 -> f k <> f (n+2).
  specialize (H_nex i).
  specialize (Hf (n+2)).
  omega.

我发现类似的question但未能将其应用到我的案例中。

Answer 1

如果你想使用not_ex_all_not引理，你想要证明的东西需要看起来像引理。例如。你可以先证明以下几点:

Lemma lma {n:nat} {f:nat->nat} : ~ (exists k, k <= n /\ f k = f (n+1)) -> 
                                 forall k, ~(k <= n /\ f k = f (n+1)).
  intro H.
  apply not_ex_all_not.
  trivial.
Qed.

然后证明其余部分:

Theorem thm (n:nat) (f:nat->nat) : ~ (exists k, k <= n /\ f k = f (n+1)) -> 
                                  forall k, k <= n -> f k <> f (n+1).
  intro P.
  specialize (lma P). intro Q.
  intro k.
  specialize (Q k).
  tauto.
Qed.