Make Texan triples persistent

[suhr]

Description

Make Texan triples persistent because they really should be.

I have noticed that Rocq Iris defines triples with □ in bi_scope, but without it in stdpp_scope. But what is the stdpp_scope?

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[MackieLoeffel]

stdpp_scope in Rocq is a top-level scope that is always open. In Lean, this corresponds to notations that are directly in the term syntax category, not below an iprop(...). It would be nice to have a term notation for Texan triples, then we could omit the ⊢ before it. For this notation, we don't need the box since top-level entailments can always be reused.

[suhr]

I think that a term notation could be added in a next PR.

[ayhon]

I implemented the term notation in this PR (branch). @suhr, feel free to merge it into this PR if you'd like.

The issue with the term notation is that it requires one to specify the GF from the IProp somewhere in the precondition or postcondition, since the Texan triple syntax doesn't provide a way to specify the underlying PROP the same way entailment does with |-@{...}

[suhr]

I rebased the last two commits from your branch onto my branch.

[MackieLoeffel]

Instead of duplicating this code, can we just desugar this to ⊢ {{ ... }} ... {{ ... }} and then continue elaboration there?

[ayhon]

You mean have two separate macros

• {{ .. }} .. {{ .. }} => ⊢ term({{ .. }} .. {{ .. }})
• term({{ ... }} ... {{ ... }}) => ∀ Φ, $P -∗ ▷ $k -∗ (WP $wpExpr {{ Φ }}), this one without a □

?

[ayhon]

I don't know if term(iprop(_)) => _ would trigger beforehand, maybe we need to translate the first one into BI.Entails iprop(emp) term({{ .. }} .. {{ .. }}) to prevent this.

[MackieLoeffel]

No, my idea idea was

• {{ .. }} .. {{ .. }} => ⊢ iprop({{ .. }} .. {{ .. }})
• iprop({{ ... }} ... {{ ... }}) => □ ∀ Φ, $P -∗ ▷ $k -∗ (WP $wpExpr {{ Φ }})

But this adds the □ also for the term notation. Not sure if there is a way to avoid this.

[MackieLoeffel]

Alternatively, we can just extract the shared code to a function that is used by both macros.