From 98ddc62f6ccb1348622879194332c311ec0152a6 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Thu, 12 Nov 2015 20:35:05 -0500
Subject: [PATCH] feat(library/data/complex): add complex numbers

---
 library/data/complex.lean | 375 ++++++++++++++++++++++++++++++++++++++
 library/data/data.md      |   3 +-
 library/data/default.lean |   2 +-
 3 files changed, 378 insertions(+), 2 deletions(-)
 create mode 100644 library/data/complex.lean

diff --git a/library/data/complex.lean b/library/data/complex.lean
new file mode 100644
index 000000000..1531dbb27
--- /dev/null
+++ b/library/data/complex.lean
@@ -0,0 +1,375 @@
+/-
+Copyright (c) 2015 Jacob Gross. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jacob Gross, Jeremy Avigad
+
+The complex numbers.
+-/
+import data.real
+open real eq.ops algebra
+
+record complex : Type :=
+(re : ℝ) (im : ℝ)
+
+notation `ℂ` := complex
+
+namespace complex
+
+variables (u w z : ℂ)
+variable n : ℕ
+
+protected proposition eq {z w : ℂ} (H1 : complex.re z = complex.re w)
+(H2 : complex.im z = complex.im w) : z = w :=
+begin
+  induction z,
+  induction w,
+  rewrite [H1, H2]
+end
+
+protected proposition eta (z : ℂ) : complex.mk (complex.re z) (complex.im z) = z :=
+by cases z; exact rfl
+
+definition of_real [coercion] (x : ℝ) : ℂ := complex.mk x 0
+definition of_rat [coercion] (q : ℚ) : ℂ := rat.to.complex q
+definition of_int [coercion] (i : ℤ) : ℂ := int.to.complex i
+definition of_nat [coercion] (n : ℕ) : ℂ := nat.to.complex n
+definition of_num [coercion] [reducible] (n : num) : ℂ := num.to.complex n
+
+protected definition prio : num := num.pred real.prio
+
+definition complex_has_zero [reducible] [instance] [priority complex.prio] : has_zero ℂ :=
+has_zero.mk (of_nat 0)
+
+definition complex_has_one [reducible] [instance] [priority complex.prio] : has_one ℂ :=
+has_one.mk (of_nat 1)
+
+theorem re_of_real (x : ℝ) : re (of_real x) = x := rfl
+
+theorem im_of_real (x : ℝ) : im (of_real x) = 0 := rfl
+
+protected definition add (z w : ℂ) : ℂ :=
+complex.mk (complex.re z + complex.re w) (complex.im z + complex.im w)
+
+protected definition neg (z : ℂ) : ℂ :=
+complex.mk (-(re z)) (-(im z))
+
+protected definition mul (z w : ℂ) : ℂ :=
+complex.mk
+  (complex.re w * complex.re z - complex.im w * complex.im z)
+  (complex.re w * complex.im z + complex.im w * complex.re z)
+
+/- notation -/
+
+definition complex_has_add [reducible] [instance] [priority complex.prio] : has_add complex :=
+has_add.mk complex.add
+
+definition complex_has_neg [reducible] [instance] [priority complex.prio] : has_neg complex :=
+has_neg.mk complex.neg
+
+definition complex_has_mul [reducible] [instance] [priority complex.prio] : has_mul complex :=
+has_mul.mk complex.mul
+
+protected theorem add_def (z w : ℂ) :
+  z + w = complex.mk (complex.re z + complex.re w) (complex.im z + complex.im w) := rfl
+
+protected theorem neg_def (z : ℂ) : -z = complex.mk (-(re z)) (-(im z)) := rfl
+
+protected theorem mul_def (z w : ℂ) :
+  z * w = complex.mk
+    (complex.re w * complex.re z - complex.im w * complex.im z)
+    (complex.re w * complex.im z + complex.im w * complex.re z) := rfl
+
+-- TODO: what notation should we use for i?
+
+definition ii := complex.mk 0 1
+
+theorem i_mul_i : ii * ii = -1 := rfl
+
+/- basic properties -/
+
+protected theorem add_comm (w z : ℂ) : w + z = z + w :=
+complex.eq !add.comm !add.comm
+
+protected theorem add_assoc (w z u : ℂ) : (w + z) + u = w + (z + u) :=
+complex.eq !add.assoc !add.assoc
+
+protected theorem add_zero (z : ℂ) : z + 0 = z :=
+complex.eq !add_zero !add_zero
+
+protected theorem zero_add (z : ℂ) : 0 + z = z := !complex.add_comm ▸ !complex.add_zero
+
+definition smul (x : ℝ) (z : ℂ) : ℂ :=
+complex.mk (x*re z) (x*im z)
+
+protected theorem add_right_inv : z + - z = 0 :=
+complex.eq !add.right_inv !add.right_inv
+
+protected theorem add_left_inv : - z + z = 0 :=
+!complex.add_comm ▸ !complex.add_right_inv
+
+protected theorem mul_comm : w * z = z * w :=
+by rewrite [*complex.mul_def, *mul.comm (re w), *mul.comm (im w), add.comm]
+
+protected theorem one_mul :  1 * z = z :=
+by krewrite [complex.mul_def, *mul_one, *mul_zero, sub_zero, zero_add, complex.eta]
+
+protected theorem mul_one :  z * 1 = z := !complex.mul_comm ▸ !complex.one_mul
+
+protected theorem left_distrib  : u * (w + z) = u * w + u * z :=
+begin
+  rewrite [*complex.mul_def, *complex.add_def, ▸*, *right_distrib, -sub_sub, *sub_eq_add_neg],
+  rewrite [*add.assoc, add.left_comm (re z * im u), add.left_comm (-_)]
+end
+
+protected theorem right_distrib : (u + w) * z = u * z + w * z :=
+by rewrite [*complex.mul_comm _ z, complex.left_distrib]
+
+protected theorem mul_assoc : (u * w) * z = u * (w * z) :=
+begin
+  rewrite [*complex.mul_def, ▸*, *sub_eq_add_neg, *left_distrib, *right_distrib, *neg_add],
+  rewrite [-*neg_mul_eq_neg_mul, -*neg_mul_eq_mul_neg, *add.assoc, *mul.assoc],
+  rewrite [add.comm (-(im z * (im w * _))), add.comm (-(im z * (im w * _))), *add.assoc]
+end
+
+theorem re_add (z w : ℂ) : re (z + w) = re z + re w := rfl
+
+theorem im_add (z w : ℂ) : im (z + w) = im z + im w := rfl
+
+/- coercions -/
+
+theorem of_real_add (a b : ℝ) : of_real (a + b) = of_real a + of_real b := rfl
+
+theorem of_real_mul (a b : ℝ) : of_real (a * b) = (of_real a) * (of_real b) :=
+by rewrite [complex.mul_def, *re_of_real, *im_of_real, *mul_zero, *zero_mul, sub_zero, add_zero,
+           mul.comm]
+
+theorem of_real_neg (a : ℝ) : of_real (-a) = -(of_real a) := rfl
+
+theorem of_real.inj {a b : ℝ} (H : of_real a = of_real b) : a = b :=
+show re (of_real a) = re (of_real b), from congr_arg re H
+
+theorem eq_of_of_real_eq_of_real {a b : ℝ} (H : of_real a = of_real b) : a = b :=
+of_real.inj H
+
+theorem of_real_eq_of_real_iff (a b : ℝ) : of_real a = of_real b ↔ a = b :=
+iff.intro eq_of_of_real_eq_of_real !congr_arg
+
+/- make complex an instance of ring -/
+
+protected definition comm_ring [reducible] : algebra.comm_ring complex :=
+  begin
+    fapply algebra.comm_ring.mk,
+    exact complex.add,
+    exact complex.add_assoc,
+    exact 0,
+    exact complex.zero_add,
+    exact complex.add_zero,
+    exact complex.neg,
+    exact complex.add_left_inv,
+    exact complex.add_comm,
+    exact complex.mul,
+    exact complex.mul_assoc,
+    exact 1,
+    apply complex.one_mul,
+    apply complex.mul_one,
+    apply complex.left_distrib,
+    apply complex.right_distrib,
+    apply complex.mul_comm
+  end
+
+local attribute complex.comm_ring [instance]
+
+definition complex_has_sub [reducible] [instance] [priority complex.prio] : has_sub complex :=
+has_sub.mk has_sub.sub
+
+theorem of_real_sub (x y : ℝ) : of_real (x - y) = of_real x - of_real y :=
+rfl
+
+-- TODO: move these
+private lemma eq_zero_of_mul_self_eq_zero {x : ℝ} (H : x * x = 0) : x = 0 :=
+ iff.mp !or_self (!eq_zero_or_eq_zero_of_mul_eq_zero H)
+
+private lemma eq_zero_of_sum_square_eq_zero {x y : ℝ} (H : x * x + y * y = 0) : x = 0 :=
+have x * x ≤ (0 : ℝ), from calc
+  x * x ≤ x * x + y * y : le_add_of_nonneg_right (mul_self_nonneg y)
+    ... = 0             : H,
+eq_zero_of_mul_self_eq_zero (le.antisymm this (mul_self_nonneg x))
+
+/- complex modulus and conjugate-/
+
+definition cmod (z : ℂ) : ℝ :=
+(complex.re z) * (complex.re z) + (complex.im z) * (complex.im z)
+
+theorem cmod_zero : cmod 0 = 0 := rfl
+
+theorem cmod_of_real (x : ℝ) : cmod x = x * x :=
+by rewrite [↑cmod, re_of_real, im_of_real, mul_zero, add_zero]
+
+theorem eq_zero_of_cmod_eq_zero {z : ℂ} (H : cmod z = 0) : z = 0 :=
+have H1 : (complex.re z) * (complex.re z) + (complex.im z) * (complex.im z) = 0,
+  from H,
+have H2 : complex.re z = 0, from eq_zero_of_sum_square_eq_zero H1,
+have H3 : complex.im z = 0, from eq_zero_of_sum_square_eq_zero (!add.comm ▸ H1),
+show z = 0, from complex.eq H2 H3
+
+definition conj (z : ℂ) : ℂ := complex.mk (complex.re z) (-(complex.im z))
+
+theorem conj_of_real {x : ℝ} : conj (of_real x) = of_real x := rfl
+
+theorem conj_add (z w : ℂ) : conj (z + w) = conj z + conj w :=
+by rewrite [↑conj, *complex.add_def, ▸*, neg_add]
+
+theorem conj_mul (z w : ℂ) : conj (z * w) = conj z * conj w :=
+by rewrite [↑conj, *complex.mul_def, ▸*, neg_mul_neg, neg_add,
+            -neg_mul_eq_mul_neg, -neg_mul_eq_neg_mul]
+
+theorem conj_conj (z : ℂ) : conj (conj z) = z :=
+by rewrite [↑conj, neg_neg, complex.eta]
+
+theorem mul_conj_eq_of_real_cmod (z : ℂ) : z * conj z = of_real (cmod z) :=
+by rewrite [↑conj, ↑cmod, ↑of_real, complex.mul_def, ▸*, -*neg_mul_eq_neg_mul,
+            sub_neg_eq_add, mul.comm (re z) (im z), add.right_inv]
+
+theorem cmod_conj (z : ℂ) : cmod (conj z) = cmod z :=
+begin
+  apply eq_of_of_real_eq_of_real,
+  rewrite [-*mul_conj_eq_of_real_cmod, conj_conj, mul.comm]
+end
+
+theorem cmod_mul (z w : ℂ) : cmod (z * w) = cmod z * cmod w :=
+begin
+  apply eq_of_of_real_eq_of_real,
+  rewrite [of_real_mul, -*mul_conj_eq_of_real_cmod, conj_mul, *mul.assoc, mul.left_comm w]
+end
+
+protected noncomputable definition inv (z : ℂ) : complex := conj z * of_real (cmod z)⁻¹
+
+protected noncomputable definition complex_has_inv [reducible] [instance] [priority complex.prio] :
+  has_inv complex := has_inv.mk complex.inv
+
+protected theorem inv_def (z : ℂ) : z⁻¹ = conj z * of_real (cmod z)⁻¹ := rfl
+
+protected theorem inv_zero : 0⁻¹ = (0 : ℂ) :=
+by krewrite [complex.inv_def, conj_of_real, zero_mul]
+
+theorem of_real_inv (x : ℝ) : of_real x⁻¹ = (of_real x)⁻¹ :=
+classical.by_cases
+  (assume H : x = 0,
+    by krewrite [H, inv_zero, complex.inv_zero])
+  (assume H : x ≠ 0,
+    by rewrite [complex.inv_def, cmod_of_real, conj_of_real, mul_inv_eq H H, -of_real_mul,
+               -mul.assoc, mul_inv_cancel H, one_mul])
+
+noncomputable protected definition div (z w : ℂ) : ℂ := z * w⁻¹
+
+noncomputable definition complex_has_div [instance] [reducible] [priority complex.prio] :
+    has_div complex :=
+  has_div.mk complex.div
+
+protected theorem div_def (z w : ℂ) : z / w = z * w⁻¹ := rfl
+
+theorem of_real_div (x y : ℝ) : of_real (x / y) = of_real x / of_real y :=
+have H : x / y = x * y⁻¹, from rfl,
+by+ rewrite [H, complex.div_def, of_real_mul, of_real_inv]
+
+theorem conj_inv (z : ℂ) : (conj z)⁻¹ = conj (z⁻¹) :=
+by rewrite [*complex.inv_def, conj_mul, *conj_conj, conj_of_real, cmod_conj]
+
+protected theorem mul_inv_cancel {z : ℂ} (H : z ≠ 0) : z * z⁻¹ = 1 :=
+by rewrite [complex.inv_def, -mul.assoc, mul_conj_eq_of_real_cmod, -of_real_mul,
+            mul_inv_cancel (assume H', H (eq_zero_of_cmod_eq_zero H'))]
+
+protected theorem inv_mul_cancel {z : ℂ} (H : z ≠ 0) : z⁻¹ * z = 1 :=
+!mul.comm ▸ complex.mul_inv_cancel H
+
+protected noncomputable definition has_decidable_eq : decidable_eq ℂ :=
+take z w, classical.prop_decidable (z = w)
+
+protected theorem zero_ne_one : (0 : ℂ) ≠ 1 :=
+assume H, zero_ne_one (eq_of_of_real_eq_of_real H)
+
+protected noncomputable definition discrete_field [reducible][trans_instance] :
+  discrete_field ℂ :=
+⦃ discrete_field, complex.comm_ring,
+  mul_inv_cancel   := @complex.mul_inv_cancel,
+  inv_mul_cancel   := @complex.inv_mul_cancel,
+  zero_ne_one      := complex.zero_ne_one,
+  inv_zero         := complex.inv_zero,
+  has_decidable_eq := complex.has_decidable_eq
+⦄
+
+-- TODO : we still need the whole family of coercion properties, for nat, int, rat
+
+-- coercions
+
+theorem of_rat_eq (a : ℚ) : of_rat a = of_real (real.of_rat a) := rfl
+
+theorem of_int_eq (a : ℤ) : of_int a = of_real (real.of_int a) := rfl
+
+theorem of_nat_eq (a : ℕ) : of_nat a = of_real (real.of_nat a) := rfl
+
+theorem of_rat.inj {x y : ℚ} (H : of_rat x = of_rat y) : x = y :=
+real.of_rat.inj (of_real.inj H)
+
+theorem eq_of_of_rat_eq_of_rat {x y : ℚ} (H : of_rat x = of_rat y) : x = y :=
+of_rat.inj H
+
+theorem of_rat_eq_of_rat_iff (x y : ℚ) : of_rat x = of_rat y ↔ x = y :=
+iff.intro eq_of_of_rat_eq_of_rat !congr_arg
+
+theorem of_int.inj {a b : ℤ} (H : of_int a = of_int b) : a = b :=
+rat.of_int.inj (of_rat.inj H)
+
+theorem eq_of_of_int_eq_of_int {a b : ℤ} (H : of_int a = of_int b) : a = b :=
+of_int.inj H
+
+theorem of_int_eq_of_int_iff (a b : ℤ) : of_int a = of_int b ↔ a = b :=
+iff.intro of_int.inj !congr_arg
+
+theorem of_nat.inj {a b : ℕ} (H : of_nat a = of_nat b) : a = b :=
+int.of_nat.inj (of_int.inj H)
+
+theorem eq_of_of_nat_eq_of_nat {a b : ℕ} (H : of_nat a = of_nat b) : a = b :=
+of_nat.inj H
+
+theorem of_nat_eq_of_nat_iff (a b : ℕ) : of_nat a = of_nat b ↔ a = b :=
+iff.intro of_nat.inj !congr_arg
+
+open rat
+
+theorem of_rat_add (a b : ℚ) : of_rat (a + b) = of_rat a + of_rat b :=
+by rewrite [of_rat_eq]
+
+theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a :=
+by rewrite [of_rat_eq]
+
+-- these show why we have to use krewrite in the next theorem: there are
+-- two different instances of "has_mul".
+
+-- set_option pp.notation false
+-- set_option pp.coercions true
+-- set_option pp.implicit true
+
+theorem of_rat_mul (a b : ℚ) : of_rat (a * b) = of_rat a * of_rat b :=
+by krewrite [of_rat_eq, real.of_rat_mul, of_real_mul]
+
+open int
+
+theorem of_int_add (a b : ℤ) : of_int (a + b) = of_int a + of_int b :=
+  by krewrite [of_int_eq, real.of_int_add, of_real_add]
+
+theorem of_int_neg (a : ℤ) : of_int (-a) = -of_int a :=
+  by krewrite [of_int_eq, real.of_int_neg, of_real_neg]
+
+theorem of_int_mul (a b : ℤ) : of_int (a * b) = of_int a * of_int b :=
+  by krewrite [of_int_eq, real.of_int_mul, of_real_mul]
+
+open nat
+
+theorem of_nat_add (a b : ℕ) : of_nat (a + b) = of_nat a + of_nat b :=
+  by krewrite [of_nat_eq, real.of_nat_add, of_real_add]
+
+theorem of_nat_mul (a b : ℕ) : of_nat (a * b) = of_nat a * of_nat b :=
+  by krewrite [of_nat_eq, real.of_nat_mul, of_real_mul]
+
+end complex
diff --git a/library/data/data.md b/library/data/data.md
index 9ed1e0669..b2e5196f8 100644
--- a/library/data/data.md
+++ b/library/data/data.md
@@ -15,7 +15,8 @@ Basic types:
 * [int](int/int.md) : the integers
 * [rat](rat/rat.md) : the rationals
 * [pnat](pnat.lean) : the positive natural numbers
-* [real](real.lean) : the real numbers 
+* [real](real/real.md) : the real numbers
+* [complex](complex.lean) : the complex numbers
 
 Constructors:
 
diff --git a/library/data/default.lean b/library/data/default.lean
index f98c9116b..07c9cbb77 100644
--- a/library/data/default.lean
+++ b/library/data/default.lean
@@ -5,4 +5,4 @@ Author: Jeremy Avigad
 -/
 import .empty .unit .bool .num .string .nat .int .rat .fintype
 import .prod .sum .sigma .option .quotient .list .finset .set .stream
-import .fin
+import .fin .real .complex