Commit 9f7e8457 authored by Ralf Jung's avatar Ralf Jung

bump std++; fix for lookup_seq renames

parent 3a2bc1bd
Pipeline #25333 passed with stage
in 10 minutes and 37 seconds
......@@ -11,7 +11,7 @@ synopsis: "A Coq formalization of the ORC11 semantics for weak memory"
depends: [
"coq" { (>= "8.9.0" & < "8.12~") | (= "dev") }
"coq-stdpp" { (= "dev.2020-03-10.2.8db97649") | (= "dev") }
"coq-stdpp" { (= "dev.2020-03-17.3.ad2e80d6") | (= "dev") }
]
build: [make "-j%{jobs}%"]
......
......@@ -1580,7 +1580,7 @@ Section Memory.
- assert (is_Some(cell_list l n M !! n')) as [C EqC].
{ apply lookup_lt_is_Some. by rewrite LEN. }
rewrite EqC. apply cell_list_Some_2 in EqC.
by rewrite (lookup_seq _ _ _ Lt) /= EqC.
by rewrite (lookup_seq_lt _ _ _ Lt) /= EqC.
- apply Nat.nlt_ge in Ge.
rewrite lookup_ge_None_2; last by rewrite LEN.
by rewrite (lookup_seq_ge _ _ _ Ge) /=.
......
......@@ -601,7 +601,7 @@ Section AllocSteps.
Proof.
rewrite /alloc_messages /=. f_equal. simpl. apply list_eq => i.
rewrite 2!list_lookup_fmap /=. case (decide (i < n)) => [Lt| Ge].
- do 2 (rewrite lookup_seq; last done). simpl.
- do 2 (rewrite lookup_seq_lt; last done). simpl.
rewrite (_: l >> Z.pos (Pos.of_succ_nat i)
= l >> 1%nat >> Z.of_nat i); first done.
rewrite shift_nat_assoc. by f_equal.
......@@ -626,7 +626,7 @@ Section AllocSteps.
- by rewrite map_length seq_length.
- move => n' 𝑚 Eq.
rewrite /𝑚s /alloc_messages in Eq.
apply list_lookup_fmap_inv in Eq as [i [Eq1 [Eq2 Lt]%lookup_seq_inv]].
apply list_lookup_fmap_inv in Eq as [i [Eq1 [Eq2 Lt]%lookup_seq]].
simpl in Eq2. subst i.
by rewrite Eq1 /=.
- have FRESH' := alloc_add_fresh _ _ _ FRESH.
......@@ -724,7 +724,7 @@ Section AllocSteps.
Proof.
rewrite /dealloc_messages /=. f_equal. apply list_eq => i.
rewrite 2!list_lookup_fmap /=. case (decide (i < n)) => [Lt| Ge].
- do 2 (rewrite lookup_seq; last done). simpl.
- do 2 (rewrite lookup_seq_lt; last done). simpl.
rewrite (_: l >> Z.pos (Pos.of_succ_nat i)
= l >> 1%nat >> Z.of_nat i); first done.
rewrite shift_nat_assoc. by f_equal.
......@@ -751,7 +751,7 @@ Section AllocSteps.
have Lt: (n' < n)%nat.
{ apply lookup_lt_Some in Eq. move : Eq. by rewrite dealloc_messages_length. }
move : Eq.
rewrite list_lookup_fmap (lookup_seq _ _ _ Lt) /= => [[<-]].
rewrite list_lookup_fmap (lookup_seq_lt _ _ _ Lt) /= => [[<-]].
by case_match; [case_match|].
Qed.
......@@ -790,7 +790,7 @@ Section AllocSteps.
constructor; last done.
- by rewrite map_length seq_length.
- move => n' 𝑚 Eq. rewrite /𝑚s /dealloc_messages in Eq.
apply list_lookup_fmap_inv in Eq as [i [Eq1 [Eq2 Lt]%lookup_seq_inv]].
apply list_lookup_fmap_inv in Eq as [i [Eq1 [Eq2 Lt]%lookup_seq]].
simpl in Eq2. subst i.
move : (REMOVE _ Lt)
=> /elem_of_difference [/memory_loc_elem_of_dom Eqm NIN].
......
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