Per @digama0 's suggestion here, we should create a class for antidiagonals on types.

The docs for cc, conv, simp are in the doc_commands.lean file in Mathlib 3 (documentation, code).
I think we'll want to migrate these docstrings & add_tactic_doc commands closer to the actual tactic implementations in Mathlib 4?

norm_num needs to support

• <, >, ≠
• Ring operations: Neg, Sub, %
• Field operations: /, ⁻¹
• Reals and rationals

Consider this example:

example : ∃ (x : Nat), x = 0 := by

If you don't import Mathlib, the goal is listed as ∃ x, x = 0. If you import Mathlib, the goal is listed as Exists fun x ↦ x = 0. It appears that it is the introduction of ↦ that is causing the problem. The unexpander for Exists isn't expecting that symbol, so it's not working.

There are other unexpanders that also expect => rather than ↦, so I suspect that they also have the same problem, although I haven't tested them. The ones I found are unexpandSigma, unexpandPSigma, and unexpandSubtype.

In Lean 3, we had:

import tactic.split_ifs
import tactic.localized

open_locale classical

example (P Q : Prop) (w : if P then (if Q then true else true) else true = true) : true :=
begin
  split_ifs at w,
  -- 3 goals, no `if`s in `w`
  all_goals { trivial, }
end

while currently in mathlib4 we have:

import Mathlib.Tactic.SplitIfs

open Classical

example (P Q : Prop) (w : if P then (if Q then true else true) else true = true) : true := by
  split_ifs at w
  -- two goals here, and in the first `w : if Q then true else true`

This first came up in porting Logic.Embedding.Basic.

In the example

  example : ∃! n, n = 0 := by

the tactic state shows the goal as ExistsUnique fun n => n = 0.

This isn't wrong, but it should be changed so that it displays as ∃! n, n = 0.

We've recently changed classical in mathlib to so that it no longer overrides the existing decidable instances. mathlib4 should be adapterd. leanprover-community/mathlib#14122

import Mathlib.Tactic.Basic

example : (by classical; exact decide (0 = 1) : Bool) = decide (0 = 1) := rfl -- this should work

If you are accepting external contributions, it will save you headaches later if you nail down the license ASAP.
Otherwise, you could get into an awkward situation where you need to chase down all contributors
to ask their permission about various ways you might want to use the code.

Simplest would be to copy the Apache license from mathlib.

Right now, to_additive is generating additive declarations which do not inherit other attributes attached to the multiplicative declaration. This is an issue because not all mathlib4 porters are aware of this, so right now some stuff is being incorrectly ported.

Here are examples:

1. simp

import Mathlib.Tactic.ToAdditive
import Mathlib.Init.ZeroOne

-- to_additive doesn't attach `simp`
@[simp, to_additive]
theorem One.foo [One α] [Mul α] (a : α) : (1 : α) * a = 1 := sorry

example [One α] [Mul α] (a : α) : (1 : α) * a = 1 := by simp

#check @Zero.foo -- exists

example [Zero α] [Add α] : (0 : α) + a = 0 := by simp -- fails (note: zero_add doesn't fire because it's not imported)

2. simps (note that the docs currently claim that this works, but it doesn't seem to?)

import Mathlib.Algebra.Hom.Group

-- `simps` doesn't run on additivised declaration
@[to_additive, simps]
def OneHom.id' (M : Type _) [One M] : OneHom M M where
  toFun x := x
  map_one' := rfl

#check OneHom.id'_apply -- exists
#check ZeroHom.id' -- exists
#check ZeroHom.id'_apply -- doesn't exist

3. ext

import Mathlib.Algebra.Group.Units

@[ext, to_additive]
theorem Units.ext' [Monoid α] : Function.Injective (fun (u : αˣ) => (u : α))
  | ⟨v, i₁, vi₁, iv₁⟩, ⟨v', i₂, vi₂, iv₂⟩, e => by
    simp only at e; subst v'; congr;
    simpa only [iv₂, vi₁, one_mul, mul_one] using mul_assoc i₂ v i₁

example [Monoid α] (a b : αˣ) : a = b := by
  ext -- does something
  sorry

example [AddMonoid α] (a b : AddUnits α) : a = b := by
  ext -- fails

Other attributes currently used with to_additive in Mathlib are norm_cast, coe, symm and trans. I'm not sure which ones currently interact in the optimal way.

I don't have time to debug now but I just bisected what looks like a pretty bad performance regression in ring, coming from 085e7ab it seems.

According to the following

import Mathlib.Tactic.Ring

set_option profiler true
set_option maxHeartbeats 700000 in
lemma a [CommRing R] (a1 a2 a3 a4 a6 : R) (P : R × R) :
  -(a1 ^ 4 * a2 * a3 ^ 2 - a1 ^ 5 * a3 * a4 + a1 ^ 6 * a6 + 8 * a1 ^ 2 * a2 ^ 2 * a3 ^ 2
  - a1 ^ 3 * a3 ^ 3 - 8 * a1 ^ 3 * a2 * a3 * a4 - a1 ^ 4 * a4 ^ 2 + 12 * a1 ^ 4 * a2 * a6
  + 16 * a2 ^ 3 * a3 ^ 2 - 36 * a1 * a2 * a3 ^ 3 - 16 * a1 * a2 ^ 2 * a3 * a4
  + 30 * a1 ^ 2 * a3 ^ 2 * a4 - 8 * a1 ^ 2 * a2 * a4 ^ 2 + 48 * a1 ^ 2 * a2 ^ 2 * a6
  - 36 * a1 ^ 3 * a3 * a6 + 27 * a3 ^ 4 - 72 * a2 * a3 ^ 2 * a4 - 16 * a2 ^ 2 * a4 ^ 2
  + 96 * a1 * a3 * a4 ^ 2 + 64 * a2 ^ 3 * a6 - 144 * a1 * a2 * a3 * a6 - 72 * a1 ^ 2 * a4 * a6
  + 64 * a4 ^ 3 + 216 * a3 ^ 2 * a6 - 288 * a2 * a4 * a6 + 432 * a6 ^ 2) =
  -((48 * P.fst * P.snd * a2 ^ 2 + 24 * a1 * a2 * a6 + 216 * P.snd * a6 + P.snd * a1 ^ 6 +
  11 * P.snd * a1 ^ 4 * a2 + P.fst * a1 ^ 4 * a3 + 38 * P.fst * a1 ^ 2 * a2 * a3
  + 8 * a1 ^ 2 * a2 ^ 2 * a3 + a1 ^ 4 * a2 * a3 + 40 * P.snd * a1 ^ 2 * a2 ^ 2
  + 32 * P.snd * a2 ^ 3 + 24 * P.fst * P.snd * a1 * a3 + 30 * P.fst ^ 2 * a2 * a3
  + 3 * P.fst * a1 ^ 3 * a4 + 60 * P.fst ^ 2 * a1 * a4 + 30 * P.fst ^ 2 * a1 ^ 2 * a3
  + 31 * a1 ^ 2 * a3 * a4 + 144 * P.snd ^ 2 * a3 + 198 * P.snd * a3 ^ 2 + 27 * a3 ^ 3
  + 60 * a1 * a4 ^ 2 + 36 * P.fst * a1 * a6 + 76 * P.fst * a2 ^ 2 * a3
  + 16 * a2 ^ 3 * a3 + 84 * P.fst * a1 * a2 * a4 - (36 * a3 * a6 + P.fst ^ 2 * a1 ^ 5
  + P.fst * a1 ^ 5 * a2 + P.fst * P.snd * a1 ^ 4
  + 9 * P.fst ^ 2 * a1 ^ 3 * a2 + 10 * P.fst * a1 ^ 3 * a2 ^ 2 + a1 ^ 5 * a4
  + 6 * P.snd ^ 2 * a1 ^ 3 + 8 * P.fst * P.snd * a1 ^ 2 * a2 + 24 * P.fst ^ 2 * a1 * a2 ^ 2
  + 32 * P.fst * a1 * a2 ^ 3 + 35 * P.snd * a1 ^ 3 * a3 + a1 ^ 3 * a3 ^ 2 + 9 * a1 ^ 3 * a2 * a4
  + 48 * P.snd ^ 2 * a1 * a2 + 134 * P.snd * a1 * a2 * a3 + 27 * P.fst * a1 * a3 ^ 2
  + 36 * a1 * a2 * a3 ^ 2 + 58 * P.snd * a1 ^ 2 * a4 + 24 * a1 * a2 ^ 2 * a4
  + 144 * P.fst * P.snd * a4 + 120 * P.snd * a2 * a4 + 168 * P.fst * a3 * a4
  + 34 * a2 * a3 * a4)) * (2 * P.snd + a1 * P.fst + a3) + (a1 ^ 2 * a3 ^ 2 + 12 * a1 ^ 2 * a6
  + 16 * a2 ^ 2 * a4 + 32 * P.fst * a2 ^ 3 + a1 ^ 4 * a4 + 144 * P.fst * a6 + 48 * a2 * a6
  + P.fst * a1 ^ 4 * a2 + 84 * P.fst * a3 ^ 2 + 56 * P.snd * a1 * a4 + 8 * a1 ^ 2 * a2 * a4
  + 28 * P.snd * a1 ^ 2 * a3 + 52 * P.snd * a2 * a3 + 96 * P.fst * P.snd * a3
  + 8 * P.fst * a1 ^ 2 * a2 ^ 2 + 38 * a2 * a3 ^ 2 + 32 * P.fst ^ 2 * a2 ^ 2
  - (2 * P.fst * a1 ^ 3 * a3 + 112 * P.fst * a2 * a4 + a1 ^ 3 * a2 * a3 + 36 * a1 * a3 * a4
  + 96 * P.fst ^ 2 * a4 + 32 * P.fst * P.snd * a1 * a2 + 32 * P.snd * a1 * a2 ^ 2 + 64 * a4 ^ 2
  + 4 * P.fst * P.snd * a1 ^ 3 + 10 * P.snd * a1 ^ 3 * a2 + P.snd * a1 ^ 5 + 8 * a1 * a2 ^ 2 * a3
  + 46 * P.fst * a1 * a2 * a3)) * (a1 * P.snd - (3 * P.fst ^ 2 + 2 * a2 * P.fst + a4))
  + (60 * a1 ^ 2 * a4 + 288 * P.fst * a4 + 240 * a2 * a4 + 12 * P.snd * a1 ^ 3
  + 36 * a1 ^ 3 * a3 + 96 * P.snd * a1 * a2 + 168 * a1 * a2 * a3 - (432 * a6 + a1 ^ 6
  + 288 * P.snd * a3 + 252 * a3 ^ 2 + 12 * a1 ^ 4 * a2 + 48 * a1 ^ 2 * a2 ^ 2 + 96 * P.fst * a2 ^ 2
  + 64 * a2 ^ 3)) * (P.snd ^ 2 + a1 * P.fst * P.snd + a3 * P.snd - (P.fst ^ 3 + a2 * P.fst ^ 2
  + a4 * P.fst + a6)))
:= by ring

the runtime of ring jumps from 2-3s to 18-40s on my machine, from d419b09 to 085e7ab.

@digama0 any ideas, both the ring and norm_num internals were affected by this commit, but I can't see a smoking gun.

Example:

def Bool_eq_iff
  {A B: Bool}
  : (A = B) = (A ↔ B)
  := by (cases A <;> cases B <;> simp)

def Bool_eq_iff2
  {A B: Bool}
  : (A = B) = (A ↔ B)
  := by library_search -- 𝔗𝔯𝔶 𝔱𝔥𝔦𝔰: exact sorryAx ((A = B) = (A = true ↔ B = true)) 

I would expect it to find the theorem Bool_eq_iff that solves the goal without sorry.

A simple fix is to add the following line to isBlackListed:

  if declName matches Name.str _ "sorryAx" _ then return true

E.g. in this slightly silly example, rather than writing

def a (t : Nat) (h : t < 7) : Nat :=
  if t = 0 then 0 else
  let b : Nat := t - 1
  (a b (by rw [(show b = t - 1 by rfl)]; sorry)) + 1

I'd like to be able to write

def a (t : Nat) (h : t < 7) : Nat :=
  if t = 0 then 0 else
  set b : Nat := t - 1 with h
  (a b (by rw [h]; sorry)) + 1

MWE:

import Mathlib.Tactic.Ring

def sum : Nat → Nat
  | 0     => 0
  | n + 1 => n + 1 + sum n

theorem mulDist {a b c : Nat} : a * (b + c) = a * b + a * c := by ring

theorem twoTimesSumEqTimesSucc {n : Nat} : 2 * sum n = n * (n + 1) := by
  induction n with
    | zero => rfl
    | succ n hi =>
      simp only [sum]
      iterate rw [mulDist]
      rw [hi]
      ring -- unknown free variable '_uniq.1942'

After some quick debugging, I noticed that the problem happens on this call.

The ∉ precedence was wrong: leanprover-community/mathlib3port@d3886c2#r67303397

Other notation probably have the wrong precedence as well.

In mathlib3 we wrote:

mk_simp_attribute monad_norm none with functor_norm

but register_simp_attr does not support a with clause.

This issue parallels the content of Mathlib/Mathport/Syntax.lean, tracking the remaining work to port mathlib3 tactics to mathlib4, but also contains "ephemeral" information that does not belong in that file.

Primarily, this issue contains a list of tactics (or groups of tactics), along with any relevant information about work-in-progress (e.g. people who've "claimed" a tactic, PRs, abandoned work, etc). Some "claims" are probably out-of-date. Feel free to remove yourself from anything here without explanation!

We hope that everyone will edit this freely to try to keep it up to date.

Currently this is in the same order as Syntax.lean (although with tactics we might skip or only "stub" deferred to the end), but it may be worthwhile to turn this into a prioritised list.

🔹 – unclaimed
◼️ – claimed
☑️ – PR'd, unneeded, or otherwise done

E: Easy. It's a simple macro in terms of existing things,
or an elab tactic for which we have many similar examples. Example: left
M: Medium. An elab tactic, not too hard, perhaps a 100-200 lines file. Example: have
N: Possibly requires new mechanisms in lean 4, some investigation required
B: Hard, because it is a big and complicated tactic
S: Possibly easy, because we can just stub it out or replace with something else
?: uncategorized

• 🔹 N parameter
  • there is a proposal in terms of nullary typeclasses
• 🔹 S abstract
• ☑️ B cc
  • @Komyyy PR'd as #5938
• 🔹 M unfold_projs
  • there are some porting notes that should be reviewed, to decide if we're just missing simp lemmas, or really want this tactic
• 🔹 N try_for
  • Started by @bollu, but leanprover/lean4#1364 stalled. @bollu is no longer working on it
• ☑️ S clean
  • @mkaratarakis PR'd as #5909
• ☑️ S refine_struct
  • Use refine' with built-in .. syntax, e.g. refine' { x := 0, y := 1 .. }
• 🔹 M match_hyp
• 🔹 N field / S have_field / S apply_field
• 🔹 M h_generalize
• ☑️ M congrm
  • #2544
• ☑️ E ac_change
  • @Komyyy PR'd as #5869
• 🔹 M decide!
• 🔹 M delta_instance
• 🔹 M generalizes
• 🔹 B itauto
• 🔹 B obviously
• 🔹 M assoc_rw
• 🔹 S dsimp_result / N simp_result
• 🔹 M trunc_cases
• 🔹 E apply_normed
• ◼️ M mono
  • A quick version is PR'd as #1740
  • @thorimur is working on the full version
• 🔹 B ac_mono
• 🔹 M unfold_cases
• 🔹 B equiv_rw
• ☑️ N nth_rw
  • PR'd as #823, although this doesn't actually reproduce the mathlib3 behaviour
• ☑️ M compute_degree_le
  • @adomani PR'd as #5882 #6221
• 🔹 M padic_index_simp
• ☑️ E uniqueDiffWithinAt_Ici_Iic_univ
• ☑️ M ghost_fun_tac
• ☑️ M ghost_calc
• ☑️ M init_ring
• ☑️ E ghost_simp
• ☑️ E witt_truncate_fun_tac
• ☑️ M pure_coherence / M coherence
• 🔹 (conv mode) E [norm_num][norm_num-conv] / E [norm_num1][norm_num1-conv]
  • @bollu claimed this is no longer working on it
• ☑️ (attribute) ? protect_proj
  • Not needed because protected can be used for constructors.
• ☑️ (attribute) M notation_class
• ◼️ (attribute) M mono
  • A quick version is PR'd as #1740
  • @thorimur is working on the full version
• ☑️ N add_tactic_doc
  • @lakesare PR'd as #639
• 🔹 (command) N mk_simp_attribute
• ☑️ (command) M add_hint_tactic
  • @Komyyy PR'd as #5363
  • @semorrison PR'd as #8363 and renamed to register_hint
• 🔹 (command) N def_replacer
• 🔹 (command) M reassoc_axiom

We then have a number of tactics and commands for which mere stubs will suffice for the port. Sometimes this is because the tactic is only used during development (but not in PRs to mathlib), other times because it is not used at all anymore in mathlib.

• 🔹 (attribute) S intro / S intro!
• 🔹 S propagate_tags
  • PR'd as #258 (abandoned?)
• 🔹 ? quote / ? pquote / ? ppquote
• 🔹 S mapply
• 🔹 S destruct
• 🔹 S rsimp
• ☑️ S comp_val
  • Use decide.
• 🔹 S async
• 🔹 S continue
• ☑️ S extract_goal
  • @robertylewis claimed this.
  • @adomani PR'd as #4595
• 🔹 S revert_deps
• 🔹 S revert_after
• ☑️ S revert_target_deps
  • PR'd as #333
• 🔹 S rcases?
• 🔹 S rintro?
• ☑️ S hint
  • @Komyyy PR'd as #5363
  • @semorrison PR'd as #8363
• 🔹 S clarify / S safe / S finish
• 🔹 S cases'' / S induction''
• 🔹 S pretty_cases
• 🔹 S suggest
• ☑️ S omega
• 🔹 S transport
• ☑️ S rw_search
  • @semorrison PR'd as #6120
• ☑️ S mk_decorations
• ☑️ S mv_bisim
• @Komyyy PR'd as #2444
• 🔹 S subtype_instance
• 🔹 S elide / S unelide
• ☑️ S guard_tags
  • PR'd as #258
• 🔹 S guard_proof_term
• ☑️ S fail_if_success
• ☑️ (command) S setup_tactic_parser
  • This command is not needed because ? and * notations for sytaxes are available without a command.
• 🔹 (command) S #list_unused_decls
• ☑️ (command) S #simp
• ☑️ (command) S #where
• ☑️ (command) S #sample

Right now we have infix:50 " ∈ " => mem in Data.List.Basic, and also a ∈ notation class Mem used for sets. I tried to replace the list notation with an instance of Mem and it broke all the proofs :-( What am I doing wrong? Obviously I could just fix all the proofs one by one and make them all longer, but I was not sure this would be welcome as a PR and I suspect I'm missing a trick.

The notation for abs clashes with some variants of the match notation:

import Mathbin.Algebra.Abs -- works if this is not imported

def test : Nat → Nat
| 0 => 0  -- expected '|'
| n + 1 => 0

On solving i + (↑n - 1 - i) = ↑n - 1 in integers:

ring failed, ring expressions not equal: 
(1) * (i)^1 + (1) * (↑n - 1 - i)^1 + 0
  !=
(1) * (↑n - 1)^1 + 0

Mathlib commit: 8f609e0

In mathlib3, pairwise_and_iff has a usage of clear_ with this context:

α : Type u_1,
R S : α → α → Prop,
l : list α,
_x : pairwise R l ∧ pairwise S l,
_fun_match : pairwise R l ∧ pairwise S l → pairwise (λ (a b : α), R a b ∧ S a b) l,
hR : pairwise R l,
hS : pairwise S l
⊢ pairwise (λ (a b : α), R a b ∧ S a b) l

(see https://github.com/leanprover-community/mathlib/blob/aff61c0f687c5d366edb248791f26fa69a4adfe2/src/data/list/pairwise.lean#L67)

A direct translation into Lean 4 leads to this context in the same place:

α : Type u_1
R : α → α → Prop
a : α
l : List α
S : α → α → Prop
: Pairwise R l ∧ Pairwise S l
hR : Pairwise R l
hS : Pairwise S l
⊢ Pairwise (fun a b => R a b ∧ S a b) l

In this case, the current version of mathlib4's clear_ won't drop the Pairwise R l ∧ Pairwise S l hypothesis, because it is anonymous inaccessible. We need to drop that hypothesis to get the later induction to work. It's easy enough to work around this problem by adapting the proof a bit, but it would be nice if we could have a direct translation. What would make most sense to me is for mathlib4's clear_ to also drop unnamed hypotheses (in addition to hypotheses whose names start with _). We could even make the behavior configurable.

https://github.com/leanprover-community/lean3port/compare/ported

Currently, to_additive overeagerly translates invFun to negFun, when it means the inverse function. Consider adding invFun as an exception to the inv -> neg rule. Example: MulEquiv.invFun_eq_symm

We need a mechanism to add protected, or otherwise to tell alias to create protected declarations.

There is an example in Mathlib/Algebra/GroupWithZero/Units/Basic.lean.

The definition of subset in Mathlib.Init.Set.lean is ∀ {a}, a ∈ s₁ → a ∈ s₂. But the corresponding definition in mathlib3 was ∀ {{a}}, a ∈ s₁ → a ∈ s₂. Floris van Doorn suggested to me that the definition should be changed to use {{a}} as it did before.

Here is an example of a problem caused by the new definition. The following proof doesn't work:

example (A B : Set Nat) (h1 : A ⊆ C) (h2 : A = B) : B ⊆ C := by
  have h3 : B ⊆ C := h2 ▸ h1
  exact h3

The exact h3 line generates the error

type mismatch
  h3
has type
  ?m.645 ∈ B → ?m.645 ∈ C : Prop
but is expected to have type
  B ⊆ C : Prop

The cause of the problem is the implicit argument {a} in the definition of subset.

import Mathlib.Tactic.ToAdditive

@[to_additive]
def IsUnit [Mul M] (a : M) : Prop := a ≠ a

-- this works fine
@[to_additive]
theorem isUnit_iff_inv [Mul M] {a : M} : IsUnit a ↔ a ≠ a :=
  ⟨fun h => absurd rfl h, fun h => h⟩
#print isAddUnit_iff_neg

/-
The declaration isUnit_iff_exists_inv depends on the declaration isUnit_iff_exists_inv.match_1 which
is in the namespace isUnit_iff_exists_inv, but does not have the `@[to_additive]` attribute.
This is not supported.  Workaround: move isUnit_iff_exists_inv.match_1 to a different namespace.
-/
@[to_additive]
theorem isUnit_iff_exists_inv [Mul M] {a : M} : IsUnit a ↔ ∃ b : α, a ≠ a :=
  ⟨fun h => absurd rfl h, fun ⟨b, hab⟩ => hab⟩

-- attribute [to_additive isAddUnit_iff_exists_neg.match_1] isUnit_iff_exists_inv.match_1
-- attribute [to_additive] isUnit_iff_exists_inv

The first example works fine. Including the Exists makes to_additive fails. I've had to do the "tag match_1" workaround repeatedly in #549.

Floris has already done some work on this.

The relevant branch / PRs are
#129
https://github.com/leanprover-community/mathlib4/compare/toAdditiveAttr

• applyReplacementFun transforms the expressions.
• Some Lean 4-specific changes are not implemented yet (guessing names with CamelCase, transforming inductives/structures properly)
• Some extra functions are not implemented yet

From #348: Lean 4 defines max and min in the prelude, while Lean 3 (as of leanprover-community/lean#609) defines them differently as part of linear_order. We will need to figure out how to resolve this conflict.

Probably the easiest thing would be to get notation typeclasses Max and Min into core.

@digama0 probably has this lying around locally since he's accidentally used it in mathport already.

I've put a temp fix in mathport: leanprover-community/mathport@eda2ffa

I'd like to suggest adding the following to Mathlib.Init.Set.lean:

macro (priority := low-1) "{ " pat:term " : " t:term " | " p:term " }" : term =>
  `({x : $t | match x with | $pat => $p})

macro (priority := low-1) "{ " pat:term " | " p:term " }" : term =>
  `({x | match x with | $pat => $p})

@[app_unexpander setOf]
def setOf.unexpander : Lean.PrettyPrinter.Unexpander
  | `($_ fun $_:ident =>
        match $_:ident with
        | $pat => $p) => `({ $pat:term | $p:term })
  | _ => throw ()

This allows set theory notation like {(a, b) : Nat × Nat | a < b}.
I have set the priority lower than all other set theory notation defined in Mathlib.Init.Set.lean, so this shouldn't interfere with any existing notation.

In Mathlib/Init/Set, the definition of the empty set is:

instance : EmptyCollection (Set α) :=
⟨λ _ => false⟩

Is this a typo? Should it be λ _ => False?

See PR #659, in Algebra.Hom.Group, around theorem MonoidHom.coe_coe. If the quickfix

attribute [to_additive AddMonoidHomClass.toZeroHomClass] MonoidHomClass.toOneHomClass

is removed, the to_additive tactic seems to be looking for AddMonoidHomClass.toOneHomClass, when it should look for AddMonoidHomClass.toZeroHomClass. It has no trouble translating OneHomClass to ZeroHomClass, but has trouble with toOneHomClass.

Becauses simp by default uses decide in Lean 4, zify has become too powerful.

In Lean 4:

import Mathlib.Tactic.Zify

example (h : 0 = 7) : False := by
  zify at h

but in Lean 3:

import tactic.zify

example (h : 0 = 7) : false :=
begin
  zify at h,
  fail_if_success { assumption, },
  revert h, dec_trivial,
end

See first item in https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Algebra.2EGroup.2EOpposite

The following code produces an error on the symm attribute:

import Mathlib.Algebra.Hom.Group
import Mathlib.Logic.Equiv.Basic

def MulHom.inverse [Mul M] [Mul N] (f : M →ₙ* N) (g : N → M) (h₁ : Function.LeftInverse g f)
    (h₂ : Function.RightInverse g f) : N →ₙ* M where
  toFun := g
  map_mul' x y :=
    calc
      g (x * y) = g (f (g x) * f (g y)) := by rw [h₂ x, h₂ y]
      _ = g (f (g x * g y)) := by rw [f.map_mul]
      _ = g x * g y := h₁ _

structure MulEquiv (M N : Type _) [Mul M] [Mul N] extends M ≃ N, M →ₙ* N

infixl:25 " ≃* " => MulEquiv

@[symm]
-- @[symm] attribute only applies to lemmas proving x ∼ y → y ∼ x, got {M : Type u_1} →
--  {N : Type u_2} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
def foo_symm {M N : Type _} [Mul M] [Mul N] (h : M ≃* N) : N ≃* M :=
  { h.toEquiv.symm with map_mul' := (h.toMulHom.inverse h.toEquiv.symm h.left_inv h.right_inv).map_mul }

It appears that trans is similarly having trouble recognising the structure of trans lemmas.

• the implementation needs to be added to core lean:
  https://github.com/EdAyers/lean4/tree/ApplyNewGoals
  leanprover/lean4#1045
• either add eapply and fapply to core lean or mathlib dependent on Lean team's view on the RFC

Currently the implementation of ring is incomplete and has no understanding of subtraction or negation:

import Mathlib.Tactic.Ring

example (a b : ℤ) : a - b = a + -b := by ring
-- ring failed, ring expressions not equal: 
-- (1) * (a - b)^1 + 0
--   !=
-- (1) * (a)^1 + (1) * (-b)^1 + 0

I'm trying to update lean4-samples to latest mathlib4 so I can pick up the new symm tactic, but the Std library build fails with:

error: > LEAN_PATH=.\build\lib;.\lean_packages\mathlib\build\lib;.\lean_packages\std\build\lib;.\lean_packages\Qq\build\lib c:\Users\clovett\.elan\toolchains\leanprover--lean4---nightly\bin\lean.exe -DwarningAsError=true -Dlinter.missingDocs=true .\lean_packages\std\.\.\Std\Data\Nat\Lemmas.lean -R .\lean_packages\std\.\. -o .\lean_packages\std\build\lib\Std\Data\Nat\Lemmas.olean -i .\lean_packages\std\build\lib\Std\Data\Nat\Lemmas.ilean -c .\lean_packages\std\build\ir\Std\Data\Nat\Lemmas.c
error: stdout:
.\lean_packages\std\.\.\Std\Data\Nat\Lemmas.lean:152:42: error: no goals to be solved
.\lean_packages\std\.\.\Std\Data\Nat\Lemmas.lean:157:26: error: application type mismatch

See Mathlib/Algebra/CovariantAndContravariant.lean for example

In Lean 3 we had:

import tactic.zify

example (h : 0 = 0) : true :=
begin
  zify at h,     -- `h` is `(0 : ℤ) = 0`, not `true`.
  fail_if_success { assumption, },
  trivial,
end

but in Lean 4 we now have:

import Mathlib.Tactic.Zify

example (h : 0 = 0) : True := by
  zify at h   -- `h` has become `True`
  assumption

See the video above and note how after I finish typing, the infoview has to churn through 18s (!!) of intermediate states before showing the current goal state. I haven't yet investigated why this happens, but I am assuming it is a consequence of the fact that we eagerly fetch and display new goal states without waiting for the user to finish typing (doing this is known as debouncing). We should add debouncing, probably with a user-configurable debounce period (the tradeoff is that waiting can also delay the display of up-to-date info). I will give implementing this a go, but if it's not done in two-ish weeks feel free to poke me.

Note also that the issue is more observable on debug builds, and even more on debug builds over remote SSH setups (which is what I used to record this).

https://leanprover-community.github.io/mathlib_docs/tactic/delta_instance.html#tactic.delta_instance_handler
In lean3 there was a default derive handler which would run delta on the goal. That is, it would pull the instance through the type synonym. We don't have this at present in lean4, so it is necessary to construct the instance by hand.

Examples:

deriving instance LargeCategory, ConcreteCategory for HeytAlgCat

turns into

deriving instance LargeCategory for HeytAlgCat

instance : ConcreteCategory HeytAlgCat := by
  dsimp [HeytAlgCat]
  infer_instance

import Mathlib.Tactic.Convert

example [Subsingleton α] (a b c : α) (w : a = c) : a = b := by
  convert w -- fails with unsolved goal `b = c`

while in Lean 3

import tactic.congr

example {α} [subsingleton α] (a b c : α) (w : a = c) : a = b :=
by convert w

succeeds.

I'm not sure yet whether this needs a change in convert or in congr in core.