Skip to content

Include fragment in `mnat_auth_auth`

Robbert Krebbers requested to merge robbert/mnat into master

This gives the following new lemma:

Lemma mnat_auth_included q n : mnat_auth_frag n ≼ mnat_auth_auth q n.

Also reorganize the files slightly so that validity lemmas are grouped together.

This follows the approach I suggested for the monotone bijections RA here. It shifts more of the work to the RA-level library, making it easier for users of Iris to implement variants of the logic-level library.

PS: Why is this library called mnat_auth and not max_nat_auth?

/cc @tchajed

Merge request reports