In this example I will give a model of what I want to do with coq but not the actual one I face because that would be too long.
I defined a fixpoint like
Fixpoint f (n: nat): nat :=
match n with
| O => O
| S n => (f n) + 2
end.
And is proving a theorem of the form:
Lemma test: forall {n}, f (S (S (S n))) = f (S (S n)) + 2.
The thing is that I want to apply simplify the statement down to f(S (S n)) + 2 = f(S (S n)) + 2
.
I know that this one is trivial to solve in other ways, but the one I am actually working with is not.
I really do think that I would need this one step simplification in order for my prove to work.
What I tried and didn't work are:
simpl
tries to reduce as far as it get to (f n) + 2 + 2 + 2
.remember (S n) as n'
does not work as there is a hypothesis (that would be needed after the simplification) involving n. For this, I imagine that setting n' = (S n)
and leaving n
in some hypothesis work be logically sound, but coq doesn't let me (?)replace
could actually work but the result I am working with is huge (50 lines), so I am really looking for an alternative.Note that you should use change
instead of replace
(but it has the same issue if terms are too large to be input manually). So, remember
is a good solution: remember (S (S n)) as n' eqn:Hn'; simpl; rewrite Hn'; clear Hn'.
It didn't work. There is a hypothesis in the context that depends on plain n
. So it couldn't be replaced.
Hypothesis IHn depends on the bodies of Hn' n'
Wait it does work on the small example. It must be the other issue then.
clear IHn
then remember gets me that Conclusion depends on the bodies of Hn' n'
.
Any idea how this happen? Might it be because of the Type
of Matrix ?n
that I am using?
If you have such a dependency in your hypotheses, you can temporarily move the corresponding hypothesis into your goal (using revert IHn
) before doing remember
.
It might be due to your type, indeed. In general, this is due to the use of dependent proofs and dependent types.
Thanks a lot. Will check it out.
Last updated: Oct 13 2024 at 01:02 UTC