Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

tc speed test #12810

Closed
wants to merge 11 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions Mathlib/Algebra/Group/MinimalAxioms.lean
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ def Group.ofLeftAxioms {G : Type u} [Mul G] [Inv G] [One G]
one_mul := one_mul,
mul_left_inv := mul_left_inv,
mul_one := fun a => by
have mul_right_inv : ∀ a, a * a⁻¹ = 1 := fun a =>
have mul_right_inv : ∀ a : G, a * a⁻¹ = 1 := fun a =>
calc a * a⁻¹ = 1 * (a * a⁻¹) := (one_mul _).symm
_ = ((a * a⁻¹)⁻¹ * (a * a⁻¹)) * (a * a⁻¹) := by
rw [mul_left_inv]
Expand All @@ -63,7 +63,7 @@ def Group.ofRightAxioms {G : Type u} [Mul G] [Inv G] [One G]
(assoc : ∀ a b c : G, (a * b) * c = a * (b * c))
(mul_one : ∀ a : G, a * 1 = a)
(mul_right_inv : ∀ a : G, a * a⁻¹ = 1) : Group G :=
have mul_left_inv : ∀ a, a⁻¹ * a = 1 := fun a =>
have mul_left_inv : ∀ a : G, a⁻¹ * a = 1 := fun a =>
calc a⁻¹ * a = (a⁻¹ * a) * 1 := (mul_one _).symm
_ = (a⁻¹ * a) * ((a⁻¹ * a) * (a⁻¹ * a)⁻¹) := by
rw [mul_right_inv]
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Order/Module/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,9 +3,9 @@ Copyright (c) 2023 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies
-/
import Mathlib.Algebra.Module.Basic
import Mathlib.Algebra.Order.Module.Synonym
import Mathlib.Algebra.Order.Ring.Lemmas
import Mathlib.GroupTheory.GroupAction.Group
import Mathlib.Tactic.Positivity.Core

/-!
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/CategoryTheory/Comma/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -239,7 +239,7 @@ instance full_map [F.Faithful] [F₁.Full] [F₂.Full] [IsIso α] [IsIso β] : (
assoc, assoc]
erw [← α.naturality_assoc, β.naturality]
dsimp
rw [F₁.image_preimage, F₂.image_preimage]
rw [F₁.map_preimage, F₂.map_preimage]
simpa using φ.w) }, by aesop_cat⟩

instance essSurj_map [F₁.EssSurj] [F₂.EssSurj] [F.Full] [IsIso α] [IsIso β] :
Expand Down
1 change: 1 addition & 0 deletions Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -666,6 +666,7 @@ theorem rightUnitor_monoidal (X₁ X₂ : C) :
coherence
#align category_theory.right_unitor_monoidal CategoryTheory.rightUnitor_monoidal

set_option maxHeartbeats 400000 in
theorem associator_monoidal (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
tensor_μ C (X₁ ⊗ X₂, X₃) (Y₁ ⊗ Y₂, Y₃) ≫
(tensor_μ C (X₁, X₂) (Y₁, Y₂) ▷ (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Lean/Elab/Term.lean
Original file line number Diff line number Diff line change
Expand Up @@ -19,5 +19,5 @@ def elabPattern (patt : Term) (expectedType? : Option Expr) : TermElabM Expr :=
withTheReader Term.Context ({ · with ignoreTCFailures := true, errToSorry := false }) <|
withSynthesizeLight do
let t ← elabTerm patt expectedType?
synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
instantiateMVars t
1 change: 1 addition & 0 deletions Mathlib/LinearAlgebra/FreeModule/Norm.lean
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ instance (b : Basis ι F[X] S) {I : Ideal S} (hI : I ≠ ⊥) (i : ι) :
refine AdjoinRoot.powerBasis ?_
exact I.smithCoeffs_ne_zero b hI i

set_option synthInstance.maxHeartbeats 40000 in
/-- For a nonzero element `f` in a `F[X]`-module `S`, the dimension of $S/\langle f \rangle$ as an
`F`-vector space is the degree of the norm of `f` relative to `F[X]`. -/
theorem finrank_quotient_span_eq_natDegree_norm [Algebra F S] [IsScalarTower F F[X] S]
Expand Down
1 change: 0 additions & 1 deletion Mathlib/LinearAlgebra/Semisimple.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ Copyright (c) 2024 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import Mathlib.RingTheory.DedekindDomain.Basic
import Mathlib.FieldTheory.Perfect
import Mathlib.LinearAlgebra.Basis.VectorSpace
import Mathlib.LinearAlgebra.AnnihilatingPolynomial
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
Original file line number Diff line number Diff line change
Expand Up @@ -102,8 +102,8 @@ theorem discr_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : F
replace H := congr_arg (Algebra.norm K) H
have hnorm : (norm K) (ζ ^ (p : ℕ) ^ k - 1) = (p : K) ^ (p : ℕ) ^ k := by
by_cases hp : p = 2
· exact mod_cast hζ.pow_sub_one_norm_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
· exact mod_cast hζ.pow_sub_one_norm_prime_ne_two hirr le_rfl hp
· exact mod_cast hζ.norm_pow_sub_one_eq_prime_pow_of_ne_zero hirr le_rfl (hp2 hp)
· exact mod_cast hζ.norm_pow_sub_one_of_prime_ne_two hirr le_rfl hp
rw [MonoidHom.map_mul, hnorm, MonoidHom.map_mul, ← map_natCast (algebraMap K L),
Algebra.norm_algebraMap, finrank L hirr] at H
conv_rhs at H => -- Porting note: need to drill down to successfully rewrite the totient
Expand Down
1 change: 0 additions & 1 deletion Mathlib/RingTheory/PowerSeries/Inverse.lean
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Kenny Lau
-/

import Mathlib.RingTheory.DedekindDomain.Basic
import Mathlib.RingTheory.DiscreteValuationRing.Basic
import Mathlib.RingTheory.MvPowerSeries.Inverse
import Mathlib.RingTheory.PowerSeries.Basic
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Convert.lean
Original file line number Diff line number Diff line change
Expand Up @@ -111,7 +111,7 @@ elab_rules : tactic
withTheReader Term.Context (fun ctx => { ctx with ignoreTCFailures := true }) do
let t ← elabTermEnsuringType (mayPostpone := true) term expectedType
-- Process everything so that tactics get run, but again allow TC failures
Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
-- Use a type hint to ensure we collect goals from the type too
mkExpectedTypeHint t (← inferType t)
liftMetaTactic fun g ↦
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/FBinop.lean
Original file line number Diff line number Diff line change
Expand Up @@ -48,7 +48,7 @@ private inductive Tree where

private partial def toTree (s : Syntax) : TermElabM Tree := do
let result ← go s
synthesizeSyntheticMVars (mayPostpone := true)
synthesizeSyntheticMVars (postpone := .yes)
return result
where
go (s : Syntax) : TermElabM Tree := do
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/Tactic/Find.lean
Original file line number Diff line number Diff line change
Expand Up @@ -99,7 +99,7 @@ lemmas which are `apply`able against the current goal.
elab "#find " t:term : command =>
liftTermElabM do
let t ← Term.elabTerm t none
Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
findType t

/- (Note that you'll get an error trying to run these here:
Expand Down Expand Up @@ -132,5 +132,5 @@ See also the `find` tactic to search for theorems matching the current goal.
-/
elab "#find " t:term : tactic => do
let t ← Term.elabTerm t none
Term.synthesizeSyntheticMVars (mayPostpone := false) (ignoreStuckTC := true)
Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
findType t
2 changes: 1 addition & 1 deletion Mathlib/Tactic/FunProp/Decl.lean
Original file line number Diff line number Diff line change
Expand Up @@ -132,7 +132,7 @@ def tacticToDischarge (tacticCode : TSyntax `tactic) : Expr → MetaM (Option Ex
instantiateMVarDeclMVars mvar.mvarId!

let _ ←
withSynthesize (mayPostpone := false) do
withSynthesize (postpone := .no) do
Tactic.run mvar.mvarId! (Tactic.evalTactic tacticCode *> Tactic.pruneSolvedGoals)

let result ← instantiateMVars mvar
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Have.lean
Original file line number Diff line number Diff line change
Expand Up @@ -72,7 +72,7 @@ def haveLetCore (goal : MVarId) (name : TSyntax ``optBinderIdent)
| none => mkFreshTypeMVar
| some stx => withRef stx do
let e ← Term.elabType stx
Term.synthesizeSyntheticMVars false
Term.synthesizeSyntheticMVars (postpone := .no)
instantiateMVars e
let p ← mkFreshExprMVar t MetavarKind.syntheticOpaque n
pure (p.mvarId!, ← mkForallFVars es t, ← mkLambdaFVars es p)
Expand Down
24 changes: 22 additions & 2 deletions Mathlib/Tactic/NormNum/Pow.lean
Original file line number Diff line number Diff line change
Expand Up @@ -226,40 +226,60 @@ theorem isRat_zpow_neg {α : Type*} [DivisionRing α] {a : α} {b : ℤ} {nb :
IsRat (a^b) num den := by
rwa [pb.out, Int.cast_negOfNat, zpow_neg, zpow_natCast]

#adaptation_note
/--
Prior to https://github.com/leanprover/lean4/pull/4096,
the repeated
```
have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
h.check
```
blocks below were not necessary: we just did it once outside the `match rb with` block.
-/
/-- The `norm_num` extension which identifies expressions of the form `a ^ b`,
such that `norm_num` successfully recognises both `a` and `b`, with `b : ℤ`. -/
@[norm_num (_ : α) ^ (_ : ℤ)]
def evalZPow : NormNumExt where eval {u α} e := do
let .app (.app (f : Q($α → ℤ → $α)) (a : Q($α))) (b : Q(ℤ)) ← whnfR e | failure
let _c ← synthInstanceQ q(DivisionSemiring $α)
let rb ← derive (α := q(ℤ)) b
have h : $e =Q $a ^ $b := ⟨⟩
h.check
match rb with
| .isBool .. | .isRat _ .. => failure
| .isNat sβ nb pb =>
match ← derive q($a ^ $nb) with
| .isBool .. => failure
| .isNat sα' ne' pe' =>
have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
h.check
assumeInstancesCommute
return .isNat sα' ne' q(isNat_zpow_pos $pb $pe')
| .isNegNat sα' ne' pe' =>
have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
h.check
let _c ← synthInstanceQ q(DivisionRing $α)
assumeInstancesCommute
return .isNegNat sα' ne' q(isInt_zpow_pos $pb $pe')
| .isRat sα' qe' nume' dene' pe' =>
have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
h.check
assumeInstancesCommute
return .isRat sα' qe' nume' dene' q(isRat_zpow_pos $pb $pe')
| .isNegNat sβ nb pb =>
match ← derive q(($a ^ $nb)⁻¹) with
| .isBool .. => failure
| .isNat sα' ne' pe' =>
have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
h.check
assumeInstancesCommute
return .isNat sα' ne' q(isNat_zpow_neg $pb $pe')
| .isNegNat sα' ne' pe' =>
have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
h.check
let _c ← synthInstanceQ q(DivisionRing $α)
assumeInstancesCommute
return .isNegNat sα' ne' q(isInt_zpow_neg $pb $pe')
| .isRat sα' qe' nume' dene' pe' =>
have h : $e =Q (HPow.hPow (γ := $α) $a $b) := ⟨⟩
h.check
assumeInstancesCommute
return .isRat sα' qe' nume' dene' q(isRat_zpow_neg $pb $pe')
4 changes: 2 additions & 2 deletions Mathlib/Tactic/TermCongr.lean
Original file line number Diff line number Diff line change
Expand Up @@ -621,7 +621,7 @@ def elabTermCongr : Term.TermElab := fun stx expectedType? => do
unless ← isDefEq expRhs rhs do
throwError "Right-hand side of elaborated pattern{indentD rhs}\n\
is not definitionally equal to right-hand side of expected type{indentD expectedType}"
Term.synthesizeSyntheticMVars (mayPostpone := true)
Term.synthesizeSyntheticMVars (postpone := .yes)
let res ← mkCongrOf 0 mvarCounterSaved lhs rhs
let expectedType' ← whnf expectedType
let pf ← if expectedType'.iff?.isSome then res.iff
Expand All @@ -632,7 +632,7 @@ def elabTermCongr : Term.TermElab := fun stx expectedType? => do
-- Case 2: No expected type or it's not obviously Iff/Eq/HEq. We generate an Eq.
let lhs ← elaboratePattern t none true
let rhs ← elaboratePattern t none false
Term.synthesizeSyntheticMVars (mayPostpone := true)
Term.synthesizeSyntheticMVars (postpone := .yes)
let res ← mkCongrOf 0 mvarCounterSaved lhs rhs
let pf ← res.eq
let ty ← mkEq res.lhs res.rhs
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/Variable.lean
Original file line number Diff line number Diff line change
Expand Up @@ -127,7 +127,7 @@ partial def getSubproblem
withTheReader Term.Context (fun ctx => {ctx with ignoreTCFailures := true}) do
Term.withAutoBoundImplicit do
_ ← Term.elabType ty
Term.synthesizeSyntheticMVars (mayPostpone := true) (ignoreStuckTC := true)
Term.synthesizeSyntheticMVars (postpone := .yes) (ignoreStuckTC := true)
let fvarIds := (← getLCtx).getFVarIds
if let some mvarId ← pendingActionableSynthMVar binder then
trace[«variable?»] "Actionable mvar:{mvarId}"
Expand Down
12 changes: 6 additions & 6 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
[{"url": "https://github.com/leanprover-community/batteries",
"type": "git",
"subDir": null,
"rev": "91d3fcfdc2e9e815954a542442b9ccf59e43e968",
"rev": "022321f7e18dc982db80f941f6784e92cb4766ff",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
Expand All @@ -13,19 +13,19 @@
{"url": "https://github.com/leanprover-community/quote4",
"type": "git",
"subDir": null,
"rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
"rev": "44f57616b0d9b8f9e5606f2c58d01df54840eba7",
"name": "Qq",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inputRev": "nightly-testing",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/aesop",
"type": "git",
"subDir": null,
"rev": "2225b0e4a3528da20499e2304b521e0c4c2a4563",
"rev": "f1bfa6ae737248969c360a3715a5c05df0eea55b",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "master",
"inputRev": "nightly-testing",
"inherited": false,
"configFile": "lakefile.toml"},
{"url": "https://github.com/leanprover-community/ProofWidgets4",
Expand All @@ -49,7 +49,7 @@
{"url": "https://github.com/leanprover-community/import-graph.git",
"type": "git",
"subDir": null,
"rev": "c46d22bbe4f8363c0829ce0eb48a95012cdc0d79",
"rev": "e9fb4ecc5d718eb36faae5308880cd3f243788df",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down
4 changes: 2 additions & 2 deletions lakefile.lean
Original file line number Diff line number Diff line change
Expand Up @@ -22,8 +22,8 @@ meta if get_config? doc = some "on" then -- do not download and build doc-gen4 b
require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "main"

require batteries from git "https://github.com/leanprover-community/batteries" @ "nightly-testing"
require Qq from git "https://github.com/leanprover-community/quote4" @ "master"
require aesop from git "https://github.com/leanprover-community/aesop" @ "master"
require Qq from git "https://github.com/leanprover-community/quote4" @ "nightly-testing"
require aesop from git "https://github.com/leanprover-community/aesop" @ "nightly-testing"
require proofwidgets from git "https://github.com/leanprover-community/ProofWidgets4" @ "v0.0.36"
require Cli from git "https://github.com/leanprover/lean4-cli" @ "main"
require importGraph from git "https://github.com/leanprover-community/import-graph.git" @ "main"
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:nightly-2024-05-07
negiizhao/lean4:meow-synthinstance6
Loading