...
 
Commits (3)
......@@ -26,42 +26,11 @@ variables:
## Build jobs
build-coq.dev:
build-iris.dev:
<<: *template
variables:
OCAML: "ocaml-base-compiler.4.07.0"
OPAM_PINS: "coq version dev"
CI_COQCHK: "1"
build-coq.8.9.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.9.0"
OPAM_PKG: "coq-iris"
DOC_DIR: "coqdoc@center.mpi-sws.org:iris"
OPAM_PINS: "coq version 8.9.0 coq-stdpp.dev git git+https://gitlab.mpi-sws.org/iris/stdpp.git#robbert/tc_opaque"
TIMING_CONF: "coq-8.9.0"
tags:
- fp-timing
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.8.0:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.0"
TIMING_CONF: "coq-8.8.0"
tags:
- fp-timing
build-coq.8.7.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.2"
build-coq.8.7.1:
<<: *template
variables:
OPAM_PINS: "coq version 8.7.1"
......@@ -89,7 +89,7 @@ Section cmra.
Proof.
move=>x'; destruct (decide (x = x')) as [->|];
by rewrite ofe_fun_lookup_core ?ofe_fun_lookup_singleton
?ofe_fun_lookup_singleton_ne // (core_id_core ).
?ofe_fun_lookup_singleton_ne // (core_id_core ε).
Qed.
Global Instance ofe_fun_singleton_core_id x (y : B x) :
......
......@@ -92,7 +92,8 @@ Proof.
by apply: discrete; rewrite -Hm lookup_insert_ne.
Qed.
Global Instance gmap_singleton_discrete i x :
Discrete x Discrete ({[ i := x ]} : gmap K A) := _.
Discrete x Discrete ({[ i := x ]} : gmap K A).
Proof. rewrite /singletonM. apply _. Qed.
Lemma insert_idN n m i x :
m !! i {n} Some x <[i:=x]>m {n} m.
Proof. intros (y'&?&->)%dist_Some_inv_r'. by rewrite insert_id. Qed.
......
......@@ -296,10 +296,10 @@ Section properties.
Lemma replicate_valid n (x : A) : x replicate n x.
Proof. apply Forall_replicate. Qed.
Global Instance list_singletonM_ne i :
NonExpansive (@list_singletonM A i).
NonExpansive (singletonM (M:=list A) i).
Proof. intros n l1 l2 ?. apply Forall2_app; by repeat constructor. Qed.
Global Instance list_singletonM_proper i :
Proper (() ==> ()) (list_singletonM i) := ne_proper _.
Proper (() ==> ()) (singletonM (M:=list A) i) := ne_proper _.
Lemma elem_of_list_singletonM i z x : z ({[i := x]} : list A) z = ε z = x.
Proof.
......@@ -332,7 +332,7 @@ Section properties.
Lemma list_core_singletonM i (x : A) : core {[ i := x ]} {[ i := core x ]}.
Proof.
rewrite /singletonM /list_singletonM.
by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ).
by rewrite {1}/core /= fmap_app fmap_replicate (core_id_core ε).
Qed.
Lemma list_op_singletonM i (x y : A) :
{[ i := x ]} {[ i := y ]} {[ i := x y ]}.
......
......@@ -24,7 +24,7 @@ Corollary ufrac_included_weak (x y : ufrac) : x ≼ y → (x ≤ y)%Qc.
Proof. intros ?%ufrac_included. auto using Qclt_le_weak. Qed.
Definition ufrac_ra_mixin : RAMixin ufrac.
Proof. split; try apply _; try done. Qed.
Proof. split; try (apply _ || done). Qed.
Canonical Structure ufracR := discreteR ufrac ufrac_ra_mixin.
Global Instance ufrac_cmra_discrete : CmraDiscrete ufracR.
......
......@@ -10,7 +10,7 @@ Definition stuckness_leb (s1 s2 : stuckness) : bool :=
| _, _ => true
end.
Instance stuckness_le : SqSubsetEq stuckness := stuckness_leb.
Instance stuckness_le_po : PreOrder stuckness_le.
Instance stuckness_le_po : PreOrder (@{stuckness}).
Proof. split; by repeat intros []. Qed.
Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
......
......@@ -375,7 +375,7 @@ Global Instance frame_monPred_at_wand p P R Q1 Q2 i j :
Frame p R Q1 Q2
FrameMonPredAt p j (R i) (P - Q1) ((P - Q2) i).
Proof.
rewrite /Frame /FrameMonPredAt=>-> Hframe.
rewrite /IsBiIndexRel /Frame /FrameMonPredAt=>-> Hframe.
rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
change ((?p R (P - Q2)) - P - Q1). apply bi.wand_intro_r.
rewrite -assoc bi.wand_elim_l. done.
......@@ -385,7 +385,7 @@ Global Instance frame_monPred_at_impl P R Q1 Q2 i j :
Frame true R Q1 Q2
FrameMonPredAt true j (R i) (P Q1) ((P Q2) i).
Proof.
rewrite /Frame /FrameMonPredAt=>-> Hframe.
rewrite /IsBiIndexRel /Frame /FrameMonPredAt=>-> Hframe.
rewrite -monPred_at_intuitionistically_if -monPred_at_sep. apply monPred_in_entails.
change (( R (P Q2)) - P Q1).
rewrite -bi.persistently_and_intuitionistically_sep_l. apply bi.impl_intro_r.
......