08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
39 lines
1.7 KiB
Text
39 lines
1.7 KiB
Text
structure BundledFunction (α β : Sort _) :=
|
||
(toFun : α → β)
|
||
|
||
namespace BundledFunction
|
||
|
||
-- `simp` doesn't seem to unify partial applications of structure projections:
|
||
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.60.20failing.20on.20partial.20application.20of.20projections
|
||
def id (α) : BundledFunction α α := ⟨λ a => a⟩
|
||
|
||
@[simp] theorem coe_id : (id α).toFun = _root_.id := rfl
|
||
|
||
example (x : α) : (id α).toFun x = x :=
|
||
by simp only [coe_id, id_eq] -- should succeed
|
||
example (x : α) : (id α).toFun x = x :=
|
||
by rw [coe_id, id_eq] -- succeeds
|
||
|
||
-- seems to be another instance of the same behaviour:
|
||
-- https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.60simp.60.20calls.20broken.20in.20mathlib4.23922/near/314790371
|
||
|
||
def otherProjection (f : BundledFunction α β) : α → β := f.toFun
|
||
|
||
-- Projections functions are expanded when populating the discrimination tree, and are indexed as `Expr.proj` objects.
|
||
-- `@toFun α β` cannot be expanded into `Expr.proj` since there is a missing argument. The workaround is to add the missing argument.
|
||
-- Then, we get `a.1 = otherProjection a`
|
||
@[simp] theorem toFun_eq_otherProjection : @toFun α β a = otherProjection a := rfl
|
||
@[simp] theorem id_apply : (id α).otherProjection x = x := rfl
|
||
|
||
example : (id α).toFun x = x := by simp only [toFun_eq_otherProjection, id_apply]; done -- should work
|
||
example : (id α).toFun x = x := by rw [toFun_eq_otherProjection, id_apply] -- succeeds
|
||
|
||
end BundledFunction
|
||
|
||
-- `simp` is happy with partial applications in other functions:
|
||
def id2 (x : α) := x
|
||
|
||
@[simp] theorem id2_eq_id : @id2 α = id := rfl
|
||
|
||
example : id2 x = x := by simp only [id2_eq_id, id_eq] -- works fine
|
||
example : id2 x = x := by rw [id2_eq_id, id_eq] -- succeeds
|