Skip to content
Snippets Groups Projects
Commit 337a29d4 authored by Ralf Jung's avatar Ralf Jung
Browse files

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

parents 6d0a38cb 99e980ae
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 69 additions and 68 deletions
algebra/agree.v
+ 1
− 1
View file @ 337a29d4
......@@ -108,7 +108,7 @@ Proof.
symmetry; apply dist_le with n; try apply Hx; auto.
- intros x. apply agree_idemp.
- by intros n x y [(?&?&?) ?].
- intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
- intros n x y1 y2 Hval Hx; exists x, x; simpl; split.
+ by rewrite agree_idemp.
+ by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
Qed.
......
algebra/auth.v
+ 3
− 3
View file @ 337a29d4
......@@ -134,10 +134,10 @@ Proof.
naive_solver eauto using cmra_validN_op_l, cmra_validN_includedN.
- intros n x y1 y2 ? [??]; simpl in *.
destruct (cmra_extend n (authoritative x) (authoritative y1)
(authoritative y2)) as (ea&?&?&?); auto using authoritative_validN.
(authoritative y2)) as (ea1&ea2&?&?&?); auto using authoritative_validN.
destruct (cmra_extend n (auth_own x) (auth_own y1) (auth_own y2))
as (b&?&?&?); auto using auth_own_validN.
by exists (Auth (ea.1) (b.1), Auth (ea.2) (b.2)).
as (b1&b2&?&?&?); auto using auth_own_validN.
by exists (Auth ea1 b1), (Auth ea2 b2).
Qed.
Canonical Structure authR := CMRAT (auth A) auth_cofe_mixin auth_cmra_mixin.
......
algebra/cmra.v
+ 15
− 16
View file @ 337a29d4
......@@ -53,7 +53,7 @@ Record CMRAMixin A `{Dist A, Equiv A, PCore A, Op A, Valid A, ValidN A} := {
mixin_cmra_validN_op_l n x y : ✓{n} (x ⋅ y) → ✓{n} x;
mixin_cmra_extend n x y1 y2 :
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }
∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2
}.
(** Bundeled version *)
......@@ -120,7 +120,7 @@ Section cmra_mixin.
Proof. apply (mixin_cmra_validN_op_l _ (cmra_mixin A)). Qed.
Lemma cmra_extend n x y1 y2 :
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }.
∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2.
Proof. apply (mixin_cmra_extend _ (cmra_mixin A)). Qed.
End cmra_mixin.
......@@ -472,7 +472,7 @@ End total_core.
Lemma cmra_timeless_included_l x y : Timeless x → ✓{0} y → x ≼{0} y → x ≼ y.
Proof.
intros ?? [x' ?].
destruct (cmra_extend 0 y x x') as ([z z']&Hy&Hz&Hz'); auto; simpl in *.
destruct (cmra_extend 0 y x x') as (z&z'&Hy&Hz&Hz'); auto; simpl in *.
by exists z'; rewrite Hy (timeless x z).
Qed.
Lemma cmra_timeless_included_r n x y : Timeless y → x ≼{0} y → x ≼{n} y.
......@@ -481,7 +481,7 @@ Lemma cmra_op_timeless x1 x2 :
✓ (x1 ⋅ x2) → Timeless x1 → Timeless x2 → Timeless (x1 ⋅ x2).
Proof.
intros ??? z Hz.
destruct (cmra_extend 0 z x1 x2) as ([y1 y2]&Hz'&?&?); auto; simpl in *.
destruct (cmra_extend 0 z x1 x2) as (y1&y2&Hz'&?&?); auto; simpl in *.
{ rewrite -?Hz. by apply cmra_valid_validN. }
by rewrite Hz' (timeless x1 y1) // (timeless x2 y2).
Qed.
......@@ -540,7 +540,7 @@ Section cmra_total.
Context (validN_op_l : ∀ n (x y : A), ✓{n} (x ⋅ y) → ✓{n} x).
Context (extend : ∀ n (x y1 y2 : A),
✓{n} x → x ≡{n}≡ y1 ⋅ y2 →
{ z | x ≡ z.1 ⋅ z.2 ∧ z.1 ≡{n}≡ y1 ∧ z.2 ≡{n}≡ y2 }).
∃ z1 z2, x ≡ z1 ⋅ z2 ∧ z1 ≡{n}≡ y1 ∧ z2 ≡{n}≡ y2).
Lemma cmra_total_mixin : CMRAMixin A.
Proof.
split; auto.
......@@ -690,7 +690,7 @@ Section discrete.
Proof.
destruct ra_mix; split; try done.
- intros x; split; first done. by move=> /(_ 0).
- intros n x y1 y2 ??; by exists (y1,y2).
- intros n x y1 y2 ??; by exists y1, y2.
Qed.
End discrete.
......@@ -881,9 +881,9 @@ Section prod.
exists (z1,z2). by rewrite prod_included prod_pcore_Some.
- intros n x y [??]; split; simpl in *; eauto using cmra_validN_op_l.
- intros n x y1 y2 [??] [??]; simpl in *.
destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z1&?&?&?); auto.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z2&?&?&?); auto.
by exists ((z1.1,z2.1),(z1.2,z2.2)).
destruct (cmra_extend n (x.1) (y1.1) (y2.1)) as (z11&z12&?&?&?); auto.
destruct (cmra_extend n (x.2) (y1.2) (y2.2)) as (z21&z22&?&?&?); auto.
by exists (z11,z21), (z12,z22).
Qed.
Canonical Structure prodR :=
CMRAT (A * B) prod_cofe_mixin prod_cmra_mixin.
......@@ -1048,13 +1048,12 @@ Section option.
eauto using cmra_validN_op_l.
- intros n mx my1 my2.
destruct mx as [x|], my1 as [y1|], my2 as [y2|]; intros Hx Hx';
try (by exfalso; inversion Hx'; auto).
+ destruct (cmra_extend n x y1 y2) as ([z1 z2]&?&?&?); auto.
{ by inversion_clear Hx'. }
by exists (Some z1, Some z2); repeat constructor.
+ by exists (Some x,None); inversion Hx'; repeat constructor.
+ by exists (None,Some x); inversion Hx'; repeat constructor.
+ exists (None,None); repeat constructor.
inversion_clear Hx'; auto.
+ destruct (cmra_extend n x y1 y2) as (z1&z2&?&?&?); auto.
by exists (Some z1), (Some z2); repeat constructor.
+ by exists (Some x), None; repeat constructor.
+ by exists None, (Some x); repeat constructor.
+ exists None, None; repeat constructor.
Qed.
Canonical Structure optionR :=
CMRAT (option A) option_cofe_mixin option_cmra_mixin.
......
algebra/cofe.v
+ 0
− 2
View file @ 337a29d4
......@@ -675,8 +675,6 @@ Inductive later (A : Type) : Type := Next { later_car : A }.
Add Printing Constructor later.
Arguments Next {_} _.
Arguments later_car {_} _.
Lemma later_eta {A} (x : later A) : Next (later_car x) = x.
Proof. by destruct x. Qed.
Section later.
Context {A : cofeT}.
......
algebra/csum.v
+ 7
− 9
View file @ 337a29d4
......@@ -209,15 +209,13 @@ Proof.
exists (Cinr cb'). rewrite csum_included; eauto 10.
- intros n [a1|b1|] [a2|b2|]; simpl; eauto using cmra_validN_op_l; done.
- intros n [a|b|] y1 y2 Hx Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
apply (inj Cinl) in Hx'.
destruct (cmra_extend n a a1 a2) as ([z1 z2]&?&?&?); auto.
exists (Cinl z1, Cinl z2). by repeat constructor.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; try (exfalso; by inversion_clear Hx').
apply (inj Cinr) in Hx'.
destruct (cmra_extend n b b1 b2) as ([z1 z2]&?&?&?); auto.
exists (Cinr z1, Cinr z2). by repeat constructor.
+ by exists (CsumBot, CsumBot); destruct y1, y2; inversion_clear Hx'.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'.
destruct (cmra_extend n a a1 a2) as (z1&z2&?&?&?); auto.
exists (Cinl z1), (Cinl z2). by repeat constructor.
+ destruct y1 as [a1|b1|], y2 as [a2|b2|]; inversion_clear Hx'.
destruct (cmra_extend n b b1 b2) as (z1&z2&?&?&?); auto.
exists (Cinr z1), (Cinr z2). by repeat constructor.
+ by exists CsumBot, CsumBot; destruct y1, y2; inversion_clear Hx'.
Qed.
Canonical Structure csumR :=
CMRAT (csum A B) csum_cofe_mixin csum_cmra_mixin.
......
algebra/excl.v
+ 1
− 5
View file @ 337a29d4
......@@ -88,11 +88,7 @@ Proof.
- by intros [?|] [?|] [?|]; constructor.
- by intros [?|] [?|]; constructor.
- by intros n [?|] [?|].
- intros n x y1 y2 ? Hx.
by exists match y1, y2 with
| Excl a1, Excl a2 => (Excl a1, Excl a2)
| ExclBot, _ => (ExclBot, y2) | _, ExclBot => (y1, ExclBot)
end; destruct y1, y2; inversion_clear Hx; repeat constructor.
- intros n x [?|] [?|] ?; inversion_clear 1; eauto.
Qed.
Canonical Structure exclR :=
CMRAT (excl A) excl_cofe_mixin excl_cmra_mixin.
......
algebra/gmap.v
+ 24
− 15
View file @ 337a29d4
......@@ -137,21 +137,30 @@ Proof.
rewrite !lookup_core. by apply cmra_core_mono.
- intros n m1 m2 Hm i; apply cmra_validN_op_l with (m2 !! i).
by rewrite -lookup_op.
- intros n m m1 m2 Hm Hm12.
assert (∀ i, m !! i ≡{n}≡ m1 !! i ⋅ m2 !! i) as Hm12'
by (by intros i; rewrite -lookup_op).
set (f i := cmra_extend n (m !! i) (m1 !! i) (m2 !! i) (Hm i) (Hm12' i)).
set (f_proj i := proj1_sig (f i)).
exists (map_imap (λ i _, (f_proj i).1) m, map_imap (λ i _, (f_proj i).2) m);
repeat split; intros i; rewrite /= ?lookup_op !lookup_imap.
+ destruct (m !! i) as [x|] eqn:Hx; rewrite !Hx /=; [|constructor].
rewrite -Hx; apply (proj2_sig (f i)).
+ destruct (m !! i) as [x|] eqn:Hx; rewrite /=; [apply (proj2_sig (f i))|].
move: (Hm12' i). rewrite Hx -!timeless_iff.
rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
+ destruct (m !! i) as [x|] eqn:Hx; simpl; [apply (proj2_sig (f i))|].
move: (Hm12' i). rewrite Hx -!timeless_iff.
rewrite !(symmetry_iff _ None) !equiv_None op_None; tauto.
- intros n m. induction m as [|i x m Hi IH] using map_ind=> m1 m2 Hmv Hm.
{ exists ∅, ∅; split_and!=> -i; symmetry; symmetry in Hm; move: Hm=> /(_ i);
rewrite !lookup_op !lookup_empty ?dist_None op_None; intuition. }
destruct (IH (delete i m1) (delete i m2)) as (m1'&m2'&Hm'&Hm1'&Hm2').
{ intros j; move: Hmv=> /(_ j). destruct (decide (i = j)) as [->|].
+ intros _. by rewrite Hi.
+ by rewrite lookup_insert_ne. }
{ intros j; move: Hm=> /(_ j); destruct (decide (i = j)) as [->|].
+ intros _. by rewrite lookup_op !lookup_delete Hi.
+ by rewrite !lookup_op lookup_insert_ne // !lookup_delete_ne. }
destruct (cmra_extend n (Some x) (m1 !! i) (m2 !! i)) as (y1&y2&?&?&?).
{ move: Hmv=> /(_ i). by rewrite lookup_insert. }
{ move: Hm=> /(_ i). by rewrite lookup_insert lookup_op. }
exists (partial_alter (λ _, y1) i m1'), (partial_alter (λ _, y2) i m2').
split_and!.
+ intros j. destruct (decide (i = j)) as [->|].
* by rewrite lookup_insert lookup_op !lookup_partial_alter.
* by rewrite lookup_insert_ne // Hm' !lookup_op !lookup_partial_alter_ne.
+ intros j. destruct (decide (i = j)) as [->|].
* by rewrite lookup_partial_alter.
* by rewrite lookup_partial_alter_ne // Hm1' lookup_delete_ne.
+ intros j. destruct (decide (i = j)) as [->|].
* by rewrite lookup_partial_alter.
* by rewrite lookup_partial_alter_ne // Hm2' lookup_delete_ne.
Qed.
Canonical Structure gmapR :=
CMRAT (gmap K A) gmap_cofe_mixin gmap_cmra_mixin.
......
algebra/iprod.v
+ 6
− 3
View file @ 337a29d4
......@@ -117,9 +117,12 @@ Section iprod_cmra.
by rewrite iprod_lookup_core; apply cmra_core_mono, Hf.
- intros n f1 f2 Hf x; apply cmra_validN_op_l with (f2 x), Hf.
- intros n f f1 f2 Hf Hf12.
set (g x := cmra_extend n (f x) (f1 x) (f2 x) (Hf x) (Hf12 x)).
exists ((λ x, (proj1_sig (g x)).1), (λ x, (proj1_sig (g x)).2)).
split_and?; intros x; apply (proj2_sig (g x)).
destruct (finite_choice (λ x (yy : B x * B x),
f x ≡ yy.1 ⋅ yy.2 ∧ yy.1 ≡{n}≡ f1 x ∧ yy.2 ≡{n}≡ f2 x)) as [gg Hgg].
{ intros x. specialize (Hf12 x).
destruct (cmra_extend n (f x) (f1 x) (f2 x)) as (y1&y2&?&?&?); eauto.
exists (y1,y2); eauto. }
exists (λ x, gg x.1), (λ x, gg x.2). split_and!=> -?; naive_solver.
Qed.
Canonical Structure iprodR :=
CMRAT (iprod B) iprod_cofe_mixin iprod_cmra_mixin.
......
algebra/list.v
+ 8
− 9
View file @ 337a29d4
......@@ -193,15 +193,14 @@ Section cmra.
rewrite !list_lookup_core. by apply cmra_core_mono.
- intros n l1 l2. rewrite !list_lookup_validN.
setoid_rewrite list_lookup_op. eauto using cmra_validN_op_l.
- intros n l. induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl Hl';
try (by exfalso; inversion_clear Hl').
+ by exists ([], []).
+ by exists ([], x :: l).
+ by exists (x :: l, []).
+ destruct (IH l1 l2) as ([l1' l2']&?&?&?),
(cmra_extend n x y1 y2) as ([y1' y2']&?&?&?);
[inversion_clear Hl; inversion_clear Hl'; auto ..|]; simplify_eq/=.
exists (y1' :: l1', y2' :: l2'); repeat constructor; auto.
- intros n l.
induction l as [|x l IH]=> -[|y1 l1] [|y2 l2] Hl; inversion_clear 1.
+ by exists [], [].
+ exists [], (x :: l); by repeat constructor.
+ exists (x :: l), []; by repeat constructor.
+ inversion_clear Hl. destruct (IH l1 l2) as (l1'&l2'&?&?&?),
(cmra_extend n x y1 y2) as (y1'&y2'&?&?&?); simplify_eq/=; auto.
exists (y1' :: l1'), (y2' :: l2'); repeat constructor; auto.
Qed.
Canonical Structure listR := CMRAT (list A) list_cofe_mixin list_cmra_mixin.
......
algebra/upred.v
+ 2
− 3
View file @ 337a29d4
......@@ -1035,7 +1035,7 @@ Proof.
- destruct n as [|n]; simpl.
{ by exists x, (core x); rewrite cmra_core_r. }
intros (x1&x2&Hx&?&?); destruct (cmra_extend n x x1 x2)
as ([y1 y2]&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
as (y1&y2&Hx'&Hy1&Hy2); eauto using cmra_validN_S; simpl in *.
exists y1, y2; split; [by rewrite Hx'|by rewrite Hy1 Hy2].
- destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
exists x1, x2; eauto using dist_S.
......@@ -1213,8 +1213,7 @@ Lemma prod_validI {A B : cmraT} (x : A * B) : ✓ x ⊣⊢ ✓ x.1 ∧ ✓ x.2.
Proof. by unseal. Qed.
(* Later *)
Lemma later_equivI {A : cofeT} (x y : later A) :
x ≡ y ⊣⊢ ▷ (later_car x ≡ later_car y).
Lemma later_equivI {A : cofeT} (x y : A) : Next x ≡ Next y ⊣⊢ ▷ (x ≡ y).
Proof. by unseal. Qed.
(* Discrete *)
......
program_logic/ownership.v
+ 1
− 1
View file @ 337a29d4
......@@ -126,7 +126,7 @@ Proof.
iRewrite "HI" in "HvI". rewrite uPred.option_validI agree_validI.
iRewrite -"HvI" in "HI". by rewrite agree_idemp. }
rewrite /invariant_unfold.
by rewrite agree_equivI uPred.later_equivI /= iProp_unfold_equivI.
by rewrite agree_equivI uPred.later_equivI iProp_unfold_equivI.
Qed.
Lemma ownI_open i P : wsat ★ ownI i P ★ ownE {[i]} ⊢ wsat ★ ▷ P ★ ownD {[i]}.
......
program_logic/saved_prop.v
+ 1
− 1
View file @ 337a29d4
......@@ -35,7 +35,7 @@ Section saved_prop.
Lemma saved_prop_agree γ x y :
saved_prop_own γ x ★ saved_prop_own γ y ⊢ ▷ (x ≡ y).
Proof.
rewrite -own_op own_valid agree_validI agree_equivI later_equivI /=.
rewrite -own_op own_valid agree_validI agree_equivI later_equivI.
set (G1 := cFunctor_map F (iProp_fold, iProp_unfold)).
set (G2 := cFunctor_map F (@iProp_unfold Σ, @iProp_fold Σ)).
assert (∀ z, G2 (G1 z) ≡ z) as help.
......
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