From 76a2878624c0e98e52f9731963162a1d588d7a95 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 11 Aug 2016 11:38:12 +0200
Subject: [PATCH] Remove internalized properties of frac.

They are redundant because frac is discrete.
---
 algebra/frac.v   | 7 -------
 heap_lang/heap.v | 2 +-
 2 files changed, 1 insertion(+), 8 deletions(-)

diff --git a/algebra/frac.v b/algebra/frac.v
index 47fd97642..2a10b1cd1 100644
--- a/algebra/frac.v
+++ b/algebra/frac.v
@@ -1,6 +1,5 @@
 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.
diff --git a/heap_lang/heap.v b/heap_lang/heap.v
index 2457a9577..597066ded 100644
--- a/heap_lang/heap.v
+++ b/heap_lang/heap.v
@@ -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.
 
-- 
GitLab