From 9a797c9f5f4f9f2bc6ce867cfa0a19cae66b4a5b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 4 Jun 2015 11:00:39 +0200
Subject: [PATCH] some minor changes for better 8.5-compatibility
---
iris_derived_rules.v | 2 +-
iris_plog.v | 3 ++-
iris_vs_rules.v | 2 +-
lib/ModuRes/Finmap.v | 30 ++++++++----------------------
lib/ModuRes/Util.v | 2 --
5 files changed, 12 insertions(+), 27 deletions(-)
diff --git a/iris_derived_rules.v b/iris_derived_rules.v
index 51a519b72..404b686ab 100644
--- a/iris_derived_rules.v
+++ b/iris_derived_rules.v
@@ -1,4 +1,4 @@
-Require Import ssreflect.
+Require Import Ssreflect.ssreflect.
Require Import world_prop core_lang lang iris_core iris_plog iris_vs_rules iris_ht_rules.
Require Import ModuRes.RA ModuRes.SPred ModuRes.BI ModuRes.PreoMet ModuRes.Finmap ModuRes.CMRA ModuRes.DecEnsemble.
diff --git a/iris_plog.v b/iris_plog.v
index 6d60d1141..3f51b3869 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -248,7 +248,8 @@ Module Type IRIS_PLOG (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORL
exists w', P w' (S (S k))
/\ wsat σ (m2 ∪ mf) (w' · wf) (S (S k)))].
Next Obligation.
- inversion HLe.
+ repeat intro.
+ by inversion HLe.
Qed.
Next Obligation.
intros n1 n2 HLe HP wf; intros.
diff --git a/iris_vs_rules.v b/iris_vs_rules.v
index 9920535f7..9c4b024bd 100644
--- a/iris_vs_rules.v
+++ b/iris_vs_rules.v
@@ -165,7 +165,7 @@ Module Type IRIS_VS_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
- exists (w2, wq). split; last split.
+ rewrite [ra_op]lock. simpl. reflexivity.
+ assumption.
- + apply propsMN, HQ. omega.
+ + eapply propsMN, HQ. omega.
- now rewrite -assoc.
Qed.
diff --git a/lib/ModuRes/Finmap.v b/lib/ModuRes/Finmap.v
index 337ab7654..f2b2282d0 100644
--- a/lib/ModuRes/Finmap.v
+++ b/lib/ModuRes/Finmap.v
@@ -1,8 +1,8 @@
-Require Import ssreflect.
+Require Import Ssreflect.ssreflect Omega.
+Require Import Arith Min Max List ListSet Lists.
Require Import MetricCore.
Require Import PreoMet.
Require Import RA CMRA SPred.
-Require Import Arith Min Max List ListSet Lists.
Set Bullet Behavior "Strict Subproofs".
@@ -548,11 +548,11 @@ Section FinDom.
refine (fix F (l: list K) :=
match l as l return (forall f, dom f = l -> T f) with
| [] => fun f Hdom => Text fdEmpty f _ Temp
- | k::l => fun f Hdom => let f' := f \ k in
- let Hindom: k ∈ dom f := _ in
- let v' := fdLookup_indom f k Hindom in
- Text (fdStrongUpdate k (Some v') f') f _
- (Tstep k v' f' _ (F l f' _))
+ | k::l' => fun f Hdom => let f' := f \ k in
+ let Hindom: k ∈ dom f := _ in
+ let v' := fdLookup_indom f k Hindom in
+ Text (fdStrongUpdate k (Some v') f') f _
+ (Tstep k v' f' _ (F l' f' _))
end); clear F.
- split.
+ move=>k /=. symmetry. apply fdLookup_notin_strong. rewrite Hdom. tauto.
@@ -566,7 +566,7 @@ Section FinDom.
+ rewrite Hdom /dom /=. f_equal. rewrite /dom /= Hdom.
rewrite DecEq_refl.
assert (Hnod := dom_nodup f). rewrite Hdom in Hnod.
- assert (Hfilt1: (filter_dupes [] l0) = l0).
+ assert (Hfilt1: (filter_dupes [] l') = l').
{ apply filter_dupes_id. simpl. inversion Hnod; subst. assumption. }
rewrite Hfilt1. apply filter_dupes_id. assumption.
- subst f'. apply fdLookup_notin. rewrite fdStrongUpdate_eq. reflexivity.
@@ -581,20 +581,6 @@ Section FinDom.
fun f => fdRectInner (dom f) f eq_refl.
End Recursion.
- (* No need to restrict this Lemma to fdRectInner - that just messes up the details. *)
-(* Lemma fdRectInner_eqL l l' f (Heq: dom f = l) (Heq': dom f = l')
- (T: (K -f> V) -> Type) (F: forall l (f: K -f> V), dom f = l -> T f) :
- F l f Heq = F l' f Heq'.
- Proof.
- assert (Heql: l = l').
- { transitivity (dom f); first symmetry; assumption. }
- revert Heq'.
- refine (match Heql in eq _ l'' return (forall Heq' : dom f = l'', F l f Heq = F l'' f Heq') with
- | eq_refl => _
- end).
- move=>Heq'. reflexivity.
- Qed. *)
-
Section Fold.
Context {T: Type}.
Context (Temp: T) (Tstep: K -> V -> T -> T).
diff --git a/lib/ModuRes/Util.v b/lib/ModuRes/Util.v
index 43eb10cdc..8de64a139 100644
--- a/lib/ModuRes/Util.v
+++ b/lib/ModuRes/Util.v
@@ -71,5 +71,3 @@ Ltac contradiction_eq := match goal with
(* Well-founded induction. *)
Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
-
-
\ No newline at end of file
--
GitLab