CODEWITHSUNDEEP
coq
Charlie Parker
Charlie Parker

Reputation: 5266

What is a good example of a simple proof in Coq where the conclusion has a existential quantifier?

I wanted to see a few hands on examples of Coq proofs of the form:

\exists A(x1,...,xn)

essentially where the Goal had an existential quantifier. I was having issues manipulating the goal in meaningful ways to make progress in my proof and wanted to see a few examples of common tactics to manipulate.

What are some good existential quantifiers examples in Coq to prove?

My specific example I had:

Theorem Big_Small_ForwardImpl   :
  forall (P : Program) (S' : State),
    (BigStepR (B_PgmConf P) (B_StateConf S')) -> (ConfigEquivR (S_PgmConf P) (S_BlkConf EmptyBlk S')).
Proof.
  intros.
  induction P.
  unfold ConfigEquivR.
  refine (ex_intro _ _ _) .

my context and goals was:

1 subgoal
l : list string
s : Statement
S' : State
H : BigStepR (B_PgmConf (Pgm l s)) (B_StateConf S')
______________________________________(1/1)
exists N : nat, NSmallSteps N (S_PgmConf (Pgm l s)) (S_BlkConf EmptyBlk S')

but then changed to:

1 subgoal
l : list string
s : Statement
S' : State
H : BigStepR (B_PgmConf (Pgm l s)) (B_StateConf S')
______________________________________(1/1)
NSmallSteps ?Goal (S_PgmConf (Pgm l s)) (S_BlkConf EmptyBlk S')

after using the refine (ex_intro _ _ _) tactic. Since I am not sure what is going on I was hoping some simpler examples could show me how to manipulate existential quantifiers in my Coq goal.

helpful comment:

The ?Goal was introduced by Coq as a placeholder for some N that will have to be deduced later in the proof.

Upvotes: 0

Views: 710

Answers (1)

J-M. Gorius
J-M. Gorius

Reputation: 786

The following example is based on the code provided in this answer.

Suppose we have a type T and a binary relation R on elements of type T. For the purpose of this example, we can define those as follows.

Variable T : Type.
Variable R : T -> T -> Prop.

Let us prove the following simple theorem.

Theorem test : forall x y, R x y -> exists t, R x t.

Here is a possible solution.

Proof.
  intros. exists y. apply H.
Qed.

Instead of explicitly specifying that y is the element we are looking for, we can rely on Coq's powerful automatic proof mechanisms in order to automatically deduce which variable satisfies R x t:

Proof.
  intros.
  eexists. (* Introduce a temporary placeholder of the form ?t *)
  apply H. (* Coq can deduce from the hypothesis H that ?t must be y *)
Qed.

There exist numerous tactics that make ise of the same automated deduction mechanisms, such as eexists, eapply, eauto, etc.

Note that their names often correspond to usual tactics prefixed with an e.

Upvotes: 1

Related Questions