Commit 76a28786 authored by Robbert Krebbers's avatar Robbert Krebbers

Remove internalized properties of frac.

They are redundant because frac is discrete.
parent 2769834f
Pipeline #2592 passed with stage
in 4 minutes and 15 seconds
From Coq.QArith Require Import Qcanon.
From iris.algebra Require Export cmra.
From iris.algebra Require Import upred.
Notation frac := Qp (only parsing).
......@@ -20,12 +19,6 @@ Qed.
Canonical Structure fracR := discreteR frac frac_ra_mixin.
End frac.
(** Internalized properties *)
Lemma frac_equivI {M} (x y : frac) : x y (x = y : uPred M).
Proof. by uPred.unseal. Qed.
Lemma frac_validI {M} (x : frac) : x ( (x 1)%Qc : uPred M).
Proof. by uPred.unseal. Qed.
(** Exclusive *)
Global Instance frac_full_exclusive : Exclusive 1%Qp.
Proof.
......
......@@ -118,7 +118,7 @@ Section heap.
rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_ne //.
apply (anti_symm ()); last by apply pure_elim_l.
rewrite auth_own_valid gmap_validI (forall_elim l) lookup_singleton.
rewrite option_validI prod_validI frac_validI discrete_valid.
rewrite option_validI prod_validI !discrete_valid /=.
by apply pure_elim_r.
Qed.
......
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