将假设中的 ~exists 转换为 forall

我陷入了假设的境地~ (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 from 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 https://stackoverflow.com/questions/21644359/coq-convert-non-exist-to-forall-statement但未能将其应用到我的案例中。

如果您想使用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.