Make proofnode notation more robust in the context of import order
This MR addresses #100 (closed): "Proof mode notation broken depending on import order". It fixes this issue by hiding the proof mode entailment under the following definition:
Definition envs_entails {M} (Δ : envs (uPred M)) (Q : uPred M) : Prop := Δ ⊢ Q.
Notation "Γ '--------------------------------------' □ Δ '--------------------------------------' ∗ Q" :=
(envs_entails (Envs Γ Δ) Q%I)
(at level 1, Q at level 200, left associativity,
format "Γ '--------------------------------------' □ '//' Δ '--------------------------------------' ∗ '//' Q '//'", only printing) :
C_scope.
Before, the proof mode notations were specific forms of the logic entailment ⊢
, causing ambiguity in the pretty printer. As such, depending on the import order, one would either get the (desired) proof mode notation, or an (undesired) plain of_envs _ ⊢ _
goal.
Status
This MR mostly works, but there is one annoying thing. We used to have global hints for the following lemmas:
Lemma big_sepL_nil' P Φ : P ⊢ [∗ list] k↦y ∈ nil, Φ k y.
Lemma internal_eq_refl' {A : ofeT} (a : A) P : P ⊢ a ≡ a.
As a result of this, these hints would also be used when the RHS is the goal in the proof mode.
However, since the turnstile is now hidden behind a definition, these hints no longer work. I tried playing around with Hint Transparent
, but failed to make things work.
As a temporary hack I inserted some Hint Extern
s:
Hint Extern 0 (envs_entails _ ([∗ list] _ ↦ _ ∈ [], _)) => apply big_sepL_nil'.
Hint Extern 0 (envs_entails _ ([∗ map] _ ↦ _ ∈ ∅, _)) => apply big_sepM_empty'.
I don't quite like this: these patterns are rather error prone. Furthermore, lemmas like big_sepL_nil'
are proven well before the proof mode even exist in the dependency chain, so the corresponding Hint Extern
s necessarily end up in totally different files (I temporarily dumped them in proofmode/tactics.v
).