diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/coq/Primitives.v | 55 | ||||
| -rw-r--r-- | backends/fstar/Primitives.fst | 75 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Int.lean | 31 | ||||
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 4 | ||||
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 238 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives.lean | 1 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Array.lean | 394 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Range.lean | 19 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Scalar.lean | 11 | ||||
| -rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 25 | ||||
| -rw-r--r-- | backends/lean/Base/UtilsBase.lean | 10 |
11 files changed, 814 insertions, 49 deletions
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v index ae961ac2..71a2d9c3 100644 --- a/backends/coq/Primitives.v +++ b/backends/coq/Primitives.v @@ -394,13 +394,15 @@ Notation "x s< y" := (scalar_ltb x y) (at level 80) : Primitives_scope. Notation "x s>= y" := (scalar_geb x y) (at level 80) : Primitives_scope. Notation "x s> y" := (scalar_gtb x y) (at level 80) : Primitives_scope. -(*** Vectors *) - -Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }. +(*** Range *) +Record range (T : Type) := mk_range { + start: T; + end_: T; +}. +Arguments mk_range {_}. -Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v. - -Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)). +(*** Arrays *) +Definition array T (n : usize) := { l: list T | Z.of_nat (length l) = to_Z n}. Lemma le_0_usize_max : 0 <= usize_max. Proof. @@ -409,6 +411,47 @@ Proof. lia. Qed. +Lemma eqb_imp_eq (x y : Z) : Z.eqb x y = true -> x = y. +Proof. + lia. +Qed. + +(* TODO: finish the definitions *) +Axiom mk_array : forall (T : Type) (n : usize) (l : list T), array T n. + +Axiom array_index_shared : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. +Axiom array_index_mut_fwd : forall (T : Type) (n : usize) (x : array T n) (i : usize), result T. +Axiom array_index_mut_back : forall (T : Type) (n : usize) (x : array T n) (i : usize) (nx : T), result (array T n). + +(*** Slice *) +Definition slice T := { l: list T | Z.of_nat (length l) <= usize_max}. + +Axiom slice_len : forall (T : Type) (s : slice T), usize. +Axiom slice_index_shared : forall (T : Type) (x : slice T) (i : usize), result T. +Axiom slice_index_mut_fwd : forall (T : Type) (x : slice T) (i : usize), result T. +Axiom slice_index_mut_back : forall (T : Type) (x : slice T) (i : usize) (nx : T), result (slice T). + +(*** Subslices *) + +Axiom array_to_slice_shared : forall (T : Type) (n : usize) (x : array T n), result (slice T). +Axiom array_to_slice_mut_fwd : forall (T : Type) (n : usize) (x : array T n), result (slice T). +Axiom array_to_slice_mut_back : forall (T : Type) (n : usize) (x : array T n) (s : slice T), result (array T n). + +Axiom array_subslice_shared: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T). +Axiom array_subslice_mut_fwd: forall (T : Type) (n : usize) (x : array T n) (r : range usize), result (slice T). +Axiom array_subslice_mut_back: forall (T : Type) (n : usize) (x : array T n) (r : range usize) (ns : slice T), result (array T n). +Axiom slice_subslice_shared: forall (T : Type) (x : slice T) (r : range usize), result (slice T). +Axiom slice_subslice_mut_fwd: forall (T : Type) (x : slice T) (r : range usize), result (slice T). +Axiom slice_subslice_mut_back: forall (T : Type) (x : slice T) (r : range usize) (ns : slice T), result (slice T). + +(*** Vectors *) + +Definition vec T := { l: list T | Z.of_nat (length l) <= usize_max }. + +Definition vec_to_list {T: Type} (v: vec T) : list T := proj1_sig v. + +Definition vec_length {T: Type} (v: vec T) : Z := Z.of_nat (length (vec_to_list v)). + Definition vec_new (T: Type) : vec T := (exist _ [] le_0_usize_max). Lemma vec_len_in_usize {T} (v: vec T) : usize_min <= vec_length v <= usize_max. diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst index 98a696b6..9db82069 100644 --- a/backends/fstar/Primitives.fst +++ b/backends/fstar/Primitives.fst @@ -259,6 +259,81 @@ let u32_mul = scalar_mul #U32 let u64_mul = scalar_mul #U64 let u128_mul = scalar_mul #U128 +(*** Range *) +type range (a : Type0) = { + start : a; + end_ : a; +} + +(*** Array *) +type array (a : Type0) (n : usize) = s:list a{length s = n} + +// We tried putting the normalize_term condition as a refinement on the list +// but it didn't work. It works with the requires clause. +let mk_array (a : Type0) (n : usize) + (l : list a) : + Pure (array a n) + (requires (normalize_term(FStar.List.Tot.length l) = n)) + (ensures (fun _ -> True)) = + normalize_term_spec (FStar.List.Tot.length l); + l + +let array_index_shared (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_fwd (a : Type0) (n : usize) (x : array a n) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let array_index_mut_back (a : Type0) (n : usize) (x : array a n) (i : usize) (nx : a) : result (array a n) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Slice *) +type slice (a : Type0) = s:list a{length s <= usize_max} + +let slice_len (a : Type0) (s : slice a) : usize = length s + +let slice_index_shared (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_fwd (a : Type0) (x : slice a) (i : usize) : result a = + if i < length x then Return (index x i) + else Fail Failure + +let slice_index_mut_back (a : Type0) (x : slice a) (i : usize) (nx : a) : result (slice a) = + if i < length x then Return (list_update x i nx) + else Fail Failure + +(*** Subslices *) + +let array_to_slice_shared (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_fwd (a : Type0) (n : usize) (x : array a n) : result (slice a) = Return x +let array_to_slice_mut_back (a : Type0) (n : usize) (x : array a n) (s : slice a) : result (array a n) = + if length s = n then Return s + else Fail Failure + +// TODO: finish the definitions below (there lacks [List.drop] and [List.take] in the standard library *) +let array_subslice_shared (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_fwd (a : Type0) (n : usize) (x : array a n) (r : range usize) : result (slice a) = + admit() + +let array_subslice_mut_back (a : Type0) (n : usize) (x : array a n) (r : range usize) (ns : slice a) : result (array a n) = + admit() + +let slice_subslice_shared (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_fwd (a : Type0) (x : slice a) (r : range usize) : result (slice a) = + admit() + +let slice_subslice_mut_back (a : Type0) (x : slice a) (r : range usize) (ns : slice a) : result (slice a) = + admit() + (*** Vector *) type vec (a : Type0) = v:list a{length v <= usize_max} diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index 7a5bbe98..531ec94f 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -53,13 +53,21 @@ open Lean Lean.Elab Lean.Meta -- Explore a term by decomposing the applications (we explore the applied -- functions and their arguments, but ignore lambdas, forall, etc. - -- should we go inside?). +-- Remark: we pretend projections are applications, and explore the projected +-- terms. partial def foldTermApps (k : α → Expr → MetaM α) (s : α) (e : Expr) : MetaM α := do - -- We do it in a very simpler manner: we deconstruct applications, - -- and recursively explore the sub-expressions. Note that we do - -- not go inside foralls and abstractions (should we?). - e.withApp fun f args => do - let s ← k s f - args.foldlM (foldTermApps k) s + -- Explore the current expression + let e := e.consumeMData + let s ← k s e + -- Recurse + match e with + | .proj _ _ e' => + foldTermApps k s e' + | .app .. => + e.withApp fun f args => do + let s ← k s f + args.foldlM (foldTermApps k) s + | _ => pure s -- Provided a function `k` which lookups type class instances on an expression, -- collect all the instances lookuped by applying `k` on the sub-expressions of `e`. @@ -83,15 +91,18 @@ def collectInstancesFromMainCtx (k : Expr → MetaM (Option Expr)) : Tactic.Tact let hs := HashSet.empty -- Explore the declarations let decls ← ctx.getDecls - decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs + let hs ← decls.foldlM (fun hs d => collectInstances k hs d.toExpr) hs + -- Also explore the goal + collectInstances k hs (← Tactic.getMainTarget) -- Helper def lookupProp (fName : String) (className : Name) (e : Expr) : MetaM (Option Expr) := do trace[Arith] fName -- TODO: do we need Lean.observing? -- This actually eliminates the error messages + trace[Arith] m!"{fName}: {e}" Lean.observing? do - trace[Arith] m!"{fName}: observing" + trace[Arith] m!"{fName}: observing: {e}" let ty ← Lean.Meta.inferType e let hasProp ← mkAppM className #[ty] let hasPropInst ← trySynthInstance hasProp @@ -112,11 +123,11 @@ def collectHasIntPropInstancesFromMainCtx : Tactic.TacticM (HashSet Expr) := do -- Return an instance of `PropHasImp` for `e` if it has some def lookupPropHasImp (e : Expr) : MetaM (Option Expr) := do - trace[Arith] "lookupPropHasImp" + trace[Arith] m!"lookupPropHasImp: {e}" -- TODO: do we need Lean.observing? -- This actually eliminates the error messages Lean.observing? do - trace[Arith] "lookupPropHasImp: observing" + trace[Arith] "lookupPropHasImp: observing: {e}" let ty ← Lean.Meta.inferType e trace[Arith] "lookupPropHasImp: ty: {ty}" let cl ← mkAppM ``PropHasImp #[ty] diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean index b792ff21..db672489 100644 --- a/backends/lean/Base/Arith/Scalar.lean +++ b/backends/lean/Base/Arith/Scalar.lean @@ -46,4 +46,8 @@ example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by scalar_tac +-- Checking that we explore the goal *and* projectors correctly +example (x : U32 × U32) : 0 ≤ x.fst.val := by + scalar_tac + end Arith diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean index 93047a1b..0b483e90 100644 --- a/backends/lean/Base/IList/IList.lean +++ b/backends/lean/Base/IList/IList.lean @@ -3,6 +3,7 @@ import Std.Data.Int.Lemmas import Base.Arith +import Base.Utils namespace List @@ -87,6 +88,28 @@ def idrop (i : Int) (ls : List α) : List α := | [] => [] | x :: tl => if i = 0 then x :: tl else idrop (i - 1) tl +def itake (i : Int) (ls : List α) : List α := + match ls with + | [] => [] + | hd :: tl => if i = 0 then [] else hd :: itake (i - 1) tl + +def slice (start end_ : Int) (ls : List α) : List α := + (ls.idrop start).itake (end_ - start) + +def replace_slice (start end_ : Int) (l nl : List α) : List α := + let l_beg := l.itake start + let l_end := l.idrop end_ + l_beg ++ nl ++ l_end + +def allP {α : Type u} (l : List α) (p: α → Prop) : Prop := + foldr (fun a r => p a ∧ r) True l + +def pairwise_rel + {α : Type u} (rel : α → α → Prop) (l: List α) : Prop + := match l with + | [] => True + | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl + section Lemmas variable {α : Type u} @@ -99,6 +122,28 @@ variable {α : Type u} @[simp] theorem idrop_zero : idrop 0 (ls : List α) = ls := by cases ls <;> simp [idrop] @[simp] theorem idrop_nzero_cons (hne : i ≠ 0) : idrop i ((x :: tl) : List α) = idrop (i - 1) tl := by simp [*, idrop] +@[simp] theorem itake_nil : itake i ([] : List α) = [] := by simp [itake] +@[simp] theorem itake_zero : itake 0 (ls : List α) = [] := by cases ls <;> simp [itake] +@[simp] theorem itake_nzero_cons (hne : i ≠ 0) : itake i ((x :: tl) : List α) = x :: itake (i - 1) tl := by simp [*, itake] + +@[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 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 + | [] => by simp [slice]; simp [*] + | hd :: tl => + if h: i - 1 = 0 then by + have : i = 1 := by int_tac + simp [*, slice] + else + have := slice_nzero_cons (i - 1) (j - 1) hd tl h + by + conv => lhs; simp [slice, *] + conv at this => lhs; simp [slice, *] + simp [*, slice] + theorem len_eq_length (ls : List α) : ls.len = ls.length := by induction ls . rfl @@ -158,8 +203,33 @@ theorem right_len_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.len = l2'.len apply right_length_eq_append_eq assumption +@[simp] +theorem index_append_beg [Inhabited α] (i : Int) (l0 l1 : List α) + (_ : 0 ≤ i) (_ : i < l0.len) : + (l0 ++ l1).index i = l0.index i := + match l0 with + | [] => by simp_all; int_tac + | hd :: tl => + if hi : i = 0 then by simp_all + else by + have := index_append_beg (i - 1) tl l1 (by int_tac) (by simp_all; int_tac) + simp_all + +@[simp] +theorem index_append_end [Inhabited α] (i : Int) (l0 l1 : List α) + (_ : l0.len ≤ i) (_ : i < l0.len + l1.len) : + (l0 ++ l1).index i = l1.index (i - l0.len) := + match l0 with + | [] => by simp_all + | hd :: tl => + have : ¬ i = 0 := by simp_all; int_tac + have := index_append_end (i - 1) tl l1 (by simp_all; int_tac) (by simp_all; int_tac) + -- TODO: canonize arith expressions + have : i - 1 - len tl = i - (1 + len tl) := by int_tac + by simp_all + open Arith in -theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by +@[simp] theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by revert i induction ls <;> simp [*] rename_i hd tl hi @@ -175,6 +245,136 @@ theorem idrop_eq_nil_of_le (hineq : ls.len ≤ i) : idrop i ls = [] := by apply hi linarith +theorem idrop_len_le (i : Int) (ls : List α) : (ls.idrop i).len ≤ ls.len := + match ls with + | [] => by simp + | hd :: tl => + if h: i = 0 then by simp [*] + else + have := idrop_len_le (i - 1) tl + by simp [*]; linarith + +@[simp] +theorem idrop_len (i : Int) (ls : List α) (_ : 0 ≤ i) (_ : i ≤ ls.len) : + (ls.idrop i).len = ls.len - i := + match ls with + | [] => by simp_all; linarith + | hd :: tl => + if h: i = 0 then by simp [*] + else + have := idrop_len (i - 1) tl (by int_tac) (by simp at *; int_tac) + by simp [*] at *; int_tac + +theorem itake_len_le (i : Int) (ls : List α) : (ls.itake i).len ≤ ls.len := + match ls with + | [] => by simp + | hd :: tl => + if h: i = 0 then by simp [*]; int_tac + else + have := itake_len_le (i - 1) tl + by simp [*] + +@[simp] +theorem itake_len (i : Int) (ls : List α) (_ : 0 ≤ i) (_ : i ≤ ls.len) : (ls.itake i).len = i := + match ls with + | [] => by simp_all; int_tac + | hd :: tl => + if h: i = 0 then by simp [*] + else + have := itake_len (i - 1) tl (by int_tac) (by simp at *; int_tac) + by simp [*] + +theorem slice_len_le (i j : Int) (ls : List α) : (ls.slice i j).len ≤ ls.len := by + simp [slice] + have := ls.idrop_len_le i + have := (ls.idrop i).itake_len_le (j - i) + int_tac + +@[simp] +theorem index_idrop [Inhabited α] (i : Int) (j : Int) (ls : List α) + (_ : 0 ≤ i) (_ : 0 ≤ j) (_ : i + j < ls.len) : + (ls.idrop i).index j = ls.index (i + j) := + match ls with + | [] => by simp at *; int_tac + | hd :: tl => + if h: i = 0 then by simp [*] + else by + have : ¬ i + j = 0 := by int_tac + simp [*] + -- TODO: rewriting rule: ¬ i = 0 → 0 ≤ i → 0 < i ? + have := index_idrop (i - 1) j tl (by int_tac) (by simp at *; int_tac) (by simp at *; int_tac) + -- TODO: canonize add/subs? + have : i - 1 + j = i + j - 1 := by int_tac + simp [*] + +@[simp] +theorem index_itake [Inhabited α] (i : Int) (j : Int) (ls : List α) + (_ : 0 ≤ j) (_ : j < i) (_ : j < ls.len) : + (ls.itake i).index j = ls.index j := + match ls with + | [] => by simp at * + | hd :: tl => + have : ¬ 0 = i := by int_tac -- TODO: this is slightly annoying + if h: j = 0 then by simp [*] at * + else by + simp [*] + -- TODO: rewriting rule: ¬ i = 0 → 0 ≤ i → 0 < i ? + have := index_itake (i - 1) (j - 1) tl (by simp at *; int_tac) (by simp at *; int_tac) (by simp at *; int_tac) + simp [*] + +@[simp] +theorem index_slice [Inhabited α] (i j k : Int) (ls : List α) + (_ : 0 ≤ i) (_ : j ≤ ls.len) (_ : 0 ≤ k) (_ : i + k < j) : + (ls.slice i j).index k = ls.index (i + k) := + match ls with + | [] => by simp at *; int_tac + | hd :: tl => + if h: i = 0 then by + simp [*, slice] at * + apply index_itake <;> simp_all + int_tac + else by + have : ¬ i + k = 0 := by int_tac + simp [*] + -- TODO: tactics simp_int_tac/simp_scalar_tac? + have := index_slice (i - 1) (j - 1) k tl (by simp at *; int_tac) (by simp at *; int_tac) + (by simp at *; int_tac) (by simp at *; int_tac) + have : (i - 1 + k) = (i + k - 1) := by int_tac -- TODO: canonize add/sub + simp [*] + +@[simp] +theorem index_itake_append_beg [Inhabited α] (i j : Int) (l0 l1 : List α) + (_ : 0 ≤ j) (_ : j < i) (_ : i ≤ l0.len) : + ((l0 ++ l1).itake i).index j = l0.index j := + match l0 with + | [] => by + simp at * + int_tac + | hd :: tl => + have : ¬ i = 0 := by simp at *; int_tac + if hj : j = 0 then by simp [*] + else by + have := index_itake_append_beg (i - 1) (j - 1) tl l1 (by simp_all; int_tac) (by simp_all) (by simp_all; int_tac) + simp [*] + +@[simp] +theorem index_itake_append_end [Inhabited α] (i j : Int) (l0 l1 : List α) + (_ : l0.len ≤ j) (_ : j < i) (_ : i ≤ l0.len + l1.len) : + ((l0 ++ l1).itake i).index j = l1.index (j - l0.len) := + match l0 with + | [] => by + simp at * + have := index_itake i j l1 (by simp_all) (by simp_all) (by simp_all; int_tac) + simp [*] + | hd :: tl => + have : ¬ i = 0 := by simp at *; int_tac + if hj : j = 0 then by simp_all; int_tac -- Contradiction + else by + have := index_itake_append_end (i - 1) (j - 1) tl l1 (by simp_all; int_tac) (by simp_all) (by simp_all; int_tac) + -- TODO: normalization of add/sub + have : j - 1 - len tl = j - (1 + len tl) := by int_tac + simp_all + @[simp] theorem index_ne {α : Type u} [Inhabited α] (l: List α) (i: ℤ) (j: ℤ) (x: α) : @@ -251,8 +451,34 @@ theorem index_map_eq {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] ( by simp [*] -def allP {α : Type u} (l : List α) (p: α → Prop) : Prop := - foldr (fun a r => p a ∧ r) True l +theorem replace_slice_index [Inhabited α] (start end_ : Int) (l nl : List α) + (_ : 0 ≤ start) (_ : start < end_) (_ : end_ ≤ l.len) (_ : nl.len = end_ - start) : + let l1 := l.replace_slice start end_ nl + (∀ i, 0 ≤ i → i < start → l1.index i = l.index i) ∧ + (∀ i, start ≤ i → i < end_ → l1.index i = nl.index (i - start)) ∧ + (∀ i, end_ ≤ i → i < l.len → l1.index i = l.index i) + := by + -- let s_end := s.val ++ a.val.idrop r.end_.val + -- We need those assumptions everywhere + -- have : 0 ≤ start := by scalar_tac + have : start ≤ l.len := by int_tac + simp only [replace_slice] + split_conjs + . intro i _ _ + -- Introducing exactly the assumptions we need to make the rewriting work + have : i < l.len := by int_tac + simp_all + . intro i _ _ + have : (List.itake start l).len ≤ i := by simp_all + have : i < (List.itake start l).len + (nl ++ List.idrop end_ l).len := by + simp_all; int_tac + simp_all + . intro i _ _ + have : 0 ≤ end_ := by scalar_tac + have : end_ ≤ l.len := by int_tac + have : (List.itake start l).len ≤ i := by simp_all; int_tac + have : i < (List.itake start l).len + (nl ++ List.idrop end_ l).len := by simp_all + simp_all @[simp] theorem allP_nil {α : Type u} (p: α → Prop) : allP [] p := @@ -263,12 +489,6 @@ theorem allP_cons {α : Type u} (hd: α) (tl : List α) (p: α → Prop) : allP (hd :: tl) p ↔ p hd ∧ allP tl p := by simp [allP, foldr] -def pairwise_rel - {α : Type u} (rel : α → α → Prop) (l: List α) : Prop - := match l with - | [] => True - | hd :: tl => allP tl (rel hd) ∧ pairwise_rel rel tl - @[simp] theorem pairwise_rel_nil {α : Type u} (rel : α → α → Prop) : pairwise_rel rel [] diff --git a/backends/lean/Base/Primitives.lean b/backends/lean/Base/Primitives.lean index 91823cb6..6b7b0792 100644 --- a/backends/lean/Base/Primitives.lean +++ b/backends/lean/Base/Primitives.lean @@ -1,3 +1,4 @@ import Base.Primitives.Base import Base.Primitives.Scalar +import Base.Primitives.Array import Base.Primitives.Vec diff --git a/backends/lean/Base/Primitives/Array.lean b/backends/lean/Base/Primitives/Array.lean new file mode 100644 index 00000000..6c95fd78 --- /dev/null +++ b/backends/lean/Base/Primitives/Array.lean @@ -0,0 +1,394 @@ +/- 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/Range.lean b/backends/lean/Base/Primitives/Range.lean new file mode 100644 index 00000000..26cbee42 --- /dev/null +++ b/backends/lean/Base/Primitives/Range.lean @@ -0,0 +1,19 @@ +/- 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.Arith +import Base.Progress.Base + +namespace Primitives + +structure Range (α : Type u) where + mk :: + start: α + end_: α + +end Primitives diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean index 2e5be8bf..ffc969f3 100644 --- a/backends/lean/Base/Primitives/Scalar.lean +++ b/backends/lean/Base/Primitives/Scalar.lean @@ -787,15 +787,8 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) := | isTrue h => isTrue (Scalar.eq_of_val_eq h) | isFalse h => isFalse (Scalar.ne_of_val_ne h) -/- Remark: we can't write the following instance because of restrictions about - the type class parameters (`ty` doesn't appear in the return type, which is - forbidden): - - ``` - instance Scalar.cast (ty : ScalarTy) : Coe (Scalar ty) Int where coe := λ v => v.val - ``` - -/ -def Scalar.toInt {ty} (n : Scalar ty) : Int := n.val +instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where + coe := λ v => v.val -- -- We now define a type class that subsumes the various machine integer types, so -- -- as to write a concise definition for scalar_cast, rather than exhaustively 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 diff --git a/backends/lean/Base/UtilsBase.lean b/backends/lean/Base/UtilsBase.lean new file mode 100644 index 00000000..f6c33be7 --- /dev/null +++ b/backends/lean/Base/UtilsBase.lean @@ -0,0 +1,10 @@ +import Lean + +namespace Utils + +open Lean Elab Term Meta + +-- We can't define and use trace classes in the same file +initialize registerTraceClass `Utils + +end Utils |