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.
122 lines
2.7 KiB
Text
122 lines
2.7 KiB
Text
module
|
|
|
|
prelude
|
|
import all Module.Basic
|
|
|
|
/-! `import all` should import private information, privately. -/
|
|
|
|
/--
|
|
info: theorem t : f = 1 :=
|
|
sorry
|
|
-/
|
|
#guard_msgs in
|
|
#print t
|
|
|
|
/--
|
|
error: type mismatch
|
|
y
|
|
has type
|
|
Vector Unit 1 : Type
|
|
but is expected to have type
|
|
Vector Unit f : Type
|
|
-/
|
|
#guard_msgs in
|
|
theorem v (x : Vector Unit f) (y : Vector Unit 1) : x = y := sorry
|
|
|
|
|
|
|
|
/-- info: f.eq_def : f = 1 -/
|
|
#guard_msgs in
|
|
#check f.eq_def
|
|
|
|
/-- info: f.eq_unfold : f = 1 -/
|
|
#guard_msgs in
|
|
#check f.eq_unfold
|
|
|
|
/-- info: f_struct.eq_1 : f_struct 0 = 0 -/
|
|
#guard_msgs in
|
|
#check f_struct.eq_1
|
|
|
|
/--
|
|
info: f_struct.eq_def (x✝ : Nat) :
|
|
f_struct x✝ =
|
|
match x✝ with
|
|
| 0 => 0
|
|
| n.succ => f_struct n
|
|
-/
|
|
#guard_msgs in
|
|
#check f_struct.eq_def
|
|
|
|
/--
|
|
info: f_struct.eq_unfold :
|
|
f_struct = fun x =>
|
|
match x with
|
|
| 0 => 0
|
|
| n.succ => f_struct n
|
|
-/
|
|
#guard_msgs in
|
|
#check f_struct.eq_unfold
|
|
|
|
/-- info: f_wfrec.eq_1 (x✝ : Nat) : f_wfrec 0 x✝ = x✝ -/
|
|
#guard_msgs(pass trace, all) in
|
|
#check f_wfrec.eq_1
|
|
|
|
/--
|
|
info: f_wfrec.eq_def (x✝ x✝¹ : Nat) :
|
|
f_wfrec x✝ x✝¹ =
|
|
match x✝, x✝¹ with
|
|
| 0, acc => acc
|
|
| n.succ, acc => f_wfrec n (acc + 1)
|
|
-/
|
|
#guard_msgs(pass trace, all) in
|
|
#check f_wfrec.eq_def
|
|
|
|
/--
|
|
info: f_wfrec.eq_unfold :
|
|
f_wfrec = fun x x_1 =>
|
|
match x, x_1 with
|
|
| 0, acc => acc
|
|
| n.succ, acc => f_wfrec n (acc + 1)
|
|
-/
|
|
#guard_msgs(pass trace, all) in
|
|
#check f_wfrec.eq_unfold
|
|
|
|
/--
|
|
info: f_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc)
|
|
(case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_wfrec n (acc + 1)) → motive n.succ acc (f_wfrec n (acc + 1)))
|
|
(a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_wfrec a✝ a✝¹)
|
|
-/
|
|
#guard_msgs(pass trace, all) in
|
|
#check f_wfrec.induct_unfolding
|
|
|
|
/-- info: f_exp_wfrec.eq_1 (x✝ : Nat) : f_exp_wfrec 0 x✝ = x✝ -/
|
|
#guard_msgs in
|
|
#check f_exp_wfrec.eq_1
|
|
|
|
/--
|
|
info: f_exp_wfrec.eq_def (x✝ x✝¹ : Nat) :
|
|
f_exp_wfrec x✝ x✝¹ =
|
|
match x✝, x✝¹ with
|
|
| 0, acc => acc
|
|
| n.succ, acc => f_exp_wfrec n (acc + 1)
|
|
-/
|
|
#guard_msgs in
|
|
#check f_exp_wfrec.eq_def
|
|
|
|
/--
|
|
info: f_exp_wfrec.eq_unfold :
|
|
f_exp_wfrec = fun x x_1 =>
|
|
match x, x_1 with
|
|
| 0, acc => acc
|
|
| n.succ, acc => f_exp_wfrec n (acc + 1)
|
|
-/
|
|
#guard_msgs in
|
|
#check f_exp_wfrec.eq_unfold
|
|
|
|
/--
|
|
info: f_exp_wfrec.induct_unfolding (motive : Nat → Nat → Nat → Prop) (case1 : ∀ (acc : Nat), motive 0 acc acc)
|
|
(case2 : ∀ (n acc : Nat), motive n (acc + 1) (f_exp_wfrec n (acc + 1)) → motive n.succ acc (f_exp_wfrec n (acc + 1)))
|
|
(a✝ a✝¹ : Nat) : motive a✝ a✝¹ (f_exp_wfrec a✝ a✝¹)
|
|
-/
|
|
#guard_msgs(pass trace, all) in
|
|
#check f_exp_wfrec.induct_unfolding
|