将〜存在转换为假设中的全部 [英] Convert ~exists to forall in hypothesis

问题描述

我陷入了假设〜（存在k，k <= n + 1 / \ fk = f（n + 2））的情况并希望将其转换为对所有k均等的假设（我希望如此），其中k< = n + 1-> f k< f（n + 2）。

I'm stuck in situation where I have hypothesis ~ (exists k, k <= n+1 /\ f k = f (n+2)) and wish to convert it into equivalent (I hope so) hypothesis 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 c $ c> Coq.Logic.Classical_Pred_Type 。

I tried to use 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.

我不明白此错误的含义，因此，我随机尝试过： p>

I don't understand what this error means, so as a random guess I tried this:

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

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

It succeeds but H_nex is complete nonsense now:

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

另一方面，如果 H_nex 表示为 forall ：

On the other hand it is easy to solve my goal if H_nex is expressed as forall:

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

我发现了类似的问题，但未能将其应用于我的情况。

I found similar question but failed to apply it to my case.

推荐答案

如果要使用 not_ex_all_not 引理，则要证明的内容看起来像引理。例如。您可以先证明以下内容：

If you want to use the not_ex_all_not lemma, what you want to proof needs to look like the lemma. E.g. you can proof the following first:

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.  

这篇关于将〜存在转换为假设中的全部的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！