summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-05-31 10:56:20 +0200
committerSon HO2023-06-04 21:54:38 +0200
commit14a6149ccae22de6581e68f0fe6f5b7434235d6c (patch)
tree4e07cca226649f2f7bb93794738e8fbb6b4f961b /backends
parent446bbc0bdbb4a03d78636ec71f85e13e66b61e08 (diff)
Make progress on the proofs of the hash map
Diffstat (limited to 'backends')
-rw-r--r--backends/hol4/ilistScript.sml19
-rw-r--r--backends/hol4/ilistTheory.sig16
-rw-r--r--backends/hol4/primitivesArithScript.sml118
-rw-r--r--backends/hol4/primitivesArithTheory.sig25
-rw-r--r--backends/hol4/primitivesLib.sml4
5 files changed, 180 insertions, 2 deletions
diff --git a/backends/hol4/ilistScript.sml b/backends/hol4/ilistScript.sml
index 157b5c00..2183ef77 100644
--- a/backends/hol4/ilistScript.sml
+++ b/backends/hol4/ilistScript.sml
@@ -64,6 +64,25 @@ Proof
exfalso >> cooper_tac
QED
+Definition drop_def:
+ drop (i : int) ([] : 'a list) = [] ∧
+ drop (i : int) (x :: ls) =
+ if i < 0 then x :: ls
+ else if i = 0 then x :: ls
+ else drop (i - 1) ls
+End
+
+Theorem drop_eq:
+ (∀ i. drop i [] = []) ∧
+ (∀ ls. drop 0 ls = ls) ∧
+ (∀ i x ls. drop i (x :: ls) =
+ if (0 < i) ∨ (0 ≤ i ∧ i ≠ 0) then drop (i - 1) ls
+ else x :: ls)
+Proof
+ rw [drop_def] >> fs [] >> try_tac int_tac >>
+ Cases_on ‘ls’ >> fs [drop_def]
+QED
+
Theorem len_eq_LENGTH:
∀ls. len ls = &(LENGTH ls)
Proof
diff --git a/backends/hol4/ilistTheory.sig b/backends/hol4/ilistTheory.sig
index 21545b6e..da7cdbb3 100644
--- a/backends/hol4/ilistTheory.sig
+++ b/backends/hol4/ilistTheory.sig
@@ -3,12 +3,14 @@ sig
type thm = Thm.thm
(* Definitions *)
+ val drop_def : thm
val index_def : thm
val len_def : thm
val update_def : thm
(* Theorems *)
val append_len_eq : thm
+ val drop_eq : thm
val index_eq : thm
val index_eq_EL : thm
val len_append : thm
@@ -20,6 +22,13 @@ sig
(*
[primitivesArith] Parent theory of "ilist"
+ [drop_def] Definition
+
+ ⊢ (∀i. drop i [] = []) ∧
+ ∀i x ls.
+ drop i (x::ls) =
+ if i < 0 then x::ls else if i = 0 then x::ls else drop (i − 1) ls
+
[index_def] Definition
⊢ ∀i x ls.
@@ -46,6 +55,13 @@ sig
∀l1 l2 l1' l2'.
len l2 = len l2' ⇒ (l1 ⧺ l2 = l1' ⧺ l2' ⇔ l1 = l1' ∧ l2 = l2')
+ [drop_eq] Theorem
+
+ ⊢ (∀i. drop i [] = []) ∧ (∀ls. drop 0 ls = ls) ∧
+ ∀i x ls.
+ drop i (x::ls) =
+ if 0 < i ∨ 0 ≤ i ∧ i ≠ 0 then drop (i − 1) ls else x::ls
+
[index_eq] Theorem
⊢ (∀x ls. index 0 (x::ls) = x) ∧
diff --git a/backends/hol4/primitivesArithScript.sml b/backends/hol4/primitivesArithScript.sml
index 727fc8c2..decb1109 100644
--- a/backends/hol4/primitivesArithScript.sml
+++ b/backends/hol4/primitivesArithScript.sml
@@ -162,6 +162,12 @@ Proof
metis_tac [INT_LE_ADDR]
QED
+Theorem pos_div_pos_ge:
+ !(x y d : int). 0 <= x ==> 0 <= y ==> 0 < d ==> x >= y ==> x / d >= y / d
+Proof
+ metis_tac [pos_div_pos_le, ge_eq_le]
+QED
+
Theorem pos_div_pos_le_init:
!(x y : int). 0 <= x ==> 0 < y ==> x / y <= x
Proof
@@ -223,4 +229,116 @@ Proof
metis_tac [pos_mod_pos_is_pos, pos_mod_pos_lt]
QED
+Theorem mul_pos_left_le:
+ ∀ (a x y : int). 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y
+Proof
+ rw [] >> Cases_on ‘a = 0’ >> fs [] >>
+ sg ‘0 < a’ >- cooper_tac >>
+ metis_tac [integerTheory.INT_LE_MONO]
+QED
+
+Theorem mul_pos_right_le:
+ ∀ (a x y : int). 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a
+Proof
+ rw [mul_pos_left_le, integerTheory.INT_MUL_COMM]
+QED
+
+Theorem mul_pos_left_lt:
+ ∀ (a x y : int). 0 < a ⇒ x < y ⇒ a * x < a * y
+Proof
+ metis_tac [integerTheory.INT_LT_MONO]
+QED
+
+Theorem mul_pos_right_lt:
+ ∀ (a x y : int). 0 < a ⇒ x < y ⇒ x * a < y * a
+Proof
+ metis_tac [mul_pos_left_lt, integerTheory.INT_MUL_COMM]
+QED
+
+Theorem pos_mul_left_pos_le:
+ ∀ a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x
+Proof
+ rw [] >>
+ Cases_on ‘a = 1’ >> fs [] >>
+ sg ‘0 ≤ (a - 1) * x’ >- (irule pos_mul_pos_is_pos >> int_tac) >>
+ sg ‘x ≤ x + (a - 1) * x’ >- fs [] >>
+ sg ‘a * x = 1 * x + (a - 1) * x’ >- fs [GSYM integerTheory.INT_RDISTRIB] >>
+ fs []
+QED
+
+Theorem pos_mul_right_pos_le:
+ ∀ a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a
+Proof
+ metis_tac [pos_mul_left_pos_le, integerTheory.INT_MUL_COMM]
+QED
+
+Theorem pos_mul_left_pos_lt:
+ ∀ a x. 1 < a ⇒ 0 < x ⇒ x < a * x
+Proof
+ rw [] >>
+ sg ‘a * x = 1 * x + (a - 1) * x’
+ >- (fs [GSYM integerTheory.INT_RDISTRIB]) >>
+ fs [] >>
+ sg ‘(a − 1) * x = 1 * x + (a - 2) * x’
+ >- (
+ fs [GSYM integerTheory.INT_RDISTRIB] >>
+ sg ‘1 + (a − 2) = a - 1’ >- int_tac >>
+ fs []
+ ) >>
+ fs [] >>
+ sg ‘0 ≤ (a − 2) * x’ >- (irule pos_mul_pos_is_pos >> int_tac) >>
+ int_tac
+QED
+
+Theorem pos_mul_right_pos_lt:
+ ∀ a x. 1 < a ⇒ 0 < x ⇒ x < x * a
+Proof
+ metis_tac [pos_mul_left_pos_lt, integerTheory.INT_MUL_COMM]
+QED
+
+Theorem pos_div_pos_mul_le:
+ ∀ x y. 0 ≤ x ⇒ 0 < y ⇒ (x / y) * y ≤ x
+Proof
+ rw [] >>
+ qspec_assume ‘y’ integerTheory.INT_DIVISION >>
+ sg ‘y ≠ 0 ∧ ~(y < 0)’ >- int_tac >> fs [] >>
+ first_x_assum (qspec_assume ‘x’) >>
+ fs [] >>
+ (* TODO: int_tac loops here *)
+ cooper_tac
+QED
+
+Theorem pos_mul_pos_div_pos_decompose:
+ ∀ x y z. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 < z ⇒ x / z + y / z ≤ (x + y) / z
+Proof
+ rw [] >>
+ sg ‘z ≠ 0’ >- int_tac >>
+ sg ‘(x / z * z + x % z) + (y / z * z + y % z) = (x + y) / z * z + (x + y) % z’ >- metis_tac [integerTheory.INT_DIVISION] >>
+ sg ‘(x + y) % z = ((x % z) + (y % z)) % z’ >- metis_tac [integerTheory.INT_MOD_PLUS] >>
+ sg ‘0 ≤ (x % z) ∧ 0 ≤ (y % z)’ >- metis_tac [pos_mod_pos_is_pos] >>
+ sg ‘0 ≤ (x % z) + (y % z)’ >- int_tac >>
+ sg ‘((x % z) + (y % z)) % z ≤ (x % z) + (y % z)’ >- metis_tac [pos_mod_pos_le_init] >>
+ sg ‘x / z * z + y / z * z ≤ (x + y) / z * z’ >- int_tac >>
+ sg ‘x / z * z + y / z * z = (x / z + y / z) * z’ >- fs [integerTheory.INT_RDISTRIB] >> fs [] >>
+ sg ‘0 ≤ x / z’ >- (irule pos_div_pos_is_pos >> fs []) >>
+ sg ‘0 ≤ y / z’ >- (irule pos_div_pos_is_pos >> fs []) >>
+ sg ‘0 ≤ (x + y) / z’ >- (irule pos_div_pos_is_pos >> fs []) >>
+ sg ‘(x / z + y / z) * z / z ≤ (x + y) / z * z / z’
+ >- (
+ irule pos_div_pos_le >> fs [] >>
+ rw [] >> irule pos_mul_pos_is_pos >> fs []) >>
+ imp_res_tac integerTheory.INT_DIV_RMUL >>
+ metis_tac []
+QED
+
+Theorem pos_mul_2_div_pos_decompose:
+ ∀ x y. 0 ≤ x ⇒ 0 < y ⇒ x / y + x / y ≤ x * 2 / y
+Proof
+ rw [] >>
+ qspecl_assume [‘x’, ‘x’, ‘y’] pos_mul_pos_div_pos_decompose >> gvs [] >>
+ sg ‘x * 2 = (x * 1) + (x * 1)’
+ >- (pure_rewrite_tac [GSYM integerTheory.INT_LDISTRIB] >> fs []) >>
+ fs []
+QED
+
val _ = export_theory ()
diff --git a/backends/hol4/primitivesArithTheory.sig b/backends/hol4/primitivesArithTheory.sig
index 531797ac..84b9b67a 100644
--- a/backends/hol4/primitivesArithTheory.sig
+++ b/backends/hol4/primitivesArithTheory.sig
@@ -14,6 +14,8 @@ sig
val int_of_num_inj : thm
val le_eq_ge : thm
val lt_eq_gt : thm
+ val mul_pos_left_le : thm
+ val mul_pos_right_le : thm
val not_ge_eq_lt : thm
val not_gt_eq_le : thm
val not_le_eq_gt : thm
@@ -23,11 +25,14 @@ sig
val pos_div_pos_is_pos : thm
val pos_div_pos_le : thm
val pos_div_pos_le_init : thm
+ val pos_div_pos_mul_le : thm
val pos_mod_pos_ineqs : thm
val pos_mod_pos_is_pos : thm
val pos_mod_pos_le_init : thm
val pos_mod_pos_lt : thm
+ val pos_mul_left_pos_le : thm
val pos_mul_pos_is_pos : thm
+ val pos_mul_right_pos_le : thm
val primitivesArith_grammars : type_grammar.grammar * term_grammar.grammar
(*
@@ -79,6 +84,14 @@ sig
⊢ ∀x y. x < y ⇔ y > x
+ [mul_pos_left_le] Theorem
+
+ ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ a * x ≤ a * y
+
+ [mul_pos_right_le] Theorem
+
+ ⊢ ∀a x y. 0 ≤ a ⇒ x ≤ y ⇒ x * a ≤ y * a
+
[not_ge_eq_lt] Theorem
⊢ ∀x y. ¬(x ≥ y) ⇔ x < y
@@ -115,6 +128,10 @@ sig
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y ≤ x
+ [pos_div_pos_mul_le] Theorem
+
+ ⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x / y * y ≤ x
+
[pos_mod_pos_ineqs] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ 0 ≤ x % y ∧ x % y < y
@@ -131,10 +148,18 @@ sig
⊢ ∀x y. 0 ≤ x ⇒ 0 < y ⇒ x % y < y
+ [pos_mul_left_pos_le] Theorem
+
+ ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ a * x
+
[pos_mul_pos_is_pos] Theorem
⊢ ∀x y. 0 ≤ x ⇒ 0 ≤ y ⇒ 0 ≤ x * y
+ [pos_mul_right_pos_le] Theorem
+
+ ⊢ ∀a x. 0 < a ⇒ 0 ≤ x ⇒ x ≤ x * a
+
*)
end
diff --git a/backends/hol4/primitivesLib.sml b/backends/hol4/primitivesLib.sml
index 0a89be4c..a90f1e32 100644
--- a/backends/hol4/primitivesLib.sml
+++ b/backends/hol4/primitivesLib.sml
@@ -272,7 +272,7 @@ fun get_spec_app (t : term) : term =
fun get_key_normalize_thm (th : thm) : const_name * thm =
let
(* Transform the theroem a bit before storing it *)
- val th = SPEC_ALL th;
+ val th = (SPEC_ALL o BETA_RULE o PURE_REWRITE_RULE [LET_DEF]) th;
(* Retrieve the app ([f x0 ... xn]) *)
val f = get_spec_app (concl th);
(* Retrieve the function name *)
@@ -532,7 +532,7 @@ val progress : tactic =
val thl =
case Redblackmap.peek (get_spec_thms (), fname) of
NONE => asms_thl
- | SOME spec => spec :: asms_thl;
+ | SOME spec => asms_thl @ [spec];
val _ =
if null thl then
raise (failwith "progress: could not find a suitable theorem to apply")