Commit 2023-10-20 20:51 214e72fd
View on Github →feat: add a SetLike
default rule set for aesop
(#7111)
This creates a new aesop
rule set called SetLike
to house lemmas about membership in subobjects.
Lemmas like pow_mem
should be included in the rule set:
@[to_additive (attr := aesop safe apply (rule_sets [SetLike]))]
theorem pow_mem {M A} [Monoid M] [SetLike A M] [SubmonoidClass A M] {S : A} {x : M}
(hx : x ∈ S) : ∀ n : ℕ, x ^ n ∈ S
Lemmas about closures, like AddSubmonoid.closure
should be included in the rule set, but they should be assigned a penalty (here we choose 20
throughout) so that they are not attempted before the general purpose ones like pow_mem
.
@[to_additive (attr := simp, aesop safe 20 apply (rule_sets [SetLike]))
"The `AddSubmonoid` generated by a set includes the set."]
theorem subset_closure : s ⊆ closure s := fun _ hx => mem_closure.2 fun _ hS => hS hx
In order for aesop
to make effective use of AddSubmonoid.closure
it needs the following new lemma.
@[aesop 5% apply (rule_sets [SetLike])]
lemma mem_of_subset {s : Set B} (hp : s ⊆ p) {x : B} (hx : x ∈ s) : x ∈ p := hp hx
Note: this lemma is marked as very unsafe (5%
) because it will apply whenever the goal is of the form x ∈ p
where p
is any term of a SetLike
instance; and moreover, it will create s
as a metavariable, which is in general a terrible idea, but necessary for the reason mentioned above.