Zhangsheng Lai (Apr 07 2021 at 04:12): Zhangsheng Lai (Apr 07 2021 at 04:12):Dear all, I have a reflection goal, reflect (X : Prop ) (b : bool)) for some expression X and 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.
The 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?
Many thanks!!
Pierre-Yves Strub (Apr 07 2021 at 06:05):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