Commit c0c61da9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris and start porting to Coq master.

parent a3867545
Pipeline #17181 failed with stage
in 6 minutes and 58 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "dev.2019-04-25.0.3a0ab5e6") | (= "dev") }
"coq-iris" { (= "dev.2019-05-20.1.eb3117bd") | (= "dev") }
]
From fri.algebra Require Export ofe step.
Class PCore (A : Type) := pcore : A option A.
Instance: Params (@pcore) 2.
Instance: Params (@pcore) 2 := {}.
Class Op (A : Type) := op : A A A.
Instance: Params (@op) 2.
Instance: Params (@op) 2 := {}.
Infix "⋅" := op (at level 50, left associativity) : stdpp_scope.
Notation "(⋅)" := op (only parsing) : stdpp_scope.
......@@ -16,23 +16,23 @@ Notation "(⋅)" := op (only parsing) : stdpp_scope.
Definition included `{Equiv A, Op A} (x y : A) := z, y x z.
Infix "≼" := included (at level 70) : stdpp_scope.
Notation "(≼)" := included (only parsing) : stdpp_scope.
Hint Extern 0 (_ _) => reflexivity.
Instance: Params (@included) 3.
Hint Extern 0 (_ _) => reflexivity : core.
Instance: Params (@included) 3 := {}.
Class ValidN (A : Type) := validN : nat A Prop.
Instance: Params (@validN) 3.
Instance: Params (@validN) 3 := {}.
Notation "✓{ n } x" := (validN n x)
(at level 20, n at next level, format "✓{ n } x").
Class Valid (A : Type) := valid : A Prop.
Instance: Params (@valid) 2.
Instance: Params (@valid) 2 := {}.
Notation "✓ x" := (valid x) (at level 20) : stdpp_scope.
Definition includedN `{Dist A, Op A} (n : nat) (x y : A) := z, y {n} x z.
Notation "x ≼{ n } y" := (includedN n x y)
(at level 70, n at next level, format "x ≼{ n } y") : stdpp_scope.
Instance: Params (@includedN) 4.
Hint Extern 0 (_ {_} _) => reflexivity.
Instance: Params (@includedN) 4 := {}.
Hint Extern 0 (_ {_} _) => reflexivity : core.
Record CMRAMixin A
`{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A, StepN A} := {
......@@ -175,7 +175,7 @@ core. *)
Class CMRATotal (A : cmraT) := cmra_total (x : A) : is_Some (pcore x).
Class Core (A : Type) := core : A A.
Instance: Params (@core) 2.
Instance: Params (@core) 2 := {}.
Instance core' `{PCore A} : Core A := λ x, from_option id x (pcore x).
Arguments core' _ _ _ /.
......@@ -625,7 +625,8 @@ Section ucmra.
Qed.
End ucmra_transport.
End ucmra.
Hint Immediate cmra_unit_total.
Hint Immediate cmra_unit_total : core.
(** * Constructing a CMRA with total core *)
Section cmra_total.
......@@ -705,14 +706,13 @@ Structure rFunctor := RFunctor {
CMRAMonotone (rFunctor_map fg)
}.
Existing Instances rFunctor_ne rFunctor_mono.
Instance: Params (@rFunctor_map) 5.
Instance: Params (@rFunctor_map) 5 := {}.
Class rFunctorContractive (F : rFunctor) :=
rFunctor_contractive A1 A2 B1 B2 :> Contractive (@rFunctor_map F A1 A2 B1 B2).
Definition rFunctor_diag (F: rFunctor) (A: ofeT) : cmraT := rFunctor_car F A A.
Coercion rFunctor_diag : rFunctor >-> Funclass.
Program Definition constRF (B : cmraT) : rFunctor :=
{| rFunctor_car A1 A2 := B; rFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.
......@@ -734,7 +734,7 @@ Structure urFunctor := URFunctor {
CMRAMonotone (urFunctor_map fg)
}.
Existing Instances urFunctor_ne urFunctor_mono.
Instance: Params (@urFunctor_map) 5.
Instance: Params (@urFunctor_map) 5 := {}.
Class urFunctorContractive (F : urFunctor) :=
urFunctor_contractive A1 A2 B1 B2 :> Contractive (@urFunctor_map F A1 A2 B1 B2).
......
......@@ -4,10 +4,10 @@ From stdpp Require Import gmap.
Fixpoint big_op {A : ucmraT} (xs : list A) : A :=
match xs with [] => | x :: xs => x big_op xs end.
Arguments big_op _ !_ /.
Instance: Params (@big_op) 1.
Instance: Params (@big_op) 1 := {}.
Definition big_opM `{Countable K} {A : ucmraT} (m : gmap K A) : A :=
big_op (snd <$> map_to_list m).
Instance: Params (@big_opM) 4.
Instance: Params (@big_opM) 4 := {}.
(** * Properties about big ops *)
Section big_op.
......
......@@ -40,11 +40,11 @@ Module ra_reflection. Section ra_reflection.
Qed.
Class Quote (Σ1 Σ2 : list A) (l : A) (e : expr) := {}.
Global Instance quote_empty: Quote E1 E1 EEmpty.
Global Instance quote_empty: Quote E1 E1 EEmpty := {}.
Global Instance quote_var Σ1 Σ2 e i:
rlist.QuoteLookup Σ1 Σ2 e i Quote Σ1 Σ2 e (EVar i) | 1000.
rlist.QuoteLookup Σ1 Σ2 e i Quote Σ1 Σ2 e (EVar i) | 1000 := {}.
Global Instance quote_app Σ1 Σ2 Σ3 x1 x2 e1 e2 :
Quote Σ1 Σ2 x1 e1 Quote Σ2 Σ3 x2 e2 Quote Σ1 Σ3 (x1 x2) (EOp e1 e2).
Quote Σ1 Σ2 x1 e1 Quote Σ2 Σ3 x2 e2 Quote Σ1 Σ3 (x1 x2) (EOp e1 e2) := {}.
End ra_reflection.
Ltac quote :=
......
......@@ -85,7 +85,7 @@ Definition csum_map {A A' B B'} (fA : A → A') (fB : B → B')
| Cinr b => Cinr (fB b)
| CsumBot => CsumBot
end.
Instance: Params (@csum_map) 4.
Instance: Params (@csum_map) 4 := {}.
Lemma csum_map_id {A B} (x : csum A B) : csum_map id id x = x.
Proof. by destruct x. Qed.
......
......@@ -8,7 +8,7 @@ Definition iprod `{Finite A} (B : A → ofeT) := ∀ x, B x.
Definition iprod_insert `{Finite A} {B : A ofeT}
(x : A) (y : B x) (f : iprod B) : iprod B := λ x',
match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
Instance: Params (@iprod_insert) 5.
Instance: Params (@iprod_insert) 5 := {}.
Section iprod_cofe.
Context `{Finite A} {B : A ofeT}.
......@@ -173,7 +173,7 @@ Arguments iprodUR {_ _ _} _.
Definition iprod_singleton `{Finite A} {B : A ucmraT}
(x : A) (y : B x) : iprod B := iprod_insert x y .
Instance: Params (@iprod_singleton) 5.
Instance: Params (@iprod_singleton) 5 := {}.
Section iprod_singleton.
Context `{Finite A} {B : A ucmraT}.
......
......@@ -7,7 +7,7 @@ Record local_update {A : cmraT} (mz : option A) (x y : A) := {
{n} (x ? mz) x ? mz {n} x ? mz' y ? mz {n} y ? mz'
}.
Notation "x ~l~> y @ mz" := (local_update mz x y) (at level 70).
Instance: Params (@local_update) 1.
Instance: Params (@local_update) 1 := {}.
Section updates.
Context {A : cmraT}.
......
......@@ -72,7 +72,7 @@ Section cofe_rel.
End cofe_rel.
Class StepN (A : Type) := stepN : nat A A Prop.
Instance: Params (@stepN) 3.
Instance: Params (@stepN) 3 := {}.
Infix "⤳_( n )" := (stepN n) (at level 51, left associativity) : stdpp_scope.
Class uStep (A: ofeT) `{StepN A} := {
ustep_ne n : Proper (dist n ==> dist n ==> impl) (stepN n);
......@@ -81,7 +81,7 @@ Class uStep (A: ofeT) `{StepN A} := {
}.
Class Step (A : Type) := step : A -> A Prop.
Instance: Params (@step) 2.
Instance: Params (@step) 2 := {}.
Infix "⤳ " := step (at level 51, left associativity) : stdpp_scope.
(* JDT: NB this is probably _NOT_ the right notion, better to say that if A is a cofe,
then there are two chains c, c' such that for each n, (c n) _(n) (c' n), and
......@@ -216,7 +216,7 @@ Section stepn.
eapply ustep_ne; try apply equiv_dist; eauto.
Qed.
Global Instance shiftN_adm_proper r (H: shiftN_admissible r) n: Proper (() ==> () ==> impl) (r n).
Global Instance shiftN_adm_proper r (_: shiftN_admissible r) n: Proper (() ==> () ==> impl) (r n).
Proof.
intros x y Hd x' y' Hd' Hs.
eapply shiftN_adm_ne; try apply equiv_dist; eauto.
......
......@@ -44,7 +44,7 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
S = λ s, up s T.
(** Tactic setup *)
Hint Resolve Step.
Hint Resolve Step : core.
Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
......@@ -337,9 +337,9 @@ Section sts_definitions.
Definition sts_frag_up (s : sts.state sts) (T : sts.tokens sts) : stsR sts :=
sts_frag (sts.up s T) T.
End sts_definitions.
Instance: Params (@sts_auth) 2.
Instance: Params (@sts_frag) 1.
Instance: Params (@sts_frag_up) 2.
Instance: Params (@sts_auth) 2 := {}.
Instance: Params (@sts_frag) 1 := {}.
Instance: Params (@sts_frag_up) 2 := {}.
Section stsRA.
Import sts.
......
......@@ -7,23 +7,23 @@ From fri.algebra Require Export cmra.
*)
Definition cmra_updateP {A : cmraT} (x : A) (P : A Prop) := n mz,
{n} (x ? mz) y, P y {n} (y ? mz).
Instance: Params (@cmra_updateP) 1.
Instance: Params (@cmra_updateP) 1 := {}.
Infix "~~>:" := cmra_updateP (at level 70).
Definition cmra_update {A : cmraT} (x y : A) := n mz,
{n} (x ? mz) {n} (y ? mz).
Infix "~~>" := cmra_update (at level 70).
Instance: Params (@cmra_update) 1.
Instance: Params (@cmra_update) 1 := {}.
Definition cmra_step_updateP {A : cmraT} (x : A) (xl: A) (P : A A Prop) := n mz,
{n} (x xl ? mz) y yl, P y yl {n} (y yl ? mz) xl _(n) yl.
Notation "x # y ~~>>: P" := (cmra_step_updateP x y P) (at level 70).
Instance: Params (@cmra_step_updateP) 1.
Instance: Params (@cmra_step_updateP) 1 := {}.
Definition cmra_step_update {A : cmraT} (x xl y yl : A) := n mz,
{n} (x xl ? mz) {n} (y yl ? mz) xl _(n) yl.
Notation "x # xl ~~>> y #' yl " := (cmra_step_update x xl y yl) (at level 70).
Instance: Params (@cmra_step_update) 1.
Instance: Params (@cmra_step_update) 1 := {}.
Section updates.
......
......@@ -15,7 +15,7 @@ Record uPred (M : ucmraT) : Type := IProp {
}.
Arguments uPred_holds {_} _ _ _ _ : simpl never.
Add Printing Constructor uPred.
Instance: Params (@uPred_holds) 3.
Instance: Params (@uPred_holds) 3 := {}.
Delimit Scope uPred_scope with IP.
Bind Scope uPred_scope with uPred.
......@@ -135,8 +135,8 @@ Qed.
(** logical entailement *)
Inductive uPred_entails {M} (P Q : uPred M) : Prop :=
{ uPred_in_entails : n x y, {n} x {n} y P n x y Q n x y}.
Hint Extern 0 (uPred_entails _ _) => reflexivity.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M).
Hint Extern 0 (uPred_entails _ _) => reflexivity : core.
Instance uPred_entails_rewrite_relation M : RewriteRelation (@uPred_entails M) := {}.
Hint Resolve uPred_mono uPred_closed : uPred_def.
......@@ -394,7 +394,7 @@ Infix "≡" := (uPred_eq) : uPred_scope.
Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P Q) (Q P))%IP.
Instance: Params (@uPred_iff) 1.
Instance: Params (@uPred_iff) 1 := {}.
Infix "↔" := uPred_iff : uPred_scope.
Program Definition uPred_plainly_def {M} (P : uPred M) : uPred M :=
......@@ -434,7 +434,7 @@ Implicit Types A : Type.
Local Notation "P ⊢ Q" := (@uPred_entails M P%IP Q%IP). (* Force implicit argument M *)
Local Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%IP Q%IP). (* Force implicit argument M *)
Arguments uPred_holds {_} !_ _ _ _ /.
Hint Immediate uPred_in_entails.
Hint Immediate uPred_in_entails : core.
Global Instance: PreOrder (@uPred_entails M).
Proof.
......
......@@ -1337,8 +1337,7 @@ Qed.
rewrite val_equiv_fix_unfold'. done. }
iExists #(). iFrame.
rewrite val_equiv_fix_unfold'. rewrite //=.
iIntros "!#". iSplitL ""; auto.
by rewrite val_equiv_fix_unfold'.
- intros; iIntros "#HS". simpl.
rewrite (msubst_unfold (sval <$> S)) // (msubst_unfold (tval <$> S)) //.
iIntros (i K) "!# !# Hown".
......
......@@ -139,7 +139,7 @@ Section compact_setoid.
l : list A, x : A, x X x' : A, x x' x' l.
Instance set_finite_setoid_subseteq `{Equiv A} `{Equiv B}
{Equ: @Equivalence A equiv} {H: ElemOf A B}:
{Equ: @Equivalence A equiv} `{ElemOf A B}:
Proper (subseteq --> impl) (@set_finite_setoid A _ B _).
Proof.
intros X Y. rewrite /flip. intros Hsub (l&Hfin_in).
......
......@@ -31,12 +31,12 @@ Arguments inG_id {_ _ _} _.
Definition to_globalF `{i: inG Λ Σ (gmapUR gname A)} (γ : gname) (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton (inG_id i) (ucmra_transport inG_prf ({[ γ := a ]})).
Instance: Params (@to_globalF) 5.
Instance: Params (@to_globalF) 5 := {}.
Typeclasses Opaque to_globalF.
Definition to_globalFe `{i: inG Λ Σ A} (a : A) : iGst Λ (globalF Σ) :=
iprod_singleton (inG_id i) (ucmra_transport inG_prf a).
Instance: Params (@to_globalFe) 4.
Instance: Params (@to_globalFe) 4 := {}.
Typeclasses Opaque to_globalFe.
(** * Properties of to_globalC *)
......
......@@ -9,10 +9,10 @@ Arguments ownI {_ _} _ _%I.
Definition ownP {Λ Σ} (σ: state Λ) : iProp Λ Σ := ( (uPred_ownM (Res (Excl' σ) )))%I.
Definition ownG {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := ( (uPred_ownM (Res m)))%I.
Definition ownGl {Λ Σ} (m: iGst Λ Σ) : iProp Λ Σ := uPred_ownMl (Res m).
Instance: Params (@ownI) 3.
Instance: Params (@ownP) 2.
Instance: Params (@ownG) 2.
Instance: Params (@ownGl) 2.
Instance: Params (@ownI) 3 := {}.
Instance: Params (@ownP) 2 := {}.
Instance: Params (@ownG) 2 := {}.
Instance: Params (@ownGl) 2 := {}.
Typeclasses Opaque ownI ownG ownP.
......
......@@ -12,10 +12,10 @@ Arguments Res {_ _ _} _ _ _.
Arguments wld {_ _ _} _.
Arguments pst {_ _ _} _.
Arguments gst {_ _ _} _.
Instance: Params (@Res) 3.
Instance: Params (@wld) 3.
Instance: Params (@pst) 3.
Instance: Params (@gst) 3.
Instance: Params (@Res) 3 := {}.
Instance: Params (@wld) 3 := {}.
Instance: Params (@pst) 3 := {}.
Instance: Params (@gst) 3 := {}.
Section res.
Context {Λ : language} {A : ofeT} {M : ucmraT}.
......@@ -219,9 +219,9 @@ Instance res_map_cmra_monotone {Λ}
CMRAMonotone (@res_map Λ _ _ _ _ f g).
Proof.
split; first apply _.
- intros n r (?&?&?); split_and!; simpl; by try apply: validN_preserving.
- intros n r (?&?&?); split_and!=> //=; by apply: validN_preserving.
- by intros r1 r2; rewrite !res_included;
intros (?&?&?); split_and!; simpl; try apply: cmra_monotone.
intros (?&?&?); split_and!=> //=; by apply: cmra_monotone.
Qed.
Definition resC_map {Λ} {A A' : ofeT} {M M' : ucmraT}
(f : A -n> A') (g : M -n> M') : resC Λ A M -n> resC Λ A' M' :=
......
......@@ -26,7 +26,7 @@ Arguments wsat_pre_wld {_ _ _ _ _ _ _} _ _ _ _ _ _.
Definition wsat {Λ Σ}
(n : nat) (E : coPset) (σ : state Λ) (r : iRes Λ Σ) (rl: iRes Λ Σ): Prop :=
match n with 0 => True | S n => rs, wsat_pre n E σ rs (r big_opM rs) rl end.
Instance: Params (@wsat) 5.
Instance: Params (@wsat) 5 := {}.
Arguments wsat : simpl never.
Section wsat.
......
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