Complex numbers as a field

[kbuzzard]

Basic complex numbers module. I verify the field axioms. Nothing topological.

[kbuzzard]

I don't really understand why the checks have failed. If I can fix this myself, or can help in any other way, let me know.

I've done some basic undergrad-level complex number questions using this module and in particular I can say that I've got it working at my end.

[digama0]

Obviously, the commentary should be removed. We can continue the discussion here on github.

[kbuzzard]

I tried to tidy up / remove comments.

[digama0]

This is fine, we're in classical land here, although you probably don't need it since the reals already have a decidable_eq instance. Easy way to find out: remove it and see what breaks.

[kbuzzard]

I removed it and stuff broke so I put it back.

[digama0]

Yes. You don't want the definition being called complex.complex.

[kbuzzard]

OK got it.

[digama0]

Personally, I would want to avoid direct reference to complex.mk, replacing { re := x, im := y } with x + i*y, which is the standard notation (except possibly in the definitions of add etc.)

A possibility for i is to use I (which is rarely used because of the capitals) or a unicode i-like character. You shouldn't protect i in any case, users will want to open complex specifically so they can use i as is, and there is little danger of overwriting a variable name since local variables take precedence.

[kbuzzard]

I've switched to I.

[digama0]

Conventionally, yes we protect add and other things that have definitions in the root namespace (although maybe that convention should change now that _root_.add is gone). This is not usually a problem because these are accessed through their has_add instances anyway.

[kbuzzard]

I've protected add, neg, mul, inv

[digama0]

Yes, they (and you) should use the coercion wherever possible.

[digama0]

You are right that this is overcomplicated. I'll clean it up after merge

[digama0]

It's true that you can define a real.cast, but it has complicated topological side conditions and I'd rather not define it until I need it. Using of_real as the designated coercion is fine, although we will want theorems saying that the casts commute with of_real, i.e. of_real ((n : nat) : real) = ((n : nat) : complex) and similarly for rat and int.

[kbuzzard]

I wrote these for nat and int; I almost wrote one for rat but I needed that the complexes had characteristic zero. I proved this but then for some reason I could not put it all together -- I was getting timeouts. I've left my proof in but commented it out.

[digama0]

This would be a good simp lemma if pointed the other direction.

[kbuzzard]

I don't really understand why but I switched them round.

[digama0]

Use coercions here

[kbuzzard]

OK I changed these to use coercions

[kbuzzard]

Thanks. I will get to these at some point (I have some major work commitments for the next 6 days and am travelling over the weekend so this might have to wait a week; I trust there's no huge hurry). As you spotted, the commentary was put there just to flag issues I wasn't sure about -- I thought it was worth explicitly flagging them rather than just guessing something (possibly incorrectly) and hoping nobody noticed/cared.

[digama0]

This is a fairly common pattern. Rather than reproving the new properties the second time around, just omit them entirely, and fill them in with { discrete_field . <new stuff> , ..complex.add_group }, where the dot dot notation says "copy the fields from here". See rat.discrete_linear_ordered_field for an example.

[kbuzzard]

I tried this but then got into a real mess with type class inference. Will try again tomorrow.

[johoelzl]

Don't use the form _ ∧ _ → _ always use the curried form _ → _ → _. In this case z.re=w.re → z.im=w.im → z=w.
Hint: use the equation compiler:

example : ∀ (z w : complex), z.re = w.re → z.im = w.im → z = w
| ⟨zr, zi⟩ ⟨wr, wi⟩ rfl rfl := rfl

[johoelzl]

no indentation after theorem name : ... :=. The cases_on should start in the first column

[kbuzzard]

OK!

[johoelzl]

I don't think you should use a tactic proof here. I suggest to use a term mode proof here.
Take more care of indentation. Indent 2 spaces between begin and end.
Also: if you want to mark a sequence of tactics to solve one subgoal use { ... }

[kbuzzard]

Why does anyone care whether I prove a lemma with a tactic proof or a term mode proof? I am serious -- I thought that by proof irrelevance nobody cares what my proofs look like. As long as they compile, we're done. Why am I wrong?

[PatrickMassot]

I guess this is for maintenance reasons. Tactic proofs tend to involve magic (like simp), and magic is fragile. If the list of simp lemma changes (say associativity comes back...) then proofs using simp can break. A term style proof tends to explicitly call out used lemmas. If such a lemma changes, it will probably much easier to understand what went wrong.

[kbuzzard]

My tactic proof was three lines long and used split, intro, rw, trivial and exact. My term proof uses pretty much the same thing :-)

[digama0]

As always, you will get the best results with a combination of tactics and terms. Here's how this is proven in prod (which is basically identical to what you want here):

@[simp] theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ (a₁ = a₂ ∧ b₁ = b₂) :=
⟨prod.mk.inj, by cc⟩

lemma eq_iff_fst_eq_snd_eq : ∀{p q : α × β}, p = q ↔ (p.1 = q.1 ∧ p.2 = q.2)
| ⟨p₁, p₂⟩ ⟨q₁, q₂⟩ := by simp

It is nice but usually surprising to see a successful proof by cc. The first thing I would have tried is λ ⟨h₁, h₂⟩, by congr; assumption instead of by cc.

[PatrickMassot]

I must admit I didn't look at the proof before writing my comment. But it gives me the opportunity to ask what is this cc tactic. The documentation is not very illuminating to me.

[kbuzzard]

cc means "congruence closure" but it's one of those tactics that I (and my students) tend to just try occasionally to see if it finishes a (typically proof-by-basic-logic-arguments-only) proof.

[johoelzl]

This should be def of_real (r : ℝ) : ℂ := { re := x, im := 0 }
This is not only an aesthetic reason (why use the unnecessary lambda?), but a practical one:
With of_real : ℝ → ℂ the generated simp rule for of_real matches all occurrences of of_real, while the later only matches of_real r.

[kbuzzard]

This I really do not understand -- I mean, I understand that you're asking me to change something, and I understand how to change it, but I do not understand why changing something to something which looks to me to be definitionally equal should be a sensible idea. Of course I do not doubt that it is! But I would really like to understand better where these comments are coming from. What is "the generated simp rule for of_real"?

[digama0]

You should try #print prefix of_real with both versions. The generated *.equations lemma for of_real will have an x in Johannes's version on the LHS, meaning that if you simp [of_real] it will not unfold unless it's already been applied to an argument.

[kbuzzard]

My slow understanding of these comments is currently at the stage where I understand that even though the two approaches give definitionally equal functions, the associated equation lemmas are not the same, however I am unclear about why one prefers Johannes' version, because I am not clear about what is unfolding or whether we want it to unfold. This, as is sometimes the case with me, seems to come back to the fact that I do not actually understand what simp is doing or how it does it. I guess that's my point here -- the two equation lemmas are "different ways of saying exactly the same thing" to me, but for someone who knows better what simp is doing I guess this is not the case.

[johoelzl]

Let me try the following explanation:
First, in this case unfold just means, that simp will rewrite occurrences of_real using the equation provided by the definition.

Second, it is hard to say why I prefer the of_real r variant. At first glance the of_real : R -> C variant would match more often. But by experience I had quiet some proofs where I only want to replace f x instead of every occurrence of f.

[johoelzl]

I don't think we need explicit constants for complex.add, complex.neg, complex.mul, this all should be in the corresponding definition of has_add etc. Especially as you do not need the equation compiler or proof anything special for them before you set up the instances of has_add etc.

[kbuzzard]

I see! Thanks.

[johoelzl]

Remove the special rules for complex.add etc. Instead of has_add.add use + etc.
Drop the proj_ prefix and the ' suffix.
These are all good simp rules, set them up globally, i.e. @[simp] everywhere instead of just local attribute.

[johoelzl]

I don't think you need this method. Just replace by crunch with by simp [add_mul, mul_add, eq_iff_re_eq_and_im_eq] {contextual:=tt}

[johoelzl]

same as before. Also move the of_real_im an of_real_re rules upwards, also see @digama0's hint to use coercion instead of of_real.

[kbuzzard]

Thanks for these comments. I did do some more work on this but I had stupid problems with splitting up the field definition into first an abelian additive group and then a field on top. Term finishes tomorrow and I will get to this soon after.

[johoelzl]

Of course take your time. For deriving the field structure after the add_comm_group: you can use the new {mul := _ ... , .. complex.add_comm_group } syntax to avoid repeating the elements for the group. (if this was part of the problem?)

[johoelzl]

of_real_add, of_real_sub, of_real_mul and of_real_inv are a rfl lemmas (i.e. they can be proved by just rfl).

[johoelzl]

Also: indentation after begin

[johoelzl]

remove this

[johoelzl]

This suffices : ..., exact this can be replaces by show ....

[johoelzl]

This is an interesting proof:
by simp [abs_mul_abs_self, norm_squared, of_real_eq_coe]

But it only works if norm_squared has as equational lemma norm_squared z = z.re*z.re+z.im*z.im!
Why: When normed_squared is rewritten using the lambda-term the simplifier gets to the term
(fun z, z.re*z.re+z.im*z.im) (of_real r), then it tries to simplify inside the lambda-term.But z.re and z.im cannot be simplified. Later it beta-reduces to (of_real r).re*(of_real r).re+(of_real r).im*(of_real r).im, somehow it does not try to rewrite after beta-reduction, so (of_real r).im and (of_real r).re isn't further simplified. Maybe this should be changed, but it is one occurrence where the normed_square c = equation form is preferred over the normed_square = fun c, ... form.

[kbuzzard]

Aah! So this is a very good way of explaining in concrete terms the issue that came up earlier. Thanks!

[johoelzl]

by begin?

[johoelzl]

indention

[PatrickMassot]

Are there automatic linters for Lean? In python all those comments would be handled by a single run of autopep8.

[kbuzzard]

Sorry, I thought I'd caught them all. In the past I never indented after a begin. I had a system with no initial indent and no {}s which I have used extensively for months now and it's only through talking about this PR that I have come to understand that it is not quite the right system.

In general I don't see the point of this indentation after a begin -- it just means that all of my proofs are indented 2 spaces.

[johoelzl]

If you write tactic proofs all your proofs are indented 2 spaces. It would be different for proof terms, where you have:

let x := ... in
have ..,
  from _,
have .., by ...,
show ..., ...

[johoelzl]

I left some more comments. The comment on of_real_abs_squared is one reason why we prefer the form normed_square r = ... over normed_square = .... But it maybe just a problem in the simplifier (i.e. continue rewriting after beta-reduction).

There are some more things: adding spaces around =, and operators. some more indentation, removing comments etc. But of course we can also changes this after accepting your PR.