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