Complex.Basic

Stream: mathlib4

[Siddhartha Gadgil]

I started porting Data/Complex/Basic and have reached an error message which I do not understand. The code I have (at line 376) is:

instance : AddCommGroup ℂ := {
  zero := (0 : ℂ)
  add := (· + ·)
  neg := Neg.neg
  sub := Sub.sub
  nsmul := fun n z => ⟨n • z.re - 0 * z.im, n • z.im + 0 * z.re⟩
  zsmul := fun n z => ⟨n • z.re - 0 * z.im, n • z.im + 0 * z.re⟩
  add_assoc := by
    intro z₁ z₂ z₃
    show (⟨z₁.re + z₂.re + z₃.re, z₁.im + z₂.im + z₃.im⟩ : ℂ)
      = ⟨z₁.re + (z₂.re + z₃.re), z₁.im + (z₂.im + z₃.im)⟩
    simp [add_assoc]
  zero_add := by
        intro z ; show  ⟨0 + z.re, 0 + z.im⟩ = z ; simp [zero_add]
  add_zero := by
      intro z ; show  ⟨z.re + 0, z.im + 0⟩ = z ; simp [zero_add]
  add_comm := by
    intro z₁ z₂
    show (⟨z₁.re + z₂.re, z₁.im + z₂.im⟩ : ℂ)
      = ⟨z₂.re + z₁.re, z₂.im + z₁.im⟩
    simp [add_comm]
  add_left_neg := by
    intro z
    show (⟨-z.re + z.re, -z.im + z.im⟩ : ℂ) = 0
    simp [add_left_neg]
  }

and the error message I get is

type mismatch
  HEq.rfl
has type
  HEq ?m.31699 ?m.31699 : Prop
but is expected to have type
  (fun n z => { re := n • ↑z - 0 * ↑z, im := n • ↑z + 0 * ↑z }) 0 x✝ = 0 : Prop
Basic.lean:376:29
type mismatch
  HEq.rfl
has type
  HEq ?m.31722 ?m.31722 : Prop
but is expected to have type
  (fun n z => { re := n • ↑z - 0 * ↑z, im := n • ↑z + 0 * ↑z }) (n✝ + 1) x✝ =
    x✝ + (fun n z => { re := n • ↑z - 0 * ↑z, im := n • ↑z + 0 * ↑z }) n✝ x✝ : Prop
Basic.lean:376:29
type mismatch
  HEq.rfl
has type
  HEq ?m.32009 ?m.32009 : Prop
but is expected to have type
  (fun n z => { re := n • ↑z - 0 * ↑z, im := n • ↑z + 0 * ↑z }) (Int.negSucc n✝) a✝ =
    -(fun n z => { re := n • ↑z - 0 * ↑z, im := n • ↑z + 0 * ↑z }) (↑(Nat.succ n✝)) a✝ : Prop

Any help will be appreciated

[Johan Commelin]

Which line is creating the error?

[Johan Commelin]

Does dsimp or simp help?

[Siddhartha Gadgil]

The error is at the top of the definition.

[Johan Commelin]

maybe some fields are running a tactic as default argument, and this is now failing?

[Siddhartha Gadgil]

It is looking as if the error is in proving nsmul 0 = 0 and hsmul 0 = 0 which it seems is attempted by rfl and fails.

[Siddhartha Gadgil]

When I added proofs of zsmul_zero' and nsmul as sorries half the errors disappeared. Looks like these and two other relations need explicit proofs.

[Siddhartha Gadgil]

Thanks. At least the error is clear - five fields proved by tactics no longer worked.

[Siddhartha Gadgil]

For completeness, these were fairly easy to prove.

[Eric Wieser]

What proof did mathlib3 use for them?

[Eric Wieser]

Were those fields true by rfl in mathlib3, but no longer in mathlib4?

[Eric Wieser]

That might be indicative of an upstream mis-port

[Sebastien Gouezel]

Those fields are not rfl in mathlib3, an explicit proof is given. Here is the relevant definition:

instance : add_comm_group ℂ :=
by refine_struct
  { zero := (0 : ℂ),
    add := (+),
    neg := has_neg.neg,
    sub := has_sub.sub,
    nsmul := λ n z, ⟨n • z.re - 0 * z.im, n • z.im + 0 * z.re⟩,
    zsmul := λ n z, ⟨n • z.re - 0 * z.im, n • z.im + 0 * z.re⟩ };
intros; try { refl }; apply ext_iff.2; split; simp; {ring1 <|> ring_nf}

[Johan Commelin]

I guess refine_struct was never properly ported?

[Eric Wieser]

Ah, and refine_struct either doesn't run, or ignores failures in, auto_params

[Siddhartha Gadgil]

I have fixed errors in over half the file, but am completely confused by the absolute value treatment and have some other questions. It is getting late here so will resume in the morning. But will be grateful for clarifications:

• I see the typeclass Abs needs an absolute value of the same type, and is meant for structures with orders. This is in scope in the file Data.Complex.Basic and apparently many lemmas are used.
• On the other hand, there is a definition of the usual complex absolute value, and this is imported with a defining property.
• From there on, it is very confusing which absolute value is referred to in statements and in proofs - it seems sometimes theorems for the general absolute value are being used.

Another part not clear to me was with norm_cast and coercions. Many lemmas are not accepting the norm_cast attribute. I added a coercion attribute to some lemmas and this fixed a few cases. But in many cases it seems to me that an inclusion has to be annotated as a coercion, and statements may have to use it explicitly if they are to have the norm_cast attribute.

[Eric Wieser]

It's possible that mathport has muddled up the two abss; comparing to the #docs for mathlib3 will help resolve the problems in the statements

[Siddhartha Gadgil]

Comparing with the source of mathlib3 did indeed resolve the issue and the file now compiles.

[Jireh Loreaux]

Did you fix all the norm_cast issues? Sometimes elaboration order between Lean 3 and Lean 4 has changed enough that now coercions need to be inserted in different places for the declaration to elaborate the same way.

[Siddhartha Gadgil]

No, I don't understand norm_cast well enough for this. In fact some proofs became rfl. I have made porting notes and removed the norm_cast where it failed.

[Thomas Murrills]

Johan Commelin said:

I guess refine_struct was never properly ported?

Finished but stalled as a core RFC issue, never to be heard from again… 🥲 (Tangent, but I wonder if I should make a different mathlib4-acceptable version now that it’s not just “Leo’s on vacation” but “core is not moving”.)

[Scott Morrison]

Yes, I guess we better put stuff in mathlib4 for now, where possible.

[Siddhartha Gadgil]

Jireh Loreaux said:

Did you fix all the norm_cast issues? Sometimes elaboration order between Lean 3 and Lean 4 has changed enough that now coercions need to be inserted in different places for the declaration to elaborate the same way.

I did manage to fix a majority by making the inclusion from reals to complex numbers an explicit function annotated coe. Some cases there is an error though.

[Jireh Loreaux]

I'll have a look.

[Siddhartha Gadgil]

Thanks a lot. I have incorporated most of the changes. In one case the original proof was correct but the original statement was not, so I had changed to rfl.

[Eric Wieser]

Which statement?

[Eric Wieser]

Generally you shouldn't change statements when porting

[Chris Hughes]

My guess is that the Lean3 statement was correct, but mathport translated it incorrectly. There are always a lot of those around coercions.

[Siddhartha Gadgil]

Eric Wieser said:

Generally you shouldn't change statements when porting

The change was in explicitly casting and as suggested by @Jireh Loreaux (I don't understand casting enough to make this) to be a better translation. The statement was ofReal_rat_cast but I also had to change the next two very similar ones so proofs using this worked.

[Eric Wieser]

Are the proofs now the same as they were in mathlib3?

[Eric Wieser]

port-status#data/complex/basic, since I don't see the PR number mentioned above

[Jireh Loreaux]

!4#2718

[Jireh Loreaux]

@Siddhartha Gadgil , can you please change the statement of ofReal_rat_cast to what I suggested and replace the proof with the original that worked?

[Siddhartha Gadgil]

I believe I did that a while back. Did I make a mistake? Here is the code of that and the next two statements that needed correspoding changes.

@[simp]
theorem ofReal_rat_cast (n : ℚ) : ((n : ℝ) : ℂ) = @RatCast.ratCast ℂ _ n :=
  map_ratCast ofReal n
#align complex.of_real_rat_cast Complex.ofReal_rat_cast

-- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑`
@[simp]
theorem rat_cast_re (q : ℚ) : (RatCast.ratCast q : ℂ).re = @RatCast.ratCast ℂ _ q := by
 rw [← ofReal_rat_cast, ofReal_re]
#align complex.rat_cast_re Complex.rat_cast_re

-- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑`
@[simp]
theorem rat_cast_im (q : ℚ) : (RatCast.ratCast q : ℂ).im = @RatCast.ratCast ℂ _ 0 := by
 rw [← ofReal_rat_cast, ofReal_im]; norm_cast
#align complex.rat_cast_im Complex.rat_cast_im

[Jireh Loreaux]

maybe you didn't push? this is what I see on GitHub (after refreshing my cache too)

@[simp, nolint synTaut]
-- Was warned that this is a syntactic tautology.
theorem ofReal_rat_cast (n : ℚ) : ((n : ℝ) : ℂ) = n := rfl

[Eric Wieser]

Also, these "removed norm_cast" porting notes are concerning

[Eric Wieser]

I think we should fix norm_cast to auto-symmetrize lemmas with the coe on the wrong side. I believe it did this already in mathlib3

[Eric Wieser]

I've left a handful of comments; I'm a little concerned that a lot of the non-trivial changes / new lemmas / defs didn't get a porting note

[Jireh Loreaux]

Did it? I'm not sure about that.

[Jireh Loreaux]

Also, norm_cast complaints are a good way to spot errors in statements for the moment.

[Jireh Loreaux]

I'm working on making sure there are no more norm_cast removals.

[Siddhartha Gadgil]

I have been pushing. Are we looking at the same branch? At https://github.com/leanprover-community/mathlib4/blob/port/Data.Complex.Basic/Mathlib/Data/Complex/Basic.lean I see

@[simp]
theorem ofReal_rat_cast (n : ℚ) : ((n : ℝ) : ℂ) = @RatCast.ratCast ℂ _ n :=
  map_ratCast ofReal n
#align complex.of_real_rat_cast Complex.ofReal_rat_cast

-- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑`
@[simp]
theorem rat_cast_re (q : ℚ) : (RatCast.ratCast q : ℂ).re = @RatCast.ratCast ℂ _ q := by
 rw [← ofReal_rat_cast, ofReal_re]
#align complex.rat_cast_re Complex.rat_cast_re

-- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑`
@[simp]
theorem rat_cast_im (q : ℚ) : (RatCast.ratCast q : ℂ).im = @RatCast.ratCast ℂ _ 0 := by
 rw [← ofReal_rat_cast, ofReal_im]; norm_cast
#align complex.rat_cast_im Complex.rat_cast_im

[Eric Wieser]

Not related to the above, but related to the PR; what should complex.I be called in mathlib4?

[Eric Wieser]

Mathport guessed Complex.i but that doesn't make it the right choice necessarily

[Jireh Loreaux]

@Siddhartha Gadgil I see it now, not sure what the problem was before, sorry for the noise.

[Jireh Loreaux]

I think we should stick to Complex.I using upper case, primarily to avoid confusion and clashes with local variables, but this is a question for the naming convention stream.

[Thomas Murrills]

Is there a reason the rhs's of these lemmas aren't simply e.g. ((n : ℚ) : ℂ) or ((0 : ℚ) : ℂ)? (I was searching mathlib4 for any stray RatCast.ratCasts and found these.)

[Eric Wieser]

They certainly should be that; are they not?

[Thomas Murrills]

Currently they're

@[simp, norm_cast]
theorem ofReal_rat_cast (n : ℚ) : ((n : ℝ) : ℂ) = @RatCast.ratCast ℂ _ n :=
  map_ratCast ofReal n
#align complex.of_real_rat_cast Complex.ofReal_rat_cast

-- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑`
@[simp]
theorem rat_cast_re (q : ℚ) : (RatCast.ratCast q : ℂ).re = @RatCast.ratCast ℂ _ q := by
 rw [← ofReal_rat_cast, ofReal_re]
#align complex.rat_cast_re Complex.rat_cast_re

-- Porting note: removed `norm_cast` attribute because the RHS can't start with `↑`
@[simp]
theorem rat_cast_im (q : ℚ) : (RatCast.ratCast q : ℂ).im = @RatCast.ratCast ℂ _ 0 := by
 rw [← ofReal_rat_cast, ofReal_im]; norm_cast
#align complex.rat_cast_im Complex.rat_cast_im

[Yaël Dillies]

The porting notes are wrong. The lemmas were mistranslated. Btw rat_cast should be ratCast

[Eric Wieser]

@Mario Carneiro, what's the easiest way to get a fresh mathport output for that file to diff against? One that isn't impacted by the version that's actually in mathlib4

[Mario Carneiro]

If you copy a mathlib4 file into oneshot you should be able to port it as though it was a new file

[Thomas Murrills]

Here's a PR on which we can fix things—I did the rename and naively changed things as they appeared to the corresponding coercions. I'll take a look at mathlib3 now !4#2947

[Thomas Murrills]

@Eric Wieser feel free to commit to that PR/branch if you're making moves (stray-ratCasts)

[Eric Wieser]

Mario Carneiro said:

If you copy a mathlib4 file into oneshot you should be able to port it as though it was a new file

Could you take a quick look at my question about one-shot here?

[Thomas Murrills]

Lol, yup (re: the message that said renaming discussion ought to be in the naming thread, which is now gone). I suppose I'll undo the renames on that PR for now, and we'll wait until it's sorted one way or the other... EDIT: actually, I'll see where we land first, just in case I'd be duplicating work.