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".
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.
"inside" means that you want to rewrite under a binder, which in general requires an additional justification.
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.
yes, the quantification is a blocking binder
but I don't know if e.g. the non-ssreflect tactic
setoid_rewrite would ask for an extra proof here
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