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

Merge branch 'ralf/solve_ndisj' into 'master'

make solve_ndisj more powerful

Closes #34

See merge request iris/stdpp!75
parents 3bf046f2 5695ee20
Pipeline #17812 passed with stage
in 13 minutes and 32 seconds
The command has indeed failed with message:
Ltac call to "solve_ndisj" failed.
No applicable tactic.
From stdpp Require Import namespaces strings.
Set Ltac Backtrace.
Lemma test1 (N1 N2 : namespace) :
N1 ## N2 N1 @{coPset} N2.
Proof. solve_ndisj. Qed.
......@@ -20,9 +18,4 @@ Proof. solve_ndisj. Qed.
Lemma test5 (N1 N2 : namespace) :
N1 N2 @{coPset} N1.@"x" N2 N1.@"y".
Proof.
Fail solve_ndisj. (* FIXME: it should be able to solve this. *)
apply namespace_subseteq_difference.
{ apply ndot_preserve_disjoint_r. set_solver. }
solve_ndisj.
Qed.
Proof. solve_ndisj. Qed.
......@@ -66,35 +66,37 @@ Section namespace.
Lemma ndot_preserve_disjoint_r N E x : E ## N E ## N.@x.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
Lemma namespace_subseteq_difference E1 E2 E3 :
E1 ## E3 E1 E2 E1 E2 E3.
Proof. set_solver. Qed.
Lemma namespace_subseteq_difference_l E1 E2 E3 : E1 E3 E1 E2 E3.
Proof. set_solver. Qed.
Lemma ndisj_difference_l E N1 N2 : N2 (N1 : coPset) E N1 ## N2.
Proof. set_solver. Qed.
End namespace.
(* The hope is that registering these will suffice to solve most goals
(** The hope is that registering these will suffice to solve most goals
of the forms:
- [N1 ## N2]
- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
Create HintDb ndisj.
Hint Resolve namespace_subseteq_difference : ndisj.
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r : ndisj.
Hint Resolve nclose_subseteq' ndisj_difference_l : ndisj.
Hint Resolve namespace_subseteq_difference_l | 100 : ndisj.
(** Rules for goals of the form [_ ⊆ _] *)
(** If-and-only-if rules. Well, not quite, but for the fragment we are
considering they are. *)
Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (union_least (A:=positive) (C:=coPset)) : ndisj.
(** Fallback, loses lots of information but lets other rules make progress. *)
Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
Hint Resolve nclose_subseteq' | 100 : ndisj.
(** Rules for goals of the form [_ ## _] *)
(** The base rule that we want to ultimately get down to. *)
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj.
(** Fallback, loses lots of information but lets other rules make progress.
Tests show trying [disjoint_difference_l1] first gives better performance. *)
Hint Resolve (disjoint_difference_l1 (A:=positive) (C:=coPset)) | 50 : ndisj.
Hint Resolve (disjoint_difference_l2 (A:=positive) (C:=coPset)) | 100 : ndisj.
Hint Resolve ndot_preserve_disjoint_l ndot_preserve_disjoint_r | 100 : ndisj.
Ltac solve_ndisj :=
repeat match goal with
| H : _ _ _ |- _ => apply union_subseteq in H as [??]
end;
solve [eauto 10 with ndisj].
solve [eauto 12 with ndisj].
Hint Extern 1000 => solve_ndisj : solve_ndisj.
......@@ -653,9 +653,23 @@ Section set.
Lemma difference_mono_r X1 X2 Y : X1 X2 X1 Y X2 Y.
Proof. set_solver. Qed.
Lemma subseteq_difference_r X Y1 Y2 :
X ## Y2 X Y1 X Y1 Y2.
Proof. set_solver. Qed.
Lemma subseteq_difference_l X1 X2 Y : X1 Y X1 X2 Y.
Proof. set_solver. Qed.
(** Disjointness *)
Lemma disjoint_intersection X Y : X ## Y X Y .
Proof. set_solver. Qed.
Lemma disjoint_difference_l1 X1 X2 Y : Y X2 X1 X2 ## Y.
Proof. set_solver. Qed.
Lemma disjoint_difference_l2 X1 X2 Y : X1 ## Y X1 X2 ## Y.
Proof. set_solver. Qed.
Lemma disjoint_difference_r1 X Y1 Y2 : X Y2 X ## Y1 Y2.
Proof. set_solver. Qed.
Lemma disjoint_difference_r2 X Y1 Y2 : X ## Y1 X ## Y1 Y2.
Proof. set_solver. Qed.
Section leibniz.
Context `{!LeibnizEquiv C}.
......
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