Skip to content
GitLab

better error when iMod/iModIntro fails due to mask mismatch

Merged Ralf Jung requested to merge ralf/mask-errors into master

We exploit the pure precondition of ElimModal to write instances like

Global Instance elim_modal_fupd_fupd_wrong_mask `{!BiFUpd PROP} p E0 E1 E2 E3 P Q :
  ElimModal
    (pm_error "Goal and eliminated modality must have the same mask.
Use [iMod (fupd_mask_subseteq E2)] to adjust the mask of your goal to [E2]")
    p false
    (|={E1,E2}=> P) False (|={E0,E3}=> Q) False | 100.

where pm_error s (the pure precondition of this instance) is equivalent to False (so these instances are trivially provable). Then we adjust iSolveSideCondition such that it recognizes pm_error side-conditions and renders them as error messages to the user.

This is a first step towards #413. To support this for iModIntro, FromModal had to be equipped with a pure precondition.

Edited by Ralf Jung

Merge request reports