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: Jun 23 2024 at 05:02 UTC