From 92af727daffd4da88f7ffc45eaccb43806b64784 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 27 Aug 2015 09:39:39 -0400 Subject: [PATCH] fix(library/data/real/{basic,division,order}: use notation for 0 and 1 These changes were needed because e.g. real.add_zero was "x + zero = x", and rewrite would not match it to a goal "t + 0". The fix was a lot harder than I expected. At first, migrate failed with resource errors. In the end, what worked was this: I defined the coercion from num to real directly (rather than infer num -> nat -> int -> rat -> real). I still don't understand what the issues are, though. There are subtle issues with numerals and coercions and migrate. (We are not alone. Isabelle also suffers from the fact that there are too many "zero"s and "one"s.) --- library/data/rat/basic.lean | 2 +- library/data/real/basic.lean | 33 ++++++++++++++++++--------------- library/data/real/division.lean | 10 +++++----- library/data/real/order.lean | 6 ++---- 4 files changed, 26 insertions(+), 25 deletions(-) diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index b584aaa01..03edc762f 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -512,7 +512,7 @@ section migrate_algebra add_comm := add.comm, mul := mul, mul_assoc := mul.assoc, - one := (of_num 1), + one := 1, one_mul := one_mul, mul_one := mul_one, left_distrib := mul.left_distrib, diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index d161ee493..4f642e9f8 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -1029,10 +1029,17 @@ definition neg (x : ℝ) : ℝ := quot.sound (rneg_well_defined Hab))) prefix [priority real.prio] `-` := neg -definition zero : ℝ := quot.mk r_zero +open rat -- no coercions before + +definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (s.r_const a) +definition of_num [coercion] [reducible] (n : num) : ℝ := of_rat (rat.of_num n) + +--definition zero : ℝ := 0 +--definition one : ℝ := 1 +--definition zero : ℝ := quot.mk r_zero --notation 0 := zero -definition one : ℝ := quot.mk r_one +--definition one : ℝ := quot.mk r_one theorem add_comm (x y : ℝ) : x + y = y + x := quot.induction_on₂ x y (λ s t, quot.sound (r_add_comm s t)) @@ -1040,13 +1047,13 @@ theorem add_comm (x y : ℝ) : x + y = y + x := theorem add_assoc (x y z : ℝ) : x + y + z = x + (y + z) := quot.induction_on₃ x y z (λ s t u, quot.sound (r_add_assoc s t u)) -theorem zero_add (x : ℝ) : zero + x = x := +theorem zero_add (x : ℝ) : 0 + x = x := quot.induction_on x (λ s, quot.sound (r_zero_add s)) -theorem add_zero (x : ℝ) : x + zero = x := +theorem add_zero (x : ℝ) : x + 0 = x := quot.induction_on x (λ s, quot.sound (r_add_zero s)) -theorem neg_cancel (x : ℝ) : -x + x = zero := +theorem neg_cancel (x : ℝ) : -x + x = 0 := quot.induction_on x (λ s, quot.sound (r_neg_cancel s)) theorem mul_assoc (x y z : ℝ) : x * y * z = x * (y * z) := @@ -1055,10 +1062,10 @@ theorem mul_assoc (x y z : ℝ) : x * y * z = x * (y * z) := theorem mul_comm (x y : ℝ) : x * y = y * x := quot.induction_on₂ x y (λ s t, quot.sound (r_mul_comm s t)) -theorem one_mul (x : ℝ) : one * x = x := +theorem one_mul (x : ℝ) : 1 * x = x := quot.induction_on x (λ s, quot.sound (r_one_mul s)) -theorem mul_one (x : ℝ) : x * one = x := +theorem mul_one (x : ℝ) : x * 1 = x := quot.induction_on x (λ s, quot.sound (r_mul_one s)) theorem distrib (x y z : ℝ) : x * (y + z) = x * y + x * z := @@ -1067,8 +1074,8 @@ theorem distrib (x y z : ℝ) : x * (y + z) = x * y + x * z := theorem distrib_l (x y z : ℝ) : (x + y) * z = x * z + y * z := by rewrite [mul_comm, distrib, {x * _}mul_comm, {y * _}mul_comm] -- this shouldn't be necessary -theorem zero_ne_one : ¬ zero = one := - take H : zero = one, +theorem zero_ne_one : ¬ (0 : ℝ) = 1 := + take H : 0 = 1, absurd (quot.exact H) (r_zero_nequiv_one) protected definition comm_ring [reducible] : algebra.comm_ring ℝ := @@ -1076,7 +1083,7 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ := fapply algebra.comm_ring.mk, exact add, exact add_assoc, - exact zero, + exact of_num 0, exact zero_add, exact add_zero, exact neg, @@ -1084,7 +1091,7 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ := exact add_comm, exact mul, exact mul_assoc, - apply one, + apply of_num 1, apply one_mul, apply mul_one, apply distrib, @@ -1092,10 +1099,6 @@ protected definition comm_ring [reducible] : algebra.comm_ring ℝ := apply mul_comm end -open rat -- no coercions before - -definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (s.r_const a) - theorem of_rat_add (a b : ℚ) : of_rat a + of_rat b = of_rat (a + b) := quot.sound (s.r_add_consts a b) diff --git a/library/data/real/division.lean b/library/data/real/division.lean index b91cdfb36..734dc7adc 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -584,10 +584,10 @@ postfix [priority real.prio] `⁻¹` := inv theorem le_total (x y : ℝ) : x ≤ y ∨ y ≤ x := quot.induction_on₂ x y (λ s t, s.r_le_total s t) -theorem mul_inv' (x : ℝ) : x ≢ zero → x * x⁻¹ = one := +theorem mul_inv' (x : ℝ) : x ≢ 0 → x * x⁻¹ = 1 := quot.induction_on x (λ s H, quot.sound (s.r_mul_inv s H)) -theorem inv_mul' (x : ℝ) : x ≢ zero → x⁻¹ * x = one := +theorem inv_mul' (x : ℝ) : x ≢ 0 → x⁻¹ * x = 1 := by rewrite real.mul_comm; apply mul_inv' theorem neq_of_sep {x y : ℝ} (H : x ≢ y) : ¬ x = y := @@ -599,11 +599,11 @@ theorem sep_of_neq {x y : ℝ} : ¬ x = y → x ≢ y := theorem sep_is_neq (x y : ℝ) : (x ≢ y) = (¬ x = y) := propext (iff.intro neq_of_sep sep_of_neq) -theorem mul_inv (x : ℝ) : x ≠ zero → x * x⁻¹ = one := !sep_is_neq ▸ !mul_inv' +theorem mul_inv (x : ℝ) : x ≠ 0 → x * x⁻¹ = 1 := !sep_is_neq ▸ !mul_inv' -theorem inv_mul (x : ℝ) : x ≠ zero → x⁻¹ * x = one := !sep_is_neq ▸ !inv_mul' +theorem inv_mul (x : ℝ) : x ≠ 0 → x⁻¹ * x = 1 := !sep_is_neq ▸ !inv_mul' -theorem inv_zero : zero⁻¹ = zero := quot.sound (s.r_inv_zero) +theorem inv_zero : (0 : ℝ)⁻¹ = 0 := quot.sound (s.r_inv_zero) theorem lt_or_eq_of_le (x y : ℝ) : x ≤ y → x < y ∨ x = y := quot.induction_on₂ x y (λ s t H, or.elim (s.r_lt_or_equiv_of_le s t H) diff --git a/library/data/real/order.lean b/library/data/real/order.lean index 7dbddd440..bb8b22982 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -17,8 +17,6 @@ local notation 0 := rat.of_num 0 local notation 1 := rat.of_num 1 local notation 2 := subtype.tag (of_num 2) dec_trivial ----------------------------------------------------------------------------------------------------- - namespace s definition pos (s : seq) := ∃ n : ℕ+, n⁻¹ < (s n) @@ -1026,8 +1024,8 @@ definition lt (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_lt a b) s.r_lt_wel infix [priority real.prio] `<` := lt definition le (x y : ℝ) := quot.lift_on₂ x y (λ a b, s.r_le a b) s.r_le_well_defined -infix [priority real.prio] `≤` := le infix [priority real.prio] `<=` := le +infix [priority real.prio] `≤` := le definition gt [reducible] (a b : ℝ) := lt b a definition ge [reducible] (a b : ℝ) := le b a @@ -1084,7 +1082,7 @@ theorem add_lt_add_left_var (x y z : ℝ) : x < y → z + x < z + y := theorem add_lt_add_left (x y : ℝ) : x < y → ∀ z : ℝ, z + x < z + y := take H z, add_lt_add_left_var x y z H -theorem zero_lt_one : zero < one := s.r_zero_lt_one +theorem zero_lt_one : (0 : ℝ) < (1 : ℝ) := s.r_zero_lt_one theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y := (quot.induction_on₂ x y (λ s t H, or.elim H (take H', begin