Commit ddb9ee0e authored by Robbert Krebbers's avatar Robbert Krebbers

Prefer modality over embedding in `iModIntro`.

parent 56f80319
Pipeline #7164 passed with stage
in 11 minutes and 12 seconds
...@@ -247,37 +247,37 @@ Global Instance from_modal_absorbingly P : ...@@ -247,37 +247,37 @@ Global Instance from_modal_absorbingly P :
Proof. by rewrite /FromModal /= -absorbingly_intro. Qed. Proof. by rewrite /FromModal /= -absorbingly_intro. Qed.
(* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer (* When having a modality nested in an embedding, e.g. [ ⎡|==> P⎤ ], we prefer
the modality over the embedding. *) the embedding over the modality. *)
Global Instance from_modal_embed `{BiEmbedding PROP PROP'} (P : PROP) : Global Instance from_modal_embed `{BiEmbedding PROP PROP'} (P : PROP) :
FromModal (@modality_embed PROP PROP' _ _) P P P | 100. FromModal (@modality_embed PROP PROP' _ _) P P P.
Proof. by rewrite /FromModal. Qed. Proof. by rewrite /FromModal. Qed.
Global Instance from_modal_id_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : Global Instance from_modal_id_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
FromModal modality_id sel P Q FromModal modality_id sel P Q
FromModal modality_id sel P Q. FromModal modality_id sel P Q | 100.
Proof. by rewrite /FromModal /= =><-. Qed. Proof. by rewrite /FromModal /= =><-. Qed.
Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : Global Instance from_modal_affinely_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
FromModal modality_affinely sel P Q FromModal modality_affinely sel P Q
FromModal modality_affinely sel P Q. FromModal modality_affinely sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed. Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely. Qed.
Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : Global Instance from_modal_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
FromModal modality_persistently sel P Q FromModal modality_persistently sel P Q
FromModal modality_persistently sel P Q. FromModal modality_persistently sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed. Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_persistently. Qed.
Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : Global Instance from_modal_affinely_persistently_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
FromModal modality_affinely_persistently sel P Q FromModal modality_affinely_persistently sel P Q
FromModal modality_affinely_persistently sel P Q. FromModal modality_affinely_persistently sel P Q | 100.
Proof. Proof.
rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
Qed. Qed.
Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : Global Instance from_modal_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
FromModal modality_plainly sel P Q FromModal modality_plainly sel P Q
FromModal modality_plainly sel P Q. FromModal modality_plainly sel P Q | 100.
Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed. Proof. rewrite /FromModal /= =><-. by rewrite bi_embed_plainly. Qed.
Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q : Global Instance from_modal_affinely_plainly_embed `{BiEmbedding PROP PROP'} `(sel : A) P Q :
FromModal modality_affinely_plainly sel P Q FromModal modality_affinely_plainly sel P Q
FromModal modality_affinely_plainly sel P Q. FromModal modality_affinely_plainly sel P Q | 100.
Proof. Proof.
rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly. rewrite /FromModal /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
Qed. Qed.
......
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