-
Notifications
You must be signed in to change notification settings - Fork 1
/
DArray.lean
147 lines (125 loc) · 4.31 KB
/
DArray.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
-- This intentionally only uses std, not mathlib
import Std.Data.Array.Lemmas
import Std.Data.Fin.Basic
import Std.Data.Fin.Lemmas
import Std.Tactic.Congr
import MemoNat.Any
set_option autoImplicit false
universe u
structure DArray (C : Nat → Sort u) : Type u:=
arr : Array Any.{u}
types : ∀ i (h : i < arr.size), (arr[i]).Sort = C i
attribute [simp] DArray.types
namespace DArray
def mkEmpty {C} (cap : Nat) : DArray C :=
⟨ Array.mkEmpty cap, λ _ hi => absurd hi (Nat.not_lt_zero _) ⟩
def size {C} (a : DArray C) := a.arr.size
def push {C} (a : DArray C) (x : C a.size) : DArray C :=
⟨ a.arr.push (Any.mk x),
by
cases a with | _ a types =>
dsimp
intro i hi
rewrite [Array.get_push]
split
case inl hi2 =>
apply types
case inr hi2 =>
rewrite [Array.size_push, <- Nat.succ_eq_add_one] at hi
have : i = Array.size a :=
Nat.le_antisymm (Nat.le_of_lt_succ hi) (Nat.le_of_not_lt hi2)
cases this
rfl
⟩
theorem size_push {C} (a : DArray C) (x : C a.size) : (a.push x).size = a.size + 1 :=
Array.size_push _ _
def get {C : Nat → Sort u} (a : DArray C) (i : Fin a.size) : C i :=
let x : Any := Array.get a.arr i
a.types i.1 i.2 ▸ x.val
theorem get_push {C} (a : DArray C) (x : C a.size) (i : Fin (a.push x).size) :
(a.push x).get i =
if h : i < a.size
then a.get ⟨i, h⟩
else
have : size a = i := Nat.le_antisymm
(Nat.le_of_not_lt h)
(Nat.le_of_lt_succ (by simpa [a.size_push x] using i.isLt))
(this ▸ x : C i) := by
apply Any.mk_inj
unfold DArray.get
simp only [Any.mk_eq_rec', Any.mk_val]
apply (Array.get_push a.arr (Any.mk x) i.val i.isLt).trans
unfold DArray.size
split
case inl _ =>
simp only [Any.mk_eq_rec']
rfl
case inr hi2 =>
simp only [Any.mk_eq_rec]
protected def ofFn {C} (n : Nat) (f : (i : Fin n) → C i) : DArray C :=
⟨ .ofFn fun i => Any.mk (f i), by simp ⟩
protected theorem size_ofFn {C : Nat → Sort _} (n : Nat) (f : (i : Fin n) → C i) :
(DArray.ofFn n f).size = n := by
dsimp [DArray.size, DArray.ofFn]
exact Array.size_ofFn _
protected theorem get_ofFn {C : Nat → Sort _} (n : Nat) (f : (i : Fin n) → C i)
(i : Fin (size (DArray.ofFn n f))) : (DArray.ofFn n f).get i =
f (i.cast (DArray.size_ofFn n f)) := by
dsimp [DArray.get, DArray.size, DArray.ofFn]
apply Any.eq_rec_val
simp only [Array.getElem_ofFn, Any.mk.injEq, heq_eq_eq, true_and]
rfl
@[ext]
theorem ext {C} (a b : DArray C)
(h₁ : a.size = b.size)
(h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
: a = b := by
cases a with | _ a ha =>
cases b with | _ b hb =>
simp only [mk.injEq]
apply Array.ext
· exact h₁
· clear h₁
intro i hi₁ hi₂
specialize h₂ i hi₁ hi₂
unfold DArray.get at h₂
simp only [Array.get_eq_getElem, Any.eq_rec_val_iff, Any.mk_eq_rec'] at h₂
assumption
theorem _root_.List.length_dropLast {α} (xs : List α) :
xs.dropLast.length = xs.length - 1 := by
match xs with
| [] => rfl
| x::xs => simp [Nat.succ_sub_succ_eq_sub]
theorem _root_.List.get_dropLast {α} (xs : List α) (i : Fin xs.dropLast.length) :
xs.dropLast.get i = xs.get (i.castLE (xs.length_dropLast ▸ Nat.sub_le _ _ )) := by
cases i with | _ i hi =>
induction i generalizing xs
case zero =>
cases xs
case nil => rfl
case cons x xs =>
cases xs
case nil => simp at hi
case cons => rfl
case succ i IH =>
cases xs
case nil => rfl
case cons x xs =>
cases xs
case nil => apply False.elim (Nat.not_lt_zero _ hi)
case cons y ys => apply IH
@[simp] theorem _root_.Array.getElem_pop {α} (a : Array α) (i : Nat) (hi : i < a.pop.size) :
a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) :=
List.get_dropLast _ _
def pop {C} (a : DArray C) : DArray C :=
⟨a.arr.pop, by simp ⟩
theorem size_pop {C} (a : DArray C) :
a.pop.size = a.size - 1 := Array.size_pop _
@[simp]
theorem get_pop {C} (a : DArray C) (i : Fin a.pop.size):
a.pop.get i = a.get (i.castLE (a.size_pop ▸ Nat.sub_le _ _)) := by
unfold DArray.pop DArray.get
apply Any.eq_rec_val
simp only [Array.get_eq_getElem, Array.getElem_pop, Fin.coe_castLE,
Any.mk_eq_rec', Any.mk_val]
end DArray