Commit 0cf35200 by Robbert Krebbers

Prove refinement lemmas for locks.

parent a61c87a0
 ... ... @@ -402,14 +402,15 @@ Lemma lookup_ge_None_1 l i : l !! i = None → length l ≤ i. Proof. by rewrite lookup_ge_None. Qed. Lemma lookup_ge_None_2 l i : length l ≤ i → l !! i = None. Proof. by rewrite lookup_ge_None. Qed. Lemma list_eq_length l1 l2 : length l2 = length l1 → (∀ i x y, l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2. Lemma list_eq_same_length l1 l2 n : length l2 = n → length l1 = n → (∀ i x y, i < n → l1 !! i = Some x → l2 !! i = Some y → x = y) → l1 = l2. Proof. intros Hl ?; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx. * destruct (lookup_lt_is_Some_2 l1 i) as [y ?]; [|naive_solver]. rewrite <-Hl. eauto using lookup_lt_Some. * by rewrite lookup_ge_None, <-Hl, <-lookup_ge_None. intros <- Hlen Hl; apply list_eq; intros i. destruct (l2 !! i) as [x|] eqn:Hx. * destruct (lookup_lt_is_Some_2 l1 i) as [y Hy]. { rewrite Hlen; eauto using lookup_lt_Some. } rewrite Hy; f_equal; apply (Hl i); eauto using lookup_lt_Some. * by rewrite lookup_ge_None, Hlen, <-lookup_ge_None. Qed. Lemma lookup_app_l l1 l2 i : i < length l1 → (l1 ++ l2) !! i = l1 !! i. Proof. revert i. induction l1; intros [|?]; simpl; auto with lia. Qed. ... ... @@ -3054,7 +3055,6 @@ Ltac decompose_elem_of_list := repeat | H : _ ∈ _ :: _ |- _ => apply elem_of_cons in H; destruct H | H : _ ∈ _ ++ _ |- _ => apply elem_of_app in H; destruct H end. Ltac simplify_list_fmap_equality := repeat match goal with | _ => progress simplify_equality ... ... @@ -3091,6 +3091,7 @@ Ltac decompose_Forall_hyps := repeat | H : Forall2 _ ?l [] |- _ => apply Forall2_nil_inv_r in H; subst l | H : Forall2 _ (_ :: _) (_ :: _) |- _ => apply Forall2_cons_inv in H; destruct H | _ => progress simplify_equality' | H : Forall2 _ (_ :: _) ?k |- _ => let k_hd := fresh k "_hd" in let k_tl := fresh k "_tl" in apply Forall2_cons_inv_l in H; destruct H as (k_hd&k_tl&?&?&->); ... ... @@ -3100,8 +3101,8 @@ Ltac decompose_Forall_hyps := repeat apply Forall2_cons_inv_r in H; destruct H as (l_hd&l_tl&?&?&->); rename l_tl into l | H : Forall2 _ (_ ++ _) (_ ++ _) |- _ => apply Forall2_app_inv in H; [destruct H | by eauto using Forall2_length, eq_sym] apply Forall2_app_inv in H; [destruct H | first [by eauto using Forall2_length | by symmetry; eauto using Forall2_length]] | H : Forall2 _ (_ ++ _) ?k |- _ => first [ let k1 := fresh k "_1" in let k2 := fresh k "_2" in apply Forall2_app_inv_l in H; destruct H as (k1&k2&?&?&->) ... ... @@ -3140,8 +3141,6 @@ Ltac decompose_Forall_hyps := repeat destruct (Forall3_lookup_r P _ _ _ _ _ H H3) as (?&?&?&?&?) end end. Ltac decompose_Forall_hyps' := repeat (progress simplify_equality' || decompose_Forall_hyps). Ltac decompose_Forall := repeat match goal with | |- Forall _ _ => by apply Forall_true ... ...
 ... ... @@ -261,14 +261,15 @@ Instance: FinMapDom nat natmap natset := mapset_dom_spec. (* Fixpoint avoids this definition from being unfolded *) Fixpoint of_bools (βs : list bool) : natset := Mapset \$ list_to_natmap \$ (λ β : bool, if β then Some () else None) <\$> βs. Definition to_bools (X : natset) : list bool := (λ mu, match mu with Some _ => true | None => false end) <\$> natmap_car (mapset_car X). let f (β : bool) := if β then Some () else None in Mapset \$ list_to_natmap \$ f <\$> βs. Definition to_bools (sz : nat) (X : natset) : list bool := let f (mu : option ()) := match mu with Some _ => true | None => false end in resize sz false \$ f <\$> natmap_car (mapset_car X). Lemma of_bools_unfold βs : of_bools βs = Mapset \$ list_to_natmap \$ (λ β : bool, if β then Some () else None) <\$> βs. let f (β : bool) := if β then Some () else None in of_bools βs = Mapset \$ list_to_natmap \$ f <\$> βs. Proof. by destruct βs. Qed. Lemma elem_of_of_bools βs i : i ∈ of_bools βs ↔ βs !! i = Some true. Proof. ... ... @@ -276,16 +277,6 @@ Proof. rewrite list_to_natmap_spec, list_lookup_fmap. destruct (βs !! i) as [[]|]; compute; intuition congruence. Qed. Lemma elem_of_to_bools X i : to_bools X !! i = Some true ↔ i ∈ X. Proof. unfold to_bools, elem_of, mapset_elem_of, lookup at 2, natmap_lookup; simpl. destruct (mapset_car X) as [l ?]; simpl. rewrite list_lookup_fmap. destruct (l !! i) as [[[]|]|]; compute; intuition congruence. Qed. Lemma of_to_bools X : of_bools (to_bools X) = X. Proof. apply elem_of_equiv_L. intros i. by rewrite elem_of_of_bools,elem_of_to_bools. Qed. Lemma of_bools_union βs1 βs2 : length βs1 = length βs2 → of_bools (βs1 ||* βs2) = of_bools βs1 ∪ of_bools βs2. ... ... @@ -294,6 +285,23 @@ Proof. apply elem_of_equiv_L. intros i. rewrite elem_of_union, !elem_of_of_bools. revert i. induction Hβs as [|[] []]; intros [|?]; naive_solver. Qed. Lemma to_bools_length (X : natset) sz : length (to_bools sz X) = sz. Proof. apply resize_length. Qed. Lemma lookup_to_bools sz X i β : i < sz → to_bools sz X !! i = Some β ↔ (i ∈ X ↔ β = true). Proof. unfold to_bools, elem_of, mapset_elem_of, lookup at 2, natmap_lookup; simpl. intros. destruct (mapset_car X) as [l ?]; simpl. destruct (l !! i) as [mu|] eqn:Hmu; simpl. { rewrite lookup_resize, list_lookup_fmap, Hmu by (rewrite ?fmap_length; eauto using lookup_lt_Some). destruct mu as [[]|], β; simpl; intuition congruence. } rewrite lookup_resize_new by (rewrite ?fmap_length; eauto using lookup_ge_None_1); destruct β; intuition congruence. Qed. Lemma lookup_to_bools_true sz X i : i < sz → to_bools sz X !! i = Some true ↔ i ∈ X. Proof. intros. rewrite lookup_to_bools by done. intuition. Qed. (** A [natmap A] forms a stack with elements of type [A] and possible holes *) Definition natmap_push {A} (o : option A) (m : natmap A) : natmap A := ... ... @@ -313,7 +321,6 @@ Lemma lookup_natmap_push_S {A} o (m : natmap A) i : Proof. by destruct o, m as [[|??]]. Qed. Lemma lookup_natmap_pop {A} (m : natmap A) i : natmap_pop m !! i = m !! S i. Proof. by destruct m as [[|??]]. Qed. Lemma natmap_push_pop {A} (m : natmap A) : natmap_push (m !! 0) (natmap_pop m) = m. Proof. ... ...
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!