Commit c798ff4f authored by Ralf Jung's avatar Ralf Jung
Browse files

make fractional lemmas use AsFractional

parent 010154e2
Pipeline #4076 passed with stage
in 2 minutes and 57 seconds
......@@ -22,21 +22,14 @@ Section fractional.
Implicit Types Φ : Qp uPred M.
Implicit Types p q : Qp.
Lemma fractional_split `{!Fractional Φ} p q :
Φ (p + q)%Qp Φ p Φ q.
Proof. by rewrite fractional. Qed.
Lemma fractional_combine `{!Fractional Φ} p q :
Φ p Φ q Φ (p + q)%Qp.
Proof. by rewrite fractional. Qed.
Lemma fractional_half_equiv `{!Fractional Φ} p :
Φ p Φ (p/2)%Qp Φ (p/2)%Qp.
Proof. by rewrite -(fractional (p/2) (p/2)) Qp_div_2. Qed.
Lemma fractional_half `{!Fractional Φ} p :
Φ p Φ (p/2)%Qp Φ (p/2)%Qp.
Proof. by rewrite fractional_half_equiv. Qed.
Lemma half_fractional `{!Fractional Φ} p q :
Φ (p/2)%Qp Φ (p/2)%Qp Φ p.
Proof. by rewrite -fractional_half_equiv. Qed.
Lemma fractional_split P P1 P2 Φ q1 q2 :
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
P P1 P2.
Proof. move=>-[-> ->] [-> _] [-> _]. done. Qed.
Lemma fractional_half P P12 Φ q :
AsFractional P Φ q AsFractional P12 Φ (q/2)
P P12 P12.
Proof. rewrite -{1}(Qp_div_2 q)=>-[->->][-> _]. done. Qed.
(** Fractional and logical connectives *)
Global Instance persistent_fractional P :
......@@ -132,25 +125,25 @@ Section fractional.
AsFractional P Φ (q1 + q2) AsFractional P1 Φ q1 AsFractional P2 Φ q2
IntoAnd b P P1 P2.
Proof.
(* TODO: We need a better way to handle this boolean here.
(* TODO: We need a better way to handle this boolean here; always
applying mk_into_and_sep (which only works after introducing all
assumptions) is rather annoying.
  • I don't understand this TODO.

  • Compare the original proof and the new proof. They are proving equivalent statements (IntoAnd false vs. IntoAnd p), but the latter is much more annoying to prove.

  • The old proof seems to make no sense, why is IntoAnd being unfolded why it is not even in the goal.

    So, what are you suggesting we should do here?

  • Of course it is in the goal...?

    So, what are you suggesting we should do here?

    Something where we have to prove only P1 * P2, not if p then P /\ Q else P * Q, which is a very annoying goal to work with. I suppose there is a good reason why you do not have an instance that goes from false to true?

  • Of course it is in the goal...?

    No, it is not: IntoAnd disappears after applying mk_into_and_sep.

    I suppose there is a good reason why you do not have an instance that goes from false to true?

    The usual; that instance leads to an exponential time complexity on failures, as it can be applied at any point during the instance search.

  • No, it is not: IntoAnd disappears after applying mk_into_and_sep.

    Ah sorry, I thought about the diff of the previous patch https://gitlab.mpi-sws.org/FP/iris-coq/commit/010154e2feceb18246f211b7068c7e9bb986a86a

  • Alright, so I guess this TODO can be removed, but we should document why we do not have the instance that goes from false to true somewhere?

  • Well, not really, proving if p then P /\ Q else P * Q is still rather annoying.

    And then there is the second part of this TODO, which is about preventing people from proving instances of the form IntoAnd false. What about (a) renaming IntoAnd to something else (IntoConj or so), introducing a notation IntoSep P Q R := \all b, IntoConj b P Q R and a notation IntoAnd P Q R := IntoConj true P Q R, and telling people to use the notation whenever they prove "leaf" instances? That should make the mistake that was made here less likely. It still leaves us without a good story for proving an IntoSep though.

  • Well, not really, proving if p then P /\ Q else P * Q is still rather annoying.

    But you hardly ever have to do that, we have the "smart" constructor mk_into_and_sep for that.

  • Unfortunately that one can only be applied after introducing all assumptions, which can be rather annoying -- see the original proof by rewrite /IntoAnd=>-[-> ->] [-> _] [-> _], how would you change that to use mk_into_and_sep? (And I've had the same problem elsewhere when proving these instances.)

    Edited by Ralf Jung
  • We could prove a Proper for all of these Into and From type classes, then you can just substitute in their arguments.

    I don't think it is worth the effort at all, though. The number occurrences where these problems actually occur are too limited.

  • What about (a) renaming IntoAnd to something else (IntoConj or so), introducing a notation IntoSep P Q R := \all b, IntoConj b P Q R and a notation IntoAnd P Q R := IntoConj true P Q R

    Would how you then state instances like:

    IntoAnd p P Q1 Q2  IntoAnd p ( P) ( Q1) ( Q2)
    Edited by Robbert Krebbers
  • Well sure, the ones just "forwarding" things would keep using the flag. They have to be proven by case distinction anyway, don't they?

    With the bigops, I am again seeing cases where iSplitL. works, and one side of the result is persistent, but iSplit does not work. Maybe an alternative would be to have iSplit also make a search for false after the search for true failed -- and if the search for false succeeds, it could try to prove that either side of the result is persistent, and then go on. That would at least make sure that the invariant "if iSplitL works and one side is persistent, then iSplit works" is maintained.

  • With the bigops, I am again seeing cases where iSplitL. works, and one side of the result is persistent, but iSplit does not work.

    There was indeed a problem that some FromAnd were forgotten whereas FromSep instances were present. To solve this issue, I have unified FromAnd and FromSep in the same way as IntoAnd by introducing a boolean. For most connectives the instances are generic, but for big operators, and ownership connectives, there are two instances.

    Edited by Robbert Krebbers
  • See 9da19881 and 1e180a24.

  • So you don't think it is worth extending iSplit to search for other instances to ensure that it will not fail unexpectedly?

  • The above commit is doing precisely that, but more generically and more efficiently. For example, also when you use iSplit and you have a box somewhere, then under that box it will search for other instances.

  • I see. How's that happening? Say I re-introduce the mistake again of the AsFractional instances being of the form IntoSep false. How would iSplit proceed? Wouldn't tac_and_split search for FromAnd true and fail?

  • Not, it does not prevent one from declaring wrong class instances.

Please register or sign in to reply
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=>-[-> ->] [-> _] [-> _].
intros H1 H2 H3. apply mk_into_and_sep. rewrite [P]fractional_split //.
Qed.
Global Instance into_and_fractional_half b P Q Φ q :
AsFractional P Φ q AsFractional Q Φ (q/2)
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)=>-[->->][-> _].
intros H1 H2. apply mk_into_and_sep. rewrite [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 ave been
that reason, we factorize the three instances that could have been
defined for that purpose into one. *)
Inductive FrameFractionalHyps R Φ RES : Qp Qp Prop :=
| frame_fractional_hyps_l Q p p' r:
......
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