summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
Diffstat (limited to 'backends/lean/Base')
-rw-r--r--backends/lean/Base/Arith/Base.lean12
-rw-r--r--backends/lean/Base/Arith/Int.lean15
-rw-r--r--backends/lean/Base/Arith/Scalar.lean13
-rw-r--r--backends/lean/Base/IList/IList.lean39
-rw-r--r--backends/lean/Base/Primitives.lean4
-rw-r--r--backends/lean/Base/Primitives/Alloc.lean37
-rw-r--r--backends/lean/Base/Primitives/Array.lean394
-rw-r--r--backends/lean/Base/Primitives/ArraySlice.lean553
-rw-r--r--backends/lean/Base/Primitives/Base.lean11
-rw-r--r--backends/lean/Base/Primitives/CoreOps.lean37
-rw-r--r--backends/lean/Base/Primitives/Range.lean2
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean127
-rw-r--r--backends/lean/Base/Primitives/Vec.lean94
-rw-r--r--backends/lean/Base/Progress/Progress.lean29
-rw-r--r--backends/lean/Base/Utils.lean75
15 files changed, 972 insertions, 470 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean
index 9c11ed45..8ada4171 100644
--- a/backends/lean/Base/Arith/Base.lean
+++ b/backends/lean/Base/Arith/Base.lean
@@ -57,4 +57,16 @@ theorem int_pos_ind (p : Int → Prop) :
-- TODO: there is probably something more general to do
theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp
+-- This is mostly used in termination proofs
+theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) :
+ ↑(x.toNat) < y := by
+ simp [*]
+
+-- This is mostly used in termination proofs
+theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ)
+ (h0 : ↑x' ≤ x) (h1 : x - ↑x' < y) :
+ ↑(x.toNat - x') < y := by
+ have : 0 ≤ x := by linarith
+ simp [Int.toNat_sub_of_le, *]
+
end Arith
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 3359ecdb..a57f8bb1 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -162,7 +162,7 @@ def introInstances (declToUnfold : Name) (lookup : Expr → MetaM (Option Expr))
-- Add a declaration
let nval ← Utils.addDeclTac name e type (asLet := false)
-- Simplify to unfold the declaration to unfold (i.e., the projector)
- Utils.simpAt [declToUnfold] [] [] (Tactic.Location.targets #[mkIdent name] false)
+ Utils.simpAt true [declToUnfold] [] [] (Location.targets #[mkIdent name] false)
-- Return the new value
pure nval
@@ -240,7 +240,7 @@ def intTac (splitGoalConjs : Bool) (extraPreprocess : Tactic.TacticM Unit) : Ta
-- the goal. I think before leads to a smaller proof term?
Tactic.allGoals (intTacPreprocess extraPreprocess)
-- More preprocessing
- Tactic.allGoals (Utils.tryTac (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard))
+ Tactic.allGoals (Utils.tryTac (Utils.simpAt true [] [``nat_zero_eq_int_zero] [] .wildcard))
-- Split the conjunctions in the goal
if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
-- Call linarith
@@ -270,6 +270,17 @@ elab "int_tac" args:(" split_goal"?): tactic =>
let split := args.raw.getArgs.size > 0
intTac split (do pure ())
+-- For termination proofs
+syntax "int_decr_tac" : tactic
+macro_rules
+ | `(tactic| int_decr_tac) =>
+ `(tactic|
+ simp_wf;
+ -- TODO: don't use a macro (namespace problems)
+ (first | apply Arith.to_int_to_nat_lt
+ | apply Arith.to_int_sub_to_nat_lt) <;>
+ simp_all <;> int_tac)
+
example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by
int_tac_preprocess
linarith
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index 47751c8a..2342cce6 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -17,7 +17,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
-- Reveal the concrete bounds, simplify calls to [ofInt]
- Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
+ Utils.simpAt true [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax,
``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min,
``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max,
``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min,
@@ -36,6 +36,17 @@ def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do
elab "scalar_tac" : tactic =>
scalarTac false
+-- For termination proofs
+syntax "scalar_decr_tac" : tactic
+macro_rules
+ | `(tactic| scalar_decr_tac) =>
+ `(tactic|
+ simp_wf;
+ -- TODO: don't use a macro (namespace problems)
+ (first | apply Arith.to_int_to_nat_lt
+ | apply Arith.to_int_sub_to_nat_lt) <;>
+ simp_all <;> scalar_tac)
+
instance (ty : ScalarTy) : HasIntProp (Scalar ty) where
-- prop_ty is inferred
prop := λ x => And.intro x.hmin x.hmax
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index a940da25..f71f2de2 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -112,7 +112,13 @@ def pairwise_rel
section Lemmas
-variable {α : Type u}
+variable {α : Type u}
+
+def ireplicate {α : Type u} (i : ℤ) (x : α) : List α :=
+ if i ≤ 0 then []
+ else x :: ireplicate (i - 1) x
+termination_by ireplicate i x => i.toNat
+decreasing_by int_decr_tac
@[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update]
@[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update]
@@ -129,6 +135,10 @@ variable {α : Type u}
@[simp] theorem slice_nil : slice i j ([] : List α) = [] := by simp [slice]
@[simp] theorem slice_zero : slice 0 0 (ls : List α) = [] := by cases ls <;> simp [slice]
+@[simp] theorem ireplicate_zero : ireplicate 0 x = [] := by rw [ireplicate]; simp
+@[simp] theorem ireplicate_nzero_cons (hne : 0 < i) : ireplicate i x = x :: ireplicate (i - 1) x := by
+ rw [ireplicate]; simp [*]; intro; linarith
+
@[simp]
theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : slice i j ((x :: tl) : List α) = slice (i - 1) (j - 1) tl :=
match tl with
@@ -144,6 +154,33 @@ theorem slice_nzero_cons (i j : Int) (x : α) (tl : List α) (hne : i ≠ 0) : s
conv at this => lhs; simp [slice, *]
simp [*, slice]
+@[simp]
+theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
+ ireplicate l x = replicate l.toNat x :=
+ if hz: l = 0 then by
+ simp [*]
+ else by
+ have : 0 < l := by int_tac
+ have hr := ireplicate_replicate (l - 1) x (by int_tac)
+ simp [*]
+ have hl : l.toNat = .succ (l.toNat - 1) := by
+ cases hl: l.toNat <;> simp_all
+ conv => rhs; rw[hl]
+termination_by ireplicate_replicate l x h => l.toNat
+decreasing_by int_decr_tac
+
+@[simp]
+theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) :
+ (ireplicate l x).len = l :=
+ if hz: l = 0 then by
+ simp [*]
+ else by
+ have : 0 < l := by int_tac
+ have hr := ireplicate_len (l - 1) x (by int_tac)
+ simp [*]
+termination_by ireplicate_len l x h => l.toNat
+decreasing_by int_decr_tac
+
theorem len_eq_length (ls : List α) : ls.len = ls.length := by
induction ls
. rfl
diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean
index 6b7b0792..613b6076 100644
--- a/backends/lean/Base/Primitives.lean
+++ b/backends/lean/Base/Primitives.lean
@@ -1,4 +1,6 @@
import Base.Primitives.Base
import Base.Primitives.Scalar
-import Base.Primitives.Array
+import Base.Primitives.ArraySlice
import Base.Primitives.Vec
+import Base.Primitives.Alloc
+import Base.Primitives.CoreOps
diff --git a/backends/lean/Base/Primitives/Alloc.lean b/backends/lean/Base/Primitives/Alloc.lean
new file mode 100644
index 00000000..34590499
--- /dev/null
+++ b/backends/lean/Base/Primitives/Alloc.lean
@@ -0,0 +1,37 @@
+import Lean
+import Base.Primitives.Base
+import Base.Primitives.CoreOps
+
+open Primitives
+open Result
+
+namespace alloc
+
+namespace boxed -- alloc.boxed
+
+namespace Box -- alloc.boxed.Box
+
+def deref (T : Type) (x : T) : Result T := ret x
+def deref_mut (T : Type) (x : T) : Result T := ret x
+def deref_mut_back (T : Type) (_ : T) (x : T) : Result T := ret x
+
+/-- Trait instance -/
+def coreOpsDerefInst (Self : Type) :
+ core.ops.deref.Deref Self := {
+ Target := Self
+ deref := deref Self
+}
+
+/-- Trait instance -/
+def coreOpsDerefMutInst (Self : Type) :
+ core.ops.deref.DerefMut Self := {
+ derefInst := coreOpsDerefInst Self
+ deref_mut := deref_mut Self
+ deref_mut_back := deref_mut_back Self
+}
+
+end Box -- alloc.boxed.Box
+
+end boxed -- alloc.boxed
+
+end alloc
diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean
deleted file mode 100644
index 6c95fd78..00000000
--- a/backends/lean/Base/Primitives/Array.lean
+++ /dev/null
@@ -1,394 +0,0 @@
-/- Arrays/slices -/
-import Lean
-import Lean.Meta.Tactic.Simp
-import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
-import Mathlib.Tactic.Linarith
-import Base.IList
-import Base.Primitives.Scalar
-import Base.Primitives.Range
-import Base.Arith
-import Base.Progress.Base
-
-namespace Primitives
-
-open Result Error
-
-def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
-
-instance (a : Type u) (n : Usize) : Arith.HasIntProp (Array a n) where
- prop_ty := λ v => v.val.len = n.val
- prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
-
-instance {α : Type u} {n : Usize} (p : Array α n → Prop) : Arith.HasIntProp (Subtype p) where
- prop_ty := λ x => p x
- prop := λ x => x.property
-
-@[simp]
-abbrev Array.length {α : Type u} {n : Usize} (v : Array α n) : Int := v.val.len
-
-@[simp]
-abbrev Array.v {α : Type u} {n : Usize} (v : Array α n) : List α := v.val
-
-example {α: Type u} {n : Usize} (v : Array α n) : v.length ≤ Scalar.max ScalarTy.Usize := by
- scalar_tac
-
-def Array.make (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val := by decide) :
- Array α n := ⟨ init, by simp [← List.len_eq_length]; apply hl ⟩
-
-example : Array Int (Usize.ofInt 2) := Array.make Int (Usize.ofInt 2) [0, 1]
-
-@[simp]
-abbrev Array.index {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α :=
- v.val.index i
-
-@[simp]
-abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i j : Int) : List α :=
- v.val.slice i j
-
-def Array.index_shared (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some x => ret x
-
-/- In the theorems below: we don't always need the `∃ ..`, but we use one
- so that `progress` introduces an opaque variable and an equality. This
- helps control the context.
- -/
-
-@[pspec]
-theorem Array.index_shared_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
- (hbound : i.val < v.length) :
- ∃ x, v.index_shared α n i = ret x ∧ x = v.val.index i.val := by
- simp only [index_shared]
- -- TODO: dependent rewrite
- have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp [*]
-
--- This shouldn't be used
-def Array.index_shared_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (_: α) : Result Unit :=
- if i.val < List.length v.val then
- .ret ()
- else
- .fail arrayOutOfBounds
-
-def Array.index_mut (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some x => ret x
-
-@[pspec]
-theorem Array.index_mut_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
- (hbound : i.val < v.length) :
- ∃ x, v.index_mut α n i = ret x ∧ x = v.val.index i.val := by
- simp only [index_mut]
- -- TODO: dependent rewrite
- have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp [*]
-
-def Array.index_mut_back (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some _ =>
- .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
-
-@[pspec]
-theorem Array.index_mut_back_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
- (hbound : i.val < v.length) :
- ∃ nv, v.index_mut_back α n i x = ret nv ∧
- nv.val = v.val.update i.val x
- := by
- simp only [index_mut_back]
- have h := List.indexOpt_bounds v.val i.val
- split
- . simp_all [length]; cases h <;> scalar_tac
- . simp_all
-
-def Slice (α : Type u) := { l : List α // l.length ≤ Usize.max }
-
-instance (a : Type u) : Arith.HasIntProp (Slice a) where
- prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
- prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
-
-instance {α : Type u} (p : Slice α → Prop) : Arith.HasIntProp (Subtype p) where
- prop_ty := λ x => p x
- prop := λ x => x.property
-
-@[simp]
-abbrev Slice.length {α : Type u} (v : Slice α) : Int := v.val.len
-
-@[simp]
-abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val
-
-example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
- scalar_tac
-
-def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
-
--- TODO: very annoying that the α is an explicit parameter
-def Slice.len (α : Type u) (v : Slice α) : Usize :=
- Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
-
-@[simp]
-theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.length :=
- by rfl
-
-@[simp]
-abbrev Slice.index {α : Type u} [Inhabited α] (v: Slice α) (i: Int) : α :=
- v.val.index i
-
-@[simp]
-abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : List α :=
- s.val.slice i j
-
-def Slice.index_shared (α : Type u) (v: Slice α) (i: Usize) : Result α :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some x => ret x
-
-/- In the theorems below: we don't always need the `∃ ..`, but we use one
- so that `progress` introduces an opaque variable and an equality. This
- helps control the context.
- -/
-
-@[pspec]
-theorem Slice.index_shared_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
- (hbound : i.val < v.length) :
- ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
- simp only [index_shared]
- -- TODO: dependent rewrite
- have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp [*]
-
--- This shouldn't be used
-def Slice.index_shared_back (α : Type u) (v: Slice α) (i: Usize) (_: α) : Result Unit :=
- if i.val < List.length v.val then
- .ret ()
- else
- .fail arrayOutOfBounds
-
-def Slice.index_mut (α : Type u) (v: Slice α) (i: Usize) : Result α :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some x => ret x
-
-@[pspec]
-theorem Slice.index_mut_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
- (hbound : i.val < v.length) :
- ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
- simp only [index_mut]
- -- TODO: dependent rewrite
- have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp [*]
-
-def Slice.index_mut_back (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some _ =>
- .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
-
-@[pspec]
-theorem Slice.index_mut_back_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
- (hbound : i.val < v.length) :
- ∃ nv, v.index_mut_back α i x = ret nv ∧
- nv.val = v.val.update i.val x
- := by
- simp only [index_mut_back]
- have h := List.indexOpt_bounds v.val i.val
- split
- . simp_all [length]; cases h <;> scalar_tac
- . simp_all
-
-/- Array to slice/subslices -/
-
-/- We could make this function not use the `Result` type. By making it monadic, we
- push the user to use the `Array.to_slice_shared_spec` spec theorem below (through the
- `progress` tactic), meaning `Array.to_slice_shared` should be considered as opaque.
- All what the spec theorem reveals is that the "representative" lists are the same. -/
-def Array.to_slice_shared (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
- ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
-
-@[pspec]
-theorem Array.to_slice_shared_spec {α : Type u} {n : Usize} (v : Array α n) :
- ∃ s, to_slice_shared α n v = ret s ∧ v.val = s.val := by simp [to_slice_shared]
-
-def Array.to_slice_mut (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
- to_slice_shared α n v
-
-@[pspec]
-theorem Array.to_slice_mut_spec {α : Type u} {n : Usize} (v : Array α n) :
- ∃ s, Array.to_slice_shared α n v = ret s ∧ v.val = s.val := to_slice_shared_spec v
-
-def Array.to_slice_mut_back (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
- if h: s.val.len = n.val then
- ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
- else fail panic
-
-@[pspec]
-theorem Array.to_slice_mut_back_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
- ∃ na, to_slice_mut_back α n a ns = ret na ∧ na.val = ns.val
- := by simp [to_slice_mut_back, *]
-
-def Array.subslice_shared (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
- -- TODO: not completely sure here
- if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then
- ret ⟨ a.val.slice r.start.val r.end_.val,
- by
- simp [← List.len_eq_length]
- have := a.val.slice_len_le r.start.val r.end_.val
- scalar_tac ⟩
- else
- fail panic
-
-@[pspec]
-theorem Array.subslice_shared_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
- (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
- ∃ s, subslice_shared α n a r = ret s ∧
- s.val = a.val.slice r.start.val r.end_.val ∧
- (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
- := by
- simp [subslice_shared, *]
- intro i _ _
- have := List.index_slice r.start.val r.end_.val i a.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
- simp [*]
-
-def Array.subslice_mut (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
- Array.subslice_shared α n a r
-
-@[pspec]
-theorem Array.subslice_mut_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
- (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
- ∃ s, subslice_mut α n a r = ret s ∧
- s.val = a.slice r.start.val r.end_.val ∧
- (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
- := subslice_shared_spec a r h0 h1
-
-def Array.subslice_mut_back (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
- -- TODO: not completely sure here
- if h: r.start.val < r.end_.val ∧ r.end_.val ≤ a.length ∧ s.val.len = r.end_.val - r.start.val then
- let s_beg := a.val.itake r.start.val
- let s_end := a.val.idrop r.end_.val
- have : s_beg.len = r.start.val := by
- apply List.itake_len
- . simp_all; scalar_tac
- . scalar_tac
- have : s_end.len = a.val.len - r.end_.val := by
- apply List.idrop_len
- . scalar_tac
- . scalar_tac
- let na := s_beg.append (s.val.append s_end)
- have : na.len = a.val.len := by simp [*]
- ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
- else
- fail panic
-
--- TODO: it is annoying to write `.val` everywhere. We could leverage coercions,
--- but: some symbols like `+` are already overloaded to be notations for monadic
--- operations/
--- We should introduce special symbols for the monadic arithmetic operations
--- (the use will never write those symbols directly).
-@[pspec]
-theorem Array.subslice_mut_back_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
- (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) :
- ∃ na, subslice_mut_back α n a r s = ret na ∧
- (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧
- (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = s.index (i - r.start.val)) ∧
- (∀ i, r.end_.val ≤ i → i < n.val → na.index i = a.index i) := by
- simp [subslice_mut_back, *]
- have h := List.replace_slice_index r.start.val r.end_.val a.val s.val
- (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
- simp [List.replace_slice] at h
- have ⟨ h0, h1, h2 ⟩ := h
- clear h
- split_conjs
- . intro i _ _
- have := h0 i (by int_tac) (by int_tac)
- simp [*]
- . intro i _ _
- have := h1 i (by int_tac) (by int_tac)
- simp [*]
- . intro i _ _
- have := h2 i (by int_tac) (by int_tac)
- simp [*]
-
-def Slice.subslice_shared (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
- -- TODO: not completely sure here
- if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then
- ret ⟨ s.val.slice r.start.val r.end_.val,
- by
- simp [← List.len_eq_length]
- have := s.val.slice_len_le r.start.val r.end_.val
- scalar_tac ⟩
- else
- fail panic
-
-@[pspec]
-theorem Slice.subslice_shared_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
- (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
- ∃ ns, subslice_shared α s r = ret ns ∧
- ns.val = s.slice r.start.val r.end_.val ∧
- (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i))
- := by
- simp [subslice_shared, *]
- intro i _ _
- have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
- simp [*]
-
-def Slice.subslice_mut (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
- Slice.subslice_shared α s r
-
-@[pspec]
-theorem Slice.subslice_mut_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
- (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
- ∃ ns, subslice_mut α s r = ret ns ∧
- ns.val = s.slice r.start.val r.end_.val ∧
- (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index i = s.index (r.start.val + i))
- := subslice_shared_spec s r h0 h1
-
-attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing
-set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
-
-def Slice.subslice_mut_back (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
- -- TODO: not completely sure here
- if h: r.start.val < r.end_.val ∧ r.end_.val ≤ s.length ∧ ss.val.len = r.end_.val - r.start.val then
- let s_beg := s.val.itake r.start.val
- let s_end := s.val.idrop r.end_.val
- have : s_beg.len = r.start.val := by
- apply List.itake_len
- . simp_all; scalar_tac
- . scalar_tac
- have : s_end.len = s.val.len - r.end_.val := by
- apply List.idrop_len
- . scalar_tac
- . scalar_tac
- let ns := s_beg.append (ss.val.append s_end)
- have : ns.len = s.val.len := by simp [*]
- ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
- else
- fail panic
-
-@[pspec]
-theorem Slice.subslice_mut_back_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
- (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) :
- ∃ na, subslice_mut_back α a r ss = ret na ∧
- (∀ i, 0 ≤ i → i < r.start.val → na.index i = a.index i) ∧
- (∀ i, r.start.val ≤ i → i < r.end_.val → na.index i = ss.index (i - r.start.val)) ∧
- (∀ i, r.end_.val ≤ i → i < a.length → na.index i = a.index i) := by
- simp [subslice_mut_back, *]
- have h := List.replace_slice_index r.start.val r.end_.val a.val ss.val
- (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
- simp [List.replace_slice, *] at h
- have ⟨ h0, h1, h2 ⟩ := h
- clear h
- split_conjs
- . intro i _ _
- have := h0 i (by int_tac) (by int_tac)
- simp [*]
- . intro i _ _
- have := h1 i (by int_tac) (by int_tac)
- simp [*]
- . intro i _ _
- have := h2 i (by int_tac) (by int_tac)
- simp [*]
-
-end Primitives
diff --git a/backends/lean/Base/Primitives/ArraySlice.lean b/backends/lean/Base/Primitives/ArraySlice.lean
new file mode 100644
index 00000000..cfc9a6b2
--- /dev/null
+++ b/backends/lean/Base/Primitives/ArraySlice.lean
@@ -0,0 +1,553 @@
+/- Arrays/Slices -/
+import Lean
+import Lean.Meta.Tactic.Simp
+import Init.Data.List.Basic
+import Mathlib.Tactic.RunCmd
+import Mathlib.Tactic.Linarith
+import Base.IList
+import Base.Primitives.Scalar
+import Base.Primitives.Range
+import Base.Primitives.CoreOps
+import Base.Arith
+import Base.Progress.Base
+
+namespace Primitives
+
+open Result Error core.ops.range
+
+def Array (α : Type u) (n : Usize) := { l : List α // l.length = n.val }
+
+instance (a : Type u) (n : Usize) : Arith.HasIntProp (Array a n) where
+ prop_ty := λ v => v.val.len = n.val
+ prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
+
+instance {α : Type u} {n : Usize} (p : Array α n → Prop) : Arith.HasIntProp (Subtype p) where
+ prop_ty := λ x => p x
+ prop := λ x => x.property
+
+@[simp]
+abbrev Array.length {α : Type u} {n : Usize} (v : Array α n) : Int := v.val.len
+
+@[simp]
+abbrev Array.v {α : Type u} {n : Usize} (v : Array α n) : List α := v.val
+
+example {α: Type u} {n : Usize} (v : Array α n) : v.length ≤ Scalar.max ScalarTy.Usize := by
+ scalar_tac
+
+def Array.make (α : Type u) (n : Usize) (init : List α) (hl : init.len = n.val := by decide) :
+ Array α n := ⟨ init, by simp [← List.len_eq_length]; apply hl ⟩
+
+example : Array Int (Usize.ofInt 2) := Array.make Int (Usize.ofInt 2) [0, 1]
+
+@[simp]
+abbrev Array.index_s {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i : Int) : α :=
+ v.val.index i
+
+@[simp]
+abbrev Array.slice {α : Type u} {n : Usize} [Inhabited α] (v : Array α n) (i j : Int) : List α :=
+ v.val.slice i j
+
+def Array.index_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) : Result α :=
+ match v.val.indexOpt i.val with
+ | none => fail .arrayOutOfBounds
+ | some x => ret x
+
+-- For initialization
+def Array.repeat (α : Type u) (n : Usize) (x : α) : Array α n :=
+ ⟨ List.ireplicate n.val x, by have h := n.hmin; simp_all [Scalar.min] ⟩
+
+@[pspec]
+theorem Array.repeat_spec {α : Type u} (n : Usize) (x : α) :
+ ∃ a, Array.repeat α n x = a ∧ a.val = List.ireplicate n.val x := by
+ simp [Array.repeat]
+
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+ so that `progress` introduces an opaque variable and an equality. This
+ helps control the context.
+ -/
+
+@[pspec]
+theorem Array.index_usize_spec {α : Type u} {n : Usize} [Inhabited α] (v: Array α n) (i: Usize)
+ (hbound : i.val < v.length) :
+ ∃ x, v.index_usize α n i = ret x ∧ x = v.val.index i.val := by
+ simp only [index_usize]
+ -- TODO: dependent rewrite
+ have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
+ simp [*]
+
+def Array.update_usize (α : Type u) (n : Usize) (v: Array α n) (i: Usize) (x: α) : Result (Array α n) :=
+ match v.val.indexOpt i.val with
+ | none => fail .arrayOutOfBounds
+ | some _ =>
+ .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+
+@[pspec]
+theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
+ (hbound : i.val < v.length) :
+ ∃ nv, v.update_usize α n i x = ret nv ∧
+ nv.val = v.val.update i.val x
+ := by
+ simp only [update_usize]
+ have h := List.indexOpt_bounds v.val i.val
+ split
+ . simp_all [length]; cases h <;> scalar_tac
+ . simp_all
+
+def Slice (α : Type u) := { l : List α // l.length ≤ Usize.max }
+
+instance (a : Type u) : Arith.HasIntProp (Slice a) where
+ prop_ty := λ v => 0 ≤ v.val.len ∧ v.val.len ≤ Scalar.max ScalarTy.Usize
+ prop := λ ⟨ _, l ⟩ => by simp[Scalar.max, List.len_eq_length, *]
+
+instance {α : Type u} (p : Slice α → Prop) : Arith.HasIntProp (Subtype p) where
+ prop_ty := λ x => p x
+ prop := λ x => x.property
+
+@[simp]
+abbrev Slice.length {α : Type u} (v : Slice α) : Int := v.val.len
+
+@[simp]
+abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val
+
+example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
+ scalar_tac
+
+def Slice.new (α : Type u): Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+
+-- TODO: very annoying that the α is an explicit parameter
+def Slice.len (α : Type u) (v : Slice α) : Usize :=
+ Usize.ofIntCore v.val.len (by scalar_tac) (by scalar_tac)
+
+@[simp]
+theorem Slice.len_val {α : Type u} (v : Slice α) : (Slice.len α v).val = v.length :=
+ by rfl
+
+@[simp]
+abbrev Slice.index_s {α : Type u} [Inhabited α] (v: Slice α) (i: Int) : α :=
+ v.val.index i
+
+@[simp]
+abbrev Slice.slice {α : Type u} [Inhabited α] (s : Slice α) (i j : Int) : List α :=
+ s.val.slice i j
+
+def Slice.index_usize (α : Type u) (v: Slice α) (i: Usize) : Result α :=
+ match v.val.indexOpt i.val with
+ | none => fail .arrayOutOfBounds
+ | some x => ret x
+
+/- In the theorems below: we don't always need the `∃ ..`, but we use one
+ so that `progress` introduces an opaque variable and an equality. This
+ helps control the context.
+ -/
+
+@[pspec]
+theorem Slice.index_usize_spec {α : Type u} [Inhabited α] (v: Slice α) (i: Usize)
+ (hbound : i.val < v.length) :
+ ∃ x, v.index_usize α i = ret x ∧ x = v.val.index i.val := by
+ simp only [index_usize]
+ -- TODO: dependent rewrite
+ have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
+ simp [*]
+
+-- This shouldn't be used
+def Slice.index_shared_back (α : Type u) (v: Slice α) (i: Usize) (_: α) : Result Unit :=
+ if i.val < List.length v.val then
+ .ret ()
+ else
+ .fail arrayOutOfBounds
+
+def Slice.update_usize (α : Type u) (v: Slice α) (i: Usize) (x: α) : Result (Slice α) :=
+ match v.val.indexOpt i.val with
+ | none => fail .arrayOutOfBounds
+ | some _ =>
+ .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
+
+@[pspec]
+theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
+ (hbound : i.val < v.length) :
+ ∃ nv, v.update_usize α i x = ret nv ∧
+ nv.val = v.val.update i.val x
+ := by
+ simp only [update_usize]
+ have h := List.indexOpt_bounds v.val i.val
+ split
+ . simp_all [length]; cases h <;> scalar_tac
+ . simp_all
+
+/- Array to slice/subslices -/
+
+/- We could make this function not use the `Result` type. By making it monadic, we
+ push the user to use the `Array.to_slice_spec` spec theorem below (through the
+ `progress` tactic), meaning `Array.to_slice` should be considered as opaque.
+ All what the spec theorem reveals is that the "representative" lists are the same. -/
+def Array.to_slice (α : Type u) (n : Usize) (v : Array α n) : Result (Slice α) :=
+ ret ⟨ v.val, by simp [← List.len_eq_length]; scalar_tac ⟩
+
+@[pspec]
+theorem Array.to_slice_spec {α : Type u} {n : Usize} (v : Array α n) :
+ ∃ s, to_slice α n v = ret s ∧ v.val = s.val := by simp [to_slice]
+
+def Array.from_slice (α : Type u) (n : Usize) (_ : Array α n) (s : Slice α) : Result (Array α n) :=
+ if h: s.val.len = n.val then
+ ret ⟨ s.val, by simp [← List.len_eq_length, *] ⟩
+ else fail panic
+
+@[pspec]
+theorem Array.from_slice_spec {α : Type u} {n : Usize} (a : Array α n) (ns : Slice α) (h : ns.val.len = n.val) :
+ ∃ na, from_slice α n a ns = ret na ∧ na.val = ns.val
+ := by simp [from_slice, *]
+
+def Array.subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) : Result (Slice α) :=
+ -- TODO: not completely sure here
+ if r.start.val < r.end_.val ∧ r.end_.val ≤ a.val.len then
+ ret ⟨ a.val.slice r.start.val r.end_.val,
+ by
+ simp [← List.len_eq_length]
+ have := a.val.slice_len_le r.start.val r.end_.val
+ scalar_tac ⟩
+ else
+ fail panic
+
+@[pspec]
+theorem Array.subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize)
+ (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ a.val.len) :
+ ∃ s, subslice α n a r = ret s ∧
+ s.val = a.val.slice r.start.val r.end_.val ∧
+ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → s.val.index i = a.val.index (r.start.val + i))
+ := by
+ simp [subslice, *]
+ intro i _ _
+ have := List.index_slice r.start.val r.end_.val i a.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
+ simp [*]
+
+def Array.update_subslice (α : Type u) (n : Usize) (a : Array α n) (r : Range Usize) (s : Slice α) : Result (Array α n) :=
+ -- TODO: not completely sure here
+ if h: r.start.val < r.end_.val ∧ r.end_.val ≤ a.length ∧ s.val.len = r.end_.val - r.start.val then
+ let s_beg := a.val.itake r.start.val
+ let s_end := a.val.idrop r.end_.val
+ have : s_beg.len = r.start.val := by
+ apply List.itake_len
+ . simp_all; scalar_tac
+ . scalar_tac
+ have : s_end.len = a.val.len - r.end_.val := by
+ apply List.idrop_len
+ . scalar_tac
+ . scalar_tac
+ let na := s_beg.append (s.val.append s_end)
+ have : na.len = a.val.len := by simp [*]
+ ret ⟨ na, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+ else
+ fail panic
+
+-- TODO: it is annoying to write `.val` everywhere. We could leverage coercions,
+-- but: some symbols like `+` are already overloaded to be notations for monadic
+-- operations/
+-- We should introduce special symbols for the monadic arithmetic operations
+-- (the use will never write those symbols directly).
+@[pspec]
+theorem Array.update_subslice_spec {α : Type u} {n : Usize} [Inhabited α] (a : Array α n) (r : Range Usize) (s : Slice α)
+ (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : s.length = r.end_.val - r.start.val) :
+ ∃ na, update_subslice α n a r s = ret na ∧
+ (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
+ (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = s.index_s (i - r.start.val)) ∧
+ (∀ i, r.end_.val ≤ i → i < n.val → na.index_s i = a.index_s i) := by
+ simp [update_subslice, *]
+ have h := List.replace_slice_index r.start.val r.end_.val a.val s.val
+ (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
+ simp [List.replace_slice] at h
+ have ⟨ h0, h1, h2 ⟩ := h
+ clear h
+ split_conjs
+ . intro i _ _
+ have := h0 i (by int_tac) (by int_tac)
+ simp [*]
+ . intro i _ _
+ have := h1 i (by int_tac) (by int_tac)
+ simp [*]
+ . intro i _ _
+ have := h2 i (by int_tac) (by int_tac)
+ simp [*]
+
+def Slice.subslice (α : Type u) (s : Slice α) (r : Range Usize) : Result (Slice α) :=
+ -- TODO: not completely sure here
+ if r.start.val < r.end_.val ∧ r.end_.val ≤ s.length then
+ ret ⟨ s.val.slice r.start.val r.end_.val,
+ by
+ simp [← List.len_eq_length]
+ have := s.val.slice_len_le r.start.val r.end_.val
+ scalar_tac ⟩
+ else
+ fail panic
+
+@[pspec]
+theorem Slice.subslice_spec {α : Type u} [Inhabited α] (s : Slice α) (r : Range Usize)
+ (h0 : r.start.val < r.end_.val) (h1 : r.end_.val ≤ s.val.len) :
+ ∃ ns, subslice α s r = ret ns ∧
+ ns.val = s.slice r.start.val r.end_.val ∧
+ (∀ i, 0 ≤ i → i + r.start.val < r.end_.val → ns.index_s i = s.index_s (r.start.val + i))
+ := by
+ simp [subslice, *]
+ intro i _ _
+ have := List.index_slice r.start.val r.end_.val i s.val (by scalar_tac) (by scalar_tac) (by trivial) (by scalar_tac)
+ simp [*]
+
+attribute [pp_dot] List.len List.length List.index -- use the dot notation when printing
+set_option pp.coercions false -- do not print coercions with ↑ (this doesn't parse)
+
+def Slice.update_subslice (α : Type u) (s : Slice α) (r : Range Usize) (ss : Slice α) : Result (Slice α) :=
+ -- TODO: not completely sure here
+ if h: r.start.val < r.end_.val ∧ r.end_.val ≤ s.length ∧ ss.val.len = r.end_.val - r.start.val then
+ let s_beg := s.val.itake r.start.val
+ let s_end := s.val.idrop r.end_.val
+ have : s_beg.len = r.start.val := by
+ apply List.itake_len
+ . simp_all; scalar_tac
+ . scalar_tac
+ have : s_end.len = s.val.len - r.end_.val := by
+ apply List.idrop_len
+ . scalar_tac
+ . scalar_tac
+ let ns := s_beg.append (ss.val.append s_end)
+ have : ns.len = s.val.len := by simp [*]
+ ret ⟨ ns, by simp_all [← List.len_eq_length]; scalar_tac ⟩
+ else
+ fail panic
+
+@[pspec]
+theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (r : Range Usize) (ss : Slice α)
+ (_ : r.start.val < r.end_.val) (_ : r.end_.val ≤ a.length) (_ : ss.length = r.end_.val - r.start.val) :
+ ∃ na, update_subslice α a r ss = ret na ∧
+ (∀ i, 0 ≤ i → i < r.start.val → na.index_s i = a.index_s i) ∧
+ (∀ i, r.start.val ≤ i → i < r.end_.val → na.index_s i = ss.index_s (i - r.start.val)) ∧
+ (∀ i, r.end_.val ≤ i → i < a.length → na.index_s i = a.index_s i) := by
+ simp [update_subslice, *]
+ have h := List.replace_slice_index r.start.val r.end_.val a.val ss.val
+ (by scalar_tac) (by scalar_tac) (by scalar_tac) (by scalar_tac)
+ simp [List.replace_slice, *] at h
+ have ⟨ h0, h1, h2 ⟩ := h
+ clear h
+ split_conjs
+ . intro i _ _
+ have := h0 i (by int_tac) (by int_tac)
+ simp [*]
+ . intro i _ _
+ have := h1 i (by int_tac) (by int_tac)
+ simp [*]
+ . intro i _ _
+ have := h2 i (by int_tac) (by int_tac)
+ simp [*]
+
+/- Trait declaration: [core::slice::index::private_slice_index::Sealed] -/
+structure core.slice.index.private_slice_index.Sealed (Self : Type) where
+
+/- Trait declaration: [core::slice::index::SliceIndex] -/
+structure core.slice.index.SliceIndex (Self T : Type) where
+ sealedInst : core.slice.index.private_slice_index.Sealed Self
+ Output : Type
+ get : Self → T → Result (Option Output)
+ get_mut : Self → T → Result (Option Output)
+ get_mut_back : Self → T → Option Output → Result T
+ get_unchecked : Self → ConstRawPtr T → Result (ConstRawPtr Output)
+ get_unchecked_mut : Self → MutRawPtr T → Result (MutRawPtr Output)
+ index : Self → T → Result Output
+ index_mut : Self → T → Result Output
+ index_mut_back : Self → T → Output → Result T
+
+/- [core::slice::index::[T]::index]: forward function -/
+def core.slice.index.Slice.index
+ (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+ (slice : Slice T) (i : I) : Result inst.Output := do
+ let x ← inst.get i slice
+ match x with
+ | none => fail panic
+ | some x => ret x
+
+/- [core::slice::index::Range:::get]: forward function -/
+def core.slice.index.Range.get (T : Type) (i : Range Usize) (slice : Slice T) :
+ Result (Option (Slice T)) :=
+ sorry -- TODO
+
+/- [core::slice::index::Range::get_mut]: forward function -/
+def core.slice.index.Range.get_mut
+ (T : Type) : Range Usize → Slice T → Result (Option (Slice T)) :=
+ sorry -- TODO
+
+/- [core::slice::index::Range::get_mut]: backward function 0 -/
+def core.slice.index.Range.get_mut_back
+ (T : Type) :
+ Range Usize → Slice T → Option (Slice T) → Result (Slice T) :=
+ sorry -- TODO
+
+/- [core::slice::index::Range::get_unchecked]: forward function -/
+def core.slice.index.Range.get_unchecked
+ (T : Type) :
+ Range Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr (Slice T)) :=
+ -- Don't know what the model should be - for now we always fail to make
+ -- sure code which uses it fails
+ fun _ _ => fail panic
+
+/- [core::slice::index::Range::get_unchecked_mut]: forward function -/
+def core.slice.index.Range.get_unchecked_mut
+ (T : Type) :
+ Range Usize → MutRawPtr (Slice T) → Result (MutRawPtr (Slice T)) :=
+ -- Don't know what the model should be - for now we always fail to make
+ -- sure code which uses it fails
+ fun _ _ => fail panic
+
+/- [core::slice::index::Range::index]: forward function -/
+def core.slice.index.Range.index
+ (T : Type) : Range Usize → Slice T → Result (Slice T) :=
+ sorry -- TODO
+
+/- [core::slice::index::Range::index_mut]: forward function -/
+def core.slice.index.Range.index_mut
+ (T : Type) : Range Usize → Slice T → Result (Slice T) :=
+ sorry -- TODO
+
+/- [core::slice::index::Range::index_mut]: backward function 0 -/
+def core.slice.index.Range.index_mut_back
+ (T : Type) : Range Usize → Slice T → Slice T → Result (Slice T) :=
+ sorry -- TODO
+
+/- [core::slice::index::[T]::index_mut]: forward function -/
+def core.slice.index.Slice.index_mut
+ (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) :
+ Slice T → I → Result inst.Output :=
+ sorry -- TODO
+
+/- [core::slice::index::[T]::index_mut]: backward function 0 -/
+def core.slice.index.Slice.index_mut_back
+ (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T)) :
+ Slice T → I → inst.Output → Result (Slice T) :=
+ sorry -- TODO
+
+/- [core::array::[T; N]::index]: forward function -/
+def core.array.Array.index
+ (T I : Type) (N : Usize) (inst : core.ops.index.Index (Slice T) I)
+ (a : Array T N) (i : I) : Result inst.Output :=
+ sorry -- TODO
+
+/- [core::array::[T; N]::index_mut]: forward function -/
+def core.array.Array.index_mut
+ (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I)
+ (a : Array T N) (i : I) : Result inst.indexInst.Output :=
+ sorry -- TODO
+
+/- [core::array::[T; N]::index_mut]: backward function 0 -/
+def core.array.Array.index_mut_back
+ (T I : Type) (N : Usize) (inst : core.ops.index.IndexMut (Slice T) I)
+ (a : Array T N) (i : I) (x : inst.indexInst.Output) : Result (Array T N) :=
+ sorry -- TODO
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.slice.index.Slice.coreopsindexIndexInst (T I : Type)
+ (inst : core.slice.index.SliceIndex I (Slice T)) :
+ core.ops.index.Index (Slice T) I := {
+ Output := inst.Output
+ index := core.slice.index.Slice.index T I inst
+}
+
+/- Trait implementation: [core::slice::index::private_slice_index::Range] -/
+def core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+ : core.slice.index.private_slice_index.Sealed (Range Usize) := {}
+
+/- Trait implementation: [core::slice::index::Range] -/
+def core.slice.index.Range.coresliceindexSliceIndexInst (T : Type) :
+ core.slice.index.SliceIndex (Range Usize) (Slice T) := {
+ sealedInst :=
+ core.slice.index.private_slice_index.Range.coresliceindexprivate_slice_indexSealedInst
+ Output := Slice T
+ get := core.slice.index.Range.get T
+ get_mut := core.slice.index.Range.get_mut T
+ get_mut_back := core.slice.index.Range.get_mut_back T
+ get_unchecked := core.slice.index.Range.get_unchecked T
+ get_unchecked_mut := core.slice.index.Range.get_unchecked_mut T
+ index := core.slice.index.Range.index T
+ index_mut := core.slice.index.Range.index_mut T
+ index_mut_back := core.slice.index.Range.index_mut_back T
+}
+
+/- Trait implementation: [core::slice::index::[T]] -/
+def core.slice.index.Slice.coreopsindexIndexMutInst (T I : Type)
+ (inst : core.slice.index.SliceIndex I (Slice T)) :
+ core.ops.index.IndexMut (Slice T) I := {
+ indexInst := core.slice.index.Slice.coreopsindexIndexInst T I inst
+ index_mut := core.slice.index.Slice.index_mut T I inst
+ index_mut_back := core.slice.index.Slice.index_mut_back T I inst
+}
+
+/- Trait implementation: [core::array::[T; N]] -/
+def core.array.Array.coreopsindexIndexInst (T I : Type) (N : Usize)
+ (inst : core.ops.index.Index (Slice T) I) :
+ core.ops.index.Index (Array T N) I := {
+ Output := inst.Output
+ index := core.array.Array.index T I N inst
+}
+
+/- Trait implementation: [core::array::[T; N]] -/
+def core.array.Array.coreopsindexIndexMutInst (T I : Type) (N : Usize)
+ (inst : core.ops.index.IndexMut (Slice T) I) :
+ core.ops.index.IndexMut (Array T N) I := {
+ indexInst := core.array.Array.coreopsindexIndexInst T I N inst.indexInst
+ index_mut := core.array.Array.index_mut T I N inst
+ index_mut_back := core.array.Array.index_mut_back T I N inst
+}
+
+/- [core::slice::index::usize::get]: forward function -/
+def core.slice.index.Usize.get
+ (T : Type) : Usize → Slice T → Result (Option T) :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::get_mut]: forward function -/
+def core.slice.index.Usize.get_mut
+ (T : Type) : Usize → Slice T → Result (Option T) :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::get_mut]: backward function 0 -/
+def core.slice.index.Usize.get_mut_back
+ (T : Type) : Usize → Slice T → Option T → Result (Slice T) :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::get_unchecked]: forward function -/
+def core.slice.index.Usize.get_unchecked
+ (T : Type) : Usize → ConstRawPtr (Slice T) → Result (ConstRawPtr T) :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::get_unchecked_mut]: forward function -/
+def core.slice.index.Usize.get_unchecked_mut
+ (T : Type) : Usize → MutRawPtr (Slice T) → Result (MutRawPtr T) :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::index]: forward function -/
+def core.slice.index.Usize.index (T : Type) : Usize → Slice T → Result T :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::index_mut]: forward function -/
+def core.slice.index.Usize.index_mut (T : Type) : Usize → Slice T → Result T :=
+ sorry -- TODO
+
+/- [core::slice::index::usize::index_mut]: backward function 0 -/
+def core.slice.index.Usize.index_mut_back
+ (T : Type) : Usize → Slice T → T → Result (Slice T) :=
+ sorry -- TODO
+
+/- Trait implementation: [core::slice::index::private_slice_index::usize] -/
+def core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+ : core.slice.index.private_slice_index.Sealed Usize := {}
+
+/- Trait implementation: [core::slice::index::usize] -/
+def core.slice.index.usize.coresliceindexSliceIndexInst (T : Type) :
+ core.slice.index.SliceIndex Usize (Slice T) := {
+ sealedInst := core.slice.index.private_slice_index.usize.coresliceindexprivate_slice_indexSealedInst
+ Output := T
+ get := core.slice.index.Usize.get T
+ get_mut := core.slice.index.Usize.get_mut T
+ get_mut_back := core.slice.index.Usize.get_mut_back T
+ get_unchecked := core.slice.index.Usize.get_unchecked T
+ get_unchecked_mut := core.slice.index.Usize.get_unchecked_mut T
+ index := core.slice.index.Usize.index T
+ index_mut := core.slice.index.Usize.index_mut T
+ index_mut_back := core.slice.index.Usize.index_mut_back T
+}
+
+end Primitives
diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean
index 7c0fa3bb..7fc33251 100644
--- a/backends/lean/Base/Primitives/Base.lean
+++ b/backends/lean/Base/Primitives/Base.lean
@@ -120,11 +120,18 @@ def Result.attach {α: Type} (o : Result α): Result { x : α // o = ret x } :=
-- MISC --
----------
-@[simp] def mem.replace (a : Type) (x : a) (_ : a) : a := x
-@[simp] def mem.replace_back (a : Type) (_ : a) (y : a) : a := y
+@[simp] def core.mem.replace (a : Type) (x : a) (_ : a) : a := x
+@[simp] def core.mem.replace_back (a : Type) (_ : a) (y : a) : a := y
/-- Aeneas-translated function -- useful to reduce non-recursive definitions.
Use with `simp [ aeneas ]` -/
register_simp_attr aeneas
+-- We don't really use raw pointers for now
+structure MutRawPtr (T : Type) where
+ v : T
+
+structure ConstRawPtr (T : Type) where
+ v : T
+
end Primitives
diff --git a/backends/lean/Base/Primitives/CoreOps.lean b/backends/lean/Base/Primitives/CoreOps.lean
new file mode 100644
index 00000000..da458f66
--- /dev/null
+++ b/backends/lean/Base/Primitives/CoreOps.lean
@@ -0,0 +1,37 @@
+import Lean
+import Base.Primitives.Base
+
+open Primitives
+open Result
+
+namespace core.ops
+
+namespace index -- core.ops.index
+
+/- Trait declaration: [core::ops::index::Index] -/
+structure Index (Self Idx : Type) where
+ Output : Type
+ index : Self → Idx → Result Output
+
+/- Trait declaration: [core::ops::index::IndexMut] -/
+structure IndexMut (Self Idx : Type) where
+ indexInst : Index Self Idx
+ index_mut : Self → Idx → Result indexInst.Output
+ index_mut_back : Self → Idx → indexInst.Output → Result Self
+
+end index -- core.ops.index
+
+namespace deref -- core.ops.deref
+
+structure Deref (Self : Type) where
+ Target : Type
+ deref : Self → Result Target
+
+structure DerefMut (Self : Type) where
+ derefInst : Deref Self
+ deref_mut : Self → Result derefInst.Target
+ deref_mut_back : Self → derefInst.Target → Result Self
+
+end deref -- core.ops.deref
+
+end core.ops
diff --git a/backends/lean/Base/Primitives/Range.lean b/backends/lean/Base/Primitives/Range.lean
index 26cbee42..a268bcba 100644
--- a/backends/lean/Base/Primitives/Range.lean
+++ b/backends/lean/Base/Primitives/Range.lean
@@ -11,7 +11,7 @@ import Base.Progress.Base
namespace Primitives
-structure Range (α : Type u) where
+structure core.ops.range.Range (α : Type u) where
mk ::
start: α
end_: α
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 55227a9f..ec9665a5 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -230,6 +230,20 @@ def Scalar.cMax (ty : ScalarTy) : Int :=
| .Usize => Scalar.max .U32
| _ => Scalar.max ty
+theorem Scalar.min_lt_max (ty : ScalarTy) : Scalar.min ty < Scalar.max ty := by
+ cases ty <;> simp [Scalar.min, Scalar.max]
+ . simp [Isize.min, Isize.max]
+ have h1 := Isize.refined_min.property
+ have h2 := Isize.refined_max.property
+ cases h1 <;> cases h2 <;> simp [*]
+ . simp [Usize.max]
+ have h := Usize.refined_max.property
+ cases h <;> simp [*]
+
+theorem Scalar.min_le_max (ty : ScalarTy) : Scalar.min ty ≤ Scalar.max ty := by
+ have := Scalar.min_lt_max ty
+ int_tac
+
theorem Scalar.cMin_bound ty : Scalar.min ty ≤ Scalar.cMin ty := by
cases ty <;> simp [Scalar.min, Scalar.max, Scalar.cMin, Scalar.cMax] at *
have h := Isize.refined_min.property
@@ -395,6 +409,34 @@ def Scalar.cast {src_ty : ScalarTy} (tgt_ty : ScalarTy) (x : Scalar src_ty) : Re
@[reducible] def U64 := Scalar .U64
@[reducible] def U128 := Scalar .U128
+-- TODO: reducible?
+@[reducible] def core_isize_min : Isize := Scalar.ofInt Isize.min (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def core_isize_max : Isize := Scalar.ofInt Isize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Isize))
+@[reducible] def core_i8_min : I8 := Scalar.ofInt I8.min
+@[reducible] def core_i8_max : I8 := Scalar.ofInt I8.max
+@[reducible] def core_i16_min : I16 := Scalar.ofInt I16.min
+@[reducible] def core_i16_max : I16 := Scalar.ofInt I16.max
+@[reducible] def core_i32_min : I32 := Scalar.ofInt I32.min
+@[reducible] def core_i32_max : I32 := Scalar.ofInt I32.max
+@[reducible] def core_i64_min : I64 := Scalar.ofInt I64.min
+@[reducible] def core_i64_max : I64 := Scalar.ofInt I64.max
+@[reducible] def core_i128_min : I128 := Scalar.ofInt I128.min
+@[reducible] def core_i128_max : I128 := Scalar.ofInt I128.max
+
+-- TODO: reducible?
+@[reducible] def core_usize_min : Usize := Scalar.ofInt Usize.min
+@[reducible] def core_usize_max : Usize := Scalar.ofInt Usize.max (by simp [Scalar.min, Scalar.max]; apply (Scalar.min_le_max .Usize))
+@[reducible] def core_u8_min : U8 := Scalar.ofInt U8.min
+@[reducible] def core_u8_max : U8 := Scalar.ofInt U8.max
+@[reducible] def core_u16_min : U16 := Scalar.ofInt U16.min
+@[reducible] def core_u16_max : U16 := Scalar.ofInt U16.max
+@[reducible] def core_u32_min : U32 := Scalar.ofInt U32.min
+@[reducible] def core_u32_max : U32 := Scalar.ofInt U32.max
+@[reducible] def core_u64_min : U64 := Scalar.ofInt U64.min
+@[reducible] def core_u64_max : U64 := Scalar.ofInt U64.max
+@[reducible] def core_u128_min : U128 := Scalar.ofInt U128.min
+@[reducible] def core_u128_max : U128 := Scalar.ofInt U128.max
+
-- TODO: below: not sure this is the best way.
-- Should we rather overload operations like +, -, etc.?
-- Also, it is possible to automate the generation of those definitions
@@ -861,33 +903,33 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
-- ofIntCore
-- TODO: typeclass?
-@[reducible] def Isize.ofIntCore := @Scalar.ofIntCore .Isize
-@[reducible] def I8.ofIntCore := @Scalar.ofIntCore .I8
-@[reducible] def I16.ofIntCore := @Scalar.ofIntCore .I16
-@[reducible] def I32.ofIntCore := @Scalar.ofIntCore .I32
-@[reducible] def I64.ofIntCore := @Scalar.ofIntCore .I64
-@[reducible] def I128.ofIntCore := @Scalar.ofIntCore .I128
-@[reducible] def Usize.ofIntCore := @Scalar.ofIntCore .Usize
-@[reducible] def U8.ofIntCore := @Scalar.ofIntCore .U8
-@[reducible] def U16.ofIntCore := @Scalar.ofIntCore .U16
-@[reducible] def U32.ofIntCore := @Scalar.ofIntCore .U32
-@[reducible] def U64.ofIntCore := @Scalar.ofIntCore .U64
-@[reducible] def U128.ofIntCore := @Scalar.ofIntCore .U128
+def Isize.ofIntCore := @Scalar.ofIntCore .Isize
+def I8.ofIntCore := @Scalar.ofIntCore .I8
+def I16.ofIntCore := @Scalar.ofIntCore .I16
+def I32.ofIntCore := @Scalar.ofIntCore .I32
+def I64.ofIntCore := @Scalar.ofIntCore .I64
+def I128.ofIntCore := @Scalar.ofIntCore .I128
+def Usize.ofIntCore := @Scalar.ofIntCore .Usize
+def U8.ofIntCore := @Scalar.ofIntCore .U8
+def U16.ofIntCore := @Scalar.ofIntCore .U16
+def U32.ofIntCore := @Scalar.ofIntCore .U32
+def U64.ofIntCore := @Scalar.ofIntCore .U64
+def U128.ofIntCore := @Scalar.ofIntCore .U128
-- ofInt
-- TODO: typeclass?
-@[reducible] def Isize.ofInt := @Scalar.ofInt .Isize
-@[reducible] def I8.ofInt := @Scalar.ofInt .I8
-@[reducible] def I16.ofInt := @Scalar.ofInt .I16
-@[reducible] def I32.ofInt := @Scalar.ofInt .I32
-@[reducible] def I64.ofInt := @Scalar.ofInt .I64
-@[reducible] def I128.ofInt := @Scalar.ofInt .I128
-@[reducible] def Usize.ofInt := @Scalar.ofInt .Usize
-@[reducible] def U8.ofInt := @Scalar.ofInt .U8
-@[reducible] def U16.ofInt := @Scalar.ofInt .U16
-@[reducible] def U32.ofInt := @Scalar.ofInt .U32
-@[reducible] def U64.ofInt := @Scalar.ofInt .U64
-@[reducible] def U128.ofInt := @Scalar.ofInt .U128
+abbrev Isize.ofInt := @Scalar.ofInt .Isize
+abbrev I8.ofInt := @Scalar.ofInt .I8
+abbrev I16.ofInt := @Scalar.ofInt .I16
+abbrev I32.ofInt := @Scalar.ofInt .I32
+abbrev I64.ofInt := @Scalar.ofInt .I64
+abbrev I128.ofInt := @Scalar.ofInt .I128
+abbrev Usize.ofInt := @Scalar.ofInt .Usize
+abbrev U8.ofInt := @Scalar.ofInt .U8
+abbrev U16.ofInt := @Scalar.ofInt .U16
+abbrev U32.ofInt := @Scalar.ofInt .U32
+abbrev U64.ofInt := @Scalar.ofInt .U64
+abbrev U128.ofInt := @Scalar.ofInt .U128
postfix:max "#isize" => Isize.ofInt
postfix:max "#i8" => I8.ofInt
@@ -905,9 +947,46 @@ postfix:max "#u128" => U128.ofInt
-- Testing the notations
example : Result Usize := 0#usize + 1#usize
+-- TODO: factor those lemmas out
@[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofInt x h).val = x := by
simp [Scalar.ofInt, Scalar.ofIntCore]
+@[simp] theorem Isize.ofInt_val_eq (h : Scalar.min ScalarTy.Isize ≤ x ∧ x ≤ Scalar.max ScalarTy.Isize) : (Isize.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I8.ofInt_val_eq (h : Scalar.min ScalarTy.I8 ≤ x ∧ x ≤ Scalar.max ScalarTy.I8) : (I8.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I16.ofInt_val_eq (h : Scalar.min ScalarTy.I16 ≤ x ∧ x ≤ Scalar.max ScalarTy.I16) : (I16.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I32.ofInt_val_eq (h : Scalar.min ScalarTy.I32 ≤ x ∧ x ≤ Scalar.max ScalarTy.I32) : (I32.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I64.ofInt_val_eq (h : Scalar.min ScalarTy.I64 ≤ x ∧ x ≤ Scalar.max ScalarTy.I64) : (I64.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem I128.ofInt_val_eq (h : Scalar.min ScalarTy.I128 ≤ x ∧ x ≤ Scalar.max ScalarTy.I128) : (I128.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem Usize.ofInt_val_eq (h : Scalar.min ScalarTy.Usize ≤ x ∧ x ≤ Scalar.max ScalarTy.Usize) : (Usize.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U8.ofInt_val_eq (h : Scalar.min ScalarTy.U8 ≤ x ∧ x ≤ Scalar.max ScalarTy.U8) : (U8.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U16.ofInt_val_eq (h : Scalar.min ScalarTy.U16 ≤ x ∧ x ≤ Scalar.max ScalarTy.U16) : (U16.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U32.ofInt_val_eq (h : Scalar.min ScalarTy.U32 ≤ x ∧ x ≤ Scalar.max ScalarTy.U32) : (U32.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U64.ofInt_val_eq (h : Scalar.min ScalarTy.U64 ≤ x ∧ x ≤ Scalar.max ScalarTy.U64) : (U64.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
+@[simp] theorem U128.ofInt_val_eq (h : Scalar.min ScalarTy.U128 ≤ x ∧ x ≤ Scalar.max ScalarTy.U128) : (U128.ofInt x h).val = x := by
+ apply Scalar.ofInt_val_eq h
+
-- Comparisons
instance {ty} : LT (Scalar ty) where
lt a b := LT.lt a.val b.val
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index c4c4d9f2..bbed6082 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -6,7 +6,7 @@ import Mathlib.Tactic.RunCmd
import Mathlib.Tactic.Linarith
import Base.IList
import Base.Primitives.Scalar
-import Base.Primitives.Array
+import Base.Primitives.ArraySlice
import Base.Arith
import Base.Progress.Base
@@ -14,6 +14,8 @@ namespace Primitives
open Result Error
+namespace alloc.vec
+
def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max }
instance (a : Type u) : Arith.HasIntProp (Vec a) where
@@ -79,7 +81,7 @@ theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α)
∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
simp [insert, *]
-def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
+def Vec.index_usize {α : Type u} (v: Vec α) (i: Usize) : Result α :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some x => ret x
@@ -90,51 +92,83 @@ def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α :=
-/
@[pspec]
-theorem Vec.index_shared_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
- (hbound : i.val < v.length) :
- ∃ x, v.index_shared α i = ret x ∧ x = v.val.index i.val := by
- simp only [index_shared]
- -- TODO: dependent rewrite
- have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
- simp [*]
-
--- This shouldn't be used
-def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
- if i.val < List.length v.val then
- .ret ()
- else
- .fail arrayOutOfBounds
-
-def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α :=
- match v.val.indexOpt i.val with
- | none => fail .arrayOutOfBounds
- | some x => ret x
-
-@[pspec]
-theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
+theorem Vec.index_usize_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize)
(hbound : i.val < v.length) :
- ∃ x, v.index_mut α i = ret x ∧ x = v.val.index i.val := by
- simp only [index_mut]
+ ∃ x, v.index_usize i = ret x ∧ x = v.val.index i.val := by
+ simp only [index_usize]
-- TODO: dependent rewrite
have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*])
simp [*]
-def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+def Vec.update_usize {α : Type u} (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
match v.val.indexOpt i.val with
| none => fail .arrayOutOfBounds
| some _ =>
.ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
@[pspec]
-theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
+theorem Vec.update_usize_spec {α : Type u} (v: Vec α) (i: Usize) (x : α)
(hbound : i.val < v.length) :
- ∃ nv, v.index_mut_back α i x = ret nv ∧
+ ∃ nv, v.update_usize i x = ret nv ∧
nv.val = v.val.update i.val x
:= by
- simp only [index_mut_back]
+ simp only [update_usize]
have h := List.indexOpt_bounds v.val i.val
split
. simp_all [length]; cases h <;> scalar_tac
. simp_all
+/- [alloc::vec::Vec::index]: forward function -/
+def Vec.index (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+ (self : Vec T) (i : I) : Result inst.Output :=
+ sorry -- TODO
+
+/- [alloc::vec::Vec::index_mut]: forward function -/
+def Vec.index_mut (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+ (self : Vec T) (i : I) : Result inst.Output :=
+ sorry -- TODO
+
+/- [alloc::vec::Vec::index_mut]: backward function 0 -/
+def Vec.index_mut_back
+ (T I : Type) (inst : core.slice.index.SliceIndex I (Slice T))
+ (self : Vec T) (i : I) (x : inst.Output) : Result (alloc.vec.Vec T) :=
+ sorry -- TODO
+
+/- Trait implementation: [alloc::vec::Vec] -/
+def Vec.coreopsindexIndexInst (T I : Type)
+ (inst : core.slice.index.SliceIndex I (Slice T)) :
+ core.ops.index.Index (alloc.vec.Vec T) I := {
+ Output := inst.Output
+ index := Vec.index T I inst
+}
+
+/- Trait implementation: [alloc::vec::Vec] -/
+def Vec.coreopsindexIndexMutInst (T I : Type)
+ (inst : core.slice.index.SliceIndex I (Slice T)) :
+ core.ops.index.IndexMut (alloc.vec.Vec T) I := {
+ indexInst := Vec.coreopsindexIndexInst T I inst
+ index_mut := Vec.index_mut T I inst
+ index_mut_back := Vec.index_mut_back T I inst
+}
+
+@[simp]
+theorem Vec.index_slice_index {α : Type} (v : Vec α) (i : Usize) :
+ Vec.index α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+ Vec.index_usize v i :=
+ sorry
+
+@[simp]
+theorem Vec.index_mut_slice_index {α : Type} (v : Vec α) (i : Usize) :
+ Vec.index_mut α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i =
+ Vec.index_usize v i :=
+ sorry
+
+@[simp]
+theorem Vec.index_mut_back_slice_index {α : Type} (v : Vec α) (i : Usize) (x : α) :
+ Vec.index_mut_back α Usize (core.slice.index.usize.coresliceindexSliceIndexInst α) v i x =
+ Vec.update_usize v i x :=
+ sorry
+
+end alloc.vec
+
end Primitives
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 8b0759c5..ba63f09d 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -8,6 +8,27 @@ namespace Progress
open Lean Elab Term Meta Tactic
open Utils
+-- TODO: the scalar types annoyingly often get reduced when we use the progress
+-- tactic. We should find a way of controling reduction. For now we use rewriting
+-- lemmas to make sure the goal remains clean, but this complexifies proof terms.
+-- It seems there used to be a `fold` tactic.
+theorem scalar_isize_eq : Primitives.Scalar .Isize = Primitives.Isize := by rfl
+theorem scalar_i8_eq : Primitives.Scalar .I8 = Primitives.I8 := by rfl
+theorem scalar_i16_eq : Primitives.Scalar .I16 = Primitives.I16 := by rfl
+theorem scalar_i32_eq : Primitives.Scalar .I32 = Primitives.I32 := by rfl
+theorem scalar_i64_eq : Primitives.Scalar .I64 = Primitives.I64 := by rfl
+theorem scalar_i128_eq : Primitives.Scalar .I128 = Primitives.I128 := by rfl
+theorem scalar_usize_eq : Primitives.Scalar .Usize = Primitives.Usize := by rfl
+theorem scalar_u8_eq : Primitives.Scalar .U8 = Primitives.U8 := by rfl
+theorem scalar_u16_eq : Primitives.Scalar .U16 = Primitives.U16 := by rfl
+theorem scalar_u32_eq : Primitives.Scalar .U32 = Primitives.U32 := by rfl
+theorem scalar_u64_eq : Primitives.Scalar .U64 = Primitives.U64 := by rfl
+theorem scalar_u128_eq : Primitives.Scalar .U128 = Primitives.U128 := by rfl
+def scalar_eqs := [
+ ``scalar_isize_eq, ``scalar_i8_eq, ``scalar_i16_eq, ``scalar_i32_eq, ``scalar_i64_eq, ``scalar_i128_eq,
+ ``scalar_usize_eq, ``scalar_u8_eq, ``scalar_u16_eq, ``scalar_u32_eq, ``scalar_u64_eq, ``scalar_u128_eq
+]
+
inductive TheoremOrLocal where
| Theorem (thName : Name)
| Local (asm : LocalDecl)
@@ -111,8 +132,11 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
splitEqAndPost fun hEq hPost ids => do
trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
tryTac (
- simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+ simpAt true []
+ [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
[hEq.fvarId!] (.targets #[] true))
+ -- TODO: remove this (some types get unfolded too much: we "fold" them back)
+ tryTac (simpAt true [] scalar_eqs [] .wildcard_dep)
-- Clear the equality, unless the user requests not to do so
let mgoal ← do
if keep.isSome then getMainGoal
@@ -359,6 +383,7 @@ namespace Test
-- #eval showStoredPSpec
-- #eval showStoredPSpecClass
-- #eval showStoredPSpecExprClass
+ open alloc.vec
example {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val + y.val)
@@ -384,7 +409,7 @@ namespace Test
`α : Type u` where u is quantified, while here we use `α : Type 0` -/
example {α : Type} (v: Vec α) (i: Usize) (x : α)
(hbounds : i.val < v.length) :
- ∃ nv, v.index_mut_back α i x = ret nv ∧
+ ∃ nv, v.update_usize i x = ret nv ∧
nv.val = v.val.update i.val x := by
progress
simp [*]
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 5224e1c3..b917a789 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -604,16 +604,12 @@ example (h : ∃ x y z, x + y + z ≥ 0) : ∃ x, x ≥ 0 := by
rename_i x y z
exists x + y + z
-/- Call the simp tactic.
- The initialization of the context is adapted from Tactic.elabSimpArgs.
- Something very annoying is that there is no function which allows to
- initialize a simp context without doing an elaboration - as a consequence
- we write our own here. -/
-def simpAt (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
- (loc : Tactic.Location) :
- Tactic.TacticM Unit := do
- -- Initialize with the builtin simp theorems
- let simpThms ← Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
+def mkSimpCtx (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
+ Tactic.TacticM Simp.Context := do
+ -- Initialize either with the builtin simp theorems or with all the simp theorems
+ let simpThms ←
+ if simpOnly then Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) ({} : SimpTheorems)
+ else getSimpTheorems
-- Add the equational theorem for the declarations to unfold
let simpThms ←
declsToUnfold.foldlM (fun thms decl => thms.addDeclToUnfold decl) simpThms
@@ -637,8 +633,63 @@ def simpAt (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVar
throwError "Not a proposition: {thmName}"
) simpThms
let congrTheorems ← getSimpCongrTheorems
- let ctx : Simp.Context := { simpTheorems := #[simpThms], congrTheorems }
+ pure { simpTheorems := #[simpThms], congrTheorems }
+
+
+inductive Location where
+ /-- Apply the tactic everywhere. Same as `Tactic.Location.wildcard` -/
+ | wildcard
+ /-- Apply the tactic everywhere, including in the variable types (i.e., in
+ assumptions which are not propositions). --/
+ | wildcard_dep
+ /-- Same as Tactic.Location -/
+ | targets (hypotheses : Array Syntax) (type : Bool)
+
+-- Comes from Tactic.simpLocation
+def customSimpLocation (ctx : Simp.Context) (discharge? : Option Simp.Discharge := none)
+ (loc : Location) : TacticM Simp.UsedSimps := do
+ match loc with
+ | Location.targets hyps simplifyTarget =>
+ withMainContext do
+ let fvarIds ← Lean.Elab.Tactic.getFVarIds hyps
+ go fvarIds simplifyTarget
+ | Location.wildcard =>
+ withMainContext do
+ go (← (← getMainGoal).getNondepPropHyps) (simplifyTarget := true)
+ | Location.wildcard_dep =>
+ withMainContext do
+ let ctx ← Lean.MonadLCtx.getLCtx
+ let decls ← ctx.getDecls
+ let tgts := (decls.map (fun d => d.fvarId)).toArray
+ go tgts (simplifyTarget := true)
+where
+ go (fvarIdsToSimp : Array FVarId) (simplifyTarget : Bool) : TacticM Simp.UsedSimps := do
+ let mvarId ← getMainGoal
+ let (result?, usedSimps) ← simpGoal mvarId ctx (simplifyTarget := simplifyTarget) (discharge? := discharge?) (fvarIdsToSimp := fvarIdsToSimp)
+ match result? with
+ | none => replaceMainGoal []
+ | some (_, mvarId) => replaceMainGoal [mvarId]
+ return usedSimps
+
+/- Call the simp tactic.
+ The initialization of the context is adapted from Tactic.elabSimpArgs.
+ Something very annoying is that there is no function which allows to
+ initialize a simp context without doing an elaboration - as a consequence
+ we write our own here. -/
+def simpAt (simpOnly : Bool) (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId)
+ (loc : Location) :
+ Tactic.TacticM Unit := do
+ -- Initialize the simp context
+ let ctx ← mkSimpCtx simpOnly declsToUnfold thms hypsToUse
+ -- Apply the simplifier
+ let _ ← customSimpLocation ctx (discharge? := .none) loc
+
+-- Call the simpAll tactic
+def simpAll (declsToUnfold : List Name) (thms : List Name) (hypsToUse : List FVarId) :
+ Tactic.TacticM Unit := do
+ -- Initialize the simp context
+ let ctx ← mkSimpCtx false declsToUnfold thms hypsToUse
-- Apply the simplifier
- let _ ← Tactic.simpLocation ctx (discharge? := .none) loc
+ let _ ← Lean.Meta.simpAll (← getMainGoal) ctx
end Utils
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 20:15:35 +0000