Commit ea353e5f authored by Robbert Krebbers's avatar Robbert Krebbers

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.
parent 5fc07ae0
...@@ -195,11 +195,11 @@ Section ofe. ...@@ -195,11 +195,11 @@ Section ofe.
End ofe. End ofe.
(** Contractive functions *) (** 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. 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. 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. 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 := ...@@ -244,7 +244,7 @@ Ltac f_contractive :=
| |- ?f _ _ {_} ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f) | |- ?f _ _ {_} ?f _ _ => apply (_ : Proper (_ ==> dist_later _ ==> _) f)
end; end;
try match goal with 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)] destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end; end;
try reflexivity. try reflexivity.
......
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