Commit ed0d0453 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Remove framing for fractional.

parent 9b53243c
...@@ -155,39 +155,4 @@ Section fractional. ...@@ -155,39 +155,4 @@ Section fractional.
AsFractional P Φ q AsFractional Q Φ (q/2) AsFractional P Φ q AsFractional Q Φ (q/2)
IntoSep P Q Q | 100. IntoSep P Q Q | 100.
Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed. Proof. intros. rewrite /IntoSep [P]fractional_half //. Qed.
(* The instance [frame_fractional] can be tried at all the nodes of
the proof search. The proof search then fails almost always on
[AsFractional R Φ r], but the slowdown is still noticeable. For
that reason, we factorize the three instances that could have been
defined for that purpose into one. *)
Inductive FrameFractionalHyps
(p : bool) (R : PROP) (Φ : Qp PROP) (RES : PROP) : Qp Qp Prop :=
| frame_fractional_hyps_l Q q q' r:
Frame p R (Φ q) Q
MakeSep Q (Φ q') RES
FrameFractionalHyps p R Φ RES r (q + q')
| frame_fractional_hyps_r Q q q' r:
Frame p R (Φ q') Q
MakeSep Q (Φ q) RES
FrameFractionalHyps p R Φ RES r (q + q')
| frame_fractional_hyps_half q :
AsFractional RES Φ (q/2)
FrameFractionalHyps p R Φ RES (q/2) q.
Existing Class FrameFractionalHyps.
Global Existing Instances frame_fractional_hyps_l frame_fractional_hyps_r
frame_fractional_hyps_half.
Global Instance frame_fractional p R r Φ P q RES:
AsFractional R Φ r AsFractional P Φ q
FrameFractionalHyps p R Φ RES r q
Frame p R P RES.
Proof.
rewrite /Frame=>-[HR _][->?]H.
revert H HR=>-[Q q0 q0' r0|Q q0 q0' r0|q0].
- rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
- rewrite fractional /Frame /MakeSep=><-<-=>_.
by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
- move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp_div_2.
Qed.
End fractional. End fractional.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment