CODEWITHSUNDEEP
coq
Bromind
Bromind

Reputation: 1128

Rewrite under exists

Say I have the following relation:

Inductive my_relation: nat -> Prop :=
constr n: my_relation n.

and I want to prove the following: 

Lemma example:
  (forall n, my_relation n -> my_relation (S n)) -> (exists n, my_relation n) -> exists n, my_relation (S n).
Proof.
  intros.

After introducing, I have the following environment:

1 subgoal
H : forall n : nat, my_relation n -> my_relation (S n)
H0 : exists n : nat, my_relation n
______________________________________(1/1)
exists n : nat, my_relation (S n)

My question is: is there a possibility to rewrite H under the exists quantifier ? If not, is there a strategy to solve this kind of problem (this particular one is not really relevant, but problems where you have to prove an exists using another exists, and where, informally, you can « deduce » a way to rewrite the exists in the hypothesis into the exists in the goal) ?

For instance, if I try rewrite H in H0. I have, an error (Error: Cannot find a relation to rewrite.).

Upvotes: 4

Views: 1872

Answers (2)

eponier
eponier

Reputation: 3122

The standard way to manipulate an existential quantification in an hypothesis is to get a witness of the property using inversion or, better and simpler, destruct.

You can give a name to the variable using one of the following syntaxes:

destruct H0 as (n, H0).
destruct H0 as [n H0].
destruct H0 as (n & H0).

Note that you can also destruct an hypothesis using intro-patterns.

intros H (n & H0).

And you can even directly apply H in H0.

intros H (n & H0%H). exists n. assumption.

Software Foundations explains this in a clear way.

Upvotes: 8

Bromind
Bromind

Reputation: 1128

I found a way, I post it here for any similar questions in the future.

It is possible to inverse the exists hypothesis, in order to "instantiate" the quantified variable, for instance, here, the proof can be finished by:

  inversion H0.
  apply H in H1.
  exists x.
  apply H1.
Qed.

After inversion H0, we have in the environment:

1 subgoal
H : forall n : nat, my_relation n -> my_relation (S n)
H0 : exists n : nat, my_relation n
x : nat
H1 : my_relation x
______________________________________(1/1)
exists n : nat, my_relation (S n)

and we can now work with x.

Upvotes: 1

Related Questions