diff --git a/theories/base_logic/lib/fractional.v b/theories/base_logic/lib/fractional.v index 8029a018ad4f4e62432209e8dcf1d32d0c784e7a..c7ae48f82ab11eafd13e6bc283fe82f007bafc6c 100644 --- a/theories/base_logic/lib/fractional.v +++ b/theories/base_logic/lib/fractional.v @@ -128,14 +128,24 @@ Section fractional. FromSep Q P P. Proof. rewrite /FromSep=>-[-> <-] [-> _]. by rewrite Qp_div_2. Qed. - Global Instance into_and_fractional P P1 P2 Φ q1 q2 : + Global Instance into_and_fractional b P P1 P2 Φ q1 q2 : AsFractional P Φ (q1 + q2) → AsFractional P1 Φ q1 → AsFractional P2 Φ q2 → - IntoAnd false P P1 P2. - Proof. by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _]. Qed. - Global Instance into_and_fractional_half P Q Φ q : + IntoAnd b P P1 P2. + Proof. + (* TODO: We need a better way to handle this boolean here. + Ideally, it'd not even be possible to make the mistake that + was originally made here, which is to give this instance for + "false" only, thus breaking some intro patterns. *) + intros H1 H2 H3. apply mk_into_and_sep. revert H1 H2 H3. + by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _]. + Qed. + Global Instance into_and_fractional_half b P Q Φ q : AsFractional P Φ q → AsFractional Q Φ (q/2) → - IntoAnd false P Q Q | 100. - Proof. by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _]. Qed. + IntoAnd b P Q Q | 100. + Proof. + intros H1 H2. apply mk_into_and_sep. revert H1 H2. + by rewrite /IntoAnd -{1}(Qp_div_2 q)=>-[->->][-> _]. + Qed. (* The instance [frame_fractional] can be tried at all the nodes of the proof search. The proof search then fails almost always on