proof_guide.md

Iris Proof Guide

This work-in-progress document serves to explain how Iris proofs are typically carried out in Coq: what are the common patterns and conventions, what are the common pitfalls. This complements the tactic documentation for the proof mode and HeapLang.

Order of Requires

In Coq, declarations in modules imported later may override the previous definition. Therefore, in order to make sure the most relevant declarations and notations always take priority, we recommend importing dependencies from the furthest to the closest.

In particular, when importing Iris, Stdpp and Coq stdlib modules, we recommend importing in the following order:

• Coq
• stdpp
• iris.algebra
• iris.bi
• iris.proofmode
• iris.base_logic
• iris.program_logic
• iris.heap_lang

Resolving mask mismatches

Sometimes, fupd masks are not exactly what they need to be to make progress. There are two situations to distinguish here.

Eliminating a [fupd] with a mask smaller than the current one

When your goal is |={E,_}=> _ and you want to do iMod on an |={E',_}=> _, Coq will complain even if E' ⊆ E. To resolve this, you first need to explicitly weaken your mask from E to E' by doing: