-
Notifications
You must be signed in to change notification settings - Fork 335
/
Basic.lean
117 lines (84 loc) · 3.01 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
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Data.Nat.Div
import Init.Data.Nat.Bitwise
import Init.Coe
open Nat
namespace Fin
instance coeToNat {n} : Coe (Fin n) Nat :=
⟨fun v => v.val⟩
def elim0.{u} {α : Sort u} : Fin 0 → α
| ⟨_, h⟩ => absurd h (not_lt_zero _)
variable {n : Nat}
protected def ofNat {n : Nat} (a : Nat) : Fin (succ n) :=
⟨a % succ n, Nat.mod_lt _ (Nat.zero_lt_succ _)⟩
protected def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
⟨a % n, Nat.mod_lt _ h⟩
private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
| 0, h => Nat.mod_lt _ h
| a+1, h =>
have : n > 0 := Nat.lt_trans (Nat.zero_lt_succ _) h;
Nat.mod_lt _ this
protected def add : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, mlt h⟩
protected def mul : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a * b) % n, mlt h⟩
protected def sub : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
/-
Remark: mod/div/modn/land/lor can be defined without using (% n), but
we are trying to minimize the number of Nat theorems
needed to boostrap Lean.
-/
protected def mod : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a % b) % n, mlt h⟩
protected def div : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a / b) % n, mlt h⟩
protected def modn : Fin n → Nat → Fin n
| ⟨a, h⟩, m => ⟨(a % m) % n, mlt h⟩
def land : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.land a b) % n, mlt h⟩
def lor : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
def xor : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.xor a b) % n, mlt h⟩
def shiftLeft : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a <<< b) % n, mlt h⟩
def shiftRight : Fin n → Fin n → Fin n
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a >>> b) % n, mlt h⟩
instance : Add (Fin n) where
add := Fin.add
instance : Sub (Fin n) where
sub := Fin.sub
instance : Mul (Fin n) where
mul := Fin.mul
instance : Mod (Fin n) where
mod := Fin.mod
instance : Div (Fin n) where
div := Fin.div
instance : AndOp (Fin n) where
and := Fin.land
instance : OrOp (Fin n) where
or := Fin.lor
instance : Xor (Fin n) where
xor := Fin.xor
instance : ShiftLeft (Fin n) where
shiftLeft := Fin.shiftLeft
instance : ShiftRight (Fin n) where
shiftRight := Fin.shiftRight
instance : HMod (Fin n) Nat (Fin n) where
hMod := Fin.modn
instance : OfNat (Fin (no_index (n+1))) i where
ofNat := Fin.ofNat i
instance : Inhabited (Fin (no_index (n+1))) where
default := 0
theorem val_ne_of_ne {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
fun h' => absurd (eq_of_val_eq h') h
theorem modn_lt : ∀ {m : Nat} (i : Fin n), m > 0 → (i % m).val < m
| m, ⟨a, h⟩, hp => Nat.lt_of_le_of_lt (mod_le _ _) (mod_lt _ hp)
end Fin
open Fin