b9243e19be
This PR makes the equational theorems of non-exposed defs private. If the author of a module chose not to expose the body of their function, then they likely don't want that implementation to leak through equational theorems. Helps with #8419. There is some amount of incidential complexity due to how `private` works in lean, by mangling the name: lots of code paths that need now do the right thing™ about private and non-private names, including the whole reserved name machinery. So this includes a number of refactorings: * The logic for calculating an equational theorem name (or similar) is now done by a single function, `mkEqLikeNameFor`, rather than all over the place. * Since the name of the equational theorem now depends on the current context (in particular whether it’s a proper module, or a non-module file), the forward map from declaration to equational theorem doesn’t quite work anymore. This map is deleted; the list of equational theorems are now always found by looking for declaration of the expected names (`alreadyGenerated). If users define such theorems themselves (and make it past the “do not allow reserved names to be declared”) they get to keep both pieces. * Because this map was deleted, mathlib’s `eqns` command can no longer easily warn if equational lemmas have already been generated too early (adaption branch exists). But in general I think lean could provide a more principled way of supporting custom unfold lemmas, and ideally the whole equational theorem machinery is just using that. * The ReservedNamePredicate is used by `resolveExact`, so we need to make sure that it returns the right name, including privateness. It is not ok to just reserve both the private and non-private name but then later in the ReservedNameAction produce just one of the two. * We create `foo.def_eq` eagerly for well-founded recursion. This is needed because we need feed in the proof of the rewriting done by `wf_preprocess`. But if `foo.def_eq` is private in a module, then a non-module importing it will still expect a non-private `foo.def_eq` to exist. To patch that, we install a `copyPrivateUnfoldTheorem : GetUnfoldEqnFn` that declares a theorem aliasing the private one. Seems to work.
55 lines
967 B
Text
55 lines
967 B
Text
/-! Tests that options affecting equational theorems work as expected. -/
|
|
|
|
namespace Test1
|
|
def nonrecfun : Bool → Nat
|
|
| false => 0
|
|
| true => 0
|
|
|
|
/--
|
|
info: equations:
|
|
theorem Test1.nonrecfun.eq_1 : nonrecfun false = 0
|
|
theorem Test1.nonrecfun.eq_2 : nonrecfun true = 0
|
|
-/
|
|
#guard_msgs in
|
|
#print equations nonrecfun
|
|
|
|
end Test1
|
|
|
|
namespace Test2
|
|
|
|
set_option backward.eqns.nonrecursive false in
|
|
def nonrecfun : Bool → Nat
|
|
| false => 0
|
|
| true => 0
|
|
|
|
/--
|
|
info: equations:
|
|
theorem Test2.nonrecfun.eq_1 : ∀ (x : Bool),
|
|
nonrecfun x =
|
|
match x with
|
|
| false => 0
|
|
| true => 0
|
|
-/
|
|
#guard_msgs in
|
|
#print equations nonrecfun
|
|
|
|
end Test2
|
|
|
|
namespace Test3
|
|
|
|
def nonrecfun : Bool → Nat
|
|
| false => 0
|
|
| true => 0
|
|
|
|
-- should have no effect
|
|
set_option backward.eqns.nonrecursive false
|
|
|
|
/--
|
|
info: equations:
|
|
theorem Test3.nonrecfun.eq_1 : nonrecfun false = 0
|
|
theorem Test3.nonrecfun.eq_2 : nonrecfun true = 0
|
|
-/
|
|
#guard_msgs in
|
|
#print equations nonrecfun
|
|
|
|
end Test3
|