Commit ca162551 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents ee98243c 03fce0a3
From iris.algebra Require Export cmra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** * Local updates *)
Definition local_update {A : cmraT} (x y : A * A) := n mz,
......
From iris.algebra Require Export base.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** This files defines (a shallow embedding of) the category of OFEs:
Complete ordered families of equivalences. This is a cartesian closed
......@@ -164,6 +164,7 @@ Instance const_contractive {A B : ofeT} (x : A) : Contractive (@const A B x).
Proof. by intros n y1 y2. Qed.
Section contractive.
Set Default Proof Using "Type*".
Context {A B : ofeT} (f : A B) `{!Contractive f}.
Implicit Types x y : A.
......@@ -556,6 +557,7 @@ Coercion cFunctor_diag : cFunctor >-> Funclass.
Program Definition constCF (B : ofeT) : cFunctor :=
{| cFunctor_car A1 A2 := B; cFunctor_map A1 A2 B1 B2 f := cid |}.
Solve Obligations with done.
Coercion constCF : ofeT >-> cFunctor.
Instance constCF_contractive B : cFunctorContractive (constCF B).
Proof. rewrite /cFunctorContractive; apply _. Qed.
......@@ -563,6 +565,7 @@ Proof. rewrite /cFunctorContractive; apply _. Qed.
Program Definition idCF : cFunctor :=
{| cFunctor_car A1 A2 := A2; cFunctor_map A1 A2 B1 B2 f := f.2 |}.
Solve Obligations with done.
Notation "∙" := idCF : cFunctor_scope.
Program Definition prodCF (F1 F2 : cFunctor) : cFunctor := {|
cFunctor_car A B := prodC (cFunctor_car F1 A B) (cFunctor_car F2 A B);
......@@ -577,6 +580,7 @@ Next Obligation.
intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [??]; simpl.
by rewrite !cFunctor_compose.
Qed.
Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
Instance prodCF_contractive F1 F2 :
cFunctorContractive F1 cFunctorContractive F2
......@@ -608,6 +612,7 @@ Next Obligation.
intros T F A1 A2 A3 B1 B2 B3 f g f' g' ??; simpl.
by rewrite !cFunctor_compose.
Qed.
Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
Instance ofe_funCF_contractive (T : Type) (F : cFunctor) :
cFunctorContractive F cFunctorContractive (ofe_funCF T F).
......@@ -633,6 +638,7 @@ Next Obligation.
intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [h ?] ?; simpl in *.
rewrite -!cFunctor_compose. do 2 apply (ne_proper _). apply cFunctor_compose.
Qed.
Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
Instance ofe_morCF_contractive F1 F2 :
cFunctorContractive F1 cFunctorContractive F2
......@@ -720,6 +726,7 @@ Next Obligation.
intros F1 F2 A1 A2 A3 B1 B2 B3 f g f' g' [?|?]; simpl;
by rewrite !cFunctor_compose.
Qed.
Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
Instance sumCF_contractive F1 F2 :
cFunctorContractive F1 cFunctorContractive F2
......@@ -953,6 +960,7 @@ Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x; simpl. rewrite -later_map_compose.
apply later_map_ext=>y; apply cFunctor_compose.
Qed.
Notation "▶ F" := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
Instance laterCF_contractive F : cFunctorContractive (laterCF F).
Proof.
......@@ -964,6 +972,21 @@ Qed.
Class LimitPreserving `{!Cofe A} (P : A Prop) : Prop :=
limit_preserving : c : chain A, ( n, P (c n)) P (compl c).
Section limit_preserving.
Context {A : ofeT} `{!Cofe A}.
(* These are not instances as they will never fire automatically...
but they can still be helpful in proving things to be limit preserving. *)
Lemma limit_preserving_and (P1 P2 : A Prop) :
LimitPreserving P1 LimitPreserving P2
LimitPreserving (λ x, P1 x P2 x).
Proof.
intros Hlim1 Hlim2 c Hc. split.
- apply Hlim1, Hc.
- apply Hlim2, Hc.
Qed.
End limit_preserving.
Section sigma.
Context {A : ofeT} {P : A Prop}.
......@@ -1015,12 +1038,3 @@ Section sigma.
End sigma.
Arguments sigC {_} _.
(** Notation for writing functors *)
Notation "∙" := idCF : cFunctor_scope.
Notation "T -c> F" := (ofe_funCF T%type F%CF) : cFunctor_scope.
Notation "F1 -n> F2" := (ofe_morCF F1%CF F2%CF) : cFunctor_scope.
Notation "F1 * F2" := (prodCF F1%CF F2%CF) : cFunctor_scope.
Notation "F1 + F2" := (sumCF F1%CF F2%CF) : cFunctor_scope.
Notation "▶ F" := (laterCF F%CF) (at level 20, right associativity) : cFunctor_scope.
Coercion constCF : ofeT >-> cFunctor.
From iris.prelude Require Export set.
From iris.algebra Require Export cmra.
From iris.algebra Require Import dra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Local Arguments valid _ _ !_ /.
Local Arguments op _ _ !_ !_ /.
Local Arguments core _ _ !_ /.
......
From iris.algebra Require Export cmra.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(** * Frame preserving updates *)
(* This quantifies over [option A] for the frame. That is necessary to
......@@ -86,6 +86,7 @@ Qed.
(** ** Frame preserving updates for total CMRAs *)
Section total_updates.
Set Default Proof Using "Type*".
Context `{CMRATotal A}.
Lemma cmra_total_updateP x (P : A Prop) :
......
From iris.prelude Require Export vector.
From iris.algebra Require Export ofe.
From iris.algebra Require Import list.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Section ofe.
Context {A : ofeT}.
......
From iris.base_logic Require Export derived.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Module Import uPred.
Export upred.uPred.
......
From iris.algebra Require Export list cmra_big_op.
From iris.base_logic Require Export base_logic.
From iris.prelude Require Import gmap fin_collections gmultiset functions.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(* We make use of the bigops on CMRAs, so we first define a (somewhat ad-hoc)
......@@ -133,8 +133,8 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Lemma big_sep_app Ps Qs : [] (Ps ++ Qs) [] Ps [] Qs.
Proof. by rewrite big_op_app. Qed.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps [] Ps [] Qs.
Proof. intros. apply uPred_included. by apply: big_op_contains. Qed.
Lemma big_sep_submseteq Ps Qs : Qs + Ps [] Ps [] Qs.
Proof. intros. apply uPred_included. by apply: big_op_submseteq. Qed.
Lemma big_sep_elem_of Ps P : P Ps [] Ps P.
Proof. intros. apply uPred_included. by apply: big_sep_elem_of. Qed.
Lemma big_sep_elem_of_acc Ps P : P Ps [] Ps P (P - [] Ps).
......@@ -220,9 +220,9 @@ Section list.
( k y, l !! k = Some y Φ k y Ψ k y)
([ list] k y l, Φ k y) ([ list] k y l, Ψ k y).
Proof. apply big_opL_proper. Qed.
Lemma big_sepL_contains (Φ : A uPred M) l1 l2 :
l1 `contains` l2 ([ list] y l2, Φ y) [ list] y l1, Φ y.
Proof. intros ?. apply uPred_included. by apply: big_opL_contains. Qed.
Lemma big_sepL_submseteq (Φ : A uPred M) l1 l2 :
l1 + l2 ([ list] y l2, Φ y) [ list] y l1, Φ y.
Proof. intros ?. apply uPred_included. by apply: big_opL_submseteq. Qed.
Global Instance big_sepL_mono' l :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
......@@ -353,8 +353,8 @@ Section gmap.
([ map] k x m1, Φ k x) [ map] k x m2, Ψ k x.
Proof.
intros Hm HΦ. trans ([ map] kx m2, Φ k x)%I.
- apply uPred_included. apply: big_op_contains.
by apply fmap_contains, map_to_list_contains.
- apply uPred_included. apply: big_op_submseteq.
by apply fmap_submseteq, map_to_list_submseteq.
- apply big_opM_forall; apply _ || auto.
Qed.
Lemma big_sepM_proper Φ Ψ m :
......@@ -517,8 +517,8 @@ Section gset.
([ set] x X, Φ x) [ set] x Y, Ψ x.
Proof.
intros HX HΦ. trans ([ set] x Y, Φ x)%I.
- apply uPred_included. apply: big_op_contains.
by apply fmap_contains, elements_contains.
- apply uPred_included. apply: big_op_submseteq.
by apply fmap_submseteq, elements_submseteq.
- apply big_opS_forall; apply _ || auto.
Qed.
Lemma big_sepS_proper Φ Ψ X :
......@@ -666,8 +666,8 @@ Section gmultiset.
([ mset] x X, Φ x) [ mset] x Y, Ψ x.
Proof.
intros HX HΦ. trans ([ mset] x Y, Φ x)%I.
- apply uPred_included. apply: big_op_contains.
by apply fmap_contains, gmultiset_elements_contains.
- apply uPred_included. apply: big_op_submseteq.
by apply fmap_submseteq, gmultiset_elements_submseteq.
- apply big_opMS_forall; apply _ || auto.
Qed.
Lemma big_sepMS_proper Φ Ψ X :
......
From iris.base_logic Require Import primitive.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(* Deprecated 2016-11-22. Use ⌜φ⌝ instead. *)
Notation "■ φ" := (uPred_pure φ%C%type)
......
From iris.base_logic Require Export primitive.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import upred.uPred primitive.uPred.
Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P Q) (Q P))%I.
......
From iris.base_logic Require Import base_logic.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
(* In this file we show that the bupd can be thought of a kind of
step-indexed double-negation when our meta-logic is classical *)
......@@ -274,7 +274,7 @@ Qed.
Section classical.
Context (not_all_not_ex: (P : M Prop), ¬ ( n : M, ¬ P n) n : M, P n).
Lemma nnupd_bupd P: (|=n=> P) (|==> P).
Proof.
Proof using Type*.
rewrite /uPred_nnupd.
split. uPred.unseal; red; rewrite //=.
intros n x ? Hforall k yf Hle ?.
......
From iris.prelude Require Export hlist.
From iris.base_logic Require Export base_logic.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Fixpoint uPred_hexist {M As} : himpl As (uPred M) uPred M :=
......
......@@ -3,7 +3,7 @@ From iris.algebra Require Export auth.
From iris.algebra Require Import gmap.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(* The CMRA we need. *)
......@@ -11,10 +11,10 @@ Class authG Σ (A : ucmraT) := AuthG {
auth_inG :> inG Σ (authR A);
auth_discrete :> CMRADiscrete A;
}.
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (authR A) ].
Instance subG_authΣ Σ A : subG (authΣ A) Σ CMRADiscrete A authG Σ A.
Proof. intros ?%subG_inG ?. by split. Qed.
Proof. solve_inG. Qed.
Section definitions.
Context `{invG Σ, authG Σ A} {T : Type} (γ : gname).
......@@ -117,7 +117,7 @@ Section auth.
auth_inv γ f φ auth_own γ a ={E}= t,
a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={E}= auth_inv γ f φ auth_own γ b.
Proof.
Proof using Type*.
iIntros "[Hinv Hγf]". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
iModIntro. iExists t.
......@@ -133,7 +133,7 @@ Section auth.
auth_ctx γ N f φ auth_own γ a ={E,E∖↑N}= t,
a f t φ t u b,
(f t, a) ~l~> (f u, b) φ u ={E∖↑N,E}= auth_own γ b.
Proof.
Proof using Type*.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
[auth_acc] and [inv_open] -- but since we don't have any good support
......
......@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export invariants.
From iris.algebra Require Import auth gmap agree.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(** The CMRAs we need. *)
......@@ -11,6 +11,13 @@ Class boxG Σ :=
(authR (optionUR (exclR boolC)))
(optionR (agreeR (laterC (iPreProp Σ))))).
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolC)) *
optionRF (agreeRF ( )) ) ].
Instance subG_stsΣ Σ :
subG boxΣ Σ boxG Σ.
Proof. solve_inG. Qed.
Section box_defs.
Context `{invG Σ, boxG Σ} (N : namespace).
......
From iris.base_logic.lib Require Export invariants fractional.
From iris.algebra Require Export frac.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Class cinvG Σ := cinv_inG :> inG Σ fracR.
......
From iris.base_logic Require Import base_logic.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(** The "core" of an assertion is its maximal persistent part.
......
From iris.base_logic Require Import base_logic soundness.
From iris.proofmode Require Import tactics.
Set Default Proof Using "All".
Set Default Proof Using "Type*".
(** This proves that we need the ▷ in a "Saved Proposition" construction with
name-dependent allocation. *)
......@@ -39,7 +39,7 @@ Module savedprop. Section savedprop.
Qed.
Lemma contradiction : False.
Proof.
Proof using All.
apply (@soundness M False 1); simpl.
iIntros "". iMod A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
......@@ -186,7 +186,7 @@ Module inv. Section inv.
Qed.
Lemma contradiction : False.
Proof.
Proof using All.
apply consistency. iIntros "".
iMod A_alloc as (i) "#H".
iPoseProof (saved_NA with "H") as "HN".
......
......@@ -4,7 +4,7 @@ From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import tactics classes.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Export invG.
Import uPred.
......
......@@ -2,7 +2,7 @@ From iris.prelude Require Import gmap gmultiset.
From iris.base_logic Require Export derived.
From iris.base_logic Require Import big_op.
From iris.proofmode Require Import classes class_instances.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Class Fractional {M} (Φ : Qp uPred M) :=
fractional p q : Φ (p + q)%Qp Φ p Φ q.
......
......@@ -2,7 +2,7 @@ From iris.algebra Require Import auth gmap frac agree.
From iris.base_logic.lib Require Export own.
From iris.base_logic.lib Require Import fractional.
From iris.proofmode Require Import tactics.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
Definition gen_heapUR (L V : Type) `{Countable L} : ucmraT :=
......@@ -20,11 +20,11 @@ Class gen_heapPreG (L V : Type) (Σ : gFunctors) `{Countable L} :=
{ gen_heap_preG_inG :> inG Σ (authR (gen_heapUR L V)) }.
Definition gen_heapΣ (L V : Type) `{Countable L} : gFunctors :=
#[GFunctor (constRF (authR (gen_heapUR L V)))].
#[GFunctor (authR (gen_heapUR L V))].
Instance subG_gen_heapPreG {Σ L V} `{Countable L} :
subG (gen_heapΣ L V) Σ gen_heapPreG L V Σ.
Proof. intros ?%subG_inG; split; apply _. Qed.
Proof. solve_inG. Qed.
Section definitions.
Context `{gen_heapG L V Σ}.
......
......@@ -2,7 +2,7 @@ From iris.base_logic.lib Require Export fancy_updates namespaces.
From iris.base_logic.lib Require Import wsat.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics coq_tactics intro_patterns.
Set Default Proof Using "Type*".
Set Default Proof Using "Type".
Import uPred.
(** Derived forms and lemmas about them. *)
......
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