## Stream: Coq users

### Topic: One Step Simplification.

#### Touch Sungkawichai (Feb 09 2024 at 05:27):

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.

#### Guillaume Melquiond (Feb 09 2024 at 06:15):

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'.`

#### Touch Sungkawichai (Feb 09 2024 at 06:28):

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'`

#### Touch Sungkawichai (Feb 09 2024 at 06:30):

Wait it does work on the small example. It must be the other issue then.

#### Touch Sungkawichai (Feb 09 2024 at 06:35):

`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?

#### Guillaume Melquiond (Feb 09 2024 at 06:37):

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

#### Guillaume Melquiond (Feb 09 2024 at 06:38):

It might be due to your type, indeed. In general, this is due to the use of dependent proofs and dependent types.

#### Touch Sungkawichai (Feb 09 2024 at 06:41):

Thanks a lot. Will check it out.

Last updated: Jun 23 2024 at 05:02 UTC