Stream: Coq users

Topic: One Step Simplification.


view this post on Zulip 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:

view this post on Zulip 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'.

view this post on Zulip 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'

view this post on Zulip Touch Sungkawichai (Feb 09 2024 at 06:30):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Touch Sungkawichai (Feb 09 2024 at 06:41):

Thanks a lot. Will check it out.


Last updated: Oct 13 2024 at 01:02 UTC