Rewrite under exists

Question

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).
(forall n : nat, my_relation n -> my_relation (S n)) ->
(exists n : nat, my_relation n) ->
exists n : nat, my_relation (S n)
Proof.
(forall n : nat, my_relation n -> my_relation (S n)) ->
(exists n : nat, my_relation n) ->
exists n : nat, my_relation (S n)
  intros.
H: forall n : nat, my_relation n -> my_relation (S n)
H0: exists n : nat, my_relation n
exists n : nat, my_relation (S n)

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
  ============================
  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

The command has indeed failed with message:
Cannot find a relation to rewrite.

Answer (eponier)

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).
H: forall n : nat, my_relation n -> my_relation (S n)
n: nat
H0: my_relation n
exists n : nat, my_relation (S n) 
  destruct H0 as [n H0].
H: forall n : nat, my_relation n -> my_relation (S n)
n: nat
H0: my_relation n
exists n : nat, my_relation (S n) 
  destruct H0 as (n & H0).
H: forall n : nat, my_relation n -> my_relation (S n)
n: nat
H0: my_relation n
exists n : nat, my_relation (S n)

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

  intros H (n & H0).
H: forall n : nat, my_relation n -> my_relation (S n)
n: nat
H0: my_relation n
exists n : nat, my_relation (S n)

And you can even directly apply H in H0.

  intros H (n & H0%H).
H: forall n : nat, my_relation n -> my_relation (S n)
n: nat
H0: my_relation (S n)
exists n : nat, my_relation (S n) exists n.
H: forall n : nat, my_relation n -> my_relation (S n)
n: nat
H0: my_relation (S n)
my_relation (S n) assumption.

Software Foundations explains this in a clear way.

Answer (Arthur Azevedo De Amorim)

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.
H: forall n : nat, my_relation n -> my_relation (S n)
H0: exists n : nat, my_relation n
x: nat
H1: my_relation x
exists n : nat, my_relation (S n) apply H in H1.
H: forall n : nat, my_relation n -> my_relation (S n)
H0: exists n : nat, my_relation n
x: nat
H1: my_relation (S x)
exists n : nat, my_relation (S n)
  exists x.
H: forall n : nat, my_relation n -> my_relation (S n)
H0: exists n : nat, my_relation n
x: nat
H1: my_relation (S x)
my_relation (S x) apply H1.

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
  ============================
  exists n : nat, my_relation (S n)

and we can now work with x.