chore: move to new frontend
This commit is contained in:
Leonardo de Moura
parent
7dfff63db6
commit
3757b26dc2
2 changed files with 95 additions and 77 deletions
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -9,53 +10,55 @@ import Init.Data.Nat.Bitwise
|
|||
import Init.Coe
|
||||
|
||||
open Nat
|
||||
structure Fin (n : Nat) := (val : Nat) (isLt : val < n)
|
||||
structure Fin (n : Nat) :=
|
||||
(val : Nat)
|
||||
(isLt : val < n)
|
||||
|
||||
namespace Fin
|
||||
|
||||
instance coeToNat {n} : Coe (Fin n) Nat :=
|
||||
⟨fun v => v.val⟩
|
||||
⟨fun v => v.val⟩
|
||||
|
||||
protected def lt {n} (a b : Fin n) : Prop :=
|
||||
a.val < b.val
|
||||
a.val < b.val
|
||||
|
||||
protected def le {n} (a b : Fin n) : Prop :=
|
||||
a.val ≤ b.val
|
||||
a.val ≤ b.val
|
||||
|
||||
instance {n} : HasLess (Fin n) := ⟨Fin.lt⟩
|
||||
instance {n} : HasLessEq (Fin n) := ⟨Fin.le⟩
|
||||
|
||||
instance decLt {n} (a b : Fin n) : Decidable (a < b) :=
|
||||
Nat.decLt _ _
|
||||
Nat.decLt ..
|
||||
|
||||
instance decLe {n} (a b : Fin n) : Decidable (a ≤ b) :=
|
||||
Nat.decLe _ _
|
||||
Nat.decLe ..
|
||||
|
||||
def elim0.{u} {α : Sort u} : Fin 0 → α
|
||||
| ⟨_, h⟩ => absurd h (notLtZero _)
|
||||
| ⟨_, h⟩ => absurd h (notLtZero _)
|
||||
|
||||
variable {n : Nat}
|
||||
|
||||
def ofNat {n : Nat} (a : Nat) : Fin (succ n) :=
|
||||
⟨a % succ n, Nat.modLt _ (Nat.zeroLtSucc _)⟩
|
||||
⟨a % succ n, Nat.modLt _ (Nat.zeroLtSucc _)⟩
|
||||
|
||||
def ofNat' {n : Nat} (a : Nat) (h : n > 0) : Fin n :=
|
||||
⟨a % n, Nat.modLt _ h⟩
|
||||
⟨a % n, Nat.modLt _ h⟩
|
||||
|
||||
private theorem mlt {n b : Nat} : ∀ {a}, n > a → b % n < n
|
||||
| 0, h => Nat.modLt _ h
|
||||
| a+1, h =>
|
||||
have n > 0 from Nat.ltTrans (Nat.zeroLtSucc _) h;
|
||||
Nat.modLt _ this
|
||||
private theorem mlt {b : Nat} : {a : Nat} → a < n → b % n < n
|
||||
| 0, h => Nat.modLt _ h
|
||||
| a+1, h =>
|
||||
have n > 0 from Nat.ltTrans (Nat.zeroLtSucc _) h;
|
||||
Nat.modLt _ this
|
||||
|
||||
protected def add : Fin n → Fin n → Fin n
|
||||
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + b) % n, mlt h⟩
|
||||
| ⟨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⟩
|
||||
| ⟨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⟩
|
||||
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a + (n - b)) % n, mlt h⟩
|
||||
|
||||
/-
|
||||
Remark: mod/div/modn/land/lor can be defined without using (% n), but
|
||||
|
|
@ -64,19 +67,19 @@ needed to boostrap Lean.
|
|||
-/
|
||||
|
||||
protected def mod : Fin n → Fin n → Fin n
|
||||
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a % b) % n, mlt h⟩
|
||||
| ⟨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⟩
|
||||
| ⟨a, h⟩, ⟨b, _⟩ => ⟨(a / b) % n, mlt h⟩
|
||||
|
||||
protected def modn : Fin n → Nat → Fin n
|
||||
| ⟨a, h⟩, m => ⟨(a % m) % n, mlt h⟩
|
||||
| ⟨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⟩
|
||||
| ⟨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⟩
|
||||
| ⟨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⟩
|
||||
|
|
@ -88,23 +91,23 @@ instance : HasDiv (Fin n) := ⟨Fin.div⟩
|
|||
instance : HasModN (Fin n) := ⟨Fin.modn⟩
|
||||
|
||||
theorem eqOfVeq : ∀ {i j : Fin n}, (val i) = (val j) → i = j
|
||||
| ⟨iv, ilt₁⟩, ⟨.(iv), ilt₂⟩, rfl => rfl
|
||||
| ⟨iv, ilt₁⟩, ⟨_, _⟩, rfl => rfl
|
||||
|
||||
theorem veqOfEq : ∀ {i j : Fin n}, i = j → (val i) = (val j)
|
||||
| ⟨iv, ilt⟩, .(_), rfl => rfl
|
||||
| ⟨iv, ilt⟩, _, rfl => rfl
|
||||
|
||||
theorem neOfVne {i j : Fin n} (h : val i ≠ val j) : i ≠ j :=
|
||||
fun h' => absurd (veqOfEq h') h
|
||||
fun h' => absurd (veqOfEq h') h
|
||||
|
||||
theorem vneOfNe {i j : Fin n} (h : i ≠ j) : val i ≠ val j :=
|
||||
fun h' => absurd (eqOfVeq h') h
|
||||
fun h' => absurd (eqOfVeq h') h
|
||||
|
||||
theorem modnLt : ∀ {m : Nat} (i : Fin n), m > 0 → (i %ₙ m).val < m
|
||||
| m, ⟨a, h⟩, hp => Nat.ltOfLeOfLt (modLe _ _) (modLt _ hp)
|
||||
| m, ⟨a, h⟩, hp => Nat.ltOfLeOfLt (modLe _ _) (modLt _ hp)
|
||||
|
||||
end Fin
|
||||
|
||||
open Fin
|
||||
|
||||
instance (n : Nat) : DecidableEq (Fin n) :=
|
||||
fun i j => decidableOfDecidableOfIff (decEq i.val j.val) ⟨eqOfVeq, veqOfEq⟩
|
||||
instance (n : Nat) : DecidableEq (Fin n) := fun i j =>
|
||||
decidableOfDecidableOfIff (decEq i.val j.val) ⟨eqOfVeq, veqOfEq⟩
|
||||
|
|
|
|||
|
|
@ -1,3 +1,4 @@
|
|||
#lang lean4
|
||||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
|
|
@ -11,7 +12,7 @@ open Nat
|
|||
|
||||
def uint8Sz : Nat := 256
|
||||
structure UInt8 :=
|
||||
(val : Fin uint8Sz)
|
||||
(val : Fin uint8Sz)
|
||||
|
||||
@[extern "lean_uint8_of_nat"]
|
||||
def UInt8.ofNat (n : @& Nat) : UInt8 := ⟨Fin.ofNat n⟩
|
||||
|
|
@ -50,29 +51,31 @@ instance : HasLess UInt8 := ⟨UInt8.lt⟩
|
|||
instance : HasLessEq UInt8 := ⟨UInt8.le⟩
|
||||
instance : Inhabited UInt8 := ⟨0⟩
|
||||
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
def UInt8.decEq (a b : UInt8) : Decidable (a = b) :=
|
||||
UInt8.casesOn a $ fun n => UInt8.casesOn b $ fun m =>
|
||||
if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt8.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
def UInt8.decLt (a b : UInt8) : Decidable (a < b) :=
|
||||
UInt8.casesOn a $ fun n => UInt8.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n < m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
def UInt8.decLe (a b : UInt8) : Decidable (a ≤ b) :=
|
||||
UInt8.casesOn a $ fun n => UInt8.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n <= m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
||||
instance : DecidableEq UInt8 := UInt8.decEq
|
||||
instance UInt8.hasDecidableLt (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
|
||||
instance UInt8.hasDecidableLe (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
|
||||
instance (a b : UInt8) : Decidable (a < b) := UInt8.decLt a b
|
||||
instance (a b : UInt8) : Decidable (a ≤ b) := UInt8.decLe a b
|
||||
|
||||
def uint16Sz : Nat := 65536
|
||||
structure UInt16 :=
|
||||
(val : Fin uint16Sz)
|
||||
(val : Fin uint16Sz)
|
||||
|
||||
@[extern "lean_uint16_of_nat"]
|
||||
def UInt16.ofNat (n : @& Nat) : UInt16 := ⟨Fin.ofNat n⟩
|
||||
|
|
@ -111,28 +114,31 @@ instance : HasLess UInt16 := ⟨UInt16.lt⟩
|
|||
instance : HasLessEq UInt16 := ⟨UInt16.le⟩
|
||||
instance : Inhabited UInt16 := ⟨0⟩
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
def UInt16.decEq (a b : UInt16) : Decidable (a = b) :=
|
||||
UInt16.casesOn a $ fun n => UInt16.casesOn b $ fun m =>
|
||||
if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt16.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
def UInt16.decLt (a b : UInt16) : Decidable (a < b) :=
|
||||
UInt16.casesOn a $ fun n => UInt16.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n < m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
def UInt16.decLe (a b : UInt16) : Decidable (a ≤ b) :=
|
||||
UInt16.casesOn a $ fun n => UInt16.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n <= m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
||||
instance : DecidableEq UInt16 := UInt16.decEq
|
||||
instance UInt16.hasDecidableLt (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
|
||||
instance UInt16.hasDecidableLe (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
|
||||
instance (a b : UInt16) : Decidable (a < b) := UInt16.decLt a b
|
||||
instance (a b : UInt16) : Decidable (a ≤ b) := UInt16.decLe a b
|
||||
|
||||
def uint32Sz : Nat := 4294967296
|
||||
structure UInt32 :=
|
||||
(val : Fin uint32Sz)
|
||||
(val : Fin uint32Sz)
|
||||
|
||||
@[extern "lean_uint32_of_nat"]
|
||||
def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨Fin.ofNat n⟩
|
||||
|
|
@ -179,20 +185,23 @@ instance : HasLess UInt32 := ⟨UInt32.lt⟩
|
|||
instance : HasLessEq UInt32 := ⟨UInt32.le⟩
|
||||
instance : Inhabited UInt32 := ⟨0⟩
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
def UInt32.decEq (a b : UInt32) : Decidable (a = b) :=
|
||||
UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
|
||||
if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt32.noConfusion h' (fun h' => absurd h' h))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt32.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
def UInt32.decLt (a b : UInt32) : Decidable (a < b) :=
|
||||
UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n < m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
def UInt32.decLe (a b : UInt32) : Decidable (a ≤ b) :=
|
||||
UInt32.casesOn a $ fun n => UInt32.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n <= m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
||||
@[extern c inline "#1 << #2"]
|
||||
constant UInt32.shiftLeft (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
|
||||
|
|
@ -200,12 +209,12 @@ constant UInt32.shiftLeft (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
|
|||
constant UInt32.shiftRight (a b : UInt32) : UInt32 := (arbitrary Nat).toUInt32
|
||||
|
||||
instance : DecidableEq UInt32 := UInt32.decEq
|
||||
instance UInt32.hasDecidableLt (a b : UInt32) : Decidable (a < b) := UInt32.decLt a b
|
||||
instance UInt32.hasDecidableLe (a b : UInt32) : Decidable (a ≤ b) := UInt32.decLe a b
|
||||
instance (a b : UInt32) : Decidable (a < b) := UInt32.decLt a b
|
||||
instance (a b : UInt32) : Decidable (a ≤ b) := UInt32.decLe a b
|
||||
|
||||
def uint64Sz : Nat := 18446744073709551616
|
||||
structure UInt64 :=
|
||||
(val : Fin uint64Sz)
|
||||
(val : Fin uint64Sz)
|
||||
|
||||
@[extern "lean_uint64_of_nat"]
|
||||
def UInt64.ofNat (n : @& Nat) : UInt64 := ⟨Fin.ofNat n⟩
|
||||
|
|
@ -261,31 +270,34 @@ instance : Inhabited UInt64 := ⟨0⟩
|
|||
@[extern c inline "(uint64_t)#1"]
|
||||
def Bool.toUInt64 (b : Bool) : UInt64 := if b then 1 else 0
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
def UInt64.decEq (a b : UInt64) : Decidable (a = b) :=
|
||||
UInt64.casesOn a $ fun n => UInt64.casesOn b $ fun m =>
|
||||
if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => UInt64.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
def UInt64.decLt (a b : UInt64) : Decidable (a < b) :=
|
||||
UInt64.casesOn a $ fun n => UInt64.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n < m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
def UInt64.decLe (a b : UInt64) : Decidable (a ≤ b) :=
|
||||
UInt64.casesOn a $ fun n => UInt64.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n <= m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
||||
instance : DecidableEq UInt64 := UInt64.decEq
|
||||
instance UInt64.hasDecidableLt (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
|
||||
instance UInt64.hasDecidableLe (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
|
||||
instance (a b : UInt64) : Decidable (a < b) := UInt64.decLt a b
|
||||
instance (a b : UInt64) : Decidable (a ≤ b) := UInt64.decLe a b
|
||||
|
||||
def usizeSz : Nat := (2:Nat) ^ System.Platform.numBits
|
||||
structure USize :=
|
||||
(val : Fin usizeSz)
|
||||
(val : Fin usizeSz)
|
||||
|
||||
theorem usizeSzGt0 : usizeSz > 0 :=
|
||||
Nat.posPowOfPos System.Platform.numBits (Nat.zeroLtSucc _)
|
||||
Nat.posPowOfPos System.Platform.numBits (Nat.zeroLtSucc _)
|
||||
|
||||
@[extern "lean_usize_of_nat"]
|
||||
def USize.ofNat (n : @& Nat) : USize := ⟨Fin.ofNat' n usizeSzGt0⟩
|
||||
|
|
@ -336,24 +348,27 @@ instance : HasLess USize := ⟨USize.lt⟩
|
|||
instance : HasLessEq USize := ⟨USize.le⟩
|
||||
instance : Inhabited USize := ⟨0⟩
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 == #2"]
|
||||
def USize.decEq (a b : USize) : Decidable (a = b) :=
|
||||
USize.casesOn a $ fun n => USize.casesOn b $ fun m =>
|
||||
if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => if h : n = m then isTrue (h ▸ rfl) else isFalse (fun h' => USize.noConfusion h' (fun h' => absurd h' h))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 < #2"]
|
||||
def USize.decLt (a b : USize) : Decidable (a < b) :=
|
||||
USize.casesOn a $ fun n => USize.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n < m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n < m))
|
||||
|
||||
set_option bootstrap.gen_matcher_code false in
|
||||
@[extern c inline "#1 <= #2"]
|
||||
def USize.decLe (a b : USize) : Decidable (a ≤ b) :=
|
||||
USize.casesOn a $ fun n => USize.casesOn b $ fun m =>
|
||||
inferInstanceAs (Decidable (n <= m))
|
||||
match a, b with
|
||||
| ⟨n⟩, ⟨m⟩ => inferInstanceAs (Decidable (n <= m))
|
||||
|
||||
instance : DecidableEq USize := USize.decEq
|
||||
instance USize.hasDecidableLt (a b : USize) : Decidable (a < b) := USize.decLt a b
|
||||
instance USize.hasDecidableLe (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
|
||||
instance (a b : USize) : Decidable (a < b) := USize.decLt a b
|
||||
instance (a b : USize) : Decidable (a ≤ b) := USize.decLe a b
|
||||
|
||||
theorem USize.modnLt {m : Nat} : ∀ (u : USize), m > 0 → USize.toNat (u %ₙ m) < m
|
||||
| ⟨u⟩, h => Fin.modnLt u h
|
||||
| ⟨u⟩, h => Fin.modnLt u h
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue