-
Notifications
You must be signed in to change notification settings - Fork 330
/
Basic.lean
173 lines (137 loc) · 4.49 KB
/
Basic.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
/-
Copyright (c) 2016 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Leonardo de Moura
The integers, with addition, multiplication, and subtraction.
-/
prelude
import Init.Coe
import Init.Data.Nat.Div
import Init.Data.List.Basic
open Nat
/- the Type, coercions, and notation -/
inductive Int : Type where
| ofNat : Nat → Int
| negSucc : Nat → Int
attribute [extern "lean_nat_to_int"] Int.ofNat
attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc
instance : Coe Nat Int := ⟨Int.ofNat⟩
instance : OfNat Int n where
ofNat := Int.ofNat n
namespace Int
instance : Inhabited Int := ⟨ofNat 0⟩
def negOfNat : Nat → Int
| 0 => 0
| succ m => negSucc m
set_option bootstrap.genMatcherCode false in
@[extern "lean_int_neg"]
protected def neg (n : @& Int) : Int :=
match n with
| ofNat n => negOfNat n
| negSucc n => succ n
def subNatNat (m n : Nat) : Int :=
match (n - m : Nat) with
| 0 => ofNat (m - n) -- m ≥ n
| (succ k) => negSucc k
set_option bootstrap.genMatcherCode false in
@[extern "lean_int_add"]
protected def add (m n : @& Int) : Int :=
match m, n with
| ofNat m, ofNat n => ofNat (m + n)
| ofNat m, negSucc n => subNatNat m (succ n)
| negSucc m, ofNat n => subNatNat n (succ m)
| negSucc m, negSucc n => negSucc (succ (m + n))
set_option bootstrap.genMatcherCode false in
@[extern "lean_int_mul"]
protected def mul (m n : @& Int) : Int :=
match m, n with
| ofNat m, ofNat n => ofNat (m * n)
| ofNat m, negSucc n => negOfNat (m * succ n)
| negSucc m, ofNat n => negOfNat (succ m * n)
| negSucc m, negSucc n => ofNat (succ m * succ n)
/-
The `Neg Int` default instance must have priority higher than `low` since
the default instance `OfNat Nat n` has `low` priority.
```
#check -42
```
-/
@[defaultInstance mid]
instance : Neg Int where
neg := Int.neg
instance : Add Int where
add := Int.add
instance : Mul Int where
mul := Int.mul
@[extern "lean_int_sub"]
protected def sub (m n : @& Int) : Int :=
m + (- n)
instance : Sub Int where
sub := Int.sub
inductive NonNeg : Int → Prop where
| mk (n : Nat) : NonNeg (ofNat n)
protected def le (a b : Int) : Prop := NonNeg (b - a)
instance : LE Int where
le := Int.le
protected def lt (a b : Int) : Prop := (a + 1) ≤ b
instance : LT Int where
lt := Int.lt
set_option bootstrap.genMatcherCode false in
@[extern "lean_int_dec_eq"]
protected def decEq (a b : @& Int) : Decidable (a = b) :=
match a, b with
| ofNat a, ofNat b => match decEq a b with
| isTrue h => isTrue <| h ▸ rfl
| isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
| negSucc a, negSucc b => match decEq a b with
| isTrue h => isTrue <| h ▸ rfl
| isFalse h => isFalse <| fun h' => Int.noConfusion h' (fun h' => absurd h' h)
| ofNat a, negSucc b => isFalse <| fun h => Int.noConfusion h
| negSucc a, ofNat b => isFalse <| fun h => Int.noConfusion h
instance : DecidableEq Int := Int.decEq
set_option bootstrap.genMatcherCode false in
@[extern "lean_int_dec_nonneg"]
private def decNonneg (m : @& Int) : Decidable (NonNeg m) :=
match m with
| ofNat m => isTrue <| NonNeg.mk m
| negSucc m => isFalse <| fun h => nomatch h
@[extern "lean_int_dec_le"]
instance decLe (a b : @& Int) : Decidable (a ≤ b) :=
decNonneg _
@[extern "lean_int_dec_lt"]
instance decLt (a b : @& Int) : Decidable (a < b) :=
decNonneg _
set_option bootstrap.genMatcherCode false in
@[extern "lean_nat_abs"]
def natAbs (m : @& Int) : Nat :=
match m with
| ofNat m => m
| negSucc m => m.succ
instance : OfNat Int n where
ofNat := Int.ofNat n
@[extern "lean_int_div"]
def div : (@& Int) → (@& Int) → Int
| ofNat m, ofNat n => ofNat (m / n)
| ofNat m, negSucc n => -ofNat (m / succ n)
| negSucc m, ofNat n => -ofNat (succ m / n)
| negSucc m, negSucc n => ofNat (succ m / succ n)
@[extern "lean_int_mod"]
def mod : (@& Int) → (@& Int) → Int
| ofNat m, ofNat n => ofNat (m % n)
| ofNat m, negSucc n => ofNat (m % succ n)
| negSucc m, ofNat n => -ofNat (succ m % n)
| negSucc m, negSucc n => -ofNat (succ m % succ n)
instance : Div Int where
div := Int.div
instance : Mod Int where
mod := Int.mod
def toNat : Int → Nat
| ofNat n => n
| negSucc n => 0
def natMod (m n : Int) : Nat := (m % n).toNat
protected def pow (m : Int) : Nat → Int
| 0 => 1
| succ n => Int.pow m n * m
instance : HPow Int Nat Int where
hPow := Int.pow
end Int