Skip to content
Snippets Groups Projects

Fix brittle rewrite proof.

Merged Fix brittle rewrite proof.
snyke7/gpfsl:ike/fix_brittle_proof into master
1 unresolved thread
Merged Ike Mulder requested to merge snyke7/gpfsl:ike/fix_brittle_proof into master
1 unresolved thread
Compare
and
1 file
+ 1
− 1
Compare changes
  • Side-by-side
  • Inline
gpfsl/algebra/to_agree.v
+ 1
− 1
@@ -186,7 +186,7 @@ Proof.
intros INCL0 INCL VALID.
destruct INCL0 as [? Eq0]. destruct INCL as [? Eq'].
apply local_update_unital_discrete => z Valid Eq. split; [done|].
rewrite Eq Eq0. rewrite -cmra_assoc (cmra_comm _ z) cmra_assoc -Eq.
rewrite Eq Eq0. rewrite -cmra_assoc (cmra_comm x z) cmra_assoc -Eq.
symmetry. apply agreeM_absorb. rewrite Eq' Eq0.
etrans; last apply cmra_included_l. apply cmra_included_r.
Qed.