CODEWITHSUNDEEP
coq
sdpoll
sdpoll

Reputation: 468

How can I reorder existential variables in Coq?

In some cases it is easier to instantiate the one existential term before another. In this contrived example, I wish to set c = 3 first, and from that choose, say a = 1 and b = 2.

Lemma three_nats : exists (a : nat) (b : nat) (c : nat),
  a + b = c.
Proof.
  eexists.
  eexists.
  exists 3.
  (* Now what? *)

Is there a way to use just the simple exists 3 on c first?

Upvotes: 1

Views: 153

Answers (1)

larsr
larsr

Reputation: 5811

You can use that it is enough to prove that there exists c,b,a such that a+b=c.

enough (exists c a b, a + b = c).

Now you have two goals. First, that

exists c a b, a + b = c  -> exists a b c, a + b = c.

and second, that

exists c a b, a + b = c.

Btw, you can finish off the first part of the proof quickly with firstorder like this:

enough (exists c a b, a + b = c) by firstorder.

Or if you don't want to repeat the goal, just apply this lemma:

Lemma ex_swap {A B C} {P:A->B->C->Prop}: 
  (exists c a b, P a b c) -> exists a b c, P a b c.
Proof. firstorder.  Qed.

Upvotes: 2

Related Questions