Commit 360de605 authored by Glen Mével's avatar Glen Mével
Browse files

add existential quantification to the rule of opening an invariant around a LA triple

parent 081e5117
...@@ -76,16 +76,14 @@ This linearization point being atomic, it allows the opening of invariants just ...@@ -76,16 +76,14 @@ This linearization point being atomic, it allows the opening of invariants just
\infer{% \infer{%
\lahoare <x> {\later I \isep P} {e} {\later I \isep Q} \lahoare <x> {\later I \isep P} {e} {\later I \isep Q}
}{% }{%
\knowInv{}{I} \vdash \lahoare <x> {P} {e} {Q} \knowInv{}{\Exists x. I} \vdash \lahoare <x> {P} {e} {Q}
} }
% %
\end{mathpar} \end{mathpar}
% TODO: faire référence aux règles ci-dessus dans le texte. % TODO: faire référence aux règles ci-dessus dans le texte.
% mentionner qu’un triplet log. atomique implique le triplet usuel ? (1re règle) % mentionner qu’un triplet log. atomique implique le triplet usuel ? (1re règle)
% I doit pouvoir parler de x, il me semble ?
% peut-être enlever le binder à cet endroit. % peut-être enlever le binder à cet endroit.
% TODO : expliquer la syntaxe des invariants, dire que \later est une technicité d'Iris % TODO : expliquer la syntaxe des invariants, dire que \later est une technicité d'Iris
% JH : le mieux, c'est peut-être de mettre ces règles dasn une figure, et de s'y référer à plusieurs endroits: % JH : le mieux, c'est peut-être de mettre ces règles dasn une figure, et de s'y référer à plusieurs endroits:
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment