Stream: math-comp users

Topic: Rewrite doesn't see subterms

Julien Puydt (Oct 15 2022 at 10:59):

I'm sure there's still something I miss about Coq/ssr: sometimes I don't manage to rewrite something as I would like because of "The LHS of ... (...) does not match any subterm of the goal".

For example:

From mathcomp Require Import all_ssreflect.
From mathcomp.analysis Require Import boolp.

Section FooOk.

Variable A B C D E: Prop.

Hypothesis c: C.
Hypothesis d: D.

Lemma ok: A -> ~ (B -> C /\ D) -> E.
Proof.
rewrite not_implyP.
rewrite not_andP.
Admitted.

End FooOk.

Section FooBad.

Lemma bad: ~ (forall P: Prop, P -> (exists Q: Prop, Q -> P /\ Q)).
Proof.
rewrite -existsNE.
rewrite not_implyP. (* FIXME: why !? *)
(* here I'm supposed to go on with migrating ~ inside *)

End FooBad.

Assia Mahboubi (Oct 19 2022 at 09:16):

"inside" means that you want to rewrite under a binder, which in general requires an additional justification.

Julien Puydt (Oct 19 2022 at 11:27):

Is the quantification a blocking binder and how can I go through?

I know how to go inside a bigop, but this much more simple situation didn't look like it would warrant this type of consideration.

Paolo Giarrusso (Oct 19 2022 at 17:07):

yes, the quantification is a blocking binder

Paolo Giarrusso (Oct 19 2022 at 17:08):

but I don't know if e.g. the non-ssreflect tactic setoid_rewrite would ask for an extra proof here

Julien Puydt (Oct 20 2022 at 11:07):

How can I go through to push the ~ further inside? And when that's done, can I easily push it some more?

Last updated: Jan 29 2023 at 18:03 UTC