Skip to content

Commit b7ef81c

Browse files
digama0kim-em
digama0
and
kim-em
committed
feat: align init.data.int.{basic, order} (#583)
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
1 parent 61b52b9 commit b7ef81c

File tree

8 files changed

+191
-58
lines changed

8 files changed

+191
-58
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -72,7 +72,7 @@ import Mathlib.Init.Core
7272
import Mathlib.Init.Data.Bool.Basic
7373
import Mathlib.Init.Data.Bool.Lemmas
7474
import Mathlib.Init.Data.Fin.Basic
75-
import Mathlib.Init.Data.Int.Notation
75+
import Mathlib.Init.Data.Int.Basic
7676
import Mathlib.Init.Data.Int.Order
7777
import Mathlib.Init.Data.Nat.Basic
7878
import Mathlib.Init.Data.Nat.Lemmas

‎Mathlib/Algebra/Group/Defs.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura, Simon Hudon, Mario Carneiro
66
import Mathlib.Tactic.Spread
77
import Mathlib.Tactic.ToAdditive
88
import Mathlib.Init.ZeroOne
9-
import Mathlib.Init.Data.Int.Notation
9+
import Mathlib.Init.Data.Int.Basic
1010
import Mathlib.Data.List.Basic
1111

1212
/-!

‎Mathlib/Data/Int/Basic.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Authors: Jeremy Avigad
55
-/
66
import Std
77
import Mathlib.Tactic.Convert
8-
import Mathlib.Init.Data.Int.Notation
8+
import Mathlib.Init.Data.Int.Basic
99
import Mathlib.Algebra.Ring.Basic
1010

1111
/-!

‎Mathlib/Init/Align.lean‎

Lines changed: 0 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -93,17 +93,6 @@ actual theorems in the files.
9393

9494
#align fin.elim0 Fin.elim0ₓ
9595

96-
/-! ## `init.data.int.basic` -/
97-
98-
-- TODO: backport?
99-
#align int.neg_succ_of_nat Int.negSucc
100-
101-
/-! ## `init.data.int.order` -/
102-
103-
#align int.nonneg Int.NonNeg
104-
#align int.le Int.le
105-
#align int.lt Int.lt
106-
10796
/-! ## `init.data.int.comp_lemmas` -/
10897

10998
/-! ## `init.data.int.default` -/

‎Mathlib/Init/Data/Int/Basic.lean‎

Lines changed: 132 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,132 @@
1+
/-
2+
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Jeremy Avigad
5+
6+
The integers, with addition, multiplication, and subtraction.
7+
-/
8+
import Mathlib.Mathport.Rename
9+
import Mathlib.Init.Data.Nat.Basic
10+
import Mathlib.Init.ZeroOne
11+
import Std.Data.Int.Lemmas
12+
13+
open Nat
14+
15+
-- TODO: backport?
16+
#align int.neg_succ_of_nat Int.negSucc
17+
18+
-- @[inherit_doc]
19+
notation "ℤ" => Int
20+
21+
namespace Int
22+
23+
/-- The number `0 : ℤ`, as a standalone definition. -/
24+
@[deprecated] protected def zero : ℤ := ofNat 0
25+
26+
/-- The number `1 : ℤ`, as a standalone definition. -/
27+
@[deprecated] protected def one : ℤ := ofNat 1
28+
29+
#align int.of_nat_zero Int.ofNat_zero
30+
#align int.of_nat_one Int.ofNat_one
31+
#align int.sub_nat_nat_of_sub_eq_zero Int.subNatNat_of_sub_eq_zero
32+
#align int.sub_nat_nat_of_sub_eq_succ Int.subNatNat_of_sub_eq_succ
33+
#align int.of_nat_add Int.ofNat_add
34+
#align int.of_nat_mul Int.ofNat_mul
35+
#align int.of_nat_succ Int.ofNat_succ
36+
#align int.neg_of_nat_of_succ Int.neg_ofNat_of_succ
37+
38+
theorem neg_negSucc (n : ℕ) : - -[n+1] = ofNat (succ n) := rfl
39+
#align int.neg_neg_of_nat_succ Int.neg_negSucc
40+
41+
@[deprecated, nolint synTaut]
42+
theorem ofNat_eq_coe (n : ℕ) : ofNat n = ↑n := rfl
43+
#align int.of_nat_eq_coe Int.ofNat_eq_coe
44+
45+
#align int.neg_succ_of_nat_coe Int.negSucc_coe
46+
#align int.coe_nat_add Int.ofNat_add
47+
#align int.coe_nat_mul Int.ofNat_mul
48+
#align int.coe_nat_zero Int.ofNat_zero
49+
#align int.coe_nat_one Int.ofNat_one
50+
#align int.coe_nat_succ Int.ofNat_succ
51+
52+
protected theorem ofNat_add_out (m n : ℕ) : ↑m + ↑n = (↑(m + n) : ℤ) := rfl
53+
#align int.coe_nat_add_out Int.ofNat_add_out
54+
55+
protected theorem ofNat_mul_out (m n : ℕ) : ↑m * ↑n = (↑(m * n) : ℤ) := rfl
56+
#align int.coe_nat_mul_out Int.ofNat_mul_out
57+
58+
protected theorem ofNat_add_one_out (n : ℕ) : ↑n + (1 : ℤ) = ↑(succ n) := rfl
59+
#align int.coe_nat_add_one_out Int.ofNat_add_one_out
60+
61+
#align int.of_nat_add_of_nat Int.ofNat_add_ofNat
62+
63+
#align int.of_nat_add_neg_succ_of_nat Int.ofNat_add_negSucc
64+
#align int.neg_succ_of_nat_add_of_nat Int.negSucc_add_ofNat
65+
#align int.neg_succ_of_nat_add_neg_succ_of_nat Int.negSucc_add_negSucc
66+
#align int.of_nat_mul_of_nat Int.ofNat_mul_ofNat
67+
#align int.of_nat_mul_neg_succ_of_nat Int.ofNat_mul_negSucc'
68+
#align int.neg_succ_of_nat_of_nat Int.negSucc_mul_ofNat'
69+
#align int.mul_neg_succ_of_nat_neg_succ_of_nat Int.negSucc_mul_negSucc'
70+
71+
#align int.coe_nat_inj Int.ofNat.inj
72+
#align int.of_nat_eq_of_nat_iff Int.ofNat_inj
73+
#align int.coe_nat_eq_coe_nat_iff Int.ofNat_inj
74+
#align int.neg_succ_of_nat_inj_iff Int.negSucc_inj
75+
#align int.neg_succ_of_nat_eq Int.negSucc_eq
76+
77+
protected theorem neg_eq_neg {a b : ℤ} (h : -a = -b) : a = b := Int.neg_inj.1 h
78+
#align int.neg_inj Int.neg_eq_neg
79+
80+
#align int.sub_nat_nat_elim Int.subNatNat_elim
81+
#align int.sub_nat_nat_add_left Int.subNatNat_add_left
82+
#align int.sub_nat_nat_add_right Int.subNatNat_add_right
83+
#align int.sub_nat_nat_add_add Int.subNatNat_add_add
84+
#align int.sub_nat_nat_of_le Int.subNatNat_of_le
85+
#align int.sub_nat_nat_of_lt Int.subNatNat_of_lt
86+
#align int.nat_abs_of_nat Int.natAbs_ofNat
87+
88+
@[deprecated natAbs_eq_zero]
89+
theorem eq_zero_of_natAbs_eq_zero : ∀ {a : ℤ}, natAbs a = 0 → a = 0 := natAbs_eq_zero.1
90+
#align int.eq_zero_of_nat_abs_eq_zero Int.eq_zero_of_natAbs_eq_zero
91+
92+
@[deprecated natAbs_pos]
93+
theorem natAbs_pos_of_ne_zero {a : ℤ} (h : a ≠ 0) : 0 < natAbs a := natAbs_pos.2 h
94+
#align int.nat_abs_pos_of_ne_zero Int.natAbs_pos_of_ne_zero
95+
96+
#align int.nat_abs_zero Int.natAbs_zero
97+
#align int.nat_abs_one Int.natAbs_one
98+
#align int.nat_abs_mul_self Int.natAbs_mul_self
99+
#align int.nat_abs_neg Int.natAbs_neg
100+
#align int.nat_abs_eq Int.natAbs_eq
101+
#align int.eq_coe_or_neg Int.eq_nat_or_neg
102+
103+
#align int.div Int.ediv
104+
#align int.mod Int.emod
105+
#align int.quot Int.div
106+
#align int.rem Int.mod
107+
108+
#align int.sub_nat_nat_sub Int.subNatNat_subₓ -- reordered implicits
109+
#align int.sub_nat_nat_add Int.subNatNat_add
110+
#align int.sub_nat_nat_add_neg_succ_of_nat Int.subNatNat_add_negSucc
111+
112+
#align int.add_assoc_aux1 Int.add_assoc.aux1
113+
#align int.add_assoc_aux2 Int.add_assoc.aux2
114+
115+
#align int.sub_nat_self Int.subNatNat_self
116+
117+
#align int.of_nat_mul_neg_of_nat Int.ofNat_mul_negOfNat
118+
#align int.neg_of_nat_mul_of_nat Int.negOfNat_mul_ofNat
119+
#align int.neg_succ_of_nat_mul_neg_of_nat Int.negSucc_mul_negOfNat
120+
#align int.neg_of_nat_mul_neg_succ_of_nat Int.negOfNat_mul_negSucc
121+
#align int.neg_of_nat_eq_sub_nat_nat_zero Int.negOfNat_eq_subNatNat_zero
122+
#align int.of_nat_mul_sub_nat_nat Int.ofNat_mul_subNatNat
123+
#align int.neg_of_nat_add Int.negOfNat_add
124+
#align int.neg_succ_of_nat_mul_sub_nat_nat Int.negSucc_mul_subNatNat
125+
#align int.distrib_left Int.mul_add
126+
#align int.distrib_right Int.add_mul
127+
#align int.of_nat_sub Int.ofNat_subₓ -- reordered implicits
128+
#align int.neg_succ_of_nat_coe' Int.negSucc_coe'
129+
#align int.coe_nat_sub Int.ofNat_sub
130+
#align int.sub_nat_nat_eq_coe Int.subNatNat_eq_coe
131+
#align int.to_nat_sub Int.toNat_sub
132+
#align int.sign_mul_nat_abs Int.sign_mul_natAbs

‎Mathlib/Init/Data/Int/Notation.lean‎

Lines changed: 0 additions & 9 deletions
This file was deleted.

‎Mathlib/Init/Data/Int/Order.lean‎

Lines changed: 51 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,14 +5,44 @@ Authors: Jeremy Avigad
55
-/
66

77
import Mathlib.Init.Algebra.Order
8-
import Mathlib.Init.Data.Int.Notation
8+
import Mathlib.Init.Data.Int.Basic
99

1010
/-! # The order relation on the integers -/
1111

1212
open Nat
1313

1414
namespace Int
1515

16+
#align int.nonneg Int.NonNeg
17+
#align int.le Int.le
18+
#align int.lt Int.lt
19+
20+
export private decNonneg from Init.Data.Int.Basic
21+
#align int.decidable_nonneg Int.decNonneg
22+
#align int.decidable_le Int.decLe
23+
#align int.decidable_lt Int.decLt
24+
25+
theorem le.elim {a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ n : ℕ, a + ↑n = b → P) : P :=
26+
Exists.elim (le.dest h) h'
27+
#align int.le.elim Int.le.elim
28+
29+
alias ofNat_le ↔ le_of_ofNat_le_ofNat ofNat_le_ofNat_of_le
30+
#align int.coe_nat_le_coe_nat_of_le Int.ofNat_le_ofNat_of_le
31+
#align int.le_of_coe_nat_le_coe_nat Int.le_of_ofNat_le_ofNat
32+
#align int.coe_nat_le_coe_nat_iff Int.ofNat_le
33+
34+
#align int.coe_zero_le Int.ofNat_zero_le
35+
#align int.eq_coe_of_zero_le Int.eq_ofNat_of_zero_le
36+
37+
theorem lt.elim {a b : ℤ} (h : a < b) {P : Prop} (h' : ∀ n : ℕ, a + ↑(Nat.succ n) = b → P) : P :=
38+
Exists.elim (lt.dest h) h'
39+
#align int.lt.elim Int.lt.elim
40+
41+
alias ofNat_lt ↔ lt_of_ofNat_lt_ofNat ofNat_lt_ofNat_of_lt
42+
#align int.coe_nat_lt_coe_nat_iff Int.ofNat_lt
43+
#align int.lt_of_coe_nat_lt_coe_nat Int.lt_of_ofNat_lt_ofNat
44+
#align int.coe_nat_lt_coe_nat_of_lt Int.ofNat_lt_ofNat_of_lt
45+
1646
instance : LinearOrder ℤ where
1747
le := (·≤·)
1848
le_refl := Int.le_refl
@@ -24,3 +54,23 @@ instance : LinearOrder ℤ where
2454
decidable_eq := by infer_instance
2555
decidable_le := by infer_instance
2656
decidable_lt := by infer_instance
57+
58+
#align int.eq_nat_abs_of_zero_le Int.eq_natAbs_of_zero_le
59+
#align int.le_nat_abs Int.le_natAbs
60+
#align int.neg_succ_lt_zero Int.negSucc_lt_zero
61+
#align int.eq_neg_succ_of_lt_zero Int.eq_negSucc_of_lt_zero
62+
#align int.sub_eq_zero_iff_eq Int.sub_eq_zero
63+
64+
theorem neg_mul_eq_neg_mul_symm (a b : ℤ) : -a * b = -(a * b) := (Int.neg_mul_eq_neg_mul a b).symm
65+
#align int.neg_mul_eq_neg_mul_symm Int.neg_mul_eq_neg_mul_symm
66+
67+
theorem mul_neg_eq_neg_mul_symm (a b : ℤ) : a * -b = -(a * b) := (Int.neg_mul_eq_mul_neg a b).symm
68+
#align int.mul_neg_eq_neg_mul_symm Int.mul_neg_eq_neg_mul_symm
69+
70+
#align int.of_nat_nonneg Int.ofNat_nonneg
71+
#align int.coe_succ_pos Int.ofNat_succ_pos
72+
#align int.exists_eq_neg_of_nat Int.exists_eq_neg_ofNat
73+
#align int.nat_abs_of_nonneg Int.natAbs_of_nonneg
74+
#align int.of_nat_nat_abs_of_nonpos Int.ofNat_natAbs_of_nonpos
75+
76+
alias mul_eq_zero ↔ eq_zero_or_eq_zero_of_mul_eq_zero _

0 commit comments

Comments
 (0)