summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJonathan Protzenko2023-01-23 18:43:45 -0800
committerSon HO2023-06-04 21:44:33 +0200
commitdee74ca1f90acb076289286f6f69df65e63604ce (patch)
tree50ddfb09bf11b20a688021c2413f45213c2c2450
parent262cb9d72593b349af522596cbae29dff03525ea (diff)
Write a tactic to discharge integer literal proof obligations
-rw-r--r--backends/lean/primitives.lean27
-rw-r--r--compiler/Extract.ml2
-rw-r--r--tests/lean/hashmap_on_disk/Hashmap/Funs.lean4
-rw-r--r--tests/lean/hashmap_on_disk/Hashmap/Primitives.lean31
4 files changed, 51 insertions, 13 deletions
diff --git a/backends/lean/primitives.lean b/backends/lean/primitives.lean
index b68df5f0..d86c0423 100644
--- a/backends/lean/primitives.lean
+++ b/backends/lean/primitives.lean
@@ -83,12 +83,13 @@ def massert (b:Bool) : result Unit :=
-- and
-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean
-- which both contain a fair amount of reasoning already!
-def USize.checked_sub (n: USize) (m: Nat): result USize :=
+def USize.checked_sub (n: USize) (m: USize): result USize :=
-- NOTE: the test USize.toNat n - m >= 0 seems to always succeed?
- if USize.toNat n >= m then
+ if n >= m then
let n' := USize.toNat n
- let r := USize.ofNatCore (n' - m) (by
- have h: n' - m <= n' := by
+ let m' := USize.toNat n
+ let r := USize.ofNatCore (n' - m') (by
+ have h: n' - m' <= n' := by
apply Nat.sub_le_of_le_add
case h => rewrite [ Nat.add_comm ]; apply Nat.le_add_left
apply Nat.lt_of_le_of_lt h
@@ -102,6 +103,24 @@ def USize.checked_sub (n: USize) (m: Nat): result USize :=
def USize.checked_mul (n: USize) (m: USize): result USize := sorry
def USize.checked_div (n: USize) (m: USize): result USize := sorry
+-- One needs to perform a little bit of reasoning in order to successfully
+-- inject constants into USize, so we provide a general-purpose macro
+
+syntax "intlit" : tactic
+
+macro_rules
+ | `(tactic| intlit) => `(tactic|
+ match USize.size, usize_size_eq with
+ | _, Or.inl rfl => decide
+ | _, Or.inr rfl => decide)
+
+-- This is how the macro is expected to be used
+#eval USize.ofNatCore 0 (by intlit)
+
+-- Also works for other integer types (at the expense of a needless disjunction)
+#eval UInt32.ofNatCore 0 (by intlit)
+
+-- Test behavior...
#eval USize.checked_sub 10 20
#eval USize.checked_sub 20 10
-- NOTE: compare with concrete behavior here, which I do not think we want
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 6bda6376..9496fcf9 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -573,7 +573,7 @@ let mk_formatter (ctx : trans_ctx) (crate_name : string)
F.pp_print_string fmt (int_name sv.int_ty);
F.pp_print_string fmt ".ofNatCore ";
Z.pp_print fmt sv.value;
- F.pp_print_string fmt (" (by simp))"))
+ F.pp_print_string fmt (" (by intlit))"))
| Bool b ->
let b = if b then "true" else "false" in
F.pp_print_string fmt b
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean
index a4f2e3e0..c67a37ff 100644
--- a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean
+++ b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean
@@ -15,10 +15,10 @@ def hashmap_hash_map_allocate_slots_loop_fwd
(T : Type) (slots : vec (hashmap_list_t T)) (n : USize) :
result (vec (hashmap_list_t T))
:=
- if n > (USize.ofNatCore 0 (by simp))
+ if n > (USize.ofNatCore 0 (by intlit))
then do
let slots0: vec (hashmap_list_t T) <- @vec_push_back (hashmap_list_t T) slots HashmapListNil
- let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by simp))
+ let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit))
hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0
else ret slots
termination_by hashmap_hash_map_allocate_slots_loop_fwd _ _ n => n
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean
index 83de98db..d86c0423 100644
--- a/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean
+++ b/tests/lean/hashmap_on_disk/Hashmap/Primitives.lean
@@ -22,12 +22,12 @@ deriving Repr
open result
-- TODO: is there automated syntax for these discriminators?
-def is_ret (α: Type) (r: result α): Bool :=
+def is_ret {α: Type} (r: result α): Bool :=
match r with
| result.ret _ => true
| result.fail _ => false
-def eval_global (α: Type) (x: result α) (h: is_ret α x): α :=
+def eval_global {α: Type} (x: result α) (h: is_ret x): α :=
match x with
| result.fail _ => by contradiction
| result.ret x => x
@@ -83,12 +83,13 @@ def massert (b:Bool) : result Unit :=
-- and
-- https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Data/UInt.lean
-- which both contain a fair amount of reasoning already!
-def USize.checked_sub (n: USize) (m: Nat): result USize :=
+def USize.checked_sub (n: USize) (m: USize): result USize :=
-- NOTE: the test USize.toNat n - m >= 0 seems to always succeed?
- if USize.toNat n >= m then
+ if n >= m then
let n' := USize.toNat n
- let r := USize.ofNatCore (n' - m) (by
- have h: n' - m <= n' := by
+ let m' := USize.toNat n
+ let r := USize.ofNatCore (n' - m') (by
+ have h: n' - m' <= n' := by
apply Nat.sub_le_of_le_add
case h => rewrite [ Nat.add_comm ]; apply Nat.le_add_left
apply Nat.lt_of_le_of_lt h
@@ -102,6 +103,24 @@ def USize.checked_sub (n: USize) (m: Nat): result USize :=
def USize.checked_mul (n: USize) (m: USize): result USize := sorry
def USize.checked_div (n: USize) (m: USize): result USize := sorry
+-- One needs to perform a little bit of reasoning in order to successfully
+-- inject constants into USize, so we provide a general-purpose macro
+
+syntax "intlit" : tactic
+
+macro_rules
+ | `(tactic| intlit) => `(tactic|
+ match USize.size, usize_size_eq with
+ | _, Or.inl rfl => decide
+ | _, Or.inr rfl => decide)
+
+-- This is how the macro is expected to be used
+#eval USize.ofNatCore 0 (by intlit)
+
+-- Also works for other integer types (at the expense of a needless disjunction)
+#eval UInt32.ofNatCore 0 (by intlit)
+
+-- Test behavior...
#eval USize.checked_sub 10 20
#eval USize.checked_sub 20 10
-- NOTE: compare with concrete behavior here, which I do not think we want