Commit f70294b1 authored by Robbert Krebbers's avatar Robbert Krebbers

Prove equivalent more useful def of valid on auth A when A is discrete.

parent 6b5909ef
Pipeline #1197 passed with stage
......@@ -100,6 +100,17 @@ Proof. by destruct x as [[[]|]]. Qed.
Lemma own_validN n (x : auth A) : {n} x {n} own x.
Proof. destruct x as [[[]|]]; naive_solver eauto using cmra_validN_includedN. Qed.
Lemma auth_valid_discrete `{CMRADiscrete A} x :
x match authoritative x with
| Excl' a => own x a a
| None => own x
| ExclBot' => False
end.
Proof.
destruct x as [[[?|]|] ?]; simpl; try done.
setoid_rewrite <-cmra_discrete_included_iff; naive_solver eauto using 0.
Qed.
Lemma auth_cmra_mixin : CMRAMixin (auth A).
Proof.
apply cmra_total_mixin.
......
Markdown is supported
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