Commit f1d77737 authored by Ralf Jung's avatar Ralf Jung
Browse files

add tactic for showing Iris assertions involving limits of chains

parent 1e519f29
......@@ -186,5 +186,21 @@ Proof.
eapply uPred_holds_ne, Hlim, HP; eauto using conv_compl.
Lemma entails_lim' {T : ofeT} `{Cofe T} (P Q : T uPredC M)
`{!NonExpansive P} `{!NonExpansive Q} (c : chain T) :
( n, P (c n) Q (c n)) P (compl c) Q (compl c).
set (cP := chain_map P c). set (cQ := chain_map Q c).
rewrite -!compl_chain_map=>HPQ. exact: entails_lim.
End entails.
Ltac entails_lim c :=
pattern (compl c);
match goal with
| |- (λ o, ?P ?Q) ?x => change (((λ o, P) x) (λ o, Q) x)
apply entails_lim'.
End uPred.
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