Commit 2022-10-23 12:09 93bd8038

View on Github →

feat: port simps (#445) @[simps] mostly works. There are a few unimplemented features, but many basic cases will work correctly. See module doc for more information.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Mathport/Syntax.lean

Deleted Mathlib/Tactic/Simps.lean

Created Mathlib/Tactic/Simps/Basic.lean

added def Lean.Meta.mkSimpContext

added def Lean.Meta.mkSimpContextResult

added def Lean.Name.getString

added def Lean.Name.updateLast

added def ParsedProjectionData.toProjectionData

added structure ParsedProjectionData

added structure ProjectionData

added def Simps.Config.asFn

added def Simps.Config.lemmasOnly

added structure Simps.Config

added def String.isPrefixOf?

added def elabInitializeSimpsProjections

added def elabSimpsRule

added def getCompositeOfProjections

added def hasSimpAttribute

added def projectionsInfo

added def simpsAddProjection

added def simpsApplyProjectionRules

added def simpsFindAutomaticProjections

added def simpsFindCustomProjection

added def simpsGetProjectionExprs

added def simpsGetRawProjections

added def simpsResolveNotationClass

added def simpsTac

added def updateName

Created Mathlib/Tactic/Simps/NotationClass.lean

Modified Mathlib/Tactic/ToAdditive.lean

added def ToAdditive.addToAdditiveAttr

Modified test/Simps.lean

added structure AddHom

added def AddHomPlus.simps.apply

added def AddHomPlus2.simps.mul

added structure AddMonoidHom

added structure AlgHom

added structure ComplicatedEquivPlusData

added def CountNested.nested1

added def CountNested.nested2

added def DecoratedEquiv.simps.apply

added def DecoratedEquiv.simps.symm_apply

added def DecoratedEquiv.symm

added structure DecoratedEquiv

added def Equiv'.trans

added structure Equiv'

added structure EquivPlusData

added structure FaultyManualCoercion.Equiv

added def FaultyUniverses.Equiv.simps.invFun

added def FaultyUniverses.Equiv.symm

added structure FaultyUniverses.Equiv

added structure Foo1

added def Foo2.simps.elim

added structure Foo2

added def FurtherDecoratedEquiv.simps.apply

added def FurtherDecoratedEquiv.simps.symm_apply

added def FurtherDecoratedEquiv.symm

added structure FurtherDecoratedEquiv

added structure Left

added def ManualCoercion.Equiv.simps.invFun

added def ManualCoercion.Equiv.symm

added structure ManualCoercion.Equiv

added def ManualInitialize.Equiv.simps.invFun

added def ManualInitialize.Equiv.symm

added structure ManualInitialize.Equiv

added def ManualProjectionNames.Equiv.simps.symm_apply

added def ManualProjectionNames.Equiv.symm

added structure ManualProjectionNames.Equiv

added def ManualUniverses.Equiv.simps.invFun

added def ManualUniverses.Equiv.symm

added structure ManualUniverses.Equiv

added structure MyFunctor

added def MyProd.map

added structure MyProd

added structure MyType

added def Nat.SetPlus1

added def Nat.SetPlus2

added def Nat.SetPlus3

added structure NeedsPropClass

added def NestedNonFullyApplied.Equiv.symm2

added def NestedNonFullyApplied.Equiv.symm3

added def NestedNonFullyApplied.Equiv.symm

added structure NestedNonFullyApplied.Equiv

added def NewTop.simps.newElim

added structure NewTop

added def OneMore.simps.apply

added def OneMore.simps.symm_apply

added def OneMore.symm

added structure OneMore

added structure PartiallyAppliedStr

added def PrefixProjectionNames.Equiv.simps.symm_apply

added def PrefixProjectionNames.Equiv.symm

added structure PrefixProjectionNames.Equiv

added def PrefixProjectionNames.foo

added structure Right

added structure RingHom

added structure SetPlus

added structure Top

added structure VeryPartiallyAppliedStr

deleted structure X

added structure ZeroHom

added def another_term

added def bar

added def baz

added structure coercing.BSemigroup

added structure coercing.Equiv2

added structure coercing.FooStr

added structure coercing.VooStr

added def coercing.bar

added def coercing.foo2

added def coercing.foo

added def coercing.new_bar

added def coercing.voo2

added def coercing.voo

added def fffoo2

added def fffoo

added def ffoo3

added def ffoo4

added def ffoo

added def foo.bar1

added def foo.foo

added def foo.rfl2

added def foo.rfl3

added def foo2

added def foo

added def let1

added def let2

added def let3

added def let4

added def myAlgHom

added def myNatEquiv

added def myRingHom

added def myTypeDef

added def my_equiv

added def partially_applied_term

added def pprodEquivProd2

added def rflWithData'

added def rflWithData

added def some_test1

added def specify.specify1

added def specify.specify2

added def specify.specify3

added def specify.specify4

added def succeed_without_simplification_possible

added def test

added def test_PropClass

added def test_sneaky

added def thing

added def very_partially_applied_term

deleted def x