Commit 1c548c0c authored by Ralf Jung's avatar Ralf Jung

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

parents 23cd0c7d 26ed8552
Pipeline #3405 passed with stage
in 16 minutes and 32 seconds
......@@ -477,24 +477,13 @@ Lemma list_lookup_middle l1 l2 x n :
n = length l1 (l1 ++ x :: l2) !! n = Some x.
Proof. intros ->. by induction l1. Qed.
Lemma nth_lookup_or_length l i d :
{l !! i = Some (nth i l d)} + {(length l i)%nat}.
Lemma nth_lookup l i d : nth i l d = from_option id d (l !! i).
Proof. revert i. induction l as [|x l IH]; intros [|i]; simpl; auto. Qed.
Lemma nth_lookup_Some l i d x : l !! i = Some x nth i l d = x.
Proof. rewrite nth_lookup. by intros ->. Qed.
Lemma nth_lookup_or_length l i d : {l !! i = Some (nth i l d)} + {length l i}.
Proof.
revert i; induction l; intros i.
- right. simpl. omega.
- destruct i; simpl.
+ left. done.
+ destruct (IHl i) as [->|]; [by left|].
right. omega.
Qed.
Lemma nth_lookup l i d x :
l !! i = Some x nth i l d = x.
Proof.
revert i; induction l; intros i; [done|].
destruct i; simpl.
- congruence.
- apply IHl.
rewrite nth_lookup. destruct (l !! i) eqn:?; eauto using lookup_ge_None_1.
Qed.
Lemma list_insert_alter l i x : <[i:=x]>l = alter (λ _, x) i l.
......@@ -2093,11 +2082,18 @@ Proof.
end); clear go; intuition.
Defined.
Definition Forall_nil_2 := @Forall_nil A.
Definition Forall_cons_2 := @Forall_cons A.
Global Instance Forall_proper:
Proper (pointwise_relation _ () ==> (=) ==> ()) (@Forall A).
Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
Global Instance Exists_proper:
Proper (pointwise_relation _ () ==> (=) ==> ()) (@Exists A).
Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
Section Forall_Exists.
Context (P : A Prop).
Definition Forall_nil_2 := @Forall_nil A.
Definition Forall_cons_2 := @Forall_cons A.
Lemma Forall_forall l : Forall P l x, x l P x.
Proof.
split; [induction 1; inversion 1; subst; auto|].
......@@ -2124,9 +2120,6 @@ Section Forall_Exists.
Lemma Forall_impl (Q : A Prop) l :
Forall P l ( x, P x Q x) Forall Q l.
Proof. intros H ?. induction H; auto. Defined.
Global Instance Forall_proper:
Proper (pointwise_relation _ () ==> (=) ==> ()) (@Forall A).
Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
Lemma Forall_iff l (Q : A Prop) :
( x, P x Q x) Forall P l Forall Q l.
Proof. intros H. apply Forall_proper. red; apply H. done. Qed.
......@@ -2237,9 +2230,7 @@ Section Forall_Exists.
Lemma Exists_impl (Q : A Prop) l :
Exists P l ( x, P x Q x) Exists Q l.
Proof. intros H ?. induction H; auto. Defined.
Global Instance Exists_proper:
Proper (pointwise_relation _ () ==> (=) ==> ()) (@Exists A).
Proof. split; subst; induction 1; constructor; by firstorder auto. Qed.
Lemma Exists_not_Forall l : Exists (not P) l ¬Forall P l.
Proof. induction 1; inversion_clear 1; contradiction. Qed.
Lemma Forall_not_Exists l : Forall (not P) l ¬Exists P l.
......@@ -2302,7 +2293,26 @@ Proof.
destruct Hj; subst. auto with lia.
Qed.
Lemma Forall2_same_length {A B} (l : list A) (k : list B) :
Forall2 (λ _ _, True) l k length l = length k.
Proof.
split; [by induction 1; f_equal/=|].
revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
Qed.
(** ** Properties of the [Forall2] predicate *)
Lemma Forall_Forall2 {A} (Q : A A Prop) l :
Forall (λ x, Q x x) l Forall2 Q l l.
Proof. induction 1; constructor; auto. Qed.
Lemma Forall2_forall `{Inhabited A} B C (Q : A B C Prop) l k :
Forall2 (λ x y, z, Q z x y) l k z, Forall2 (Q z) l k.
Proof.
split; [induction 1; constructor; auto|].
intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor.
- intros z. by feed inversion (Hlk z).
- apply IH. intros z. by feed inversion (Hlk z).
Qed.
Section Forall2.
Context {A B} (P : A B Prop).
Implicit Types x : A.
......@@ -2310,12 +2320,6 @@ Section Forall2.
Implicit Types l : list A.
Implicit Types k : list B.
Lemma Forall2_same_length l k :
Forall2 (λ _ _, True) l k length l = length k.
Proof.
split; [by induction 1; f_equal/=|].
revert k. induction l; intros [|??] ?; simplify_eq/=; auto.
Qed.
Lemma Forall2_length l k : Forall2 P l k length l = length k.
Proof. by induction 1; f_equal/=. Qed.
Lemma Forall2_length_l l k n : Forall2 P l k length l = n length k = n.
......@@ -2340,18 +2344,7 @@ Section Forall2.
Proof.
intros H. revert k2. induction H; inversion_clear 1; intros; f_equal; eauto.
Qed.
Lemma Forall2_forall `{Inhabited C} (Q : C A B Prop) l k :
Forall2 (λ x y, z, Q z x y) l k z, Forall2 (Q z) l k.
Proof.
split; [induction 1; constructor; auto|].
intros Hlk. induction (Hlk inhabitant) as [|x y l k _ _ IH]; constructor.
- intros z. by feed inversion (Hlk z).
- apply IH. intros z. by feed inversion (Hlk z).
Qed.
Lemma Forall_Forall2 (Q : A A Prop) l :
Forall (λ x, Q x x) l Forall2 Q l l.
Proof. induction 1; constructor; auto. Qed.
Lemma Forall2_Forall_l (Q : A Prop) l k :
Forall2 P l k Forall (λ y, x, P x y Q x) k Forall Q l.
Proof. induction 1; inversion_clear 1; eauto. Qed.
......@@ -2812,11 +2805,12 @@ Section setoid.
End setoid.
(** * Properties of the monadic operations *)
Lemma list_fmap_id {A} (l : list A) : id <$> l = l.
Proof. induction l; f_equal/=; auto. Qed.
Section fmap.
Context {A B : Type} (f : A B).
Lemma list_fmap_id (l : list A) : id <$> l = l.
Proof. induction l; f_equal/=; auto. Qed.
Lemma list_fmap_compose {C} (g : B C) l : g f <$> l = g <$> f <$> l.
Proof. induction l; f_equal/=; auto. Qed.
Lemma list_fmap_ext (g : A B) (l1 l2 : list A) :
......
......@@ -46,12 +46,9 @@ Local Notation "l ↦{ q } -" := (∃ v, l ↦{q} v)%I
(at level 20, q at level 50, format "l ↦{ q } -") : uPred_scope.
Local Notation "l ↦ -" := (l {1} -)%I (at level 20) : uPred_scope.
Section gen_heap.
Context `{gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Section to_gen_heap.
Context (L V : Type) `{Countable L}.
Implicit Types σ : gmap L V.
Implicit Types h g : gen_heapUR L V.
(** Conversion to heaps and back *)
Lemma to_gen_heap_valid σ : to_gen_heap σ.
......@@ -71,6 +68,14 @@ Section gen_heap.
Lemma to_gen_heap_delete l σ :
to_gen_heap (delete l σ) = delete l (to_gen_heap σ).
Proof. by rewrite /to_gen_heap fmap_delete. Qed.
End to_gen_heap.
Section gen_heap.
Context `{gen_heapG L V Σ}.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : V iProp Σ.
Implicit Types σ : gmap L V.
Implicit Types h g : gen_heapUR L V.
(** General properties of mapsto *)
Global Instance mapsto_timeless l q v : TimelessP (l {q} v).
......
......@@ -13,7 +13,9 @@ Definition client : expr :=
(worker 12 "b" "y" ||| worker 17 "b" "y").
Section client.
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ} (N : namespace).
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ}.
Local Definition N := nroot .@ "barrier".
Definition y_inv (q : Qp) (l : loc) : iProp Σ :=
( f : val, l {q} f n : Z, WP f #n {{ v, v = #(n + 42) }})%I.
......@@ -58,9 +60,7 @@ Section ClosedProofs.
Let Σ : gFunctors := #[ heapΣ ; barrierΣ ; spawnΣ ].
Lemma client_adequate σ : adequate client σ (λ _, True).
Proof.
apply (heap_adequacy Σ)=> ?. apply (client_safe (nroot .@ "barrier")).
Qed.
Proof. apply (heap_adequacy Σ)=> ?. apply client_safe. Qed.
End ClosedProofs.
......
......@@ -29,7 +29,7 @@ Instance subG_one_shotΣ {Σ} : subG one_shotΣ Σ → one_shotG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !one_shotG Σ} (N : namespace).
Context `{!heapG Σ, !one_shotG Σ}.
Definition one_shot_inv (γ : gname) (l : loc) : iProp Σ :=
(l NONEV own γ Pending n : Z, l SOMEV #n own γ (Shot n))%I.
......@@ -40,7 +40,7 @@ Lemma wp_one_shot (Φ : val → iProp Σ) :
WP f2 #() {{ g, WP g #() {{ _, True }} }} - Φ (f1,f2)%V)
WP one_shot_example #() {{ Φ }}.
Proof.
iIntros "Hf /=".
iIntros "Hf /=". pose proof (nroot .@ "N") as N.
rewrite -wp_fupd /one_shot_example /=. wp_seq. wp_alloc l as "Hl". wp_let.
iMod (own_alloc Pending) as (γ) "Hγ"; first done.
iMod (inv_alloc N _ (one_shot_inv γ l) with "[Hl Hγ]") as "#HN".
......
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