Stream: math-comp users

Topic: Ways to dispose of hypotheses

Guillaume Dubach (Mar 26 2021 at 17:45):

It is written in the Mathematical Components book that rewrite {}H should rewrite H and then erase it from the context. For some reason, this never works for me. Only move {H} works. Any explanation or way to fix it?...

Pierre-Yves Strub (Mar 26 2021 at 17:49):

Lemma L (x y : nat) P : x = y -> P x.
Proof.
move=> h. rewrite {}h.

gives

  x, y : nat
  P : nat -> Type
  ============================
  P y

Pierre-Yves Strub (Mar 26 2021 at 17:49):

What version of Coq/ssr are you using?

Enrico Tassi (Mar 26 2021 at 19:26):

Is H a section variable? (cause these cannot be cleared)

Guillaume Dubach (Mar 26 2021 at 19:52):

@Enrico Tassi @Pierre-Yves Strub Could it be that it does not work with by rewrite ? Your example works, but for instance

Lemma L (x y : nat) (P : nat -> Prop) : x = y -> P x -> (P y /\ P y).
Proof.
move=> h hPx. split. by rewrite -{}h.

returns a context with h still in it, so {} did not change anything. I think the few times I have tried to use it and it failed, it wasn't a section variable, but it must have been with a by rewrite...

Pierre-Yves Strub (Mar 26 2021 at 20:21):

In your example, by is closing the current goal. What you see is hence your second goal where h has not be cleared.

Guillaume Dubach (Mar 26 2021 at 20:38):

Yes of course, that's right. It must have been the same in my other issues. Thank you very much for clarifying this to me!

Last updated: Feb 02 2023 at 13:03 UTC