Stream: math-comp users

Topic: reversing the tactic apply : (iffP idP)

view this post on Zulip 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!!

view this post on Zulip 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.

view this post on Zulip Zhangsheng Lai (Apr 07 2021 at 07:13):

Thanks @Pierre-Yves Strub ! equivP is exactly what I'm looking for :)

Last updated: Jul 23 2024 at 20:01 UTC