summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Diverge/Base.lean3
-rw-r--r--backends/lean/Base/IList/IList.lean66
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean1
-rw-r--r--backends/lean/Base/Primitives/Vec.lean89
-rw-r--r--backends/lean/Base/Progress/Base.lean3
-rw-r--r--backends/lean/Base/Progress/Progress.lean4
6 files changed, 116 insertions, 50 deletions
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 0a9ea4c4..4ff1d923 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -3,8 +3,7 @@ import Lean.Meta.Tactic.Simp
import Init.Data.List.Basic
import Mathlib.Tactic.RunCmd
import Mathlib.Tactic.Linarith
-
-import Base.Primitives
+import Base.Primitives.Base
/- TODO: this is very useful, but is there more? -/
set_option profiler true
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 2a335cac..ddb10236 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -11,12 +11,27 @@ def len (ls : List α) : Int :=
| [] => 0
| _ :: tl => 1 + len tl
+@[simp] theorem len_nil : len ([] : List α) = 0 := by simp [len]
+@[simp] theorem len_cons : len ((x :: tl) : List α) = 1 + len tl := by simp [len]
+
+theorem len_pos : 0 ≤ (ls : List α).len := by
+ induction ls <;> simp [*]
+ linarith
+
+instance (a : Type u) : Arith.HasIntProp (List a) where
+ prop_ty := λ ls => 0 ≤ ls.len
+ prop := λ ls => ls.len_pos
+
-- Remark: if i < 0, then the result is none
def indexOpt (ls : List α) (i : Int) : Option α :=
match ls with
| [] => none
| hd :: tl => if i = 0 then some hd else indexOpt tl (i - 1)
+@[simp] theorem indexOpt_nil : indexOpt ([] : List α) i = none := by simp [indexOpt]
+@[simp] theorem indexOpt_zero_cons : indexOpt ((x :: tl) : List α) 0 = some x := by simp [indexOpt]
+@[simp] theorem indexOpt_nzero_cons (hne : i ≠ 0) : indexOpt ((x :: tl) : List α) i = indexOpt tl (i - 1) := by simp [*, indexOpt]
+
-- Remark: if i < 0, then the result is the defaul element
def index [Inhabited α] (ls : List α) (i : Int) : α :=
match ls with
@@ -24,6 +39,43 @@ def index [Inhabited α] (ls : List α) (i : Int) : α :=
| x :: tl =>
if i = 0 then x else index tl (i - 1)
+@[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index]
+@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index]
+
+theorem indexOpt_bounds (ls : List α) (i : Int) :
+ ls.indexOpt i = none ↔ i < 0 ∨ ls.len ≤ i :=
+ match ls with
+ | [] =>
+ have : ¬ (i < 0) → 0 ≤ i := by intro; linarith -- TODO: simplify (we could boost int_tac)
+ by simp; tauto
+ | _ :: tl =>
+ have := indexOpt_bounds tl (i - 1)
+ if h: i = 0 then
+ by
+ simp [*];
+ -- TODO: int_tac/scalar_tac should also explore the goal!
+ have := tl.len_pos
+ linarith
+ else by
+ simp [*]
+ constructor <;> intros <;>
+ -- TODO: tactic to split all disjunctions
+ rename_i hor <;> cases hor <;>
+ first | left; int_tac | right; int_tac
+
+theorem indexOpt_eq_index [Inhabited α] (ls : List α) (i : Int) :
+ 0 ≤ i →
+ i < ls.len →
+ ls.indexOpt i = some (ls.index i) :=
+ match ls with
+ | [] => by simp; intros; linarith
+ | hd :: tl =>
+ if h: i = 0 then
+ by simp [*]
+ else
+ have hi := indexOpt_eq_index tl (i - 1)
+ by simp [*]; intros; apply hi <;> int_tac
+
-- Remark: the list is unchanged if the index is not in bounds (in particular
-- if it is < 0)
def update (ls : List α) (i : Int) (y : α) : List α :=
@@ -42,12 +94,6 @@ section Lemmas
variable {α : Type u}
-@[simp] theorem len_nil : len ([] : List α) = 0 := by simp [len]
-@[simp] theorem len_cons : len ((x :: tl) : List α) = 1 + len tl := by simp [len]
-
-@[simp] theorem index_zero_cons [Inhabited α] : index ((x :: tl) : List α) 0 = x := by simp [index]
-@[simp] theorem index_nzero_cons [Inhabited α] (hne : i ≠ 0) : index ((x :: tl) : List α) i = index tl (i - 1) := by simp [*, index]
-
@[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]
@[simp] theorem update_nzero_cons (hne : i ≠ 0) : update ((x :: tl) : List α) i y = x :: update tl (i - 1) y := by simp [*, update]
@@ -81,14 +127,6 @@ theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.
simp [len_eq_length]
-theorem len_pos : 0 ≤ (ls : List α).len := by
- induction ls <;> simp [*]
- linarith
-
-instance (a : Type u) : Arith.HasIntProp (List a) where
- prop_ty := λ ls => 0 ≤ ls.len
- prop := λ ls => ls.len_pos
-
theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1'.length) :
l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by
revert l1'
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 241dfa07..3f88caa2 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -2,6 +2,7 @@ import Lean
import Lean.Meta.Tactic.Simp
import Mathlib.Tactic.Linarith
import Base.Primitives.Base
+import Base.Diverge.Base
namespace Primitives
diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean
index 7851a232..4ecfa28f 100644
--- a/backends/lean/Base/Primitives/Vec.lean
+++ b/backends/lean/Base/Primitives/Vec.lean
@@ -6,6 +6,7 @@ import Mathlib.Tactic.Linarith
import Base.IList
import Base.Primitives.Scalar
import Base.Arith
+import Base.Progress.Base
namespace Primitives
@@ -56,58 +57,80 @@ def Vec.push (α : Type u) (v : Vec α) (x : α) : Result (Vec α)
fail maximumSizeExceeded
-- This shouldn't be used
-def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
- if i.val < List.length v.val then
+def Vec.insert_fwd (α : Type u) (v: Vec α) (i: Usize) (_: α) : Result Unit :=
+ if i.val < v.length then
.ret ()
else
.fail arrayOutOfBounds
-- This is actually the backward function
-def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
- if i.val < List.length v.val then
- -- TODO: maybe we should redefine a list library which uses integers
- -- (instead of natural numbers)
+def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) :=
+ if i.val < v.length then
.ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩
else
.fail arrayOutOfBounds
--- TODO: remove
-def Vec.index_to_fin {α : Type u} {v: Vec α} {i: Usize} (h : i.val < List.length v.val) :
- Fin (List.length v.val) :=
- let j := i.val.toNat
- let h: j < List.length v.val := by
- have heq := @Int.toNat_lt (List.length v.val) i.val i.hmin
- apply heq.mpr
- assumption
- ⟨j, h⟩
-
-def Vec.index (α : Type u) (v: Vec α) (i: Usize): Result α :=
+@[pspec]
+theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) :
+ i.val < v.length →
+ ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by
+ intro h
+ simp [insert, *]
+
+def Vec.index (α : 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_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
+ i.val < v.length →
+ v.index α i = ret (v.val.index i.val) := by
+ intro
+ simp only [index]
+ -- TODO: dependent rewrite
+ have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*])
+ simp only [*]
+
-- This shouldn't be used
-def Vec.index_back (α : Type u) (v: Vec α) (i: Usize) (_: α): Result Unit :=
+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 α :=
- if h: i.val < List.length v.val then
- let i := Vec.index_to_fin h
- .ret (List.get v.val i)
- 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
-def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α): Result (Vec α) :=
- if h: i.val < List.length v.val then
- let i := Vec.index_to_fin h
- .ret ⟨ List.set v.val i x, by
- have h: List.length v.val ≤ Usize.max := v.property
- simp [*] at *
- ⟩
- else
- .fail arrayOutOfBounds
+@[pspec]
+theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) :
+ i.val < v.length →
+ v.index_mut α i = ret (v.val.index i.val) := by
+ intro
+ simp only [index_mut]
+ -- TODO: dependent rewrite
+ have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp[length] at *; simp [*])
+ simp only [*]
+
+def Vec.index_mut_back (α : 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 : α) :
+ i.val < v.length →
+ ∃ nv, v.index_mut_back α i x = ret nv ∧
+ nv.val = v.val.update i.val x
+ := by
+ intro
+ simp only [index_mut_back]
+ have h := List.indexOpt_bounds v.val i.val
+ split
+ . simp_all [length]; cases h <;> scalar_tac
+ . simp_all
end Primitives
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index a288d889..00b0a478 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -1,6 +1,7 @@
import Lean
+import Std.Lean.HashSet
import Base.Utils
-import Base.Primitives
+import Base.Primitives.Base
namespace Progress
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index af7b426a..001967e5 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -7,6 +7,7 @@ namespace Progress
open Lean Elab Term Meta Tactic
open Utils
+/-
-- TODO: remove
namespace Test
open Primitives
@@ -20,6 +21,7 @@ namespace Test
#eval pspecAttr.find? ``Primitives.Vec.index
end Test
+-/
inductive TheoremOrLocal where
| Theorem (thName : Name)
@@ -200,6 +202,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
elab "progress" args:progressArgs : tactic =>
evalProgress args
+/-
-- TODO: remove
namespace Test
open Primitives
@@ -215,5 +218,6 @@ namespace Test
set_option trace.Progress false
end Test
+-/
end Progress