CODEWITHSUNDEEP
coq
max taldykin
max taldykin

Reputation: 12898

Convert ~exists to forall in hypothesis

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).

Here is little example:

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).

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.

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.

It succeeds but H_nex is complete nonsense now:

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

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.

Upvotes: 3

Views: 1915

Answers (2)

Konstantin Weitz
Konstantin Weitz

Reputation: 6422

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.

and then proof the rest:

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.

Upvotes: 2

Ptival
Ptival

Reputation: 9437

I'm not quite sure what your problem is.

Here is how to show trivially that your implication holds.

Section S.

  Variable n : nat.
  Variable f : nat -> nat.
  Hypothesis H : ~ (exists k, k <= n /\ f k = f (n+1)).
  Goal forall k, k <= n -> f k <> f (n+1).
  Proof.
    intros k H1 H2.
    apply H.
    exists k.
    split; assumption.
  Qed.

End S.

Also your goal is provable by apply Hf., so I'm not sure but you seem to have some confusion...

Upvotes: 2

Related Questions