Commit 5695ee20 authored by Ralf Jung's avatar Ralf Jung

coqdoc++

parent c081e1b7
...@@ -68,27 +68,27 @@ Section namespace. ...@@ -68,27 +68,27 @@ Section namespace.
Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed. Proof. intros. by apply symmetry, ndot_preserve_disjoint_l. Qed.
End namespace. 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: of the forms:
- [N1 ## N2] - [N1 ## N2]
- [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn] - [↑N1 ⊆ E ∖ ↑N2 ∖ .. ∖ ↑Nn]
- [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *) - [E1 ∖ ↑N1 ⊆ E2 ∖ ↑N2 ∖ .. ∖ ↑Nn] *)
Create HintDb ndisj. Create HintDb ndisj.
(* Rules for goals of the form [_ ⊆ _] *) (** Rules for goals of the form [_ ⊆ _] *)
(* If-and-only-if rules. Well, not quite, but for the fragment we are (** If-and-only-if rules. Well, not quite, but for the fragment we are
considering they are. *) considering they are. *)
Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj. Hint Resolve (subseteq_difference_r (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj. Hint Resolve (empty_subseteq (A:=positive) (C:=coPset)) : ndisj.
Hint Resolve (union_least (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. *) (** Fallback, loses lots of information but lets other rules make progress. *)
Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj. Hint Resolve (subseteq_difference_l (A:=positive) (C:=coPset)) | 100 : ndisj.
Hint Resolve nclose_subseteq' | 100 : ndisj. Hint Resolve nclose_subseteq' | 100 : ndisj.
(* Rules for goals of the form [_ ## _] *) (** Rules for goals of the form [_ ## _] *)
(* The base rule that we want to ultimately get down to. *) (** The base rule that we want to ultimately get down to. *)
Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : ndisj. Hint Extern 0 (_ ## _) => apply ndot_ne_disjoint; congruence : 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. *)
Hint Resolve (disjoint_difference_l1 (A:=positive) (C:=coPset)) | 50 : ndisj. Hint Resolve (disjoint_difference_l1 (A:=positive) (C:=coPset)) | 50 : ndisj.
Hint Resolve (disjoint_difference_l2 (A:=positive) (C:=coPset)) | 100 : ndisj. Hint Resolve (disjoint_difference_l2 (A:=positive) (C:=coPset)) | 100 : ndisj.
......
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