diff options
author | Son HO | 2023-08-07 10:42:15 +0200 |
---|---|---|
committer | GitHub | 2023-08-07 10:42:15 +0200 |
commit | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (patch) | |
tree | c15a16b591cf25df3ccff87ad4cd7c46ddecc489 /backends/lean/Base/Primitives/Vec.lean | |
parent | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (diff) | |
parent | 9e14cdeaf429e9faff2d1efdcf297c1ac7dc7f1f (diff) |
Merge pull request #32 from AeneasVerif/son_arrays
Add support for arrays/slices and const generics
Diffstat (limited to 'backends/lean/Base/Primitives/Vec.lean')
-rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index a09d6ac2..c4c4d9f2 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -1,3 +1,4 @@ +/- Vectors -/ import Lean import Lean.Meta.Tactic.Simp import Init.Data.List.Basic @@ -5,6 +6,7 @@ import Mathlib.Tactic.RunCmd import Mathlib.Tactic.Linarith import Base.IList import Base.Primitives.Scalar +import Base.Primitives.Array import Base.Arith import Base.Progress.Base @@ -12,19 +14,16 @@ namespace Primitives open Result Error -------------- --- VECTORS -- -------------- - def Vec (α : Type u) := { l : List α // l.length ≤ Usize.max } --- TODO: do we really need it? It should be with Subtype by default -instance Vec.cast (a : Type u): Coe (Vec a) (List a) where coe := λ v => v.val - instance (a : Type u) : Arith.HasIntProp (Vec 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 : Vec α → Prop) : Arith.HasIntProp (Subtype p) where + prop_ty := λ x => p x + prop := λ x => x.property + @[simp] abbrev Vec.length {α : Type u} (v : Vec α) : Int := v.val.len @@ -80,7 +79,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 (α : Type u) (v: Vec α) (i: Usize) : Result α := +def Vec.index_shared (α : Type u) (v: Vec α) (i: Usize) : Result α := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds | some x => ret x @@ -91,10 +90,10 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α := -/ @[pspec] -theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) +theorem Vec.index_shared_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) (hbound : i.val < v.length) : - ∃ x, v.index α i = ret x ∧ x = v.val.index i.val := by - simp only [index] + ∃ 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 [*] @@ -120,10 +119,6 @@ theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) simp [*] -instance {α : Type u} (p : Vec α → Prop) : Arith.HasIntProp (Subtype p) where - prop_ty := λ x => p x - prop := λ x => x.property - def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) := match v.val.indexOpt i.val with | none => fail .arrayOutOfBounds |