Commit 472a85c0 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Use ssreflect unification rather that Coq's for applying [res_validN_inv]. For...

Use ssreflect unification rather that Coq's for applying [res_validN_inv]. For some reason, this seems way faster...
parent 3f66fc06
......@@ -32,7 +32,7 @@ Proof. rewrite /ownI. apply _. Qed.
Lemma ownP_twice σ1 σ2 : ownP σ1 ownP σ2 (False : iProp Λ Σ).
Proof.
rewrite /ownP -uPred.ownM_op Res_op.
apply uPred.ownM_invalid. intros (?&[]&?)%res_validN_inv.
apply uPred.ownM_invalid. move=>/res_validN_inv [?[[]?]].
Qed.
Global Instance ownP_timeless σ : TimelessP (@ownP Λ Σ σ).
Proof. rewrite /ownP; apply _. Qed.
......@@ -61,7 +61,7 @@ Lemma ownI_spec n r i P :
{n} r
(ownI i P) n r wld r !! i {n} Some (to_agree (Next (iProp_unfold P))).
Proof.
intros (?&?&?)%res_validN_inv. rewrite /ownI; uPred.unseal.
move=> /res_validN_inv[?[??]]. rewrite /ownI; uPred.unseal.
rewrite /uPred_holds/=res_includedN/=singleton_includedN; split.
- intros [(P'&Hi&HP) _]; rewrite Hi.
constructor; symmetry; apply agree_valid_includedN.
......@@ -71,7 +71,7 @@ Proof.
Qed.
Lemma ownP_spec n r σ : {n} r (ownP σ) n r pst r Excl' σ.
Proof.
intros (?&?&?)%res_validN_inv. rewrite /ownP; uPred.unseal.
move=> /res_validN_inv[?[??]]. rewrite /ownP; uPred.unseal.
rewrite /uPred_holds /= res_includedN /= Excl_includedN //.
rewrite (timeless_iff n). naive_solver (apply ucmra_unit_leastN).
Qed.
......
......@@ -117,7 +117,7 @@ Lemma wsat_update_pst n E σ1 σ1' r rf :
pst r {S n} Excl' σ1 wsat (S n) E σ1' (r rf)
σ1' = σ1 σ2, wsat (S n) E σ2 (update_pst σ2 r rf).
Proof.
intros Hpst_r [rs [(?&?&?)%res_validN_inv Hpst HE Hwld]].
move=> Hpst_r [rs [/res_validN_inv[?[??]] Hpst HE Hwld]].
assert (pst rf pst (big_opM rs) = ) as Hpst'.
{ by apply: (excl_validN_inv_l (S n) _ σ1); rewrite -Hpst_r assoc. }
assert (σ1' = σ1) as ->.
......@@ -132,7 +132,7 @@ Lemma wsat_update_gst n E σ r rf m1 (P : iGst Λ Σ → Prop) :
m1 {S n} gst r m1 ~~>: P
wsat (S n) E σ (r rf) m2, wsat (S n) E σ (update_gst m2 r rf) P m2.
Proof.
intros [mf Hr] Hup [rs [(?&?&?)%res_validN_inv Hσ HE Hwld]].
move=> [mf Hr] Hup [rs [/res_validN_inv [?[??]] Hσ HE Hwld]].
destruct (Hup (S n) (Some (mf gst (rf big_opM rs)))) as (m2&?&Hval'); try done.
{ by rewrite /= (assoc _ m1) -Hr -gst_op assoc. }
exists m2; split; [exists rs|done].
......@@ -158,7 +158,7 @@ Proof.
assert (r big_opM (<[i:=rP]> rs) rP r big_opM rs) as Hr.
{ by rewrite (comm _ rP) -assoc big_opM_insert. }
exists i; split_and?; [exists (<[i:=rP]>rs); constructor| |]; auto.
- move:Hval=>/res_validN_inv[?[A?]]; rewrite -assoc Hr.
- move:Hval=>/res_validN_inv[?[??]]; rewrite -assoc Hr.
rewrite res_validN_inv -wld_op -pst_op -gst_op !left_id; split_and!=>//.
intros j; destruct (decide (j = i)) as [->|].
+ by rewrite !lookup_op Hri HrPi Hrsi !right_id lookup_singleton.
......
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