Skip to content

Commit

Permalink
chore: adaptations for nightly-2024-05-09
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed May 9, 2024
1 parent 266f11a commit c8ba1f8
Show file tree
Hide file tree
Showing 15 changed files with 46 additions and 26 deletions.
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/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
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
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
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
leanprover/lean4:nightly-2024-05-09

0 comments on commit c8ba1f8

Please sign in to comment.