Commit 87729375 authored by Robbert's avatar Robbert

Merge branch 'ci/robbert/iprop_structures' into 'master'

Let `iProp` refer to `uPred ... : Type` instead of `uPredO ... : ofeT`

See merge request iris/iris!314
parents 7b9acc61 1c162639
...@@ -9,6 +9,8 @@ Coq development, but not every API-breaking change is listed. Changes marked ...@@ -9,6 +9,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
* A new tactic `iStopProof` to turn the proof mode entailment into an ordinary * A new tactic `iStopProof` to turn the proof mode entailment into an ordinary
Coq goal `big star of context ⊢ proof mode goal`. Coq goal `big star of context ⊢ proof mode goal`.
* Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s.
Introduce `iProp` for the `Type` carrier of `iPropO`.
## Iris 3.2.0 (released 2019-08-29) ## Iris 3.2.0 (released 2019-08-29)
......
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
Instance test_cofe {Σ} : Cofe (iPreProp Σ) := _. Instance test_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Section tests. Section tests.
Context `{!invG Σ}. Context `{!invG Σ}.
Program Definition test : (iProp Σ -n> iProp Σ) -n> (iProp Σ -n> iProp Σ) := Program Definition test : (iPropO Σ -n> iPropO Σ) -n> (iPropO Σ -n> iPropO Σ) :=
λne P v, ( (P v))%I. λne P v, ( (P v))%I.
Solve Obligations with solve_proper. Solve Obligations with solve_proper.
......
...@@ -8,7 +8,7 @@ Import uPred. ...@@ -8,7 +8,7 @@ Import uPred.
Class boxG Σ := Class boxG Σ :=
boxG_inG :> inG Σ (prodR boxG_inG :> inG Σ (prodR
(authR (optionUR (exclR boolO))) (authR (optionUR (exclR boolO)))
(optionR (agreeR (laterO (iPreProp Σ))))). (optionR (agreeR (laterO (iPrePropO Σ))))).
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolO)) * Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolO)) *
optionRF (agreeRF ( )) ) ]. optionRF (agreeRF ( )) ) ].
......
...@@ -116,20 +116,21 @@ Qed. ...@@ -116,20 +116,21 @@ Qed.
the construction, this way we are sure we do not use any properties of the the construction, this way we are sure we do not use any properties of the
construction, and also avoid Coq from blindly unfolding it. *) construction, and also avoid Coq from blindly unfolding it. *)
Module Type iProp_solution_sig. Module Type iProp_solution_sig.
Parameter iPreProp : gFunctors ofeT. Parameter iPrePropO : gFunctors ofeT.
Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ). Global Declare Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ).
Definition iResUR (Σ : gFunctors) : ucmraT := Definition iResUR (Σ : gFunctors) : ucmraT :=
discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)). discrete_funUR (λ i, gmapUR gname (Σ i (iPrePropO Σ) _)).
Notation iProp Σ := (uPredO (iResUR Σ)). Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
Notation iPropI Σ := (uPredI (iResUR Σ)). Notation iPropI Σ := (uPredI (iResUR Σ)).
Notation iPropSI Σ := (uPredSI (iResUR Σ)). Notation iPropSI Σ := (uPredSI (iResUR Σ)).
Parameter iProp_unfold: {Σ}, iProp Σ -n> iPreProp Σ. Parameter iProp_unfold: {Σ}, iPropO Σ -n> iPrePropO Σ.
Parameter iProp_fold: {Σ}, iPreProp Σ -n> iProp Σ. Parameter iProp_fold: {Σ}, iPrePropO Σ -n> iPropO Σ.
Parameter iProp_fold_unfold: {Σ} (P : iProp Σ), Parameter iProp_fold_unfold: {Σ} (P : iProp Σ),
iProp_fold (iProp_unfold P) P. iProp_fold (iProp_unfold P) P.
Parameter iProp_unfold_fold: {Σ} (P : iPreProp Σ), Parameter iProp_unfold_fold: {Σ} (P : iPrePropO Σ),
iProp_unfold (iProp_fold P) P. iProp_unfold (iProp_fold P) P.
End iProp_solution_sig. End iProp_solution_sig.
...@@ -137,19 +138,20 @@ Module Export iProp_solution : iProp_solution_sig. ...@@ -137,19 +138,20 @@ Module Export iProp_solution : iProp_solution_sig.
Import cofe_solver. Import cofe_solver.
Definition iProp_result (Σ : gFunctors) : Definition iProp_result (Σ : gFunctors) :
solution (uPredOF (iResF Σ)) := solver.result _. solution (uPredOF (iResF Σ)) := solver.result _.
Definition iPreProp (Σ : gFunctors) : ofeT := iProp_result Σ. Definition iPrePropO (Σ : gFunctors) : ofeT := iProp_result Σ.
Global Instance iPreProp_cofe {Σ} : Cofe (iPreProp Σ) := _. Global Instance iPreProp_cofe {Σ} : Cofe (iPrePropO Σ) := _.
Definition iResUR (Σ : gFunctors) : ucmraT := Definition iResUR (Σ : gFunctors) : ucmraT :=
discrete_funUR (λ i, gmapUR gname (Σ i (iPreProp Σ) _)). discrete_funUR (λ i, gmapUR gname (Σ i (iPrePropO Σ) _)).
Notation iProp Σ := (uPredO (iResUR Σ)). Notation iProp Σ := (uPred (iResUR Σ)).
Notation iPropO Σ := (uPredO (iResUR Σ)).
Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := Definition iProp_unfold {Σ} : iPropO Σ -n> iPrePropO Σ :=
solution_fold (iProp_result Σ). solution_fold (iProp_result Σ).
Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _. Definition iProp_fold {Σ} : iPrePropO Σ -n> iPropO Σ := solution_unfold _.
Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) P. Lemma iProp_fold_unfold {Σ} (P : iProp Σ) : iProp_fold (iProp_unfold P) P.
Proof. apply solution_unfold_fold. Qed. Proof. apply solution_unfold_fold. Qed.
Lemma iProp_unfold_fold {Σ} (P : iPreProp Σ) : iProp_unfold (iProp_fold P) P. Lemma iProp_unfold_fold {Σ} (P : iPrePropO Σ) : iProp_unfold (iProp_fold P) P.
Proof. apply solution_fold_unfold. Qed. Proof. apply solution_fold_unfold. Qed.
End iProp_solution. End iProp_solution.
......
...@@ -9,10 +9,10 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is ...@@ -9,10 +9,10 @@ individual CMRAs instead of (lists of) CMRA *functors*. This additional class is
needed because Coq is otherwise unable to solve type class constraints due to needed because Coq is otherwise unable to solve type class constraints due to
higher-order unification problems. *) higher-order unification problems. *)
Class inG (Σ : gFunctors) (A : cmraT) := Class inG (Σ : gFunctors) (A : cmraT) :=
InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPreProp Σ) _ }. InG { inG_id : gid Σ; inG_prf : A = Σ inG_id (iPrePropO Σ) _ }.
Arguments inG_id {_ _} _. Arguments inG_id {_ _} _.
Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPreProp Σ) _). Lemma subG_inG Σ (F : gFunctor) : subG F Σ inG Σ (F (iPrePropO Σ) _).
Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed. Proof. move=> /(_ 0%fin) /= [j ->]. by exists j. Qed.
(** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *) (** This tactic solves the usual obligations "subG ? Σ → {in,?}G ? Σ" *)
......
...@@ -9,7 +9,7 @@ Import uPred. ...@@ -9,7 +9,7 @@ Import uPred.
saved whatever-you-like. *) saved whatever-you-like. *)
Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG { Class savedAnythingG (Σ : gFunctors) (F : oFunctor) := SavedAnythingG {
saved_anything_inG :> inG Σ (agreeR (F (iPreProp Σ) _)); saved_anything_inG :> inG Σ (agreeR (F (iPrePropO Σ) _));
saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *) saved_anything_contractive : oFunctorContractive F (* NOT an instance to avoid cycles with [subG_savedAnythingΣ]. *)
}. }.
Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors := Definition savedAnythingΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
...@@ -20,14 +20,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} : ...@@ -20,14 +20,14 @@ Instance subG_savedAnythingΣ {Σ F} `{!oFunctorContractive F} :
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
Definition saved_anything_own `{!savedAnythingG Σ F} Definition saved_anything_own `{!savedAnythingG Σ F}
(γ : gname) (x : F (iProp Σ) _) : iProp Σ := (γ : gname) (x : F (iPropO Σ) _) : iProp Σ :=
own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)). own γ (to_agree $ (oFunctor_map F (iProp_fold, iProp_unfold) x)).
Typeclasses Opaque saved_anything_own. Typeclasses Opaque saved_anything_own.
Instance: Params (@saved_anything_own) 4 := {}. Instance: Params (@saved_anything_own) 4 := {}.
Section saved_anything. Section saved_anything.
Context `{!savedAnythingG Σ F}. Context `{!savedAnythingG Σ F}.
Implicit Types x y : F (iProp Σ) _. Implicit Types x y : F (iPropO Σ) _.
Implicit Types γ : gname. Implicit Types γ : gname.
Global Instance saved_anything_persistent γ x : Global Instance saved_anything_persistent γ x :
...@@ -106,7 +106,7 @@ Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ) ...@@ -106,7 +106,7 @@ Definition saved_pred_own `{!savedPredG Σ A} (γ : gname) (Φ : A → iProp Σ)
saved_anything_own (F := A -d> ) γ (OfeMor Next Φ). saved_anything_own (F := A -d> ) γ (OfeMor Next Φ).
Instance saved_pred_own_contractive `{!savedPredG Σ A} γ : Instance saved_pred_own_contractive `{!savedPredG Σ A} γ :
Contractive (saved_pred_own γ : (A -d> iProp Σ) iProp Σ). Contractive (saved_pred_own γ : (A -d> iPropO Σ) iProp Σ).
Proof. Proof.
solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]). solve_proper_core ltac:(fun _ => first [ intros ?; progress simpl | by auto | f_contractive | f_equiv ]).
Qed. Qed.
......
...@@ -9,7 +9,7 @@ exception of what's in the [invG] module. The module [invG] is thus exported in ...@@ -9,7 +9,7 @@ exception of what's in the [invG] module. The module [invG] is thus exported in
[fancy_updates], which [wsat] is only imported. *) [fancy_updates], which [wsat] is only imported. *)
Module invG. Module invG.
Class invG (Σ : gFunctors) : Set := WsatG { Class invG (Σ : gFunctors) : Set := WsatG {
inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ))))); inv_inG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPrePropO Σ)))));
enabled_inG :> inG Σ coPset_disjR; enabled_inG :> inG Σ coPset_disjR;
disabled_inG :> inG Σ (gset_disjR positive); disabled_inG :> inG Σ (gset_disjR positive);
invariant_name : gname; invariant_name : gname;
...@@ -23,7 +23,7 @@ Module invG. ...@@ -23,7 +23,7 @@ Module invG.
GFunctor (gset_disjUR positive)]. GFunctor (gset_disjUR positive)].
Class invPreG (Σ : gFunctors) : Set := WsatPreG { Class invPreG (Σ : gFunctors) : Set := WsatPreG {
inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPreProp Σ))))); inv_inPreG :> inG Σ (authR (gmapUR positive (agreeR (laterO (iPrePropO Σ)))));
enabled_inPreG :> inG Σ coPset_disjR; enabled_inPreG :> inG Σ coPset_disjR;
disabled_inPreG :> inG Σ (gset_disjR positive); disabled_inPreG :> inG Σ (gset_disjR positive);
}. }.
...@@ -33,7 +33,7 @@ Module invG. ...@@ -33,7 +33,7 @@ Module invG.
End invG. End invG.
Import invG. Import invG.
Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPreProp Σ)) := Definition invariant_unfold {Σ} (P : iProp Σ) : agree (later (iPrePropO Σ)) :=
to_agree (Next (iProp_unfold P)). to_agree (Next (iProp_unfold P)).
Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ := Definition ownI `{!invG Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
own invariant_name ( {[ i := invariant_unfold P ]}). own invariant_name ( {[ i := invariant_unfold P ]}).
......
...@@ -37,8 +37,8 @@ Qed. ...@@ -37,8 +37,8 @@ Qed.
(* Uncurry [twp_pre] and equip its type with an OFE structure *) (* Uncurry [twp_pre] and equip its type with an OFE structure *)
Definition twp_pre' `{!irisG Λ Σ} (s : stuckness) : Definition twp_pre' `{!irisG Λ Σ} (s : stuckness) :
(prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) iProp Σ) (prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) iPropO Σ)
prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) iProp Σ := prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) iPropO Σ :=
curry3 twp_pre s uncurry3. curry3 twp_pre s uncurry3.
Local Instance twp_pre_mono' `{!irisG Λ Σ} s : BiMonoPred (twp_pre' s). Local Instance twp_pre_mono' `{!irisG Λ Σ} s : BiMonoPred (twp_pre' s).
...@@ -76,7 +76,7 @@ Lemma twp_ind s Ψ : ...@@ -76,7 +76,7 @@ Lemma twp_ind s Ψ :
Proof. Proof.
iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq. iIntros (HΨ). iIntros "#IH" (e E Φ) "H". rewrite twp_eq.
set (Ψ' := curry3 Ψ : set (Ψ' := curry3 Ψ :
prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iProp Σ) iProp Σ). prodO (prodO (leibnizO coPset) (exprO Λ)) (val Λ -d> iPropO Σ) iPropO Σ).
assert (NonExpansive Ψ'). assert (NonExpansive Ψ').
{ intros n [[E1 e1] Φ1] [[E2 e2] Φ2] { intros n [[E1 e1] Φ1] [[E2 e2] Φ2]
[[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. } [[?%leibniz_equiv ?%leibniz_equiv] ?]; simplify_eq/=. by apply HΨ. }
......
...@@ -25,8 +25,8 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG { ...@@ -25,8 +25,8 @@ Class irisG (Λ : language) (Σ : gFunctors) := IrisG {
Global Opaque iris_invG. Global Opaque iris_invG.
Definition wp_pre `{!irisG Λ Σ} (s : stuckness) Definition wp_pre `{!irisG Λ Σ} (s : stuckness)
(wp : coPset -d> expr Λ -d> (val Λ -d> iProp Σ) -d> iProp Σ) : (wp : coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ) :
coPset -d> expr Λ -d> (val Λ -d> iProp Σ) -d> iProp Σ := λ E e1 Φ, coPset -d> expr Λ -d> (val Λ -d> iPropO Σ) -d> iPropO Σ := λ E e1 Φ,
match to_val e1 with match to_val e1 with
| Some v => |={E}=> Φ v | Some v => |={E}=> Φ v
| None => σ1 κ κs n, | None => σ1 κ κs n,
......
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