Skip to content

Make proofnode notation more robust in the context of import order

Robbert Krebbers requested to merge proofmode_notation_fix into master

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] ky  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 Externs:

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 Externs necessarily end up in totally different files (I temporarily dumped them in proofmode/tactics.v).

Merge request reports