Skip to content
Snippets Groups Projects
Commit f1a4f71c authored by Ralf Jung's avatar Ralf Jung
Browse files

prefer Hint Resolve over Hint Extern

parent a9c8861d
No related branches found
No related tags found
1 merge request!303solve_ndisj: handle goals containing _ ∖ _ ∖ _
Pipeline #50909 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 5 additions and 2 deletions
theories/namespaces.v
+ 5
− 2
View file @ f1a4f71c
...@@ -111,8 +111,11 @@ Global Hint Extern 10 (_ ## (_ ∖ _)) => ...@@ -111,8 +111,11 @@ Global Hint Extern 10 (_ ## (_ ∖ _)) =>
end : ndisj. end : ndisj.
(** Before we apply disjoint_difference, let's make sure we normalize the goal (** Before we apply disjoint_difference, let's make sure we normalize the goal
to [_ ∖ (_ ∪ _)]. *) to [_ ∖ (_ ∪ _)]. *)
Global Hint Extern 20 ((?X ∖ ?Y ∖ ?Z) ## _) => Local Lemma coPset_difference_difference (X1 X2 X3 Y : coPset) :
rewrite (difference_difference_L (C:=coPset) X Y Z) : ndisj. X1 ∖ (X2 ∪ X3) ## Y →
X1 ∖ X2 ∖ X3 ## Y.
Proof. set_solver. Qed.
Global Hint Resolve coPset_difference_difference | 20 : ndisj.
(** Fallback, loses lots of information but lets other rules make progress. (** Fallback, loses lots of information but lets other rules make progress.
Tests show trying [disjoint_difference_l1] first gives better performance. *) Tests show trying [disjoint_difference_l1] first gives better performance. *)
Local Definition coPset_disjoint_difference_l1 := disjoint_difference_l1 (C:=coPset). Local Definition coPset_disjoint_difference_l1 := disjoint_difference_l1 (C:=coPset).
......
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