summaryrefslogtreecommitdiff
path: root/backends/lean/Base
diff options
context:
space:
mode:
authorSon HO2023-09-18 13:59:38 +0200
committerGitHub2023-09-18 13:59:38 +0200
commit28f4ea9ffe02d4204bb60273b6a77db7ed48781b (patch)
tree156dc513299f3144a00d2a684d5e633aadf0cee6 /backends/lean/Base
parent242aca3092c6594206896ea62eb40395accc8459 (diff)
parenta053ad9739248ade939aa04355672362221883d7 (diff)
Merge pull request #37 from AeneasVerif/son_tuto
Tutorial for the Lean backend
Diffstat (limited to 'backends/lean/Base')
-rw-r--r--backends/lean/Base/Arith/Int.lean8
-rw-r--r--backends/lean/Base/Arith/Scalar.lean17
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean274
-rw-r--r--backends/lean/Base/Progress/Base.lean57
-rw-r--r--backends/lean/Base/Progress/Progress.lean14
5 files changed, 299 insertions, 71 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index eb6701c2..3359ecdb 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -211,9 +211,11 @@ def intTacPreprocess (extraPreprocess : Tactic.TacticM Unit) : Tactic.TacticM U
let _ ← introHasIntPropInstances
-- Extra preprocessing, before we split on the disjunctions
extraPreprocess
- -- Split
- let asms ← introInstances ``PropHasImp.concl lookupPropHasImp
- splitOnAsms asms.toList
+ -- Split - note that the extra-preprocessing step might actually have
+ -- proven the goal (by doing simplifications for instance)
+ Tactic.allGoals do
+ let asms ← introInstances ``PropHasImp.concl lookupPropHasImp
+ splitOnAsms asms.toList
elab "int_tac_preprocess" : tactic =>
intTacPreprocess (do pure ())
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean
index db672489..47751c8a 100644
--- a/backends/lean/Base/Arith/Scalar.lean
+++ b/backends/lean/Base/Arith/Scalar.lean
@@ -16,14 +16,15 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do
add (← mkAppM ``Scalar.cMin_bound #[.const ``ScalarTy.Isize []])
add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []])
add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []])
- -- Reveal the concrete bounds
+ -- Reveal the concrete bounds, simplify calls to [ofInt]
Utils.simpAt [``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,
``U8.max, ``U16.max, ``U32.max, ``U64.max, ``U128.max,
``Usize.min
- ] [] [] .wildcard
+ ] [``Scalar.ofInt_val_eq, ``Scalar.neq_to_neq_val] [] .wildcard
+
elab "scalar_tac_preprocess" : tactic =>
intTacPreprocess scalarTacExtraPreprocess
@@ -50,4 +51,16 @@ example (x y : U32) : x.val ≤ Scalar.max ScalarTy.U32 := by
example (x : U32 × U32) : 0 ≤ x.fst.val := by
scalar_tac
+-- Checking that we properly handle [ofInt]
+example : U32.ofInt 1 ≤ U32.max := by
+ scalar_tac
+
+example (x : Int) (h0 : 0 ≤ x) (h1 : x ≤ U32.max) :
+ U32.ofInt x (by constructor <;> scalar_tac) ≤ U32.max := by
+ scalar_tac
+
+-- Not equal
+example (x : U32) (h0 : ¬ x = U32.ofInt 0) : 0 < x.val := by
+ scalar_tac
+
end Arith
diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index ffc969f3..55227a9f 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -491,6 +491,36 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
apply Scalar.add_unsigned_spec <;> simp only [Scalar.max, *]
+@[cepspec] theorem Isize.add_spec {x y : Isize}
+ (hmin : Isize.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ Isize.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I8.add_spec {x y : I8}
+ (hmin : I8.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I8.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I16.add_spec {x y : I16}
+ (hmin : I16.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I16.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I32.add_spec {x y : I32}
+ (hmin : I32.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I32.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I64.add_spec {x y : I64}
+ (hmin : I64.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I64.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
+@[cepspec] theorem I128.add_spec {x y : I128}
+ (hmin : I128.min ≤ x.val + y.val) (hmax : x.val + y.val ≤ I128.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val :=
+ Scalar.add_spec hmin hmax
+
-- Generic theorem - shouldn't be used much
@[cpspec]
theorem Scalar.sub_spec {ty} {x y : Scalar ty}
@@ -540,6 +570,36 @@ theorem Scalar.sub_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
∃ z, x - y = ret z ∧ z.val = x.val - y.val := by
apply Scalar.sub_unsigned_spec <;> simp only [Scalar.min, *]
+@[cepspec] theorem Isize.sub_spec {x y : Isize} (hmin : Isize.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ Isize.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I8.sub_spec {x y : I8} (hmin : I8.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I8.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I16.sub_spec {x y : I16} (hmin : I16.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I16.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I32.sub_spec {x y : I32} (hmin : I32.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I32.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I64.sub_spec {x y : I64} (hmin : I64.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I64.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
+@[cepspec] theorem I128.sub_spec {x y : I128} (hmin : I128.min ≤ x.val - y.val)
+ (hmax : x.val - y.val ≤ I128.max) :
+ ∃ z, x - y = ret z ∧ z.val = x.val - y.val :=
+ Scalar.sub_spec hmin hmax
+
-- Generic theorem - shouldn't be used much
theorem Scalar.mul_spec {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val * y.val)
@@ -586,6 +646,36 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
∃ z, x * y = ret z ∧ z.val = x.val * y.val := by
apply Scalar.mul_unsigned_spec <;> simp only [Scalar.max, *]
+@[cepspec] theorem Isize.mul_spec {x y : Isize} (hmin : Isize.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ Isize.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I8.mul_spec {x y : I8} (hmin : I8.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I8.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I16.mul_spec {x y : I16} (hmin : I16.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I16.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I32.mul_spec {x y : I32} (hmin : I32.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I32.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I64.mul_spec {x y : I64} (hmin : I64.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I64.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
+@[cepspec] theorem I128.mul_spec {x y : I128} (hmin : I128.min ≤ x.val * y.val)
+ (hmax : x.val * y.val ≤ I128.max) :
+ ∃ z, x * y = ret z ∧ z.val = x.val * y.val :=
+ Scalar.mul_spec hmin hmax
+
-- Generic theorem - shouldn't be used much
@[cpspec]
theorem Scalar.div_spec {ty} {x y : Scalar ty}
@@ -639,6 +729,48 @@ theorem Scalar.div_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
∃ z, x / y = ret z ∧ z.val = x.val / y.val := by
apply Scalar.div_unsigned_spec <;> simp [Scalar.max, *]
+@[cepspec] theorem Isize.div_spec (x : Isize) {y : Isize}
+ (hnz : y.val ≠ 0)
+ (hmin : Isize.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ Isize.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I8.div_spec (x : I8) {y : I8}
+ (hnz : y.val ≠ 0)
+ (hmin : I8.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I8.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I16.div_spec (x : I16) {y : I16}
+ (hnz : y.val ≠ 0)
+ (hmin : I16.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I16.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I32.div_spec (x : I32) {y : I32}
+ (hnz : y.val ≠ 0)
+ (hmin : I32.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I32.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I64.div_spec (x : I64) {y : I64}
+ (hnz : y.val ≠ 0)
+ (hmin : I64.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I64.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
+@[cepspec] theorem I128.div_spec (x : I128) {y : I128}
+ (hnz : y.val ≠ 0)
+ (hmin : I128.min ≤ scalar_div x.val y.val)
+ (hmax : scalar_div x.val y.val ≤ I128.max):
+ ∃ z, x / y = ret z ∧ z.val = scalar_div x.val y.val :=
+ Scalar.div_spec hnz hmin hmax
+
-- Generic theorem - shouldn't be used much
@[cpspec]
theorem Scalar.rem_spec {ty} {x y : Scalar ty}
@@ -692,76 +824,89 @@ theorem Scalar.rem_unsigned_spec {ty} (s: ¬ ty.isSigned) (x : Scalar ty) {y : S
∃ z, x % y = ret z ∧ z.val = x.val % y.val := by
apply Scalar.rem_unsigned_spec <;> simp [Scalar.max, *]
--- ofIntCore
--- TODO: typeclass?
-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?
-def Isize.ofInt := @Scalar.ofInt .Isize
-def I8.ofInt := @Scalar.ofInt .I8
-def I16.ofInt := @Scalar.ofInt .I16
-def I32.ofInt := @Scalar.ofInt .I32
-def I64.ofInt := @Scalar.ofInt .I64
-def I128.ofInt := @Scalar.ofInt .I128
-def Usize.ofInt := @Scalar.ofInt .Usize
-def U8.ofInt := @Scalar.ofInt .U8
-def U16.ofInt := @Scalar.ofInt .U16
-def U32.ofInt := @Scalar.ofInt .U32
-def U64.ofInt := @Scalar.ofInt .U64
-def U128.ofInt := @Scalar.ofInt .U128
-
--- 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
+@[cepspec] theorem I8.rem_spec (x : I8) {y : I8}
+ (hnz : y.val ≠ 0)
+ (hmin : I8.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I8.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
-@[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
+@[cepspec] theorem I16.rem_spec (x : I16) {y : I16}
+ (hnz : y.val ≠ 0)
+ (hmin : I16.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I16.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
-@[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
+@[cepspec] theorem I32.rem_spec (x : I32) {y : I32}
+ (hnz : y.val ≠ 0)
+ (hmin : I32.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I32.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
-@[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
+@[cepspec] theorem I64.rem_spec (x : I64) {y : I64}
+ (hnz : y.val ≠ 0)
+ (hmin : I64.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I64.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
-@[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
+@[cepspec] theorem I128.rem_spec (x : I128) {y : I128}
+ (hnz : y.val ≠ 0)
+ (hmin : I128.min ≤ scalar_rem x.val y.val)
+ (hmax : scalar_rem x.val y.val ≤ I128.max):
+ ∃ z, x % y = ret z ∧ z.val = scalar_rem x.val y.val :=
+ Scalar.rem_spec hnz hmin hmax
-@[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
+-- 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
-@[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
+-- 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
+
+postfix:max "#isize" => Isize.ofInt
+postfix:max "#i8" => I8.ofInt
+postfix:max "#i16" => I16.ofInt
+postfix:max "#i32" => I32.ofInt
+postfix:max "#i64" => I64.ofInt
+postfix:max "#i128" => I128.ofInt
+postfix:max "#usize" => Usize.ofInt
+postfix:max "#u8" => U8.ofInt
+postfix:max "#u16" => U16.ofInt
+postfix:max "#u32" => U32.ofInt
+postfix:max "#u64" => U64.ofInt
+postfix:max "#u128" => U128.ofInt
+
+-- Testing the notations
+example : Result Usize := 0#usize + 1#usize
+@[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]
-- Comparisons
instance {ty} : LT (Scalar ty) where
@@ -790,6 +935,9 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
instance (ty : ScalarTy) : CoeOut (Scalar ty) Int where
coe := λ v => v.val
+@[simp] theorem Scalar.neq_to_neq_val {ty} : ∀ {i j : Scalar ty}, (¬ i = j) ↔ ¬ i.val = j.val := by
+ intro i j; cases i; cases j; simp
+
-- -- 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
-- -- enumerating all of the possible pairs. We remark that Rust has sane semantics
diff --git a/backends/lean/Base/Progress/Base.lean b/backends/lean/Base/Progress/Base.lean
index 6f820a84..76a92795 100644
--- a/backends/lean/Base/Progress/Base.lean
+++ b/backends/lean/Base/Progress/Base.lean
@@ -167,7 +167,8 @@ structure PSpecClassExprAttr where
deriving Inhabited
-- TODO: the original function doesn't define correctly the `addImportedFn`. Do a PR?
-def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) : IO (MapDeclarationExtension α) :=
+def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%) :
+ IO (MapDeclarationExtension α) :=
registerSimplePersistentEnvExtension {
name := name,
addImportedFn := fun a => a.foldl (fun s a => a.foldl (fun s (k, v) => s.insert k v) s) RBMap.empty,
@@ -175,6 +176,54 @@ def mkMapDeclarationExtension [Inhabited α] (name : Name := by exact decl_name%
toArrayFn := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
}
+-- Declare an extension of maps of maps (using [RBMap]).
+-- The important point is that we need to merge the bound values (which are maps).
+def mkMapMapDeclarationExtension [Inhabited β] (ord : α → α → Ordering)
+ (name : Name := by exact decl_name%) :
+ IO (MapDeclarationExtension (RBMap α β ord)) :=
+ registerSimplePersistentEnvExtension {
+ name := name,
+ addImportedFn := fun a =>
+ a.foldl (fun s a => a.foldl (
+ -- We need to merge the maps
+ fun s (k0, k1_to_v) =>
+ match s.find? k0 with
+ | none =>
+ -- No binding: insert one
+ s.insert k0 k1_to_v
+ | some m =>
+ -- There is already a binding: merge
+ let m := RBMap.fold (fun m k v => m.insert k v) m k1_to_v
+ s.insert k0 m)
+ s) RBMap.empty,
+ addEntryFn := fun s n => s.insert n.1 n.2 ,
+ toArrayFn := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
+ }
+
+-- Declare an extension of maps of maps (using [HashMap]).
+-- The important point is that we need to merge the bound values (which are maps).
+def mkMapHashMapDeclarationExtension [BEq α] [Hashable α] [Inhabited β]
+ (name : Name := by exact decl_name%) :
+ IO (MapDeclarationExtension (HashMap α β)) :=
+ registerSimplePersistentEnvExtension {
+ name := name,
+ addImportedFn := fun a =>
+ a.foldl (fun s a => a.foldl (
+ -- We need to merge the maps
+ fun s (k0, k1_to_v) =>
+ match s.find? k0 with
+ | none =>
+ -- No binding: insert one
+ s.insert k0 k1_to_v
+ | some m =>
+ -- There is already a binding: merge
+ let m := HashMap.fold (fun m k v => m.insert k v) m k1_to_v
+ s.insert k0 m)
+ s) RBMap.empty,
+ addEntryFn := fun s n => s.insert n.1 n.2 ,
+ toArrayFn := fun es => es.toArray.qsort (fun a b => Name.quickLt a.1 b.1)
+ }
+
/- The persistent map from function to pspec theorems. -/
initialize pspecAttr : PSpecAttr ← do
let ext ← mkMapDeclarationExtension `pspecMap
@@ -200,7 +249,8 @@ initialize pspecAttr : PSpecAttr ← do
/- The persistent map from type classes to pspec theorems -/
initialize pspecClassAttr : PSpecClassAttr ← do
- let ext : MapDeclarationExtension (NameMap Name) ← mkMapDeclarationExtension `pspecClassMap
+ let ext : MapDeclarationExtension (NameMap Name) ←
+ mkMapMapDeclarationExtension Name.quickCmp `pspecClassMap
let attrImpl : AttributeImpl := {
name := `cpspec
descr := "Marks theorems to use for type classes with the `progress` tactic"
@@ -231,7 +281,8 @@ initialize pspecClassAttr : PSpecClassAttr ← do
/- The 2nd persistent map from type classes to pspec theorems -/
initialize pspecClassExprAttr : PSpecClassExprAttr ← do
- let ext : MapDeclarationExtension (HashMap Expr Name) ← mkMapDeclarationExtension `pspecClassExprMap
+ let ext : MapDeclarationExtension (HashMap Expr Name) ←
+ mkMapHashMapDeclarationExtension `pspecClassExprMap
let attrImpl : AttributeImpl := {
name := `cepspec
descr := "Marks theorems to use for type classes with the `progress` tactic"
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 4fd88e36..8b0759c5 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -243,21 +243,26 @@ def progressAsmsOrLookupTheorem (keep : Option Name) (withTh : Option TheoremOrL
tryLookupApply keep ids splitPost asmTac fExpr "pspec theorem" pspec do
-- It failed: try to lookup a *class* expr spec theorem (those are more
-- specific than class spec theorems)
+ trace[Progress] "Failed using a pspec theorem: trying to lookup a pspec class expr theorem"
let pspecClassExpr ← do
match getFirstArg args with
| none => pure none
| some arg => do
+ trace[Progress] "Using: f:{fName}, arg: {arg}"
let thName ← pspecClassExprAttr.find? fName arg
pure (thName.map fun th => .Theorem th)
tryLookupApply keep ids splitPost asmTac fExpr "pspec class expr theorem" pspecClassExpr do
-- It failed: try to lookup a *class* spec theorem
+ trace[Progress] "Failed using a pspec class expr theorem: trying to lookup a pspec class theorem"
let pspecClass ← do
match ← getFirstArgAppName args with
| none => pure none
| some argName => do
+ trace[Progress] "Using: f: {fName}, arg: {argName}"
let thName ← pspecClassAttr.find? fName argName
pure (thName.map fun th => .Theorem th)
tryLookupApply keep ids splitPost asmTac fExpr "pspec class theorem" pspecClass do
+ trace[Progress] "Failed using a pspec class theorem: trying to use a recursive assumption"
-- Try a recursive call - we try the assumptions of kind "auxDecl"
let ctx ← Lean.MonadLCtx.getLCtx
let decls ← ctx.getAllDecls
@@ -346,11 +351,14 @@ elab "progress" args:progressArgs : tactic =>
namespace Test
open Primitives Result
+ -- Show the traces
-- set_option trace.Progress true
-- set_option pp.rawOnError true
+ -- The following commands display the databases of theorems
-- #eval showStoredPSpec
-- #eval showStoredPSpecClass
+ -- #eval showStoredPSpecExprClass
example {ty} {x y : Scalar ty}
(hmin : Scalar.min ty ≤ x.val + y.val)
@@ -366,6 +374,12 @@ namespace Test
progress keep h with Scalar.add_spec as ⟨ z ⟩
simp [*, h]
+ example {x y : U32}
+ (hmax : x.val + y.val ≤ U32.max) :
+ ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by
+ progress keep _ as ⟨ z, h1 .. ⟩
+ simp [*, h1]
+
/- Checking that universe instantiation works: the original spec uses
`α : Type u` where u is quantified, while here we use `α : Type 0` -/
example {α : Type} (v: Vec α) (i: Usize) (x : α)