Skip to content

add limit_preserving_impl'

Ralf Jung requested to merge jung/iris:limit_preserving_iff into master

This will help porting lambda-rust to Coq 8.16, where a proof using limit_preserving_impl now fails.

Specifically this line. The first subgoal there is

Proper (dist 0 ==> impl) (λ x : typeO, shr_locsE y3 (ty_size x + 1) ⊆ y2)

which after a bunch of f_equiv becomes

shr_locsE y3 (ty_size y6 + 1) ⊆ shr_locsE y3 (ty_size x + 1)

and we don't have Proper instances for shr_locsE and ⊆.

On old Coq, something very strange happens when one does f_equiv on that goal: it turns into

  (ty_size y6 + 1)%nat ⊆ (ty_size x + 1)%nat

which, uh, shouldn't even typecheck? Without notation the term prints as

  @subseteq nat (@eq nat) (Init.Nat.add (@ty_size Σ typeGS0 y6) 1)
    (Init.Nat.add (@ty_size Σ typeGS0 x) 1)

So, this is actually =@{nat}, but using subseteq to print like ⊆... amazing. And also clearly nonsense. But this explains why the proof then used to complete: now we have an = and f_equiv continues to work fine.

In contrast, with the _iff lemma, f_equiv produces

  shr_locsE y3 (ty_size x + 1) ≡ shr_locsE y3 (ty_size y6 + 1)

using the ≡ on gset. Another f_equiv creates a goal with ≡@{nat}, using ofe_equiv natO. With this, solve_proper_core is able to complete the proof.

Edited by Ralf Jung

Merge request reports