From ea353e5f79aa49ea8204064080043a11dceaee8e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 15 Aug 2017 19:54:15 +0200
Subject: [PATCH] Have dist_later not depend on an ofeT, but on an unbundled
Dist.
That way, we can use Contractive as part of structure definitions in
which we do not have a bundled OFE yet.
---
theories/algebra/ofe.v | 8 ++++----
1 file changed, 4 insertions(+), 4 deletions(-)
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index c32b4af9e..1796ace9e 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -195,11 +195,11 @@ Section ofe.
End ofe.
(** Contractive functions *)
-Definition dist_later {A : ofeT} (n : nat) (x y : A) : Prop :=
+Definition dist_later `{Dist A} (n : nat) (x y : A) : Prop :=
match n with 0 => True | S n => x ≡{n}≡ y end.
-Arguments dist_later _ !_ _ _ /.
+Arguments dist_later _ _ !_ _ _ /.
-Global Instance dist_later_equivalence A n : Equivalence (@dist_later A n).
+Global Instance dist_later_equivalence (A : ofeT) n : Equivalence (@dist_later A _ n).
Proof. destruct n as [|n]. by split. apply dist_equivalence. Qed.
Lemma dist_dist_later {A : ofeT} n (x y : A) : dist n x y → dist_later n x y.
@@ -244,7 +244,7 @@ Ltac f_contractive :=
| |- ?f _ _ ≡{_}≡ ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
end;
try match goal with
- | |- @dist_later ?A ?n ?x ?y =>
+ | |- @dist_later ?A _ ?n ?x ?y =>
destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end;
try reflexivity.
--
GitLab