88b746dd48
This PR adjusts the results of `inferInstanceAs` and the `def` `deriving` handler to conform to recently strengthened restrictions on reducibility. This change ensures that when deriving or inferring an instance for a semireducible type definition, the definition's RHS is not leaked when the instance is reduced at lower than semireducible transparency. More specifically, given the "source type" and "target type" (the given and expected type for `inferInstanceAs`, the right-hand side and applied left-hand side of the `def` for `deriving`), we synthesize an instance for the source type and then unfold and rewrap its components (fields, nested instances) as necessary to make them compatible with the target type. The individual steps are represented by the following options, which all default to enabled and can be disabled to help with porting: - `backward.inferInstanceAs.wrap`: master switch for instance adjustment in both `inferInstanceAs` and the default `deriving` handler - `backward.inferInstanceAs.wrap.reuseSubInstances`: reuse existing instances for the target type for sub-instance fields to avoid non-defeq instance diamonds - `backward.inferInstanceAs.wrap.instances`: wrap non-reducible instances in auxiliary definitions - `backward.inferInstanceAs.wrap.data`: wrap data fields in auxiliary definitions (proof fields are always wrapped) This PR is an extension and rewrite of prior work in Mathlib: https://github.com/leanprover-community/mathlib4/pull/36420 Last(?) part of fix for #9077 🤖 Prepared with Claude Code # Breaking changes Proofs that relied on the prior "defeq abuse" of these instance or that depended on their specific structure may need adjustments. As `inferInstanceAs A` now needs to know the source and target types exactly before it can continue, it cannot be used anymore as a synonym for `(inferInstance : A)`, use the latter instead when source and target type are identical.
136 lines
4.1 KiB
Text
136 lines
4.1 KiB
Text
import Init.Data.Order.PackageFactories
|
||
|
||
set_option warn.classDefReducibility false
|
||
|
||
variable {α : Type u}
|
||
|
||
opaque X : Type := Unit
|
||
|
||
namespace X
|
||
|
||
#guard_msgs(error, drop warning) in
|
||
opaque instLE : LE X := sorry
|
||
attribute [scoped instance] instLE
|
||
|
||
#guard_msgs(error, drop warning) in
|
||
@[scoped instance] opaque instDecidableLE : DecidableLE X := sorry
|
||
|
||
#guard_msgs(error, drop warning) in
|
||
@[instance] opaque instTotal : Std.Total (α := X) (· ≤ ·) := sorry
|
||
|
||
#guard_msgs(error, drop warning) in
|
||
@[instance] opaque instAntisymm : Std.Antisymm (α := X) (· ≤ ·) := sorry
|
||
|
||
#guard_msgs(error, drop warning) in
|
||
@[instance] opaque instTrans : Trans (α := X) (· ≤ ·) (· ≤ ·) (· ≤ ·) := sorry
|
||
|
||
namespace LinearOrderPackage
|
||
|
||
scoped instance packageOfLE : Std.LinearOrderPackage X := .ofLE X
|
||
|
||
example : instLE = (inferInstance : Std.PreorderPackage X).toLE := rfl
|
||
example : Std.IsLinearOrder X := inferInstance
|
||
example : Std.LawfulOrderLT X := inferInstance
|
||
example : Std.LawfulOrderOrd X := inferInstance
|
||
example : Std.LawfulOrderMin X := inferInstance
|
||
example : Std.LawfulOrderMax X := inferInstance
|
||
example : Std.LawfulOrderLeftLeaningMin X := inferInstance
|
||
example : Std.LawfulOrderLeftLeaningMax X := inferInstance
|
||
|
||
end LinearOrderPackage
|
||
|
||
namespace LinearPreorderPackage
|
||
|
||
scoped instance packageOfLE : Std.LinearPreorderPackage X := .ofLE X
|
||
|
||
scoped instance instMin : Min X := .leftLeaningOfLE X
|
||
scoped instance instMax : Max X := .leftLeaningOfLE X
|
||
|
||
example : instLE = (inferInstance : Std.LinearPreorderPackage X).toLE := rfl
|
||
example : Std.IsLinearPreorder X := inferInstance
|
||
example : Std.LawfulOrderLT X := inferInstance
|
||
example : Std.LawfulOrderOrd X := inferInstance
|
||
example : Std.LawfulOrderMin X := inferInstance
|
||
example : Std.LawfulOrderMax X := inferInstance
|
||
example : Std.LawfulOrderLeftLeaningMin X := inferInstance
|
||
example : Std.LawfulOrderLeftLeaningMax X := inferInstance
|
||
|
||
end LinearPreorderPackage
|
||
|
||
end X
|
||
|
||
section
|
||
|
||
@[implicit_reducible] def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofLE X {
|
||
le := X.instLE
|
||
decidableLE := X.instDecidableLE }
|
||
|
||
end
|
||
|
||
section
|
||
|
||
attribute [local instance] X.LinearOrderPackage.packageOfLE
|
||
|
||
@[implicit_reducible] def packageWithoutSynthesizableInstances' : Std.LinearOrderPackage X := .ofLE X {
|
||
le := X.instLE
|
||
decidableLE := X.instDecidableLE
|
||
}
|
||
|
||
end
|
||
|
||
/--
|
||
error: could not synthesize default value for field 'lt_iff' of 'Std.Packages.PreorderOfLEArgs' using tactics
|
||
---
|
||
error: Failed to automatically prove that the `LE` and `LT` instances are compatible. Please ensure that a `LawfulOrderLT` instance can be synthesized or manually provide the field `lt_iff`.
|
||
α : Type u
|
||
inst✝² : LE α
|
||
inst✝¹ : DecidableLE α
|
||
inst✝ : LT α
|
||
this✝¹ : LE α := inferInstance
|
||
this✝ : LT α := inferInstance
|
||
⊢ ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a
|
||
-/
|
||
#guard_msgs in
|
||
@[implicit_reducible] def packageOfLEOfLT1 [LE α] [DecidableLE α] [LT α] : Std.PreorderPackage α := .ofLE α {
|
||
le_refl := sorry
|
||
le_trans := sorry }
|
||
|
||
@[implicit_reducible] def packageOfLEOfLT2 [LE α] [DecidableLE α] [LT α] (h : ∀ a b : α, a < b ↔ a ≤ b ∧ ¬ b ≤ a) :
|
||
Std.PreorderPackage α := .ofLE α {
|
||
lt_iff := h
|
||
le_refl := sorry
|
||
le_trans := sorry }
|
||
|
||
namespace OrdTests
|
||
|
||
section WithoutSynthesizableInstances
|
||
|
||
#guard_msgs(error, drop warning) in
|
||
opaque _root_.X.instOrd : Ord X := sorry
|
||
|
||
#guard_msgs(error, drop warning) in
|
||
opaque _root_.X.instTransOrd : haveI := X.instOrd; Std.TransOrd X := sorry
|
||
|
||
#guard_msgs(error, drop warning) in
|
||
opaque _root_.X.instLawfulEqOrd : haveI := X.instOrd; Std.LawfulEqOrd X := sorry
|
||
|
||
@[implicit_reducible] def packageWithoutSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X {
|
||
ord := X.instOrd
|
||
transOrd := X.instTransOrd
|
||
eq_of_compare := by
|
||
extract_lets
|
||
intro a b
|
||
letI := X.instOrd
|
||
exact X.instLawfulEqOrd.eq_of_compare }
|
||
|
||
end WithoutSynthesizableInstances
|
||
|
||
section WithSynthesizableInstances
|
||
|
||
attribute [scoped instance] X.instOrd X.instTransOrd X.instLawfulEqOrd
|
||
|
||
@[implicit_reducible] def packageWithSynthesizableInstances : Std.LinearOrderPackage X := .ofOrd X
|
||
|
||
end WithSynthesizableInstances
|
||
|
||
end OrdTests
|