Dear all, I have a reflection goal,
reflect (X : Prop ) (b : bool)) for some expression
b. I would like to perform some manipulation (
rewrite or_assoc) to X to some equivalent
X' expression as I have a lemma which solve for
reflect (X' : Prop )(b : bool ) easily.
reflect predicate does not allow rewriting directly, so
apply: (iffP idP) is used to unfold
reflect, so that the required manipulation can be performed. After which I would like to reverse the
apply: (iffP idP) tactic to restore the
reflect expression. Is there anyway to do this?
From mathcomp Require Import all_ssreflect. Context (P Q : Prop) (b : bool). Hypothesis (PQ : P <-> Q) (Pb : reflect P b). Goal reflect Q b. Proof. by apply/(equivP Pb PQ). Qed.
Thanks @Pierre-Yves Strub !
equivP is exactly what I'm looking for :)
Last updated: Feb 08 2023 at 07:02 UTC