Commit eae4cc01 authored by Ralf Jung's avatar Ralf Jung

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

parents 1b711f33 2b96b14d
Pipeline #377 passed with stage
......@@ -55,6 +55,7 @@ algebra/upred_tactics.v
algebra/upred_big_op.v
algebra/frac.v
algebra/one_shot.v
algebra/list.v
program_logic/model.v
program_logic/adequacy.v
program_logic/hoare_lifting.v
......
From iris.algebra Require Export cmra.
From iris.algebra Require Export cmra list.
From iris.prelude Require Import gmap.
Fixpoint big_op {A : cmraT} `{Empty A} (xs : list A) : A :=
......@@ -25,8 +25,9 @@ Proof.
- by rewrite !assoc (comm _ x).
- by trans (big_op xs2).
Qed.
Global Instance big_op_proper : Proper (() ==> ()) big_op.
Global Instance big_op_ne n : Proper (dist n ==> dist n) big_op.
Proof. by induction 1; simpl; repeat apply (_ : Proper (_ ==> _ ==> _) op). Qed.
Global Instance big_op_proper : Proper (() ==> ()) big_op := ne_proper _.
Lemma big_op_app xs ys : big_op (xs ++ ys) big_op xs big_op ys.
Proof.
induction xs as [|x xs IH]; simpl; first by rewrite ?left_id.
......@@ -64,7 +65,7 @@ Proof.
{ by intros m2; rewrite (symmetry_iff ()) map_equiv_empty; intros ->. }
intros m2 Hm2; rewrite big_opM_insert //.
rewrite (IH (delete i m2)); last by rewrite -Hm2 delete_insert.
destruct (map_equiv_lookup (<[i:=x]> m1) m2 i x)
destruct (map_equiv_lookup_l (<[i:=x]> m1) m2 i x)
as (y&?&Hxy); auto using lookup_insert.
rewrite Hxy -big_opM_insert; last auto using lookup_delete.
by rewrite insert_delete.
......
From iris.algebra Require Export option.
From iris.prelude Require Export list.
Section cofe.
Context {A : cofeT}.
Instance list_dist : Dist (list A) := λ n, Forall2 (dist n).
Global Instance cons_ne n : Proper (dist n ==> dist n ==> dist n) (@cons A) := _.
Global Instance app_ne n : Proper (dist n ==> dist n ==> dist n) (@app A) := _.
Global Instance length_ne n : Proper (dist n ==> (=)) (@length A) := _.
Global Instance tail_ne n : Proper (dist n ==> dist n) (@tail A) := _.
Global Instance take_ne n : Proper (dist n ==> dist n) (@take A n) := _.
Global Instance drop_ne n : Proper (dist n ==> dist n) (@drop A n) := _.
Global Instance list_lookup_ne n i :
Proper (dist n ==> dist n) (lookup (M:=list A) i).
Proof. intros ???. by apply dist_option_Forall2, Forall2_lookup. Qed.
Global Instance list_alter_ne n f i :
Proper (dist n ==> dist n) f
Proper (dist n ==> dist n) (alter (M:=list A) f i) := _.
Global Instance list_insert_ne n i :
Proper (dist n ==> dist n ==> dist n) (insert (M:=list A) i) := _.
Global Instance list_inserts_ne n i :
Proper (dist n ==> dist n ==> dist n) (@list_inserts A i) := _.
Global Instance list_delete_ne n i :
Proper (dist n ==> dist n) (delete (M:=list A) i) := _.
Global Instance option_list_ne n : Proper (dist n ==> dist n) (@option_list A).
Proof. intros ???; by apply Forall2_option_list, dist_option_Forall2. Qed.
Global Instance list_filter_ne n P `{ x, Decision (P x)} :
Proper (dist n ==> iff) P
Proper (dist n ==> dist n) (filter (B:=list A) P) := _.
Global Instance replicate_ne n :
Proper (dist n ==> dist n) (@replicate A n) := _.
Global Instance reverse_ne n : Proper (dist n ==> dist n) (@reverse A) := _.
Global Instance last_ne n : Proper (dist n ==> dist n) (@last A).
Proof. intros ???; by apply dist_option_Forall2, Forall2_last. Qed.
Global Instance resize_ne n :
Proper (dist n ==> dist n ==> dist n) (@resize A n) := _.
Program Definition list_chain
(c : chain (list A)) (x : A) (k : nat) : chain A :=
{| chain_car n := from_option x (c n !! k) |}.
Next Obligation. intros c x k n i ?. by rewrite /= (chain_cauchy c n i). Qed.
Instance list_compl : Compl (list A) := λ c,
match c 0 with
| [] => []
| x :: _ => compl list_chain c x <$> seq 0 (length (c 0))
end.
Definition list_cofe_mixin : CofeMixin (list A).
Proof.
split.
- intros l k. rewrite equiv_Forall2 -Forall2_forall.
split; induction 1; constructor; intros; try apply equiv_dist; auto.
- apply _.
- rewrite /dist /list_dist. eauto using Forall2_impl, dist_S.
- intros n c; rewrite /compl /list_compl.
destruct (c 0) as [|x l] eqn:Hc0 at 1.
{ by destruct (chain_cauchy c 0 n); auto with omega. }
rewrite -(λ H, length_ne _ _ _ (chain_cauchy c 0 n H)); last omega.
apply Forall2_lookup=> i; apply dist_option_Forall2.
rewrite list_lookup_fmap. destruct (decide (i < length (c n))); last first.
{ rewrite lookup_seq_ge ?lookup_ge_None_2; auto with omega. }
rewrite lookup_seq //= (conv_compl n (list_chain c _ _)) /=.
by destruct (lookup_lt_is_Some_2 (c n) i) as [? ->].
Qed.
Canonical Structure listC := CofeT list_cofe_mixin.
Global Instance list_discrete : Discrete A Discrete listC.
Proof. induction 2; constructor; try apply (timeless _); auto. Qed.
Global Instance nil_timeless : Timeless (@nil A).
Proof. inversion_clear 1; constructor. Qed.
Global Instance cons_timeless x l : Timeless x Timeless l Timeless (x :: l).
Proof. intros ??; inversion_clear 1; constructor; by apply timeless. Qed.
End cofe.
Arguments listC : clear implicits.
(** Functor *)
Instance list_fmap_ne {A B : cofeT} (f : A B) n:
Proper (dist n ==> dist n) f Proper (dist n ==> dist n) (fmap (M:=list) f).
Proof. intros Hf l k ?; by eapply Forall2_fmap, Forall2_impl; eauto. Qed.
Definition listC_map {A B} (f : A -n> B) : listC A -n> listC B :=
CofeMor (fmap f : listC A listC B).
Instance listC_map_ne A B n : Proper (dist n ==> dist n) (@listC_map A B).
Proof. intros f f' ? l; by apply Forall2_fmap, Forall_Forall2, Forall_true. Qed.
Program Definition listCF (F : cFunctor) : cFunctor := {|
cFunctor_car A B := listC (cFunctor_car F A B);
cFunctor_map A1 A2 B1 B2 fg := listC_map (cFunctor_map F fg)
|}.
Next Obligation.
by intros F A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_ne.
Qed.
Next Obligation.
intros F A B x. rewrite /= -{2}(list_fmap_id x).
apply list_fmap_setoid_ext=>y. apply cFunctor_id.
Qed.
Next Obligation.
intros F A1 A2 A3 B1 B2 B3 f g f' g' x. rewrite /= -list_fmap_compose.
apply list_fmap_setoid_ext=>y; apply cFunctor_compose.
Qed.
Instance listCF_contractive F :
cFunctorContractive F cFunctorContractive (listCF F).
Proof.
by intros ? A1 A2 B1 B2 n f g Hfg; apply listC_map_ne, cFunctor_contractive.
Qed.
......@@ -4,40 +4,50 @@ From iris.algebra Require Import upred.
(* COFE *)
Section cofe.
Context {A : cofeT}.
Inductive option_dist : Dist (option A) :=
| Some_dist n x y : x {n} y Some x {n} Some y
| None_dist n : None {n} None.
Existing Instance option_dist.
Inductive option_dist' (n : nat) : relation (option A) :=
| Some_dist x y : x {n} y option_dist' n (Some x) (Some y)
| None_dist : option_dist' n None None.
Instance option_dist : Dist (option A) := option_dist'.
Lemma dist_option_Forall2 n mx my : mx {n} my option_Forall2 (dist n) mx my.
Proof. split; destruct 1; constructor; auto. Qed.
Program Definition option_chain (c : chain (option A)) (x : A) : chain A :=
{| chain_car n := from_option x (c n) |}.
Next Obligation. intros c x n i ?; simpl. by destruct (chain_cauchy c n i). Qed.
Instance option_compl : Compl (option A) := λ c,
match c 0 with Some x => Some (compl (option_chain c x)) | None => None end.
Definition option_cofe_mixin : CofeMixin (option A).
Proof.
split.
- intros mx my; split; [by destruct 1; constructor; apply equiv_dist|].
intros Hxy; feed inversion (Hxy 1); subst; constructor; apply equiv_dist.
intros Hxy; destruct (Hxy 0); constructor; apply equiv_dist.
by intros n; feed inversion (Hxy n).
- intros n; split.
+ by intros [x|]; constructor.
+ by destruct 1; constructor.
+ destruct 1; inversion_clear 1; constructor; etrans; eauto.
- by inversion_clear 1; constructor; apply dist_S.
- destruct 1; constructor; by apply dist_S.
- intros n c; rewrite /compl /option_compl.
feed inversion (chain_cauchy c 0 n); first auto with lia; constructor.
rewrite (conv_compl n (option_chain c _)) /=. destruct (c n); naive_solver.
Qed.
Canonical Structure optionC := CofeT option_cofe_mixin.
Global Instance option_discrete : Discrete A Discrete optionC.
Proof. inversion_clear 2; constructor; by apply (timeless _). Qed.
Proof. destruct 2; constructor; by apply (timeless _). Qed.
Global Instance Some_ne : Proper (dist n ==> dist n) (@Some A).
Proof. by constructor. Qed.
Global Instance is_Some_ne n : Proper (dist n ==> iff) (@is_Some A).
Proof. inversion_clear 1; split; eauto. Qed.
Proof. destruct 1; split; eauto. Qed.
Global Instance Some_dist_inj : Inj (dist n) (dist n) (@Some A).
Proof. by inversion_clear 1. Qed.
Global Instance from_option_ne n :
Proper (dist n ==> dist n ==> dist n) (@from_option A).
Proof. by destruct 2. Qed.
Global Instance None_timeless : Timeless (@None A).
Proof. inversion_clear 1; constructor. Qed.
Global Instance Some_timeless x : Timeless x Timeless (Some x).
......@@ -125,16 +135,16 @@ Global Instance option_persistent (mx : option A) :
Proof. intros. destruct mx. apply _. apply cmra_unit_persistent. Qed.
(** Internalized properties *)
Lemma option_equivI {M} (x y : option A) :
(x y) (match x, y with
| Some a, Some b => a b | None, None => True | _, _ => False
end : uPred M).
Lemma option_equivI {M} (mx my : option A) :
(mx my) (match mx, my with
| Some x, Some y => x y | None, None => True | _, _ => False
end : uPred M).
Proof.
uPred.unseal. do 2 split. by destruct 1. by destruct x, y; try constructor.
uPred.unseal. do 2 split. by destruct 1. by destruct mx, my; try constructor.
Qed.
Lemma option_validI {M} (x : option A) :
( x) (match x with Some a => a | None => True end : uPred M).
Proof. uPred.unseal. by destruct x. Qed.
Lemma option_validI {M} (mx : option A) :
( mx) (match mx with Some x => x | None => True end : uPred M).
Proof. uPred.unseal. by destruct mx. Qed.
(** Updates *)
Lemma option_updateP (P : A Prop) (Q : option A Prop) x :
......@@ -146,7 +156,7 @@ Proof.
by exists (Some y'); split; [auto|apply cmra_validN_op_l with (core x)].
Qed.
Lemma option_updateP' (P : A Prop) x :
x ~~>: P Some x ~~>: λ y, default False y P.
x ~~>: P Some x ~~>: λ my, default False my P.
Proof. eauto using option_updateP. Qed.
Lemma option_update x y : x ~~> y Some x ~~> Some y.
Proof.
......
From iris.algebra Require Export upred.
From iris.algebra Require Export upred list.
From iris.prelude Require Import gmap fin_collections.
Import uPred.
......@@ -44,11 +44,9 @@ Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_proper : Proper (() ==> ()) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_ne n :
Proper (Forall2 (dist n) ==> dist n) (@uPred_big_and M).
Global Instance big_and_ne n : Proper (dist n ==> dist n) (@uPred_big_and M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_sep_ne n :
Proper (Forall2 (dist n) ==> dist n) (@uPred_big_sep M).
Global Instance big_sep_ne n : Proper (dist n ==> dist n) (@uPred_big_sep M).
Proof. by induction 1 as [|P Q Ps Qs HPQ ? IH]; rewrite /= ?HPQ ?IH. Qed.
Global Instance big_and_mono' : Proper (Forall2 () ==> ()) (@uPred_big_and M).
......@@ -71,26 +69,26 @@ Proof.
- etrans; eauto.
Qed.
Lemma big_and_app Ps Qs : (Π (Ps ++ Qs)) (Π Ps Π Qs).
Lemma big_and_app Ps Qs : Π (Ps ++ Qs) (Π Ps Π Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_sep_app Ps Qs : (Π★ (Ps ++ Qs)) (Π★ Ps Π★ Qs).
Lemma big_sep_app Ps Qs : Π★ (Ps ++ Qs) (Π★ Ps Π★ Qs).
Proof. by induction Ps as [|?? IH]; rewrite /= ?left_id -?assoc ?IH. Qed.
Lemma big_and_contains Ps Qs : Qs `contains` Ps (Π Ps) (Π Qs).
Lemma big_and_contains Ps Qs : Qs `contains` Ps Π Ps Π Qs.
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_and_app and_elim_l.
Qed.
Lemma big_sep_contains Ps Qs : Qs `contains` Ps (Π★ Ps) (Π★ Qs).
Lemma big_sep_contains Ps Qs : Qs `contains` Ps Π★ Ps Π★ Qs.
Proof.
intros [Ps' ->]%contains_Permutation. by rewrite big_sep_app sep_elim_l.
Qed.
Lemma big_sep_and Ps : (Π★ Ps) (Π Ps).
Lemma big_sep_and Ps : Π★ Ps Π Ps.
Proof. by induction Ps as [|P Ps IH]; simpl; auto with I. Qed.
Lemma big_and_elem_of Ps P : P Ps (Π Ps) P.
Lemma big_and_elem_of Ps P : P Ps Π Ps P.
Proof. induction 1; simpl; auto with I. Qed.
Lemma big_sep_elem_of Ps P : P Ps (Π★ Ps) P.
Lemma big_sep_elem_of Ps P : P Ps Π★ Ps P.
Proof. induction 1; simpl; auto with I. Qed.
(* Big ops over finite maps *)
......@@ -101,11 +99,11 @@ Section gmap.
Lemma big_sepM_mono Φ Ψ m1 m2 :
m2 m1 ( x k, m2 !! k = Some x Φ k x Ψ k x)
(Π★{map m1} Φ) (Π★{map m2} Ψ).
Π★{map m1} Φ Π★{map m2} Ψ.
Proof.
intros HX HΦ. trans (Π★{map m2} Φ)%I.
- by apply big_sep_contains, fmap_contains, map_to_list_contains.
- apply big_sep_mono', Forall2_fmap, Forall2_Forall.
- apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall=> -[i x] ? /=. by apply HΦ, elem_of_map_to_list.
Qed.
......@@ -114,7 +112,7 @@ Section gmap.
(uPred_big_sepM (M:=M) m).
Proof.
intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
apply Forall2_Forall, Forall_true=> -[i x]; apply HΦ.
apply Forall_Forall2, Forall_true=> -[i x]; apply HΦ.
Qed.
Global Instance big_sepM_proper m :
Proper (pointwise_relation _ (pointwise_relation _ ()) ==> ())
......@@ -128,25 +126,25 @@ Section gmap.
(uPred_big_sepM (M:=M) m).
Proof. intros Φ1 Φ2 HΦ. apply big_sepM_mono; intros; [done|apply HΦ]. Qed.
Lemma big_sepM_empty Φ : (Π★{map } Φ) True.
Lemma big_sepM_empty Φ : Π★{map } Φ True.
Proof. by rewrite /uPred_big_sepM map_to_list_empty. Qed.
Lemma big_sepM_insert Φ (m : gmap K A) i x :
m !! i = None (Π★{map <[i:=x]> m} Φ) (Φ i x Π★{map m} Φ).
m !! i = None Π★{map <[i:=x]> m} Φ (Φ i x Π★{map m} Φ).
Proof. intros ?; by rewrite /uPred_big_sepM map_to_list_insert. Qed.
Lemma big_sepM_singleton Φ i x : (Π★{map {[i := x]}} Φ) (Φ i x).
Lemma big_sepM_singleton Φ i x : Π★{map {[i := x]}} Φ (Φ i x).
Proof.
rewrite -insert_empty big_sepM_insert/=; last auto using lookup_empty.
by rewrite big_sepM_empty right_id.
Qed.
Lemma big_sepM_sepM Φ Ψ m :
(Π★{map m} (λ i x, Φ i x Ψ i x)) (Π★{map m} Φ Π★{map m} Ψ).
Π★{map m} (λ i x, Φ i x Ψ i x) (Π★{map m} Φ Π★{map m} Ψ).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?right_id //.
by rewrite IH -!assoc (assoc _ (Ψ _ _)) [(Ψ _ _ _)%I]comm -!assoc.
Qed.
Lemma big_sepM_later Φ m : ( Π★{map m} Φ) (Π★{map m} (λ i x, Φ i x)).
Lemma big_sepM_later Φ m : Π★{map m} Φ Π★{map m} (λ i x, Φ i x).
Proof.
rewrite /uPred_big_sepM.
induction (map_to_list m) as [|[i x] l IH]; csimpl; rewrite ?later_True //.
......@@ -161,11 +159,11 @@ Section gset.
Implicit Types Φ : A uPred M.
Lemma big_sepS_mono Φ Ψ X Y :
Y X ( x, x Y Φ x Ψ x) (Π★{set X} Φ) (Π★{set Y} Ψ).
Y X ( x, x Y Φ x Ψ x) Π★{set X} Φ Π★{set Y} Ψ.
Proof.
intros HX HΦ. trans (Π★{set Y} Φ)%I.
- by apply big_sep_contains, fmap_contains, elements_contains.
- apply big_sep_mono', Forall2_fmap, Forall2_Forall.
- apply big_sep_mono', Forall2_fmap, Forall_Forall2.
apply Forall_forall=> x ? /=. by apply HΦ, elem_of_elements.
Qed.
......@@ -173,7 +171,7 @@ Section gset.
Proper (pointwise_relation _ (dist n) ==> dist n) (uPred_big_sepS (M:=M) X).
Proof.
intros Φ1 Φ2 HΦ. apply big_sep_ne, Forall2_fmap.
apply Forall2_Forall, Forall_true=> x; apply HΦ.
apply Forall_Forall2, Forall_true=> x; apply HΦ.
Qed.
Lemma big_sepS_proper X :
Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
......@@ -185,29 +183,29 @@ Section gset.
Proper (pointwise_relation _ () ==> ()) (uPred_big_sepS (M:=M) X).
Proof. intros Φ1 Φ2 HΦ. apply big_sepS_mono; naive_solver. Qed.
Lemma big_sepS_empty Φ : (Π★{set } Φ) True.
Lemma big_sepS_empty Φ : Π★{set } Φ True.
Proof. by rewrite /uPred_big_sepS elements_empty. Qed.
Lemma big_sepS_insert Φ X x :
x X (Π★{set {[ x ]} X} Φ) (Φ x Π★{set X} Φ).
x X Π★{set {[ x ]} X} Φ (Φ x Π★{set X} Φ).
Proof. intros. by rewrite /uPred_big_sepS elements_union_singleton. Qed.
Lemma big_sepS_delete Φ X x :
x X (Π★{set X} Φ) (Φ x Π★{set X {[ x ]}} Φ).
x X Π★{set X} Φ (Φ x Π★{set X {[ x ]}} Φ).
Proof.
intros. rewrite -big_sepS_insert; last set_solver.
by rewrite -union_difference_L; last set_solver.
Qed.
Lemma big_sepS_singleton Φ x : (Π★{set {[ x ]}} Φ) (Φ x).
Lemma big_sepS_singleton Φ x : Π★{set {[ x ]}} Φ (Φ x).
Proof. intros. by rewrite /uPred_big_sepS elements_singleton /= right_id. Qed.
Lemma big_sepS_sepS Φ Ψ X :
(Π★{set X} (λ x, Φ x Ψ x)) (Π★{set X} Φ Π★{set X} Ψ).
Π★{set X} (λ x, Φ x Ψ x) (Π★{set X} Φ Π★{set X} Ψ).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?right_id.
by rewrite IH -!assoc (assoc _ (Ψ _)) [(Ψ _ _)%I]comm -!assoc.
Qed.
Lemma big_sepS_later Φ X : ( Π★{set X} Φ) (Π★{set X} (λ x, Φ x)).
Lemma big_sepS_later Φ X : Π★{set X} Φ Π★{set X} (λ x, Φ x).
Proof.
rewrite /uPred_big_sepS.
induction (elements X) as [|x l IH]; csimpl; first by rewrite ?later_True.
......
......@@ -173,11 +173,9 @@ Section setoid.
split; [intros Hm; apply map_eq; intros i|by intros ->].
by rewrite lookup_empty, <-equiv_None, Hm, lookup_empty.
Qed.
Lemma map_equiv_lookup (m1 m2 : M A) i x :
Lemma map_equiv_lookup_l (m1 m2 : M A) i x :
m1 m2 m1 !! i = Some x y, m2 !! i = Some y x y.
Proof.
intros Hm ?. destruct (equiv_Some (m1 !! i) (m2 !! i) x) as (y&?&?); eauto.
Qed.
Proof. generalize (equiv_Some_inv_l (m1 !! i) (m2 !! i) x); naive_solver. Qed.
End setoid.
(** ** General properties *)
......
This diff is collapsed.
This diff is collapsed.
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