Commit 4eb6e55d authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

AddModal instances for except0 and later, to recover the old behavior

parent 1622b639
Pipeline #6226 passed with stages
in 10 minutes and 23 seconds
......@@ -868,16 +868,16 @@ Proof.
intros. rewrite /ElimModal (except_0_intro (_ - _)).
by rewrite -except_0_sep wand_elim_r.
Qed.
Global Instance elim_modal_timeless_bupd P Q :
Global Instance elim_modal_later_timeless P Q :
Timeless P IsExcept0 Q ElimModal ( P) P Q Q.
Proof.
intros. rewrite /ElimModal (except_0_intro (_ - _)) (timeless P).
by rewrite -except_0_sep wand_elim_r.
Qed.
Global Instance elim_modal_timeless_bupd' p P Q :
Global Instance elim_modal_later_if_timeless p P Q :
Timeless P IsExcept0 Q ElimModal (?p P) P Q Q.
Proof.
destruct p; simpl; auto using elim_modal_timeless_bupd.
destruct p; simpl; auto using elim_modal_later_timeless.
intros _ _. by rewrite /ElimModal wand_elim_r.
Qed.
......@@ -896,6 +896,30 @@ Qed.
Global Instance add_modal_bupd P Q : AddModal (|==> P) P (|==> Q).
Proof. by rewrite /AddModal bupd_frame_r wand_elim_r bupd_trans. Qed.
(* High priority to add a ▷ rather than a ◇ when P is timeless. *)
Global Instance add_modal_later_except_0 P Q :
Timeless P AddModal ( P) P ( Q) | 0.
Proof.
intros. rewrite /AddModal (except_0_intro (_ - _)) (timeless P).
by rewrite -except_0_sep wand_elim_r except_0_idemp.
Qed.
Global Instance add_modal_later P Q :
Timeless P AddModal ( P) P ( Q) | 0.
Proof.
intros. rewrite /AddModal (except_0_intro (_ - _)) (timeless P).
by rewrite -except_0_sep wand_elim_r except_0_later.
Qed.
Global Instance add_modal_except_0 P Q : AddModal ( P) P ( Q).
Proof.
intros. rewrite /AddModal (except_0_intro (_ - _)).
by rewrite -except_0_sep wand_elim_r except_0_idemp.
Qed.
Global Instance add_modal_except_0_later P Q : AddModal ( P) P ( Q).
Proof.
intros. rewrite /AddModal (except_0_intro (_ - _)).
by rewrite -except_0_sep wand_elim_r except_0_later.
Qed.
(** IsExcept0 *)
Global Instance is_except_0_except_0 P : IsExcept0 ( P).
Proof. by rewrite /IsExcept0 except_0_idemp. Qed.
......
  • I find the first two instances rather strange; does not having them break any existing development?

    Edited by Robbert
  • It actually broke the test test_iAssert_modality of the genproofmode branch. Moreover, even if I haven't checked, I do remember having used this sometimes in RustBelt (not sure any occurrence of that still exists).

    Why do you find this strange? AddModal is for adding the current modality in a side generated goal. Later and except0 certainly fit in this category. Moreover, in the proofmode, we mostly treat these modalities just like we treat updates. So why not for AddModal?

  • I think add_modal_except_0 is pretty reasonable since it adds the same modality as that's in the goal. The others, especially the first two, seem more ad-hoc.

    In principle, we also may be able to add a later to a timeless proposition when the goal is an update modality, but that cannot be done.

  • I think add_modal_except_0 is pretty reasonable since it adds the same modality as that's in the goal. The others, especially the first two, seem more ad-hoc.

    The thing is, we never use in actual developments. Most often, is used. Hence, at least, we should have add_modal_later. But of course, this cannot be done for non-timeless propositions, so add_modal_except_0_later sounds reasonable in this case. The last one is here for consistency.

    In principle, we also may be able to add a later to a timeless proposition when the goal is an update modality, but that cannot be done.

    Well, I think I never had to do something like that. But note that, if you need, you can always do that after the fact if you have an fupd: iApply fupd_except_0; iModIntro; iApply timeless..

  • Right, let's leave it as it is now.

    Ideally, we would have better syntax for the > specialization pattern so that you can actually say which modality you want to have. This is however not going to happen, maybe once we reimplement the proof mode in Ltac2 or Mtac2 (which will solve all our problems, of course ;)).

    Edited by Robbert
  • which will solve all our problems, of course ;)

    Yeah, and create a billion others.

Markdown is supported
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