Commit 4f836b8e authored by Ralf Jung's avatar Ralf Jung
Browse files

adjust for f_equiv optimizations

parent 38392de4
......@@ -261,7 +261,9 @@ Ltac f_contractive :=
| |- @dist_later ?A _ ?n ?x ?y =>
destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end;
try simple apply reflexivity.
(* Only try reflexivity if the terms are syntactically equal. This avoids
very expensive failing unification. *)
try match goal with |- _ ?x ?x => simple apply reflexivity end.
Ltac solve_contractive :=
solve_proper_core ltac:(fun _ => first [f_contractive | f_equiv]).
......
......@@ -100,9 +100,6 @@ Global Instance wp_ne s E e n :
Proof.
revert e. induction (lt_wf n) as [n _ IH]=> e Φ Ψ HΦ.
rewrite !wp_unfold /wp_pre /=.
(* FIXME: figure out a way to properly automate this proof *)
(* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
is very slow here *)
do 24 (f_contractive || f_equiv).
(* FIXME : simplify this proof once we have a good definition and a
proper instance for step_fupdN. *)
......
......@@ -473,7 +473,7 @@ Lemma tac_twp_cmpxchg_fail Δ s E i K l q v v1 v2 Φ :
Proof.
rewrite envs_entails_eq. intros. rewrite -twp_bind.
eapply wand_apply; first exact: twp_cmpxchg_fail.
rewrite envs_lookup_split //=. by do 2 f_equiv.
rewrite envs_lookup_split //=. simpl. by do 2 f_equiv.
Qed.
Lemma tac_wp_cmpxchg_suc Δ Δ' s E i K l v v1 v2 Φ :
......
Supports Markdown
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