chore: move Core.lean to new frontend
This commit is contained in:
Leonardo de Moura
parent
5a130c6393
commit
1d338c4fc4
10 changed files with 792 additions and 1033 deletions
1660
src/Init/Core.lean
1660
src/Init/Core.lean
File diff suppressed because it is too large
Load diff
|
|
@ -81,8 +81,6 @@ def land : Fin n → Fin n → Fin n
|
|||
def lor : Fin n → Fin n → Fin n
|
||||
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(Nat.lor a b) % n, mlt h⟩
|
||||
|
||||
instance : HasZero (Fin (succ n)) := ⟨⟨0, succPos n⟩⟩
|
||||
instance : HasOne (Fin (succ n)) := ⟨ofNat 1⟩
|
||||
instance : HasAdd (Fin n) := ⟨Fin.add⟩
|
||||
instance : HasSub (Fin n) := ⟨Fin.sub⟩
|
||||
instance : HasMul (Fin n) := ⟨Fin.mul⟩
|
||||
|
|
|
|||
|
|
@ -45,8 +45,6 @@ def Float.lt : Float → Float → Prop := fun a b =>
|
|||
def Float.le : Float → Float → Prop := fun a b =>
|
||||
floatSpec.le a.val b.val
|
||||
|
||||
instance : HasZero Float := ⟨Float.ofNat 0⟩
|
||||
instance : HasOne Float := ⟨Float.ofNat 1⟩
|
||||
instance : HasOfNat Float := ⟨Float.ofNat⟩
|
||||
instance : HasAdd Float := ⟨Float.add⟩
|
||||
instance : HasSub Float := ⟨Float.sub⟩
|
||||
|
|
|
|||
|
|
@ -25,11 +25,6 @@ attribute [extern "lean_int_neg_succ_of_nat"] Int.negSucc
|
|||
instance : Coe Nat Int := ⟨Int.ofNat⟩
|
||||
|
||||
namespace Int
|
||||
protected def zero : Int := ofNat 0
|
||||
protected def one : Int := ofNat 1
|
||||
|
||||
instance : HasZero Int := ⟨Int.zero⟩
|
||||
instance : HasOne Int := ⟨Int.one⟩
|
||||
instance : Inhabited Int := ⟨ofNat 0⟩
|
||||
|
||||
def negOfNat : Nat → Int
|
||||
|
|
|
|||
|
|
@ -330,7 +330,7 @@ instance hasDecidableLt [HasLess α] [h : DecidableRel (α:=α) (·<·)] : (l₁
|
|||
instance [HasLess α] : HasLessEq (List α) := ⟨List.LessEq⟩
|
||||
|
||||
instance [HasLess α] [h : DecidableRel (HasLess.Less : α → α → Prop)] : (l₁ l₂ : List α) → Decidable (l₁ ≤ l₂) :=
|
||||
fun a b => Not.Decidable
|
||||
fun a b => inferInstanceAs (Decidable (Not _))
|
||||
|
||||
/-- `isPrefixOf l₁ l₂` returns `true` Iff `l₁` is a prefix of `l₂`. -/
|
||||
def isPrefixOf [HasBeq α] : List α → List α → Bool
|
||||
|
|
|
|||
|
|
@ -518,141 +518,6 @@ protected theorem zeroNeOne : 0 ≠ (1 : Nat) :=
|
|||
theorem succNeZero (n : Nat) : succ n ≠ 0 :=
|
||||
fun h => Nat.noConfusion h
|
||||
|
||||
protected theorem bit0SuccEq (n : Nat) : bit0 (succ n) = succ (succ (bit0 n)) :=
|
||||
show succ (succ n + n) = succ (succ (n + n)) from
|
||||
congrArg succ (succAdd n n)
|
||||
|
||||
protected theorem zeroLtBit0 : ∀ {n : Nat}, n ≠ 0 → 0 < bit0 n
|
||||
| 0, h => absurd rfl h
|
||||
| succ n, h =>
|
||||
have h₁ : 0 < succ (succ (bit0 n)) from zeroLtSucc _
|
||||
have h₂ : succ (succ (bit0 n)) = bit0 (succ n) from (Nat.bit0SuccEq n).symm
|
||||
transRelLeft (fun a b => a < b) h₁ h₂
|
||||
|
||||
protected theorem zeroLtBit1 (n : Nat) : 0 < bit1 n :=
|
||||
zeroLtSucc _
|
||||
|
||||
protected theorem bit0NeZero : ∀ {n : Nat}, n ≠ 0 → bit0 n ≠ 0
|
||||
| 0, h => absurd rfl h
|
||||
| n+1, _ => fun h => Nat.noConfusion h
|
||||
|
||||
protected theorem bit1NeZero (n : Nat) : bit1 n ≠ 0 :=
|
||||
show succ (n + n) ≠ 0 from
|
||||
fun h => Nat.noConfusion h
|
||||
|
||||
protected theorem bit1EqSuccBit0 (n : Nat) : bit1 n = succ (bit0 n) :=
|
||||
rfl
|
||||
|
||||
protected theorem bit1SuccEq (n : Nat) : bit1 (succ n) = succ (succ (bit1 n)) :=
|
||||
Eq.trans (Nat.bit1EqSuccBit0 (succ n)) (congrArg succ (Nat.bit0SuccEq n))
|
||||
|
||||
protected theorem bit1NeOne : ∀ {n : Nat}, n ≠ 0 → bit1 n ≠ 1
|
||||
| 0, h, h1 => absurd rfl h
|
||||
| n+1, h, h1 => Nat.noConfusion h1 (fun h2 => absurd h2 (succNeZero _))
|
||||
|
||||
protected theorem bit0NeOne : ∀ (n : Nat), bit0 n ≠ 1
|
||||
| 0, h => absurd h (Ne.symm Nat.oneNeZero)
|
||||
| n+1, h =>
|
||||
have h1 : succ (succ (n + n)) = 1 from succAdd n n ▸ h
|
||||
Nat.noConfusion h1
|
||||
(fun h2 => absurd h2 (succNeZero (n + n)))
|
||||
|
||||
protected theorem addSelfNeOne : ∀ (n : Nat), n + n ≠ 1
|
||||
| 0, h => Nat.noConfusion h
|
||||
| n+1, h =>
|
||||
have h1 : succ (succ (n + n)) = 1 from succAdd n n ▸ h
|
||||
Nat.noConfusion h1 (fun h2 => absurd h2 (Nat.succNeZero (n + n)))
|
||||
|
||||
protected theorem bit1NeBit0 : ∀ (n m : Nat), bit1 n ≠ bit0 m
|
||||
| 0, m, h => absurd h (Ne.symm (Nat.addSelfNeOne m))
|
||||
| n+1, 0, h =>
|
||||
have h1 : succ (bit0 (succ n)) = 0 from h
|
||||
absurd h1 (Nat.succNeZero _)
|
||||
| n+1, m+1, h =>
|
||||
have h1 : succ (succ (bit1 n)) = succ (succ (bit0 m)) from
|
||||
Nat.bit0SuccEq m ▸ Nat.bit1SuccEq n ▸ h
|
||||
have h2 : bit1 n = bit0 m from
|
||||
Nat.noConfusion h1 (fun h2' => Nat.noConfusion h2' (fun h2'' => h2''))
|
||||
absurd h2 (Nat.bit1NeBit0 n m)
|
||||
|
||||
protected theorem bit0NeBit1 : ∀ (n m : Nat), bit0 n ≠ bit1 m :=
|
||||
fun n m => Ne.symm (Nat.bit1NeBit0 m n)
|
||||
|
||||
protected theorem bit0Inj : ∀ {n m : Nat}, bit0 n = bit0 m → n = m
|
||||
| 0, 0, h => rfl
|
||||
| 0, m+1, h => absurd h.symm (succNeZero _)
|
||||
| n+1, 0, h => absurd h (succNeZero _)
|
||||
| n+1, m+1, h =>
|
||||
have (n+1) + n = (m+1) + m from Nat.noConfusion h id
|
||||
have n + (n+1) = m + (m+1) from Nat.addComm (m+1) m ▸ Nat.addComm (n+1) n ▸ this
|
||||
have succ (n + n) = succ (m + m) from this
|
||||
have n + n = m + m from Nat.noConfusion this id
|
||||
have n = m from Nat.bit0Inj this
|
||||
congrArg (fun a => a + 1) this
|
||||
|
||||
protected theorem bit1Inj {n m : Nat} : bit1 n = bit1 m → n = m :=
|
||||
fun h =>
|
||||
have succ (bit0 n) = succ (bit0 m) from Nat.bit1EqSuccBit0 n ▸ Nat.bit1EqSuccBit0 m ▸ h
|
||||
have bit0 n = bit0 m from Nat.noConfusion this id
|
||||
Nat.bit0Inj this
|
||||
|
||||
protected theorem bit0Ne {n m : Nat} : n ≠ m → bit0 n ≠ bit0 m :=
|
||||
fun h₁ h₂ => absurd (Nat.bit0Inj h₂) h₁
|
||||
|
||||
protected theorem bit1Ne {n m : Nat} : n ≠ m → bit1 n ≠ bit1 m :=
|
||||
fun h₁ h₂ => absurd (Nat.bit1Inj h₂) h₁
|
||||
|
||||
protected theorem zeroNeBit0 {n : Nat} : n ≠ 0 → 0 ≠ bit0 n :=
|
||||
fun h => Ne.symm (Nat.bit0NeZero h)
|
||||
|
||||
protected theorem zeroNeBit1 (n : Nat) : 0 ≠ bit1 n :=
|
||||
Ne.symm (Nat.bit1NeZero n)
|
||||
|
||||
protected theorem oneNeBit0 (n : Nat) : 1 ≠ bit0 n :=
|
||||
Ne.symm (Nat.bit0NeOne n)
|
||||
|
||||
protected theorem oneNeBit1 {n : Nat} : n ≠ 0 → 1 ≠ bit1 n :=
|
||||
fun h => Ne.symm (Nat.bit1NeOne h)
|
||||
|
||||
protected theorem oneLtBit1 : ∀ {n : Nat}, n ≠ 0 → 1 < bit1 n
|
||||
| 0, h => absurd rfl h
|
||||
| succ n, h =>
|
||||
have succ 0 < succ (succ (bit1 n)) from succLtSucc (zeroLtSucc _)
|
||||
(Nat.bit1SuccEq n).symm ▸ this
|
||||
|
||||
protected theorem oneLtBit0 : ∀ {n : Nat}, n ≠ 0 → 1 < bit0 n
|
||||
| 0, h => absurd rfl h
|
||||
| succ n, h =>
|
||||
have succ 0 < succ (succ (bit0 n)) from succLtSucc (zeroLtSucc _)
|
||||
(Nat.bit0SuccEq n).symm ▸ this
|
||||
|
||||
protected theorem bit0Lt {n m : Nat} (h : n < m) : bit0 n < bit0 m :=
|
||||
Nat.addLtAdd h h
|
||||
|
||||
protected theorem bit1Lt {n m : Nat} (h : n < m) : bit1 n < bit1 m :=
|
||||
succLtSucc (Nat.addLtAdd h h)
|
||||
|
||||
protected theorem bit0LtBit1 {n m : Nat} (h : n ≤ m) : bit0 n < bit1 m :=
|
||||
ltSuccOfLe (Nat.addLeAdd h h)
|
||||
|
||||
protected theorem bit1LtBit0 : ∀ {n m : Nat}, n < m → bit1 n < bit0 m
|
||||
| n, 0, h => absurd h (notLtZero _)
|
||||
| n, succ m, h =>
|
||||
have n ≤ m from leOfLtSucc h
|
||||
have succ (n + n) ≤ succ (m + m) from succLeSucc (addLeAdd this this)
|
||||
have succ (n + n) ≤ succ m + m from (succAdd m m).symm ▸ this
|
||||
show succ (n + n) < succ (succ m + m) from ltSuccOfLe this
|
||||
|
||||
protected theorem oneLeBit1 (n : Nat) : 1 ≤ bit1 n :=
|
||||
show 1 ≤ succ (bit0 n) from
|
||||
succLeSucc (zeroLe (bit0 n))
|
||||
|
||||
protected theorem oneLeBit0 : ∀ (n : Nat), n ≠ 0 → 1 ≤ bit0 n
|
||||
| 0, h => absurd rfl h
|
||||
| n+1, h =>
|
||||
have 1 ≤ succ (succ (bit0 n)) from succLeSucc (zeroLe (succ (bit0 n)))
|
||||
Eq.symm (Nat.bit0SuccEq n) ▸ this
|
||||
|
||||
/- mul + order -/
|
||||
|
||||
theorem mulLeMulLeft {n m : Nat} (k : Nat) (h : n ≤ m) : k * n ≤ k * m :=
|
||||
|
|
|
|||
|
|
@ -23,9 +23,9 @@ partial def bitwise (f : Bool → Bool → Bool) (n m : Nat) : Nat :=
|
|||
let b₂ := m % 2 = 1
|
||||
let r := bitwise f n' m'
|
||||
if f b₁ b₂ then
|
||||
bit1 r
|
||||
r+r+1
|
||||
else
|
||||
bit0 r
|
||||
r+r
|
||||
|
||||
@[extern "lean_nat_land"]
|
||||
def land : Nat → Nat → Nat := bitwise and
|
||||
|
|
|
|||
|
|
@ -38,8 +38,6 @@ def UInt8.lor (a b : UInt8) : UInt8 := ⟨Fin.lor a.val b.val⟩
|
|||
def UInt8.lt (a b : UInt8) : Prop := a.val < b.val
|
||||
def UInt8.le (a b : UInt8) : Prop := a.val ≤ b.val
|
||||
|
||||
instance : HasZero UInt8 := ⟨UInt8.ofNat 0⟩
|
||||
instance : HasOne UInt8 := ⟨UInt8.ofNat 1⟩
|
||||
instance : HasOfNat UInt8 := ⟨UInt8.ofNat⟩
|
||||
instance : HasAdd UInt8 := ⟨UInt8.add⟩
|
||||
instance : HasSub UInt8 := ⟨UInt8.sub⟩
|
||||
|
|
@ -101,8 +99,7 @@ def UInt16.lor (a b : UInt16) : UInt16 := ⟨Fin.lor a.val b.val⟩
|
|||
def UInt16.lt (a b : UInt16) : Prop := a.val < b.val
|
||||
def UInt16.le (a b : UInt16) : Prop := a.val ≤ b.val
|
||||
|
||||
instance : HasZero UInt16 := ⟨UInt16.ofNat 0⟩
|
||||
instance : HasOne UInt16 := ⟨UInt16.ofNat 1⟩
|
||||
|
||||
instance : HasOfNat UInt16 := ⟨UInt16.ofNat⟩
|
||||
instance : HasAdd UInt16 := ⟨UInt16.add⟩
|
||||
instance : HasSub UInt16 := ⟨UInt16.sub⟩
|
||||
|
|
@ -172,8 +169,6 @@ def UInt32.toUInt16 (a : UInt32) : UInt16 := a.toNat.toUInt16
|
|||
@[extern c inline "((uint32_t)#1)"]
|
||||
def UInt8.toUInt32 (a : UInt8) : UInt32 := a.toNat.toUInt32
|
||||
|
||||
instance : HasZero UInt32 := ⟨UInt32.ofNat 0⟩
|
||||
instance : HasOne UInt32 := ⟨UInt32.ofNat 1⟩
|
||||
instance : HasOfNat UInt32 := ⟨UInt32.ofNat⟩
|
||||
instance : HasAdd UInt32 := ⟨UInt32.add⟩
|
||||
instance : HasSub UInt32 := ⟨UInt32.sub⟩
|
||||
|
|
@ -254,8 +249,6 @@ constant UInt64.shiftLeft (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64
|
|||
@[extern c inline "#1 >> #2"]
|
||||
constant UInt64.shiftRight (a b : UInt64) : UInt64 := (arbitrary Nat).toUInt64
|
||||
|
||||
instance : HasZero UInt64 := ⟨UInt64.ofNat 0⟩
|
||||
instance : HasOne UInt64 := ⟨UInt64.ofNat 1⟩
|
||||
instance : HasOfNat UInt64 := ⟨UInt64.ofNat⟩
|
||||
instance : HasAdd UInt64 := ⟨UInt64.add⟩
|
||||
instance : HasSub UInt64 := ⟨UInt64.sub⟩
|
||||
|
|
@ -335,8 +328,6 @@ constant USize.shiftRight (a b : USize) : USize := (arbitrary Nat).toUSize
|
|||
def USize.lt (a b : USize) : Prop := a.val < b.val
|
||||
def USize.le (a b : USize) : Prop := a.val ≤ b.val
|
||||
|
||||
instance : HasZero USize := ⟨USize.ofNat 0⟩
|
||||
instance : HasOne USize := ⟨USize.ofNat 1⟩
|
||||
instance : HasOfNat USize := ⟨USize.ofNat⟩
|
||||
instance : HasAdd USize := ⟨USize.add⟩
|
||||
instance : HasSub USize := ⟨USize.sub⟩
|
||||
|
|
|
|||
|
|
@ -86,7 +86,7 @@ partial def moveEntries [Hashable α] : Nat → Array (AssocList α β) → Hash
|
|||
|
||||
def expand [Hashable α] (size : Nat) (buckets : HashMapBucket α β) : HashMapImp α β :=
|
||||
let nbuckets := buckets.val.size * 2
|
||||
have nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero)
|
||||
have nbuckets > 0 from Nat.mulPos buckets.property (decide! : 2 > 0)
|
||||
have (mkArray nbuckets (@AssocList.nil α β)).size = nbuckets from Array.szMkArrayEq _ _
|
||||
have Array.size (mkArray nbuckets AssocList.nil) > 0 by rw this; assumption
|
||||
let new_buckets : HashMapBucket α β := ⟨mkArray nbuckets AssocList.nil, this⟩
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ partial def moveEntries [Hashable α] : Nat → Array (List α) → HashSetBucke
|
|||
|
||||
def expand [Hashable α] (size : Nat) (buckets : HashSetBucket α) : HashSetImp α :=
|
||||
let nbuckets := buckets.val.size * 2
|
||||
have nbuckets > 0 from Nat.mulPos buckets.property (Nat.zeroLtBit0 Nat.oneNeZero)
|
||||
have nbuckets > 0 from Nat.mulPos buckets.property (decide! : 2 > 0)
|
||||
have (mkArray nbuckets ([] : List α)).size = nbuckets from Array.szMkArrayEq _ _
|
||||
have Array.size (mkArray nbuckets List.nil) > 0 by rw this; assumption
|
||||
let new_buckets : HashSetBucket α := ⟨mkArray nbuckets [], this⟩;
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue