diff options
Diffstat (limited to '')
| -rw-r--r-- | backends/hol4/testHashmapScript.sml | 416 | ||||
| -rw-r--r-- | backends/hol4/testHashmapTheory.sig | 305 | ||||
| -rw-r--r-- | backends/hol4/testScript.sml | 1747 | ||||
| -rw-r--r-- | backends/hol4/testTheory.sig | 834 |
4 files changed, 0 insertions, 3302 deletions
diff --git a/backends/hol4/testHashmapScript.sml b/backends/hol4/testHashmapScript.sml deleted file mode 100644 index c3f04cca..00000000 --- a/backends/hol4/testHashmapScript.sml +++ /dev/null @@ -1,416 +0,0 @@ -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib - -val _ = new_theory "testHashmap" - -(* - * Examples of proofs - *) - -Datatype: - list_t = - ListCons 't list_t - | ListNil -End - -val nth_mut_fwd_def = Define ‘ - nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth_mut_fwd tl i0 - od - | ListNil => - Fail Failure -’ - -(*** Examples of proofs on [nth] *) -val list_t_v_def = Define ‘ - list_t_v ListNil = [] /\ - list_t_v (ListCons x tl) = x :: list_t_v tl -’ - -Theorem nth_mut_fwd_spec: - !(ls : 't list_t) (i : u32). - u32_to_int i < len (list_t_v ls) ==> - case nth_mut_fwd ls i of - | Return x => x = index (u32_to_int i) (list_t_v ls) - | Fail _ => F - | Diverge => F -Proof - Induct_on ‘ls’ >> rw [list_t_v_def, len_def] >~ [‘ListNil’] - >-(massage >> int_tac) >> - pure_once_rewrite_tac [nth_mut_fwd_def] >> rw [] >> - fs [index_eq] >> - progress >> progress -QED - -val _ = save_spec_thm "nth_mut_fwd_spec" - -val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”) -val insert_def = new_axiom ("insert_def", “ - insert (key : u32) (value : 't) (ls : (u32 # 't) list_t) : (u32 # 't) list_t result = - case ls of - | ListCons (ckey, cvalue) tl => - if ckey = key - then Return (ListCons (ckey, value) tl) - else - do - tl0 <- insert key value tl; - Return (ListCons (ckey, cvalue) tl0) - od - | ListNil => Return (ListCons (key, value) ListNil) - ”) - -(* Property that keys are pairwise distinct *) -val distinct_keys_def = Define ‘ - distinct_keys (ls : (u32 # 't) list) = - !i j. - 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ - FST (index i ls) ≠ FST (index j ls) -’ - -val lookup_raw_def = Define ‘ - lookup_raw key [] = NONE /\ - lookup_raw key ((k, v) :: ls) = - if k = key then SOME v else lookup_raw key ls -’ - -val lookup_def = Define ‘ - lookup key ls = lookup_raw key (list_t_v ls) -’ - -(* Lemma about ‘insert’, without the invariant *) -Theorem insert_lem_aux: - !ls key value. - (* The keys are pairwise distinct *) - case insert key value ls of - | Return ls1 => - (* We updated the binding *) - lookup key ls1 = SOME value /\ - (* The other bindings are left unchanged *) - (!k. k <> key ==> lookup k ls = lookup k ls1) - | Fail _ => F - | Diverge => F -Proof - Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >> - pure_once_rewrite_tac [insert_def] >> rw [] - >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) - >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >> - case_tac >> rw [] - >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) - >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >> - progress >> - fs [lookup_def, lookup_raw_def, list_t_v_def] -QED - -(* - * Invariant proof 1 - *) - -Theorem distinct_keys_cons: - ∀ k v ls. - (∀ i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒ - distinct_keys ls ⇒ - distinct_keys ((k,v) :: ls) -Proof - rw [] >> - rw [distinct_keys_def] >> - Cases_on ‘i = 0’ >> fs [] - >-( - (* Use the first hypothesis *) - fs [index_eq] >> - last_x_assum (qspecl_assume [‘j - 1’]) >> - sg ‘0 ≤ j - 1’ >- int_tac >> - fs [len_def] >> - sg ‘j - 1 < len ls’ >- int_tac >> - fs [] - ) >> - (* Use the second hypothesis *) - sg ‘0 < i’ >- int_tac >> - sg ‘0 < j’ >- int_tac >> - fs [distinct_keys_def, index_eq, len_def] >> - first_x_assum (qspecl_assume [‘i - 1’, ‘j - 1’]) >> - sg ‘0 ≤ i - 1 ∧ i - 1 < j - 1 ∧ j - 1 < len ls’ >- int_tac >> - fs [] -QED - -Theorem distinct_keys_tail: - ∀ k v ls. - distinct_keys ((k,v) :: ls) ⇒ - distinct_keys ls -Proof - rw [distinct_keys_def] >> - last_x_assum (qspecl_assume [‘i + 1’, ‘j + 1’]) >> - fs [len_def] >> - sg ‘0 ≤ i + 1 ∧ i + 1 < j + 1 ∧ j + 1 < 1 + len ls’ >- int_tac >> fs [] >> - sg ‘0 < i + 1 ∧ 0 < j + 1’ >- int_tac >> fs [index_eq] >> - sg ‘i + 1 - 1 = i ∧ j + 1 - 1 = j’ >- int_tac >> fs [] -QED - -Theorem insert_index_neq: - ∀ q k v ls0 ls1 i. - (∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))) ⇒ - q ≠ k ⇒ - insert k v ls0 = Return ls1 ⇒ - 0 ≤ i ⇒ - i < len (list_t_v ls1) ⇒ - FST (index i (list_t_v ls1)) ≠ q -Proof - ntac 3 strip_tac >> - Induct_on ‘ls0’ >> rw [] >~ [‘ListNil’] - >-( - fs [insert_def] >> - sg ‘ls1 = ListCons (k,v) ListNil’ >- fs [] >> fs [list_t_v_def, len_def] >> - sg ‘i = 0’ >- int_tac >> fs [index_eq]) >> - Cases_on ‘t’ >> - Cases_on ‘i = 0’ >> fs [] - >-( - qpat_x_assum ‘insert _ _ _ = _’ mp_tac >> - simp [MK_BOUNDED insert_def 1, bind_def] >> - Cases_on ‘q' = k’ >> rw [] - >- (fs [list_t_v_def, index_eq]) >> - Cases_on ‘insert k v ls0’ >> fs [] >> - gvs [list_t_v_def, index_eq] >> - first_x_assum (qspec_assume ‘0’) >> - fs [len_def] >> - strip_tac >> - qspec_assume ‘list_t_v ls0’ len_pos >> - sg ‘0 < 1 + len (list_t_v ls0)’ >- int_tac >> - fs []) >> - qpat_x_assum ‘insert _ _ _ = _’ mp_tac >> - simp [MK_BOUNDED insert_def 1, bind_def] >> - Cases_on ‘q' = k’ >> rw [] - >-( - fs [list_t_v_def, index_eq, len_def] >> - first_x_assum (qspec_assume ‘i’) >> rfs []) >> - Cases_on ‘insert k v ls0’ >> fs [] >> - gvs [list_t_v_def, index_eq] >> - last_x_assum (qspec_assume ‘i - 1’) >> - fs [len_def] >> - sg ‘0 ≤ i - 1 ∧ i - 1 < len (list_t_v a)’ >- int_tac >> fs [] >> - first_x_assum irule >> - rw [] >> - last_x_assum (qspec_assume ‘j + 1’) >> - rfs [] >> - sg ‘j + 1 < 1 + len (list_t_v ls0) ∧ j + 1 − 1 = j ∧ j + 1 ≠ 0’ >- int_tac >> fs [] -QED - -Theorem distinct_keys_insert_index_neq: - ∀ k v q r ls0 ls1 i. - distinct_keys ((q,r)::list_t_v ls0) ⇒ - q ≠ k ⇒ - insert k v ls0 = Return ls1 ⇒ - 0 ≤ i ⇒ - i < len (list_t_v ls1) ⇒ - FST (index i (list_t_v ls1)) ≠ q -Proof - rw [] >> - (* Use the first assumption to prove the following assertion *) - sg ‘∀ j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ q ≠ FST (index j (list_t_v ls0))’ - >-( - strip_tac >> - fs [distinct_keys_def] >> - last_x_assum (qspecl_assume [‘0’, ‘j + 1’]) >> - fs [index_eq] >> - sg ‘j + 1 - 1 = j’ >- int_tac >> fs [len_def] >> - rw []>> - first_x_assum irule >> int_tac) >> - qspecl_assume [‘q’, ‘k’, ‘v’, ‘ls0’, ‘ls1’, ‘i’] insert_index_neq >> - fs [] -QED - -Theorem distinct_keys_insert: - ∀ k v ls0 ls1. - distinct_keys (list_t_v ls0) ⇒ - insert k v ls0 = Return ls1 ⇒ - distinct_keys (list_t_v ls1) -Proof - Induct_on ‘ls0’ >~ [‘ListNil’] - >-( - rw [distinct_keys_def, list_t_v_def, insert_def] >> - fs [list_t_v_def, len_def] >> - int_tac) >> - Cases >> - pure_once_rewrite_tac [insert_def] >> fs[] >> - rw [] >> fs [] - >-( - (* k = q *) - last_x_assum ignore_tac >> - fs [distinct_keys_def] >> - rw [] >> - last_x_assum (qspecl_assume [‘i’, ‘j’]) >> - rfs [list_t_v_def, len_def] >> - sg ‘0 < j’ >- int_tac >> - Cases_on ‘i = 0’ >> gvs [index_eq]) >> - (* k ≠ q: recursion *) - Cases_on ‘insert k v ls0’ >> fs [bind_def] >> - last_x_assum (qspecl_assume [‘k’, ‘v’, ‘a’]) >> - gvs [list_t_v_def] >> - imp_res_tac distinct_keys_tail >> fs [] >> - irule distinct_keys_cons >> rw [] >> - metis_tac [distinct_keys_insert_index_neq] -QED - -Theorem insert_lem: - !ls key value. - (* The keys are pairwise distinct *) - distinct_keys (list_t_v ls) ==> - case insert key value ls of - | Return ls1 => - (* We updated the binding *) - lookup key ls1 = SOME value /\ - (* The other bindings are left unchanged *) - (!k. k <> key ==> lookup k ls = lookup k ls1) ∧ - (* The keys are still pairwise disjoint *) - distinct_keys (list_t_v ls1) - | Fail _ => F - | Diverge => F -Proof - rw [] >> - qspecl_assume [‘ls’, ‘key’, ‘value’] insert_lem_aux >> - case_tac >> fs [] >> - metis_tac [distinct_keys_insert] -QED - -(* - * Invariant proof 2: functional version of the invariant - *) -val for_all_def = Define ‘ - for_all p [] = T ∧ - for_all p (x :: ls) = (p x ∧ for_all p ls) -’ - -val pairwise_rel_def = Define ‘ - pairwise_rel p [] = T ∧ - pairwise_rel p (x :: ls) = (for_all (p x) ls ∧ pairwise_rel p ls) -’ - -val distinct_keys_f_def = Define ‘ - distinct_keys_f (ls : (u32 # 't) list) = - pairwise_rel (\x y. FST x ≠ FST y) ls -’ - -Theorem distinct_keys_f_insert_for_all: - ∀k v k1 ls0 ls1. - k1 ≠ k ⇒ - for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒ - pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒ - insert k v ls0 = Return ls1 ⇒ - for_all (λy. k1 ≠ FST y) (list_t_v ls1) -Proof - Induct_on ‘ls0’ >> rw [pairwise_rel_def] >~ [‘ListNil’] >> - gvs [list_t_v_def, pairwise_rel_def, for_all_def] - >-(gvs [MK_BOUNDED insert_def 1, bind_def, list_t_v_def, for_all_def]) >> - pat_undisch_tac ‘insert _ _ _ = _’ >> - simp [MK_BOUNDED insert_def 1, bind_def] >> - Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >> - Cases_on ‘insert k v ls0’ >> - gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >> - metis_tac [] -QED - -Theorem distinct_keys_f_insert: - ∀ k v ls0 ls1. - distinct_keys_f (list_t_v ls0) ⇒ - insert k v ls0 = Return ls1 ⇒ - distinct_keys_f (list_t_v ls1) -Proof - Induct_on ‘ls0’ >> rw [distinct_keys_f_def] >~ [‘ListNil’] - >-( - fs [list_t_v_def, insert_def] >> - gvs [list_t_v_def, pairwise_rel_def, for_all_def]) >> - last_x_assum (qspecl_assume [‘k’, ‘v’]) >> - pat_undisch_tac ‘insert _ _ _ = _’ >> - simp [MK_BOUNDED insert_def 1, bind_def] >> - (* TODO: improve case_tac *) - Cases_on ‘t’ >> rw [] >> gvs [list_t_v_def, pairwise_rel_def, for_all_def] >> - Cases_on ‘insert k v ls0’ >> - gvs [distinct_keys_f_def, list_t_v_def, pairwise_rel_def, for_all_def] >> - metis_tac [distinct_keys_f_insert_for_all] -QED - -(* - * Proving equivalence between the two version - exercise. - *) -Theorem for_all_quant: - ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls) -Proof - strip_tac >> Induct_on ‘ls’ - >-(rw [for_all_def, len_def] >> int_tac) >> - rw [for_all_def, len_def, index_eq] >> - equiv_tac - >-( - rw [] >> - Cases_on ‘i = 0’ >> fs [] >> - first_x_assum irule >> - int_tac) >> - rw [] - >-( - first_x_assum (qspec_assume ‘0’) >> fs [] >> - first_x_assum irule >> - qspec_assume ‘ls’ len_pos >> - int_tac) >> - first_x_assum (qspec_assume ‘i + 1’) >> - fs [] >> - sg ‘i + 1 ≠ 0 ∧ i + 1 - 1 = i’ >- int_tac >> fs [] >> - first_x_assum irule >> int_tac -QED - -Theorem pairwise_rel_quant: - ∀p ls. pairwise_rel p ls ⇔ - (∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls)) -Proof - strip_tac >> Induct_on ‘ls’ - >-(rw [pairwise_rel_def, len_def] >> int_tac) >> - rw [pairwise_rel_def, len_def] >> - equiv_tac - >-( - (* ==> *) - rw [] >> - sg ‘0 < j’ >- int_tac >> - Cases_on ‘i = 0’ - >-( - simp [index_eq] >> - qspecl_assume [‘p h’, ‘ls’] (iffLR for_all_quant) >> - first_x_assum irule >> fs [] >> int_tac - ) >> - rw [index_eq] >> - first_x_assum irule >> int_tac - ) >> - (* <== *) - rw [] - >-( - rw [for_all_quant] >> - first_x_assum (qspecl_assume [‘0’, ‘i + 1’]) >> - sg ‘0 < i + 1 ∧ i + 1 - 1 = i’ >- int_tac >> - fs [index_eq] >> - first_x_assum irule >> int_tac - ) >> - sg ‘pairwise_rel p ls’ - >-( - rw [pairwise_rel_def] >> - first_x_assum (qspecl_assume [‘i' + 1’, ‘j' + 1’]) >> - sg ‘0 < i' + 1 ∧ 0 < j' + 1’ >- int_tac >> - fs [index_eq, int_add_minus_same_eq] >> - first_x_assum irule >> int_tac - ) >> - fs [] -QED - -Theorem distinct_keys_f_eq_distinct_keys: - ∀ ls. - distinct_keys_f ls ⇔ distinct_keys ls -Proof - rw [distinct_keys_def, distinct_keys_f_def] >> - qspecl_assume [‘(λx y. FST x ≠ FST y)’, ‘ls’] pairwise_rel_quant >> - fs [] -QED - -val _ = export_theory () diff --git a/backends/hol4/testHashmapTheory.sig b/backends/hol4/testHashmapTheory.sig deleted file mode 100644 index 1d304723..00000000 --- a/backends/hol4/testHashmapTheory.sig +++ /dev/null @@ -1,305 +0,0 @@ -signature testHashmapTheory = -sig - type thm = Thm.thm - - (* Axioms *) - val insert_def : thm - - (* Definitions *) - val distinct_keys_def : thm - val distinct_keys_f_def : thm - val for_all_def : thm - val list_t_TY_DEF : thm - val list_t_case_def : thm - val list_t_size_def : thm - val list_t_v_def : thm - val lookup_def : thm - val pairwise_rel_def : thm - - (* Theorems *) - val datatype_list_t : thm - val distinct_keys_cons : thm - val distinct_keys_f_eq_distinct_keys : thm - val distinct_keys_f_insert : thm - val distinct_keys_f_insert_for_all : thm - val distinct_keys_insert : thm - val distinct_keys_insert_index_neq : thm - val distinct_keys_tail : thm - val for_all_quant : thm - val insert_index_neq : thm - val insert_lem : thm - val insert_lem_aux : thm - val list_t_11 : thm - val list_t_Axiom : thm - val list_t_case_cong : thm - val list_t_case_eq : thm - val list_t_distinct : thm - val list_t_induction : thm - val list_t_nchotomy : thm - val lookup_raw_def : thm - val lookup_raw_ind : thm - val nth_mut_fwd_def : thm - val nth_mut_fwd_ind : thm - val nth_mut_fwd_spec : thm - val pairwise_rel_quant : thm - - val testHashmap_grammars : type_grammar.grammar * term_grammar.grammar -(* - [primitives] Parent theory of "testHashmap" - - [insert_def] Axiom - - [oracles: ] [axioms: insert_def] [] - ⊢ insert key value ls = - case ls of - ListCons (ckey,cvalue) tl => - if ckey = key then Return (ListCons (ckey,value) tl) - else - do - tl0 <- insert key value tl; - Return (ListCons (ckey,cvalue) tl0) - od - | ListNil => Return (ListCons (key,value) ListNil) - - [distinct_keys_def] Definition - - ⊢ ∀ls. - distinct_keys ls ⇔ - ∀i j. - 0 ≤ i ⇒ - i < j ⇒ - j < len ls ⇒ - FST (index i ls) ≠ FST (index j ls) - - [distinct_keys_f_def] Definition - - ⊢ ∀ls. distinct_keys_f ls ⇔ pairwise_rel (λx y. FST x ≠ FST y) ls - - [for_all_def] Definition - - ⊢ (∀p. for_all p [] ⇔ T) ∧ - ∀p x ls. for_all p (x::ls) ⇔ p x ∧ for_all p ls - - [list_t_TY_DEF] Definition - - ⊢ ∃rep. - TYPE_DEFINITION - (λa0'. - ∀ $var$('list_t'). - (∀a0'. - (∃a0 a1. - a0' = - (λa0 a1. - ind_type$CONSTR 0 a0 - (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) - a0 a1 ∧ $var$('list_t') a1) ∨ - a0' = - ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒ - $var$('list_t') a0') ⇒ - $var$('list_t') a0') rep - - [list_t_case_def] Definition - - ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧ - ∀f v. list_t_CASE ListNil f v = v - - [list_t_size_def] Definition - - ⊢ (∀f a0 a1. - list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧ - ∀f. list_t_size f ListNil = 0 - - [list_t_v_def] Definition - - ⊢ list_t_v ListNil = [] ∧ - ∀x tl. list_t_v (ListCons x tl) = x::list_t_v tl - - [lookup_def] Definition - - ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls) - - [pairwise_rel_def] Definition - - ⊢ (∀p. pairwise_rel p [] ⇔ T) ∧ - ∀p x ls. - pairwise_rel p (x::ls) ⇔ for_all (p x) ls ∧ pairwise_rel p ls - - [datatype_list_t] Theorem - - ⊢ DATATYPE (list_t ListCons ListNil) - - [distinct_keys_cons] Theorem - - ⊢ ∀k v ls. - (∀i. 0 ≤ i ⇒ i < len ls ⇒ FST (index i ls) ≠ k) ⇒ - distinct_keys ls ⇒ - distinct_keys ((k,v)::ls) - - [distinct_keys_f_eq_distinct_keys] Theorem - - ⊢ ∀ls. distinct_keys_f ls ⇔ distinct_keys ls - - [distinct_keys_f_insert] Theorem - - [oracles: DISK_THM] [axioms: insert_def] [] - ⊢ ∀k v ls0 ls1. - distinct_keys_f (list_t_v ls0) ⇒ - insert k v ls0 = Return ls1 ⇒ - distinct_keys_f (list_t_v ls1) - - [distinct_keys_f_insert_for_all] Theorem - - [oracles: DISK_THM] [axioms: insert_def] [] - ⊢ ∀k v k1 ls0 ls1. - k1 ≠ k ⇒ - for_all (λy. k1 ≠ FST y) (list_t_v ls0) ⇒ - pairwise_rel (λx y. FST x ≠ FST y) (list_t_v ls0) ⇒ - insert k v ls0 = Return ls1 ⇒ - for_all (λy. k1 ≠ FST y) (list_t_v ls1) - - [distinct_keys_insert] Theorem - - [oracles: DISK_THM] [axioms: insert_def] [] - ⊢ ∀k v ls0 ls1. - distinct_keys (list_t_v ls0) ⇒ - insert k v ls0 = Return ls1 ⇒ - distinct_keys (list_t_v ls1) - - [distinct_keys_insert_index_neq] Theorem - - [oracles: DISK_THM] [axioms: insert_def] [] - ⊢ ∀k v q r ls0 ls1 i. - distinct_keys ((q,r)::list_t_v ls0) ⇒ - q ≠ k ⇒ - insert k v ls0 = Return ls1 ⇒ - 0 ≤ i ⇒ - i < len (list_t_v ls1) ⇒ - FST (index i (list_t_v ls1)) ≠ q - - [distinct_keys_tail] Theorem - - ⊢ ∀k v ls. distinct_keys ((k,v)::ls) ⇒ distinct_keys ls - - [for_all_quant] Theorem - - ⊢ ∀p ls. for_all p ls ⇔ ∀i. 0 ≤ i ⇒ i < len ls ⇒ p (index i ls) - - [insert_index_neq] Theorem - - [oracles: DISK_THM] [axioms: insert_def] [] - ⊢ ∀q k v ls0 ls1 i. - (∀j. 0 ≤ j ∧ j < len (list_t_v ls0) ⇒ - q ≠ FST (index j (list_t_v ls0))) ⇒ - q ≠ k ⇒ - insert k v ls0 = Return ls1 ⇒ - 0 ≤ i ⇒ - i < len (list_t_v ls1) ⇒ - FST (index i (list_t_v ls1)) ≠ q - - [insert_lem] Theorem - - [oracles: DISK_THM] [axioms: insert_def] [] - ⊢ ∀ls key value. - distinct_keys (list_t_v ls) ⇒ - case insert key value ls of - Return ls1 => - lookup key ls1 = SOME value ∧ - (∀k. k ≠ key ⇒ lookup k ls = lookup k ls1) ∧ - distinct_keys (list_t_v ls1) - | Fail v1 => F - | Diverge => F - - [insert_lem_aux] Theorem - - [oracles: DISK_THM] [axioms: insert_def] [] - ⊢ ∀ls key value. - case insert key value ls of - Return ls1 => - lookup key ls1 = SOME value ∧ - ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1 - | Fail v1 => F - | Diverge => F - - [list_t_11] Theorem - - ⊢ ∀a0 a1 a0' a1'. - ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1' - - [list_t_Axiom] Theorem - - ⊢ ∀f0 f1. ∃fn. - (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧ - fn ListNil = f1 - - [list_t_case_cong] Theorem - - ⊢ ∀M M' f v. - M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧ - (M' = ListNil ⇒ v = v') ⇒ - list_t_CASE M f v = list_t_CASE M' f' v' - - [list_t_case_eq] Theorem - - ⊢ list_t_CASE x f v = v' ⇔ - (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v' - - [list_t_distinct] Theorem - - ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil - - [list_t_induction] Theorem - - ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l - - [list_t_nchotomy] Theorem - - ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil - - [lookup_raw_def] Theorem - - ⊢ (∀key. lookup_raw key [] = NONE) ∧ - ∀v ls key k. - lookup_raw key ((k,v)::ls) = - if k = key then SOME v else lookup_raw key ls - - [lookup_raw_ind] Theorem - - ⊢ ∀P. (∀key. P key []) ∧ - (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒ - ∀v v1. P v v1 - - [nth_mut_fwd_def] Theorem - - ⊢ ∀ls i. - nth_mut_fwd ls i = - case ls of - ListCons x tl => - if u32_to_int i = 0 then Return x - else do i0 <- u32_sub i (int_to_u32 1); nth_mut_fwd tl i0 od - | ListNil => Fail Failure - - [nth_mut_fwd_ind] Theorem - - ⊢ ∀P. (∀ls i. - (∀x tl i0. ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ P tl i0) ⇒ - P ls i) ⇒ - ∀v v1. P v v1 - - [nth_mut_fwd_spec] Theorem - - ⊢ ∀ls i. - u32_to_int i < len (list_t_v ls) ⇒ - case nth_mut_fwd ls i of - Return x => x = index (u32_to_int i) (list_t_v ls) - | Fail v1 => F - | Diverge => F - - [pairwise_rel_quant] Theorem - - ⊢ ∀p ls. - pairwise_rel p ls ⇔ - ∀i j. 0 ≤ i ⇒ i < j ⇒ j < len ls ⇒ p (index i ls) (index j ls) - - -*) -end diff --git a/backends/hol4/testScript.sml b/backends/hol4/testScript.sml deleted file mode 100644 index 8b4d523c..00000000 --- a/backends/hol4/testScript.sml +++ /dev/null @@ -1,1747 +0,0 @@ -open HolKernel boolLib bossLib Parse - -val primitives_theory_name = "test" -val _ = new_theory primitives_theory_name - -open boolTheory integerTheory wordsTheory stringTheory - -Datatype: - error = Failure -End - -Datatype: - result = Return 'a | Fail error | Loop -End - -Type M = ``: 'a result`` - -(* TODO: rename *) -val st_ex_bind_def = Define ` - (st_ex_bind : 'a M -> ('a -> 'b M) -> 'b M) x f = - case x of - Return y => f y - | Fail e => Fail e - | Loop => Loop`; - -val bind_name = fst (dest_const “st_ex_bind”) - -val st_ex_return_def = Define ` - (st_ex_return : 'a -> 'a M) x = - Return x`; - -Overload monad_bind[local] = ``st_ex_bind`` -Overload monad_unitbind[local] = ``\x y. st_ex_bind x (\z. y)`` -Overload monad_ignore_bind[local] = ``\x y. st_ex_bind x (\z. y)`` -(*Overload ex_bind[local] = ``st_ex_bind`` *) -(* Overload ex_return[local] = ``st_ex_return`` *) -(*Overload failwith = ``raise_Fail``*) - -(* Temporarily allow the monadic syntax *) -val _ = monadsyntax.temp_add_monadsyntax () - -val test1_def = Define ` - test1 (x : bool) = Return x` - -val is_true_def = Define ‘ - is_true (x : bool) = if x then Return () else Fail Failure’ - -val test1_def = Define ‘ - test1 (x : bool) = Return x’ - -val test_monad_def = Define ` - test_monad v = - do - x <- Return v; - Return x - od` - -val test_monad2_def = Define ` - test_monad2 = - do - x <- Return T; - Return x - od` - -val test_monad3_def = Define ` - test_monad3 x = - do - is_true x; - Return x - od` - -(** - * Arithmetic - *) - -open intLib - -val test_int1 = Define ‘int1 = 32’ -val test_int2 = Define ‘int2 = -32’ - -Theorem INT_THM1: - !(x y : int). x > 0 ==> y > 0 ==> x + y > 0 -Proof - ARITH_TAC -QED - -Theorem INT_THM2: - !(x : int). T -Proof - rw[] -QED - -val _ = prefer_int () - -val x = “-36217863217862718” - -(* Deactivate notations for int *) -val _ = deprecate_int () -open arithmeticTheory - - -val m = Hol_pp.print_apropos -val f = Hol_pp.print_find - -(* Display types on/off: M-h C-t *) -(* Move back: M-h b *) - -val _ = numLib.deprecate_num () -val _ = numLib.prefer_num () - -Theorem NAT_THM1: - !(n : num). n < n + 1 -Proof - Induct_on ‘n’ >> DECIDE_TAC -QED - -Theorem NAT_THM2: - !(n : num). n < n + (1 : num) -Proof - gen_tac >> - Induct_on ‘n’ >- ( - PURE_REWRITE_TAC [ADD, NUMERAL_DEF, BIT1, ALT_ZERO] >> - PURE_REWRITE_TAC [prim_recTheory.LESS_0_0]) >> - PURE_REWRITE_TAC [ADD] >> - irule prim_recTheory.LESS_MONO >> - asm_rewrite_tac [] -QED - - -val x = “1278361286371286:num” - - -(********************** PRIMITIVES *) -val _ = prefer_int () - -val _ = new_type ("u32", 0) -val _ = new_type ("i32", 0) - -(*val u32_min_def = Define ‘u32_min = (0:int)’*) -val u32_max_def = Define ‘u32_max = (4294967295:int)’ - -(* TODO: change that *) -val usize_max_def = Define ‘usize_max = (4294967295:int)’ - -val i32_min_def = Define ‘i32_min = (-2147483648:int)’ -val i32_max_def = Define ‘i32_max = (2147483647:int)’ - -val _ = new_constant ("u32_to_int", “:u32 -> int”) -val _ = new_constant ("i32_to_int", “:i32 -> int”) - -val _ = new_constant ("int_to_u32", “:int -> u32”) -val _ = new_constant ("int_to_i32", “:int -> i32”) - - -(* TODO: change to "...of..." *) -val u32_to_int_bounds = - new_axiom ( - "u32_to_int_bounds", - “!n. 0 <= u32_to_int n /\ u32_to_int n <= u32_max”) - -val i32_to_int_bounds = - new_axiom ( - "i32_to_int_bounds", - “!n. i32_min <= i32_to_int n /\ i32_to_int n <= i32_max”) - -val int_to_u32_id = new_axiom ("int_to_u32_id", - “!n. 0 <= n /\ n <= u32_max ==> u32_to_int (int_to_u32 n) = n”) - -val int_to_i32_id = - new_axiom ( - "int_to_i32_id", - “!n. i32_min <= n /\ n <= i32_max ==> - i32_to_int (int_to_i32 n) = n”) - -val mk_u32_def = Define - ‘mk_u32 n = - if 0 <= n /\ n <= u32_max then Return (int_to_u32 n) - else Fail Failure’ - -val u32_add_def = Define ‘u32_add x y = mk_u32 ((u32_to_int x) + (u32_to_int y))’ - -Theorem MK_U32_SUCCESS: - !n. 0 <= n /\ n <= u32_max ==> - mk_u32 n = Return (int_to_u32 n) -Proof - rw[mk_u32_def] -QED - -Theorem U32_ADD_EQ: - !x y. - u32_to_int x + u32_to_int y <= u32_max ==> - ?z. u32_add x y = Return z /\ u32_to_int z = u32_to_int x + u32_to_int y -Proof - rpt gen_tac >> - rpt DISCH_TAC >> - exists_tac “int_to_u32 (u32_to_int x + u32_to_int y)” >> - imp_res_tac MK_U32_SUCCESS >> - (* There is probably a better way of doing this *) - sg ‘0 <= u32_to_int x’ >- (rw[u32_to_int_bounds]) >> - sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >> - fs [u32_add_def] >> - irule int_to_u32_id >> - fs[] -QED - -val u32_sub_def = Define ‘u32_sub x y = mk_u32 ((u32_to_int x) - (u32_to_int y))’ - -Theorem U32_SUB_EQ: - !x y. - 0 <= u32_to_int x - u32_to_int y ==> - ?z. u32_sub x y = Return z /\ u32_to_int z = u32_to_int x - u32_to_int y -Proof - rpt gen_tac >> - rpt DISCH_TAC >> - exists_tac “int_to_u32 (u32_to_int x - u32_to_int y)” >> - imp_res_tac MK_U32_SUCCESS >> - (* There is probably a better way of doing this *) - sg ‘u32_to_int x − u32_to_int y ≤ u32_max’ >-( - sg ‘u32_to_int x <= u32_max’ >- (rw[u32_to_int_bounds]) >> - sg ‘0 <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >> - COOPER_TAC - ) >> - fs [u32_sub_def] >> - irule int_to_u32_id >> - fs[] -QED - -val mk_i32_def = Define - ‘mk_i32 n = - if i32_min <= n /\ n <= i32_max then Return (int_to_i32 n) - else Fail Failure’ - -val i32_add_def = Define ‘i32_add x y = mk_i32 ((i32_to_int x) + (i32_to_int y))’ - -Theorem MK_I32_SUCCESS: - !n. i32_min <= n /\ n <= i32_max ==> - mk_i32 n = Return (int_to_i32 n) -Proof - rw[mk_i32_def] -QED - -Theorem I32_ADD_EQ: - !x y. - i32_min <= i32_to_int x + i32_to_int y ==> - i32_to_int x + i32_to_int y <= i32_max ==> - ?z. i32_add x y = Return z /\ i32_to_int z = i32_to_int x + i32_to_int y -Proof - rpt gen_tac >> - rpt DISCH_TAC >> - exists_tac “int_to_i32 (i32_to_int x + i32_to_int y)” >> - imp_res_tac MK_I32_SUCCESS >> - fs [i32_min_def, i32_add_def] >> - irule int_to_i32_id >> - fs[i32_min_def] -QED - -open listTheory - -val _ = new_type ("vec", 1) -val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”) - -val VEC_TO_LIST_NUM_BOUNDS = - new_axiom ( - "VEC_TO_LIST_BOUNDS", - “!v. let l = LENGTH (vec_to_list v) in - (0:num) <= l /\ l <= (4294967295:num)”) - -Theorem VEC_TO_LIST_INT_BOUNDS: - !v. let l = int_of_num (LENGTH (vec_to_list v)) in - 0 <= l /\ l <= u32_max -Proof - gen_tac >> - rw [u32_max_def] >> - assume_tac VEC_TO_LIST_NUM_BOUNDS >> - fs[] -QED - -val VEC_LEN_DEF = Define ‘vec_len v = int_to_u32 (int_of_num (LENGTH (vec_to_list v)))’ - -(* -(* Useless *) -Theorem VEC_LEN_BOUNDS: - !v. u32_min <= u32_to_int (vec_len v) /\ u32_to_int (vec_len v) <= u32_max -Proof - gen_tac >> - qspec_then ‘v’ assume_tac VEC_TO_LIST_INT_BOUNDS >> - fs[VEC_LEN_DEF] >> - IMP_RES_TAC int_to_u32_id >> - fs[] -QED -*) - -(* The type parameters are ordered in alphabetical order *) -Datatype: - test = Variant1 'b | Variant2 'a -End - -Datatype: - test2 = Variant1_1 'T2 | Variant2_1 'T1 -End - -Datatype: - test2 = Variant1_2 'T1 | Variant2_2 'T2 -End - -(* -“Variant1_1 3” -“Variant1_2 3” - -type_of “CONS 3” -*) - -(* TODO: argument order, we must also omit arguments in new type *) -Datatype: - list_t = - ListCons 't list_t - | ListNil -End - -val list_nth_mut_loop_loop_fwd_def = Define ‘ - list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - list_nth_mut_loop_loop_fwd tl i0 - od - | ListNil => - Fail Failure -’ - -(* -CoInductive coind: - !x y. coind x /\ coind y ==> coind (x + y) -End -*) - -(* -(* This generates inconsistent theorems *) -CoInductive loop: - !x. loop x = if x then loop x else 0 -End - -CoInductive loop: - !(x : int). loop x = if x > 0 then loop (x - 1) else 0 -End -*) - -(* This terminates *) -val list_nth_mut_loop_loop_fwd_def = Define ‘ - list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - list_nth_mut_loop_loop_fwd tl i0 - od - | ListNil => - Fail Failure -’ - -(* This is sort of a coinductive definition. - - This can be justified: - - we first define a version [nth_fuel] which uses fuel (and is thus terminating) - - we define the predicate P: - P ls i n = case nth_fuel n ls i of Return _ => T | _ => F - - we then use [LEAST] (least upper bound for natural numbers) to define nth as: - “nth ls i = if (?n. P n) then nth_fuel (LEAST (P ls i)) ls i else Fail Loop ” - - we finally prove that nth satisfies the proper equation. - - We would need the following intermediate lemma: - !n. - n < LEAST (P ls i) ==> nth_fuel n ls i = Fail _ /\ - n >= LEAST (P ls i) ==> nth_fuel n ls i = nth_fuel (LEAST P ls i) ls i - - *) -val _ = new_constant ("nth", “:'t list_t -> u32 -> 't result”) -val nth_def = new_axiom ("nth_def", “ - nth (ls : 't list_t) (i : u32) : 't result = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth tl i0 - od - | ListNil => - Fail Failure - ”) - - -(*** Examples of proofs on [nth] *) -val list_t_v_def = Define ‘ - list_t_v ListNil = [] /\ - list_t_v (ListCons x tl) = x :: list_t_v tl -’ - -(* TODO: move *) -open dep_rewrite -open integerTheory - -(* Ignore a theorem. - - To be used in conjunction with {!pop_assum} for instance. - *) -fun IGNORE_TAC (_ : thm) : tactic = ALL_TAC - - -Theorem INT_OF_NUM_INJ: - !n m. &n = &m ==> n = m -Proof - rpt strip_tac >> - fs [Num] -QED - -Theorem NUM_SUB_EQ: - !(x y z : int). x = y - z ==> 0 <= x ==> 0 <= z ==> Num y = Num z + Num x -Proof - rpt strip_tac >> - sg ‘0 <= y’ >- COOPER_TAC >> - rfs [] >> - (* Convert to integers *) - irule INT_OF_NUM_INJ >> - imp_res_tac (GSYM INT_OF_NUM) >> - (* Associativity of & *) - PURE_REWRITE_TAC [GSYM INT_ADD] >> - fs [] -QED - -Theorem NUM_SUB_1_EQ: - !(x y : int). x = y - 1 ==> 0 <= x ==> Num y = SUC (Num x) -Proof - rpt strip_tac >> - (* Get rid of the SUC *) - sg ‘SUC (Num x) = 1 + Num x’ >-(rw [ADD]) >> rw [] >> - (* Massage a bit the goal *) - qsuff_tac ‘Num y = Num (y − 1) + Num 1’ >- COOPER_TAC >> - (* Apply the general theorem *) - irule NUM_SUB_EQ >> - COOPER_TAC -QED - -(* TODO: remove *) -Theorem NUM_SUB_1_EQ1: - !i. 0 <= i - 1 ==> Num i = SUC (Num (i-1)) -Proof - rpt strip_tac >> - (* 0 <= i *) - sg ‘0 <= i’ >- COOPER_TAC >> - (* Get rid of the SUC *) - sg ‘SUC (Num (i - 1)) = 1 + Num (i - 1)’ >-(rw [ADD]) >> - rw [] >> - (* Convert to integers*) - irule INT_OF_NUM_INJ >> - imp_res_tac (GSYM INT_OF_NUM) >> - (* Associativity of & *) - PURE_REWRITE_TAC [GSYM INT_ADD] >> - fs [] -QED - -(* TODO: - - list all the integer variables, and insert bounds in the assumptions - - replace u32_min by 0? - - i - 1 - - auto lookup of spec lemmas -*) - -(* Add a list of theorems in the assumptions - TODO: move *) -fun ASSUME_TACL (thms : thm list) : tactic = - let - (* TODO: use MAP_EVERY *) - fun t thms = - case thms of - [] => ALL_TAC - | thm :: thms => ASSUME_TAC thm >> t thms - in - t thms - end - -(* The map from integer type to bounds lemmas *) -val integer_bounds_lemmas = - Redblackmap.fromList String.compare - [ - ("u32", u32_to_int_bounds), - ("i32", i32_to_int_bounds) - ] - -(* The map from integer type to conversion lemmas *) -val integer_conversion_lemmas = - Redblackmap.fromList String.compare - [ - ("u32", int_to_u32_id), - ("i32", int_to_i32_id) - ] - -val integer_conversion_lemmas_list = - map snd (Redblackmap.listItems integer_conversion_lemmas) - -(* Not sure how term nets work, nor how we are supposed to convert Term.term - to mlibTerm.term. - - TODO: it seems we need to explore the term and convert everything to strings. - *) -fun term_to_mlib_term (t : term) : mlibTerm.term = - mlibTerm.string_to_term (term_to_string t) - -(* -(* The lhs of the conclusion of the integer conversion lemmas - we use this for - pattern matching *) -val integer_conversion_lhs_concls = - let - val thms = map snd (Redblackmap.listItems integer_conversion_lemmas); - val concls = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms; - in concls end -*) - -(* -val integer_conversion_concls_net = - let - val maplets = map (fn x => fst (dest_eq x) |-> ()) integer_conversion_concls; - - val maplets = map (fn x => fst (mlibTerm.dest_eq x) |-> ()) integer_conversion_concls; - val maplets = map (fn x => fst (mlibThm.dest_unit_eq x) |-> ()) integer_conversion_concls; - val parameters = { fifo=false }; - in mlibTermnet.from_maplets parameters maplets end - -mlibTerm.string_to_term (term_to_string “u32_to_int (int_to_u32 n) = n”) -term_to_quote - -SIMP_CONV -mlibThm.dest_thm u32_to_int_bounds -mlibThm.dest_unit u32_to_int_bounds -*) - -(* The integer types *) -val integer_types_names = - Redblackset.fromList String.compare - (map fst (Redblackmap.listItems integer_bounds_lemmas)) - -val all_integer_bounds = [ - u32_max_def, - i32_min_def, - i32_max_def -] - -(* Small utility: compute the set of assumptions in the context. - - We isolate this code in a utility in order to be able to improve it: - for now we simply put all the assumptions in a set, but in the future - we might want to split the assumptions which are conjunctions in order - to be more precise. - *) -fun compute_asms_set ((asms,g) : goal) : term Redblackset.set = - Redblackset.fromList Term.compare asms - -(* See {!assume_bounds_for_all_int_vars}. - - This tactic is in charge of adding assumptions for one variable. - *) - -fun assume_bounds_for_int_var - (asms_set: term Redblackset.set) (var : string) (ty : string) : - tactic = - let - (* Lookup the lemma to apply *) - val lemma = Redblackmap.find (integer_bounds_lemmas, ty); - (* Instantiate the lemma *) - val ty_t = mk_type (ty, []); - val var_t = mk_var (var, ty_t); - val lemma = SPEC var_t lemma; - (* Split the theorem into a list of conjuncts. - - The bounds are typically a conjunction: - {[ - ⊢ 0 ≤ u32_to_int x ∧ u32_to_int x ≤ u32_max: thm - ]} - *) - val lemmas = CONJUNCTS lemma; - (* Filter the conjuncts: some of them might already be in the context, - we don't want to introduce them again, as it would pollute it. - *) - val lemmas = filter (fn lem => not (Redblackset.member (asms_set, concl lem))) lemmas; - in - (* Introduce the assumptions in the context *) - ASSUME_TACL lemmas - end - -(* Destruct if possible a term of the shape: [x y], - where [x] is not a comb. - - Returns [(x, y)] - *) -fun dest_single_comb (t : term) : (term * term) option = - case strip_comb t of - (x, [y]) => SOME (x, y) - | _ => NONE - -(** Destruct if possible a term of the shape: [x (y z)]. - Returns [(x, y, z)] - *) -fun dest_single_comb_twice (t : term) : (term * term * term) option = - case dest_single_comb t of - NONE => NONE - | SOME (x, y) => - case dest_single_comb y of - NONE => NONE - | SOME (y, z) => SOME (x, y, z) - -(* A utility map to lookup integer conversion lemmas *) -val integer_conversion_pat_map = - let - val thms = map snd (Redblackmap.listItems integer_conversion_lemmas); - val tl = map (lhs o concl o UNDISCH_ALL o SPEC_ALL) thms; - val tl = map (valOf o dest_single_comb_twice) tl; - val tl = map (fn (x, y, _) => (x, y)) tl; - val m = Redblackmap.fromList Term.compare tl - in m end - -(* Introduce bound assumptions for all the machine integers in the context. - - Exemple: - ======== - If there is “x : u32” in the input set, then we introduce: - {[ - 0 <= u32_to_int x - u32_to_int x <= u32_max - ]} - *) -fun assume_bounds_for_all_int_vars (asms, g) = - let - (* Compute the set of integer variables in the context *) - val vars = free_varsl (g :: asms); - (* Compute the set of assumptions already present in the context *) - val asms_set = compute_asms_set (asms, g); - (* Filter the variables to keep only the ones with type machine integer, - decompose the types at the same time *) - fun decompose_var (v : term) : (string * string) = - let - val (v, ty) = dest_var v; - val {Args=args, Thy=thy, Tyop=ty} = dest_thy_type ty; - val _ = assert null args; - val _ = assert (fn thy => thy = primitives_theory_name) thy; - val _ = assert (fn ty => Redblackset.member (integer_types_names, ty)) ty; - in (v, ty) end; - val vars = mapfilter decompose_var vars; - (* Add assumptions for one variable *) - fun add_var_asm (v, ty) : tactic = - assume_bounds_for_int_var asms_set v ty; - (* Add assumptions for all the variables *) - (* TODO: use MAP_EVERY *) - fun add_vars_asm vl : tactic = - case vl of - [] => ALL_TAC - | v :: vl => - add_var_asm v >> add_vars_asm vl; - in - add_vars_asm vars (asms, g) - end - -(* -dest_thy_type “:u32” -val massage : tactic = assume_bounds_for_all_int_vars -val vl = vars -val (v::vl) = vl -*) - -(* -val (asms, g) = top_goal () -fun bounds_for_ints_in_list (vars : (string * hol_type) list) : tactic = - foldl - FAIL_TAC "" -val var = "x" -val ty = "u32" - -val asms_set = Redblackset.fromList Term.compare asms; - -val x = “1: int” -val ty = "u32" - -val thm = lemma -*) - -(* Given a theorem of the shape: - {[ - A0, ..., An ⊢ B0 ==> ... ==> Bm ==> concl - ]} - - Rewrite it so that it has the shape: - {[ - ⊢ (A0 /\ ... /\ An /\ B0 /\ ... /\ Bm) ==> concl - ]} - *) -fun thm_to_conj_implies (thm : thm) : thm = - let - (* Discharge all the assumptions *) - val thm = DISCH_ALL thm; - (* Rewrite the implications as one conjunction *) - val thm = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] thm; - in thm end - - -(* Like THEN1 and >-, but doesn't fail if the first subgoal is not completely - solved. - - TODO: how to get the notation right? - *) -fun op PARTIAL_THEN1 (tac1: tactic) (tac2: tactic) : tactic = tac1 THEN_LT (NTH_GOAL tac2 1) - -(* If the current goal is [asms ⊢ g], and given a lemma of the form - [⊢ H ==> C], do the following: - - introduce [asms ⊢ H] as a subgoal and apply the given tactic on it - - also calls the theorem tactic with the theorem [asms ⊢ C] - - If the lemma is not an implication, we directly call the theorem tactic. - *) -fun sg_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = - let - val c = concl thm; - (* First case: there is a premise to prove *) - fun prove_premise_then (h : term) = - PARTIAL_THEN1 (SUBGOAL_THEN h (fn h_thm => then_tac (MP thm h_thm))) premise_tac; - (* Second case: no premise to prove *) - val no_prove_premise_then = then_tac thm; - in - if is_imp c then prove_premise_then (fst (dest_imp c)) else no_prove_premise_then - end - -(* Same as {!sg_premise_then} but fails if the premise_tac fails to prove the premise *) -fun prove_premise_then (premise_tac: tactic) (then_tac: thm_tactic) (thm : thm) : tactic = - sg_premise_then - (premise_tac >> FAIL_TAC "prove_premise_then: could not prove premise") - then_tac thm - -(* -val thm = th -*) - -(* Call a function on all the subterms of a term *) -fun dep_apply_in_subterms - (f : string Redblackset.set -> term -> unit) - (bound_vars : string Redblackset.set) - (t : term) : unit = - let - val dep = dep_apply_in_subterms f; - val _ = f bound_vars t; - in - case dest_term t of - VAR (name, ty) => () - | CONST {Name=name, Thy=thy, Ty=ty} => () - | COMB (app, arg) => - let - val _ = dep bound_vars app; - val _ = dep bound_vars arg; - in () end - | LAMB (bvar, body) => - let - val (varname, ty) = dest_var bvar; - val bound_vars = Redblackset.add (bound_vars, varname); - val _ = dep bound_vars body; - in () end - end - -(* Return the set of free variables appearing in the residues of a term substitution *) -fun free_vars_in_subst_residue (s: (term, term) Term.subst) : string Redblackset.set = - let - val free_vars = free_varsl (map (fn {redex=_, residue=x} => x) s); - val free_vars = map (fst o dest_var) free_vars; - val free_vars = Redblackset.fromList String.compare free_vars; - in free_vars end - -(* Attempt to instantiate a rewrite theorem. - - Remark: this theorem should be of the form: - H ⊢ x = y - - (without quantified variables). - - **REMARK**: the function raises a HOL_ERR exception if it fails. - - [forbid_vars]: forbid substituting with those vars (typically because - we are maching in a subterm under lambdas, and some of those variables - are bounds in the outer lambdas). -*) -fun inst_match_concl (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm = - let - (* Retrieve the lhs of the conclusion of the theorem *) - val l = lhs (concl th); - (* Match this lhs with the term *) - val (var_s, ty_s) = match_term l t; - (* Check that we are allowed to perform the substitution *) - val free_vars = free_vars_in_subst_residue var_s; - val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars)); - in - (* Perform the substitution *) - INST var_s (INST_TYPE ty_s th) - end - -(* -val forbid_vars = Redblackset.empty String.compare -val t = “u32_to_int (int_to_u32 x)” -val t = “u32_to_int (int_to_u32 3)” -val th = (UNDISCH_ALL o SPEC_ALL) int_to_u32_id -*) - -(* Attempt to instantiate a theorem by matching its first premise. - - Note that we make the hypothesis tha all the free variables which need - to be instantiated appear in the first premise, of course (the caller should - enforce this). - - Remark: this theorem should be of the form: - ⊢ H0 ==> ... ==> Hn ==> H - - (without quantified variables). - - **REMARK**: the function raises a HOL_ERR exception if it fails. - - [forbid_vars]: see [inst_match_concl] -*) -fun inst_match_first_premise - (forbid_vars : string Redblackset.set) (th : thm) (t : term) : thm = - let - (* Retrieve the first premise *) - val l = (fst o dest_imp o concl) th; - (* Match this with the term *) - val (var_s, ty_s) = match_term l t; - (* Check that we are allowed to perform the substitution *) - val free_vars = free_vars_in_subst_residue var_s; - val _ = assert Redblackset.isEmpty (Redblackset.intersection (free_vars, forbid_vars)); - in - (* Perform the substitution *) - INST var_s (INST_TYPE ty_s th) - end - -(* -val forbid_vars = Redblackset.empty String.compare -val t = “u32_to_int z = u32_to_int i − 1” -val th = SPEC_ALL NUM_SUB_1_EQ -*) - -(* Call a matching function on all the subterms in the provided list of term. - This is a generic function. - - [try_match] should return an instantiated theorem, as well as a term which - identifies this theorem (the lhs of the equality, if this is a rewriting - theorem for instance - we use this to check for collisions, and discard - redundant instantiations). - *) -fun inst_match_in_terms - (try_match: string Redblackset.set -> term -> term * thm) - (tl : term list) : thm list = - let - (* We use a map when storing the theorems, to avoid storing the same theorem twice *) - val inst_thms: (term, thm) Redblackmap.dict ref = ref (Redblackmap.mkDict Term.compare); - fun try_instantiate bvars t = - let - val (inst_th_tm, inst_th) = try_match bvars t; - in - inst_thms := Redblackmap.insert (!inst_thms, inst_th_tm, inst_th) - end - handle HOL_ERR _ => (); - (* Explore the term *) - val _ = app (dep_apply_in_subterms try_instantiate (Redblackset.empty String.compare)) tl; - in - map snd (Redblackmap.listItems (!inst_thms)) - end - -(* Given a rewriting theorem [th] which has premises, return all the - instantiations of this theorem which make its conclusion match subterms - in the provided list of term. - *) -fun inst_match_concl_in_terms (th : thm) (tl : term list) : thm list = - let - val th = (UNDISCH_ALL o SPEC_ALL) th; - fun try_match bvars t = - let - val inst_th = inst_match_concl bvars th t; - in - (lhs (concl inst_th), inst_th) - end; - in - inst_match_in_terms try_match tl - end - -(* -val t = “!x. u32_to_int (int_to_u32 x) = u32_to_int (int_to_u32 y)” -val th = int_to_u32_id - -val thms = inst_match_concl_in_terms int_to_u32_id [t] -*) - - -(* Given a theorem [th] which has premises, return all the - instantiations of this theorem which make its first premise match subterms - in the provided list of term. - *) -fun inst_match_first_premise_in_terms (th : thm) (tl : term list) : thm list = - let - val th = SPEC_ALL th; - fun try_match bvars t = - let - val inst_th = inst_match_first_premise bvars th t; - in - ((fst o dest_imp o concl) inst_th, inst_th) - end; - in - inst_match_in_terms try_match tl - end - -(* -val t = “x = y - 1 ==> T” -val th = SPEC_ALL NUM_SUB_1_EQ - -val thms = inst_match_first_premise_in_terms th [t] -*) - -(* Attempt to apply dependent rewrites with a theorem by matching its - conclusion with subterms of the goal. - *) -fun apply_dep_rewrites_match_concl_tac - (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic = - fn (asms, g) => - let - (* Discharge the assumptions so that the goal is one single term *) - val thms = inst_match_concl_in_terms th (g :: asms); - val thms = map thm_to_conj_implies thms; - in - (* Apply each theorem *) - MAP_EVERY (prove_premise_then prove_premise then_tac) thms (asms, g) - end - -(* -val (asms, g) = ([ - “u32_to_int z = u32_to_int i − u32_to_int (int_to_u32 1)”, - “u32_to_int (int_to_u32 2) = 2” -], “T”) - -apply_dep_rewrites_match_concl_tac - (FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC) - (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]) - int_to_u32_id -*) - -(* Attempt to apply dependent rewrites with a theorem by matching its - first premise with subterms of the goal. - *) -fun apply_dep_rewrites_match_first_premise_tac - (prove_premise : tactic) (then_tac : thm_tactic) (th : thm) : tactic = - fn (asms, g) => - let - (* Discharge the assumptions so that the goal is one single term *) - val thms = inst_match_first_premise_in_terms th (g :: asms); - val thms = map thm_to_conj_implies thms; - fun apply_tac th = - let - val th = thm_to_conj_implies th; - in - prove_premise_then prove_premise then_tac th - end; - in - (* Apply each theorem *) - MAP_EVERY apply_tac thms (asms, g) - end - -(* See {!rewrite_all_int_conversion_ids}. - - Small utility which takes care of one rewriting. - - TODO: we actually don't use it. REMOVE? - *) -fun rewrite_int_conversion_id - (asms_set: term Redblackset.set) (x : term) (ty : string) : - tactic = - let - (* Lookup the theorem *) - val lemma = Redblackmap.find (integer_conversion_lemmas, ty); - (* Instantiate *) - val lemma = SPEC x lemma; - (* Rewrite the lemma. The lemma typically has the shape: - ⊢ u32_min <= x /\ x <= u32_max ==> u32_to_int (int_to_u32 x) = x - - Make sure the lemma has the proper shape, attempt to prove the premise, - then use the conclusion if it succeeds. - *) - val lemma = thm_to_conj_implies lemma; - (* Retrieve the conclusion of the lemma - we do this to check if it is not - already in the assumptions *) - val c = concl (UNDISCH_ALL lemma); - val already_in_asms = Redblackset.member (asms_set, c); - (* Small utility: the tactic to prove the premise *) - val prove_premise = - (* We might need to unfold the bound definitions, in particular if the - term is a constant (e.g., “3:int”) *) - FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> - COOPER_TAC; - (* Rewrite with a lemma, then assume it *) - fun rewrite_then_assum (thm : thm) : tactic = - FULL_SIMP_TAC simpLib.empty_ss [thm] >> assume_tac thm; - in - (* If the conclusion is not already in the assumptions, prove it, use - it to rewrite the goal and add it in the assumptions, otherwise do nothing *) - if already_in_asms then ALL_TAC - else prove_premise_then prove_premise rewrite_then_assum lemma - end - -(* Look for conversions from integers to machine integers and back. - {[ - u32_to_int (int_to_u32 x) - ]} - - Attempts to prove and apply equalities of the form: - {[ - u32_to_int (int_to_u32 x) = x - ]} - - **REMARK**: this function can fail, if it doesn't manage to prove the - premises of the theorem to apply. - - TODO: update - *) -val rewrite_with_dep_int_lemmas : tactic = - (* We're not trying to be smart: we just try to rewrite with each theorem at - a time *) - let - val prove_premise = FULL_SIMP_TAC simpLib.empty_ss all_integer_bounds >> COOPER_TAC; - val then_tac1 = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]); - val rewr_tac1 = apply_dep_rewrites_match_concl_tac prove_premise then_tac1; - val then_tac2 = (fn th => FULL_SIMP_TAC simpLib.empty_ss [th]); - val rewr_tac2 = apply_dep_rewrites_match_first_premise_tac prove_premise then_tac2; - in - MAP_EVERY rewr_tac1 integer_conversion_lemmas_list >> - MAP_EVERY rewr_tac2 [NUM_SUB_1_EQ] - end - -(* -apply_dep_rewrites_match_first_premise_tac prove_premise then_tac NUM_SUB_1_EQ - -sg ‘u32_to_int z = u32_to_int i − 1 /\ 0 ≤ u32_to_int z’ >- prove_premise - -prove_premise_then prove_premise - -val thm = thm_to_conj_implies (SPECL [“u32_to_int z”, “u32_to_int i”] NUM_SUB_1_EQ) - -val h = “u32_to_int z = u32_to_int i − 1 ∧ 0 ≤ u32_to_int z” -*) - -(* Massage a bit the goal, for instance by introducing integer bounds in the - assumptions. -*) -val massage : tactic = - assume_bounds_for_all_int_vars >> - rewrite_with_dep_int_lemmas - -(* Lexicographic order over pairs *) -fun pair_compare (comp1 : 'a * 'a -> order) (comp2 : 'b * 'b -> order) - ((p1, p2) : (('a * 'b) * ('a * 'b))) : order = - let - val (x1, y1) = p1; - val (x2, y2) = p2; - in - case comp1 (x1, x2) of - LESS => LESS - | GREATER => GREATER - | EQUAL => comp2 (y1, y2) - end - -(* A constant name (theory, constant name) *) -type const_name = string * string - -val const_name_compare = pair_compare String.compare String.compare - -(* The registered spec theorems, that {!progress} will automatically apply. - - The keys are the function names (it is a pair, because constant names - are made of the theory name and the name of the constant itself). - - Also note that we can store several specs per definition (in practice, when - looking up specs, we will try them all one by one, in a LIFO order). - - We store theorems where all the premises are in the goal, with implications - (i.e.: [⊢ H0 ==> ... ==> Hn ==> H], not [H0, ..., Hn ⊢ H]). - - We do this because, when doing proofs by induction, {!progress} might have to - handle *unregistered* theorems coming the current goal assumptions and of the shape - (the conclusion of the theorem is an assumption, and we want to ignore this assumption): - {[ - [∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ - case nth ls i of - Return x => ... - | ... => ...] - ⊢ ∀i. u32_to_int i < &LENGTH (list_t_v ls) ⇒ - case nth ls i of - Return x => ... - | ... => ... - ]} - *) -val reg_spec_thms: (const_name, thm) Redblackmap.dict ref = - ref (Redblackmap.mkDict const_name_compare) - -(* Retrieve the specified application in a spec theorem. - - A spec theorem for a function [f] typically has the shape: - {[ - !x0 ... xn. - H0 ==> ... Hm ==> - (exists ... - (exists ... . f y0 ... yp = ... /\ ...) \/ - (exists ... . f y0 ... yp = ... /\ ...) \/ - ... - ]} - - Or: - {[ - !x0 ... xn. - H0 ==> ... Hm ==> - case f y0 ... yp of - ... => ... - | ... => ... - ]} - - We return: [f y0 ... yp] -*) -fun get_spec_app (t : term) : term = - let - (* Remove the universally quantified variables, the premises and - the existentially quantified variables *) - val t = (snd o strip_exists o snd o strip_imp o snd o strip_forall) t; - (* Remove the exists, take the first disjunct *) - val t = (hd o strip_disj o snd o strip_exists) t; - (* Split the conjunctions and take the first conjunct *) - val t = (hd o strip_conj) t; - (* Remove the case if there is, otherwise destruct the equality *) - val t = - if TypeBase.is_case t then let val (_, t, _) = TypeBase.dest_case t in t end - else (fst o dest_eq) t; - in t end - -(* Given a function call [f y0 ... yn] return the name of the function *) -fun get_fun_name_from_app (t : term) : const_name = - let - val f = (fst o strip_comb) t; - val {Name=name, Thy=thy, Ty=_} = dest_thy_const f; - val cn = (thy, name); - in cn end - -(* Register a spec theorem in the spec database. - - For the shape of spec theorems, see {!get_spec_thm_app}. - *) -fun register_spec_thm (th: thm) : unit = - let - (* Transform the theroem a bit before storing it *) - val th = SPEC_ALL th; - (* Retrieve the app ([f x0 ... xn]) *) - val f = get_spec_app (concl th); - (* Retrieve the function name *) - val cn = get_fun_name_from_app f; - in - (* Store *) - reg_spec_thms := Redblackmap.insert (!reg_spec_thms, cn, th) - end - -(* TODO: I32_SUB_EQ *) -val _ = app register_spec_thm [U32_ADD_EQ, U32_SUB_EQ, I32_ADD_EQ] - -(* -app register_spec_thm [U32_ADD_EQ, U32_SUB_EQ, I32_ADD_EQ] -Redblackmap.listItems (!reg_spec_thms) -*) - -(* -(* TODO: remove? *) -datatype monadic_app_kind = - Call | Bind | Case -*) - -(* Repeatedly destruct cases and return the last scrutinee we get *) -fun strip_all_cases_get_scrutinee (t : term) : term = - if TypeBase.is_case t - then (strip_all_cases_get_scrutinee o fst o TypeBase.strip_case) t - else t - -(* -TypeBase.dest_case “case ls of [] => T | _ => F” -TypeBase.strip_case “case ls of [] => T | _ => F” -TypeBase.strip_case “case (if b then [] else [0, 1]) of [] => T | _ => F” -TypeBase.strip_case “3” -TypeBase.dest_case “3” - -strip_all_cases_get_scrutinee “case ls of [] => T | _ => F” -strip_all_cases_get_scrutinee “case (if b then [] else [0, 1]) of [] => T | _ => F” -strip_all_cases_get_scrutinee “3” -*) - - -(* Provided the goal contains a call to a monadic function, return this function call. - - The goal should be of the shape: - 1. - {[ - case (* potentially expanded function body *) of - ... => ... - | ... => ... - ]} - - 2. Or: - {[ - exists ... . - ... (* potentially expanded function body *) = Return ... /\ - ... (* Various properties *) - ]} - - 3. Or a disjunction of cases like the one above, below existential binders - (actually: note sure this last case exists in practice): - {[ - exists ... . - (exists ... . (* body *) = Return ... /\ ...) \/ - ... - ]} - - The function body should be of the shape: - {[ - x <- f y0 ... yn; - ... - ]} - - Or (typically if we expanded the monadic binds): - {[ - case f y0 ... yn of - ... - ]} - - Or simply (typically if we reached the end of the function we're analyzing): - {[ - f y0 ... yn - ]} - - For all the above cases we would return [f y0 ... yn]. - *) -fun get_monadic_app_call (t : term) : term = - (* We do something slightly imprecise but hopefully general and robut *) - let - (* Case 3.: strip the existential binders, and take the first disjuntion *) - val t = (hd o strip_disj o snd o strip_exists) t; - (* Case 2.: strip the existential binders, and take the first conjunction *) - val t = (hd o strip_conj o snd o strip_exists) t; - (* If it is an equality, take the lhs *) - val t = if is_eq t then lhs t else t; - (* Expand the binders to transform them to cases *) - val t = - (rhs o concl) (REWRITE_CONV [st_ex_bind_def] t) - handle UNCHANGED => t; - (* Strip all the cases *) - val t = strip_all_cases_get_scrutinee t; - in t end - -(* Use the given theorem to progress by one step (we use this when - analyzing a function body: this goes forward by one call to a monadic function). - - We transform the goal by: - - pushing the theorem premises to a subgoal - - adding the theorem conclusion in the assumptions in another goal, and - getting rid of the monadic call - - Then [then_tac] receives as paramter the monadic call on which we applied - the lemma. This can be useful, for instance, to make a case disjunction. - - This function is the most primitive of the [progress...] functions. - *) -fun pure_progress_with (premise_tac : tactic) - (then_tac : term -> thm_tactic) (th : thm) : tactic = - fn (asms,g) => - let - (* Remove all the universally quantified variables from the theorem *) - val th = SPEC_ALL th; - (* Retrieve the monadic call from the goal *) - val fgoal = get_monadic_app_call g; - (* Retrieve the app call from the theroem *) - val gth = get_spec_app (concl th); - (* Match and instantiate *) - val (var_s, ty_s) = match_term gth fgoal; - (* Instantiate the theorem *) - val th = INST var_s (INST_TYPE ty_s th); - (* Retrieve the premises of the theorem *) - val th = PURE_REWRITE_RULE [GSYM satTheory.AND_IMP] th; - in - (* Apply the theorem *) - sg_premise_then premise_tac (then_tac fgoal) th (asms, g) - end - -(* -val (asms, g) = top_goal () -val t = g - -val th = U32_SUB_EQ - -val premise_tac = massage >> TRY COOPER_TAC -fun then_tac fgoal = - fn thm => ASSUME_TAC thm >> Cases_on ‘^fgoal’ >> - rw [] >> fs [st_ex_bind_def] >> massage >> fs [] - -pure_progress_with premise_tac then_tac th -*) - -fun progress_with (th : thm) : tactic = - let - val premise_tac = massage >> fs [] >> rw [] >> TRY COOPER_TAC; - fun then_tac fgoal thm = - ASSUME_TAC thm >> Cases_on ‘^fgoal’ >> - rw [] >> fs [st_ex_bind_def] >> massage >> fs []; - in - pure_progress_with premise_tac then_tac th - end - -(* -progress_with U32_SUB_EQ -*) - -(* This function lookups the theorem to use to make progress *) -val progress : tactic = - fn (asms, g) => - let - (* Retrieve the monadic call from the goal *) - val fgoal = get_monadic_app_call g; - val fname = get_fun_name_from_app fgoal; - (* Lookup the theorem: first look in the assumptions (we might want to - use the inductive hypothesis for instance) *) - fun asm_to_spec asm = - let - (* Fail if there are no universal quantifiers *) - val _ = - if is_forall asm then asm - else assert is_forall ((snd o strip_imp) asm); - val asm_fname = (get_fun_name_from_app o get_spec_app) asm; - (* Fail if the name is not the one we're looking for *) - val _ = assert (fn n => fname = n) asm_fname; - in - ASSUME asm - end - val asms_thl = mapfilter asm_to_spec asms; - (* Lookup a spec in the database *) - val thl = - case Redblackmap.peek (!reg_spec_thms, fname) of - NONE => asms_thl - | SOME spec => spec :: asms_thl; - val _ = - if null thl then - raise (failwith "progress: could not find a suitable theorem to apply") - else (); - in - (* Attempt to use the theorems one by one *) - MAP_FIRST progress_with thl (asms, g) - end - -(* -val (asms, g) = top_goal () -*) - -(* TODO: no exfalso tactic?? *) -val EX_FALSO : tactic = - SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[]) - -Theorem nth_lem: - !(ls : 't list_t) (i : u32). - u32_to_int i < int_of_num (LENGTH (list_t_v ls)) ==> - case nth ls i of - | Return x => x = EL (Num (u32_to_int i)) (list_t_v ls) - | Fail _ => F - | Loop => F -Proof - Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] - >-(massage >> EX_FALSO >> COOPER_TAC) >> - PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >> - progress >> progress -QED - -(* Example from the hashmap *) -val _ = new_constant ("insert", “: u32 -> 't -> (u32 # 't) list_t -> (u32 # 't) list_t result”) -val insert_def = new_axiom ("insert_def", “ - insert (key : u32) (value : 't) (ls : (u32 # 't) list_t) : (u32 # 't) list_t result = - case ls of - | ListCons (ckey, cvalue) tl => - if ckey = key - then Return (ListCons (ckey, value) tl) - else - do - tl0 <- insert key value tl; - Return (ListCons (ckey, cvalue) tl0) - od - | ListNil => Return (ListCons (key, value) ListNil) - ”) - -(* Property that keys are pairwise distinct *) -val distinct_keys_def = Define ‘ - distinct_keys (ls : (u32 # 't) list) = - !i j. - i < LENGTH ls ==> - j < LENGTH ls ==> - FST (EL i ls) = FST (EL j ls) ==> - i = j -’ - -val lookup_raw_def = Define ‘ - lookup_raw key [] = NONE /\ - lookup_raw key ((k, v) :: ls) = - if k = key then SOME v else lookup_raw key ls -’ - -val lookup_def = Define ‘ - lookup key ls = lookup_raw key (list_t_v ls) -’ - -Theorem insert_lem: - !ls key value. - (* The keys are pairwise distinct *) - distinct_keys (list_t_v ls) ==> - case insert key value ls of - | Return ls1 => - (* We updated the binding *) - lookup key ls1 = SOME value /\ - (* The other bindings are left unchanged *) - (!k. k <> key ==> lookup k ls = lookup k ls1) - | Fail _ => F - | Loop => F -Proof - Induct_on ‘ls’ >> rw [list_t_v_def] >~ [‘ListNil’] >> - PURE_ONCE_REWRITE_TAC [insert_def] >> rw [] - >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) - >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >> - CASE_TAC >> rw [] - >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) - >- (rw [lookup_def, lookup_raw_def, list_t_v_def]) >> - progress - >- ( - fs [distinct_keys_def] >> - rpt strip_tac >> - first_assum (qspecl_then [‘SUC i’, ‘SUC j’] ASSUME_TAC) >> - fs [] - (* Alternative: *) - (* - PURE_ONCE_REWRITE_TAC [GSYM prim_recTheory.INV_SUC_EQ] >> - first_assum irule >> fs [] - *)) >> - fs [lookup_def, lookup_raw_def, list_t_v_def] -QED - -(*** - * Example of how to get rid of the fuel in practice - *) -val nth_fuel_def = Define ‘ - nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result = - case n of - | 0 => Loop - | SUC n => - do case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth_fuel n tl i0 - od - | ListNil => - Fail Failure - od - ’ - -val is_loop_def = Define ‘is_loop r = case r of Loop => T | _ => F’ - -val nth_fuel_P_def = Define ‘ - nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i) -’ - -(* TODO: this is not the theorem we want: we want the one below *) -Theorem nth_fuel_mono: - !n m ls i. - n <= m ==> - if is_loop (nth_fuel n ls i) then T - else nth_fuel n ls i = nth_fuel m ls i -Proof - Induct_on ‘n’ >- ( - rpt gen_tac >> - DISCH_TAC >> - PURE_ONCE_REWRITE_TAC [nth_fuel_def] >> - rw[is_loop_def] - ) >> - (* Interesting case *) - rpt gen_tac >> - DISCH_TAC >> - CASE_TAC >> - Cases_on ‘m’ >- ( - (* Contradiction: SUC n < 0 *) - sg ‘SUC n = 0’ >- decide_tac >> - fs [is_loop_def] - ) >> - fs [is_loop_def] >> - pop_assum mp_tac >> - PURE_ONCE_REWRITE_TAC [nth_fuel_def] >> - fs [] >> - DISCH_TAC >> - (* We just have to explore all the paths: we can have dedicated tactics for that - (we need to do case analysis) *) - Cases_on ‘ls’ >> fs [] >> - Cases_on ‘u32_to_int (i :u32) = (0 :int)’ >> fs [] >> - fs [st_ex_bind_def] >> - Cases_on ‘u32_sub (i :u32) (int_to_u32 (1 :int))’ >> fs [] >> - (* Apply the induction hypothesis *) - first_x_assum (qspecl_then [‘n'’, ‘l’, ‘a’] assume_tac) >> - first_x_assum imp_res_tac >> - pop_assum mp_tac >> - CASE_TAC -QED - -Theorem nth_fuel_P_mono: - !n m ls i. - n <= m ==> - nth_fuel_P ls i n ==> - nth_fuel n ls i = nth_fuel m ls i -Proof - rpt gen_tac >> rpt DISCH_TAC >> - fs [nth_fuel_P_def] >> - imp_res_tac nth_fuel_mono >> - pop_assum (qspecl_then [‘ls’, ‘i’] assume_tac) >> - pop_assum mp_tac >> CASE_TAC >> fs [] -QED - -(*Theorem nth_fuel_least_fail_mono: - !n ls i. - n < $LEAST (nth_fuel_P ls i) ==> - nth_fuel n ls i = Loop -Proof - rpt gen_tac >> - disch_tac >> - imp_res_tac whileTheory.LESS_LEAST >> - fs [nth_fuel_P_def, is_loop_def] >> - pop_assum mp_tac >> - CASE_TAC -QED*) - -Theorem nth_fuel_least_success_mono: - !n ls i. - $LEAST (nth_fuel_P ls i) <= n ==> - nth_fuel n ls i = nth_fuel ($LEAST (nth_fuel_P ls i)) ls i -Proof - rpt gen_tac >> - disch_tac >> - (* Case disjunction on whether there exists a fuel such that it terminates *) - Cases_on ‘?m. nth_fuel_P ls i m’ >- ( - (* Terminates *) - irule EQ_SYM >> - irule nth_fuel_P_mono >> fs [] >> - (* Prove that calling with the least upper bound of fuel succeeds *) - qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP - ) >> - (* Doesn't terminate *) - fs [] >> - sg ‘~(nth_fuel_P ls i n)’ >- fs [] >> - sg ‘~(nth_fuel_P ls i ($LEAST (nth_fuel_P ls i)))’ >- fs [] >> - fs [nth_fuel_P_def, is_loop_def] >> - pop_assum mp_tac >> CASE_TAC >> - pop_assum mp_tac >> - pop_assum mp_tac >> CASE_TAC -QED - -val nth_def_raw = Define ‘ - nth ls i = - if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i - else Loop -’ - -(* This makes the proofs easier, in that it helps us control the context *) -val nth_expand_def = Define ‘ - nth_expand nth ls i = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth tl i0 - od - | ListNil => - Fail Failure -’ - -(* Prove the important theorems: termination case *) -Theorem nth_def_terminates: - !ls i. - (?n. nth_fuel_P ls i n) ==> - nth ls i = - nth_expand nth ls i -Proof - rpt strip_tac >> - fs [nth_expand_def] >> - PURE_ONCE_REWRITE_TAC [nth_def_raw] >> - (* Prove that the least upper bound is <= n *) - sg ‘$LEAST (nth_fuel_P ls i) <= n’ >-( - qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >> - spose_not_then assume_tac >> fs [] - ) >> - (* Use the monotonicity theorem - TODO: ? *) - imp_res_tac nth_fuel_least_success_mono >> - (* Rewrite only on the left - TODO: easy way ?? *) - qspecl_then [‘$LEAST (nth_fuel_P ls i)’, ‘ls’, ‘i’] assume_tac nth_fuel_def >> - (* TODO: how to discard assumptions?? *) - fs [] >> pop_assum (fn _ => fs []) >> - (* Cases on the least upper bound *) - Cases_on ‘$LEAST (nth_fuel_P ls i)’ >> rw [] >- ( - (* The bound is equal to 0: contradiction *) - sg ‘nth_fuel 0 ls i = Loop’ >- (PURE_ONCE_REWRITE_TAC [nth_fuel_def] >> rw []) >> - fs [nth_fuel_P_def, is_loop_def] - ) >> - (* Bound not equal to 0 *) - fs [nth_fuel_P_def, is_loop_def] >> - (* Explore all the paths *) - fs [st_ex_bind_def] >> - Cases_on ‘ls’ >> rw [] >> fs [] >> - Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >> - (* Recursive call: use monotonicity - we have an assumption which eliminates the Loop case *) - Cases_on ‘nth_fuel n' l a’ >> rw [] >> fs [] >> - (sg ‘nth_fuel_P l a n'’ >- fs [nth_fuel_P_def, is_loop_def]) >> - (sg ‘$LEAST (nth_fuel_P l a) <= n'’ >-( - qspec_then ‘nth_fuel_P l a’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >> - spose_not_then assume_tac >> fs [])) >> - imp_res_tac nth_fuel_least_success_mono >> fs [] -QED - -(* Prove the important theorems: divergence case *) -Theorem nth_def_loop: - !ls i. - (!n. ~nth_fuel_P ls i n) ==> - nth ls i = - nth_expand nth ls i -Proof - rpt gen_tac >> - PURE_ONCE_REWRITE_TAC [nth_def_raw] >> - strip_tac >> rw[] >> - (* Non-terminating case *) - sg ‘∀n. ¬nth_fuel_P ls i (SUC n)’ >- rw [] >> - fs [nth_fuel_P_def, is_loop_def] >> - pop_assum mp_tac >> - PURE_ONCE_REWRITE_TAC [nth_fuel_def] >> - rw [] >> - fs [nth_expand_def] >> - (* Evaluate all the paths *) - fs [st_ex_bind_def] >> - Cases_on ‘ls’ >> rw [] >> fs [] >> - Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >> - (* Use the definition of nth *) - rw [nth_def_raw] >> - first_x_assum (qspec_then ‘$LEAST (nth_fuel_P l a)’ assume_tac) >> - Cases_on ‘nth_fuel ($LEAST (nth_fuel_P l a)) l a’ >> fs [] -QED - -(* The final theorem *) -Theorem nth_def: - !ls i. - nth ls i = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth tl i0 - od - | ListNil => - Fail Failure -Proof - rpt strip_tac >> - Cases_on ‘?n. nth_fuel_P ls i n’ >-( - assume_tac nth_def_terminates >> - fs [nth_expand_def] >> - pop_assum irule >> - metis_tac []) >> - fs [] >> imp_res_tac nth_def_loop >> fs [nth_expand_def] -QED - -(* - -Je viens de finir ma petite expérimentation avec le fuel : ça marche bien. Par exemple, si je pose les définitions suivantes : -Datatype: - result = Return 'a | Fail error | Loop -End - -(* Omitting some definitions like the bind *) - -val _ = Define ‘ - nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result = - case n of - | 0 => Loop - | SUC n => - do case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth_fuel n tl i0 - od - | ListNil => - Fail Failure - od - ’ - -val _ = Define 'is_loop r = case r of Loop => T | _ => F' - -val _ = Define 'nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)' - -(* $LEAST returns the least upper bound for a predicate (if it exists - otherwise it returns an arbitrary number) *) -val _ = Define ‘ - nth ls i = - if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i - else Loop -’ -J'arrive à montrer (c'est un chouïa technique) : -Theorem nth_def: - !ls i. - nth ls i = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth tl i0 - od - | ListNil => - Fail Failure - -*) - -val _ = export_theory () diff --git a/backends/hol4/testTheory.sig b/backends/hol4/testTheory.sig deleted file mode 100644 index 21b74a39..00000000 --- a/backends/hol4/testTheory.sig +++ /dev/null @@ -1,834 +0,0 @@ -signature testTheory = -sig - type thm = Thm.thm - - (* Axioms *) - val VEC_TO_LIST_BOUNDS : thm - val i32_to_int_bounds : thm - val insert_def : thm - val int_to_i32_id : thm - val int_to_u32_id : thm - val u32_to_int_bounds : thm - - (* Definitions *) - val distinct_keys_def : thm - val error_BIJ : thm - val error_CASE : thm - val error_TY_DEF : thm - val error_size_def : thm - val i32_add_def : thm - val i32_max_def : thm - val i32_min_def : thm - val int1_def : thm - val int2_def : thm - val is_loop_def : thm - val is_true_def : thm - val list_t_TY_DEF : thm - val list_t_case_def : thm - val list_t_size_def : thm - val list_t_v_def : thm - val lookup_def : thm - val mk_i32_def : thm - val mk_u32_def : thm - val nth_expand_def : thm - val nth_fuel_P_def : thm - val result_TY_DEF : thm - val result_case_def : thm - val result_size_def : thm - val st_ex_bind_def : thm - val st_ex_return_def : thm - val test1_def : thm - val test2_TY_DEF : thm - val test2_case_def : thm - val test2_size_def : thm - val test_TY_DEF : thm - val test_case_def : thm - val test_monad2_def : thm - val test_monad3_def : thm - val test_monad_def : thm - val test_size_def : thm - val u32_add_def : thm - val u32_max_def : thm - val u32_sub_def : thm - val usize_max_def : thm - val vec_len_def : thm - - (* Theorems *) - val I32_ADD_EQ : thm - val INT_OF_NUM_INJ : thm - val INT_THM1 : thm - val INT_THM2 : thm - val MK_I32_SUCCESS : thm - val MK_U32_SUCCESS : thm - val NAT_THM1 : thm - val NAT_THM2 : thm - val NUM_SUB_1_EQ : thm - val NUM_SUB_1_EQ1 : thm - val NUM_SUB_EQ : thm - val U32_ADD_EQ : thm - val U32_SUB_EQ : thm - val VEC_TO_LIST_INT_BOUNDS : thm - val datatype_error : thm - val datatype_list_t : thm - val datatype_result : thm - val datatype_test : thm - val datatype_test2 : thm - val error2num_11 : thm - val error2num_ONTO : thm - val error2num_num2error : thm - val error2num_thm : thm - val error_Axiom : thm - val error_EQ_error : thm - val error_case_cong : thm - val error_case_def : thm - val error_case_eq : thm - val error_induction : thm - val error_nchotomy : thm - val insert_lem : thm - val list_nth_mut_loop_loop_fwd_def : thm - val list_nth_mut_loop_loop_fwd_ind : thm - val list_t_11 : thm - val list_t_Axiom : thm - val list_t_case_cong : thm - val list_t_case_eq : thm - val list_t_distinct : thm - val list_t_induction : thm - val list_t_nchotomy : thm - val lookup_raw_def : thm - val lookup_raw_ind : thm - val nth_def : thm - val nth_def_loop : thm - val nth_def_terminates : thm - val nth_fuel_P_mono : thm - val nth_fuel_def : thm - val nth_fuel_ind : thm - val nth_fuel_least_success_mono : thm - val nth_fuel_mono : thm - val num2error_11 : thm - val num2error_ONTO : thm - val num2error_error2num : thm - val num2error_thm : thm - val result_11 : thm - val result_Axiom : thm - val result_case_cong : thm - val result_case_eq : thm - val result_distinct : thm - val result_induction : thm - val result_nchotomy : thm - val test2_11 : thm - val test2_Axiom : thm - val test2_case_cong : thm - val test2_case_eq : thm - val test2_distinct : thm - val test2_induction : thm - val test2_nchotomy : thm - val test_11 : thm - val test_Axiom : thm - val test_case_cong : thm - val test_case_eq : thm - val test_distinct : thm - val test_induction : thm - val test_nchotomy : thm - - val test_grammars : type_grammar.grammar * term_grammar.grammar -(* - [Omega] Parent theory of "test" - - [int_arith] Parent theory of "test" - - [words] Parent theory of "test" - - [insert_def] Axiom - - [oracles: ] [axioms: insert_def] [] - ⊢ insert key value ls = - case ls of - ListCons (ckey,cvalue) tl => - if ckey = key then Return (ListCons (ckey,value) tl) - else - do - tl0 <- insert key value tl; - Return (ListCons (ckey,cvalue) tl0) - od - | ListNil => Return (ListCons (key,value) ListNil) - - [u32_to_int_bounds] Axiom - - [oracles: ] [axioms: u32_to_int_bounds] [] - ⊢ ∀n. 0 ≤ u32_to_int n ∧ u32_to_int n ≤ u32_max - - [i32_to_int_bounds] Axiom - - [oracles: ] [axioms: i32_to_int_bounds] [] - ⊢ ∀n. i32_min ≤ i32_to_int n ∧ i32_to_int n ≤ i32_max - - [int_to_u32_id] Axiom - - [oracles: ] [axioms: int_to_u32_id] [] - ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ u32_to_int (int_to_u32 n) = n - - [int_to_i32_id] Axiom - - [oracles: ] [axioms: int_to_i32_id] [] - ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ i32_to_int (int_to_i32 n) = n - - [VEC_TO_LIST_BOUNDS] Axiom - - [oracles: ] [axioms: VEC_TO_LIST_BOUNDS] [] - ⊢ ∀v. (let l = LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ 4294967295) - - [distinct_keys_def] Definition - - ⊢ ∀ls. - distinct_keys ls ⇔ - ∀i j. - i < LENGTH ls ⇒ - j < LENGTH ls ⇒ - FST (EL i ls) = FST (EL j ls) ⇒ - i = j - - [error_BIJ] Definition - - ⊢ (∀a. num2error (error2num a) = a) ∧ - ∀r. (λn. n < 1) r ⇔ error2num (num2error r) = r - - [error_CASE] Definition - - ⊢ ∀x v0. (case x of Failure => v0) = (λm. v0) (error2num x) - - [error_TY_DEF] Definition - - ⊢ ∃rep. TYPE_DEFINITION (λn. n < 1) rep - - [error_size_def] Definition - - ⊢ ∀x. error_size x = 0 - - [i32_add_def] Definition - - ⊢ ∀x y. i32_add x y = mk_i32 (i32_to_int x + i32_to_int y) - - [i32_max_def] Definition - - ⊢ i32_max = 2147483647 - - [i32_min_def] Definition - - ⊢ i32_min = -2147483648 - - [int1_def] Definition - - ⊢ int1 = 32 - - [int2_def] Definition - - ⊢ int2 = -32 - - [is_loop_def] Definition - - ⊢ ∀r. is_loop r ⇔ case r of Return v2 => F | Fail v3 => F | Loop => T - - [is_true_def] Definition - - ⊢ ∀x. is_true x = if x then Return () else Fail Failure - - [list_t_TY_DEF] Definition - - ⊢ ∃rep. - TYPE_DEFINITION - (λa0'. - ∀ $var$('list_t'). - (∀a0'. - (∃a0 a1. - a0' = - (λa0 a1. - ind_type$CONSTR 0 a0 - (ind_type$FCONS a1 (λn. ind_type$BOTTOM))) - a0 a1 ∧ $var$('list_t') a1) ∨ - a0' = - ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒ - $var$('list_t') a0') ⇒ - $var$('list_t') a0') rep - - [list_t_case_def] Definition - - ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧ - ∀f v. list_t_CASE ListNil f v = v - - [list_t_size_def] Definition - - ⊢ (∀f a0 a1. - list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧ - ∀f. list_t_size f ListNil = 0 - - [list_t_v_def] Definition - - ⊢ list_t_v ListNil = [] ∧ - ∀x tl. list_t_v (ListCons x tl) = x::list_t_v tl - - [lookup_def] Definition - - ⊢ ∀key ls. lookup key ls = lookup_raw key (list_t_v ls) - - [mk_i32_def] Definition - - ⊢ ∀n. mk_i32 n = - if i32_min ≤ n ∧ n ≤ i32_max then Return (int_to_i32 n) - else Fail Failure - - [mk_u32_def] Definition - - ⊢ ∀n. mk_u32 n = - if 0 ≤ n ∧ n ≤ u32_max then Return (int_to_u32 n) - else Fail Failure - - [nth_expand_def] Definition - - ⊢ ∀nth ls i. - nth_expand nth ls i = - case ls of - ListCons x tl => - if u32_to_int i = 0 then Return x - else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od - | ListNil => Fail Failure - - [nth_fuel_P_def] Definition - - ⊢ ∀ls i n. nth_fuel_P ls i n ⇔ ¬is_loop (nth_fuel n ls i) - - [result_TY_DEF] Definition - - ⊢ ∃rep. - TYPE_DEFINITION - (λa0. - ∀ $var$('result'). - (∀a0. - (∃a. a0 = - (λa. - ind_type$CONSTR 0 (a,ARB) - (λn. ind_type$BOTTOM)) a) ∨ - (∃a. a0 = - (λa. - ind_type$CONSTR (SUC 0) (ARB,a) - (λn. ind_type$BOTTOM)) a) ∨ - a0 = - ind_type$CONSTR (SUC (SUC 0)) (ARB,ARB) - (λn. ind_type$BOTTOM) ⇒ - $var$('result') a0) ⇒ - $var$('result') a0) rep - - [result_case_def] Definition - - ⊢ (∀a f f1 v. result_CASE (Return a) f f1 v = f a) ∧ - (∀a f f1 v. result_CASE (Fail a) f f1 v = f1 a) ∧ - ∀f f1 v. result_CASE Loop f f1 v = v - - [result_size_def] Definition - - ⊢ (∀f a. result_size f (Return a) = 1 + f a) ∧ - (∀f a. result_size f (Fail a) = 1 + error_size a) ∧ - ∀f. result_size f Loop = 0 - - [st_ex_bind_def] Definition - - ⊢ ∀x f. - monad_bind x f = - case x of Return y => f y | Fail e => Fail e | Loop => Loop - - [st_ex_return_def] Definition - - ⊢ ∀x. st_ex_return x = Return x - - [test1_def] Definition - - ⊢ ∀x. test1 x = Return x - - [test2_TY_DEF] Definition - - ⊢ ∃rep. - TYPE_DEFINITION - (λa0. - ∀ $var$('test2'). - (∀a0. - (∃a. a0 = - (λa. - ind_type$CONSTR 0 (a,ARB) - (λn. ind_type$BOTTOM)) a) ∨ - (∃a. a0 = - (λa. - ind_type$CONSTR (SUC 0) (ARB,a) - (λn. ind_type$BOTTOM)) a) ⇒ - $var$('test2') a0) ⇒ - $var$('test2') a0) rep - - [test2_case_def] Definition - - ⊢ (∀a f f1. test2_CASE (Variant1_2 a) f f1 = f a) ∧ - ∀a f f1. test2_CASE (Variant2_2 a) f f1 = f1 a - - [test2_size_def] Definition - - ⊢ (∀f f1 a. test2_size f f1 (Variant1_2 a) = 1 + f a) ∧ - ∀f f1 a. test2_size f f1 (Variant2_2 a) = 1 + f1 a - - [test_TY_DEF] Definition - - ⊢ ∃rep. - TYPE_DEFINITION - (λa0. - ∀ $var$('test'). - (∀a0. - (∃a. a0 = - (λa. - ind_type$CONSTR 0 (a,ARB) - (λn. ind_type$BOTTOM)) a) ∨ - (∃a. a0 = - (λa. - ind_type$CONSTR (SUC 0) (ARB,a) - (λn. ind_type$BOTTOM)) a) ⇒ - $var$('test') a0) ⇒ - $var$('test') a0) rep - - [test_case_def] Definition - - ⊢ (∀a f f1. test_CASE (Variant1 a) f f1 = f a) ∧ - ∀a f f1. test_CASE (Variant2 a) f f1 = f1 a - - [test_monad2_def] Definition - - ⊢ test_monad2 = do x <- Return T; Return x od - - [test_monad3_def] Definition - - ⊢ ∀x. test_monad3 x = monad_ignore_bind (is_true x) (Return x) - - [test_monad_def] Definition - - ⊢ ∀v. test_monad v = do x <- Return v; Return x od - - [test_size_def] Definition - - ⊢ (∀f f1 a. test_size f f1 (Variant1 a) = 1 + f1 a) ∧ - ∀f f1 a. test_size f f1 (Variant2 a) = 1 + f a - - [u32_add_def] Definition - - ⊢ ∀x y. u32_add x y = mk_u32 (u32_to_int x + u32_to_int y) - - [u32_max_def] Definition - - ⊢ u32_max = 4294967295 - - [u32_sub_def] Definition - - ⊢ ∀x y. u32_sub x y = mk_u32 (u32_to_int x − u32_to_int y) - - [usize_max_def] Definition - - ⊢ usize_max = 4294967295 - - [vec_len_def] Definition - - ⊢ ∀v. vec_len v = int_to_u32 (&LENGTH (vec_to_list v)) - - [I32_ADD_EQ] Theorem - - [oracles: DISK_THM] [axioms: int_to_i32_id] [] - ⊢ ∀x y. - i32_min ≤ i32_to_int x + i32_to_int y ⇒ - i32_to_int x + i32_to_int y ≤ i32_max ⇒ - ∃z. i32_add x y = Return z ∧ - i32_to_int z = i32_to_int x + i32_to_int y - - [INT_OF_NUM_INJ] Theorem - - ⊢ ∀n m. &n = &m ⇒ n = m - - [INT_THM1] Theorem - - ⊢ ∀x y. x > 0 ⇒ y > 0 ⇒ x + y > 0 - - [INT_THM2] Theorem - - ⊢ ∀x. T - - [MK_I32_SUCCESS] Theorem - - ⊢ ∀n. i32_min ≤ n ∧ n ≤ i32_max ⇒ mk_i32 n = Return (int_to_i32 n) - - [MK_U32_SUCCESS] Theorem - - ⊢ ∀n. 0 ≤ n ∧ n ≤ u32_max ⇒ mk_u32 n = Return (int_to_u32 n) - - [NAT_THM1] Theorem - - ⊢ ∀n. n < n + 1 - - [NAT_THM2] Theorem - - ⊢ ∀n. n < n + 1 - - [NUM_SUB_1_EQ] Theorem - - ⊢ ∀x y. x = y − 1 ⇒ 0 ≤ x ⇒ Num y = SUC (Num x) - - [NUM_SUB_1_EQ1] Theorem - - ⊢ ∀i. 0 ≤ i − 1 ⇒ Num i = SUC (Num (i − 1)) - - [NUM_SUB_EQ] Theorem - - ⊢ ∀x y z. x = y − z ⇒ 0 ≤ x ⇒ 0 ≤ z ⇒ Num y = Num z + Num x - - [U32_ADD_EQ] Theorem - - [oracles: DISK_THM] [axioms: int_to_u32_id, u32_to_int_bounds] [] - ⊢ ∀x y. - u32_to_int x + u32_to_int y ≤ u32_max ⇒ - ∃z. u32_add x y = Return z ∧ - u32_to_int z = u32_to_int x + u32_to_int y - - [U32_SUB_EQ] Theorem - - [oracles: DISK_THM] [axioms: int_to_u32_id, u32_to_int_bounds] [] - ⊢ ∀x y. - 0 ≤ u32_to_int x − u32_to_int y ⇒ - ∃z. u32_sub x y = Return z ∧ - u32_to_int z = u32_to_int x − u32_to_int y - - [VEC_TO_LIST_INT_BOUNDS] Theorem - - [oracles: DISK_THM] [axioms: VEC_TO_LIST_BOUNDS] [] - ⊢ ∀v. (let l = &LENGTH (vec_to_list v) in 0 ≤ l ∧ l ≤ u32_max) - - [datatype_error] Theorem - - ⊢ DATATYPE (error Failure) - - [datatype_list_t] Theorem - - ⊢ DATATYPE (list_t ListCons ListNil) - - [datatype_result] Theorem - - ⊢ DATATYPE (result Return Fail Loop) - - [datatype_test] Theorem - - ⊢ DATATYPE (test Variant1 Variant2) - - [datatype_test2] Theorem - - ⊢ DATATYPE (test2 Variant1_2 Variant2_2) - - [error2num_11] Theorem - - ⊢ ∀a a'. error2num a = error2num a' ⇔ a = a' - - [error2num_ONTO] Theorem - - ⊢ ∀r. r < 1 ⇔ ∃a. r = error2num a - - [error2num_num2error] Theorem - - ⊢ ∀r. r < 1 ⇔ error2num (num2error r) = r - - [error2num_thm] Theorem - - ⊢ error2num Failure = 0 - - [error_Axiom] Theorem - - ⊢ ∀x0. ∃f. f Failure = x0 - - [error_EQ_error] Theorem - - ⊢ ∀a a'. a = a' ⇔ error2num a = error2num a' - - [error_case_cong] Theorem - - ⊢ ∀M M' v0. - M = M' ∧ (M' = Failure ⇒ v0 = v0') ⇒ - (case M of Failure => v0) = case M' of Failure => v0' - - [error_case_def] Theorem - - ⊢ ∀v0. (case Failure of Failure => v0) = v0 - - [error_case_eq] Theorem - - ⊢ (case x of Failure => v0) = v ⇔ x = Failure ∧ v0 = v - - [error_induction] Theorem - - ⊢ ∀P. P Failure ⇒ ∀a. P a - - [error_nchotomy] Theorem - - ⊢ ∀a. a = Failure - - [insert_lem] Theorem - - [oracles: DISK_THM] [axioms: u32_to_int_bounds, insert_def] [] - ⊢ ∀ls key value. - distinct_keys (list_t_v ls) ⇒ - case insert key value ls of - Return ls1 => - lookup key ls1 = SOME value ∧ - ∀k. k ≠ key ⇒ lookup k ls = lookup k ls1 - | Fail v1 => F - | Loop => F - - [list_nth_mut_loop_loop_fwd_def] Theorem - - ⊢ ∀ls i. - list_nth_mut_loop_loop_fwd ls i = - case ls of - ListCons x tl => - if u32_to_int i = 0 then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - list_nth_mut_loop_loop_fwd tl i0 - od - | ListNil => Fail Failure - - [list_nth_mut_loop_loop_fwd_ind] Theorem - - ⊢ ∀P. (∀ls i. - (∀x tl i0. ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ P tl i0) ⇒ - P ls i) ⇒ - ∀v v1. P v v1 - - [list_t_11] Theorem - - ⊢ ∀a0 a1 a0' a1'. - ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1' - - [list_t_Axiom] Theorem - - ⊢ ∀f0 f1. ∃fn. - (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧ - fn ListNil = f1 - - [list_t_case_cong] Theorem - - ⊢ ∀M M' f v. - M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧ - (M' = ListNil ⇒ v = v') ⇒ - list_t_CASE M f v = list_t_CASE M' f' v' - - [list_t_case_eq] Theorem - - ⊢ list_t_CASE x f v = v' ⇔ - (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v' - - [list_t_distinct] Theorem - - ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil - - [list_t_induction] Theorem - - ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l - - [list_t_nchotomy] Theorem - - ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil - - [lookup_raw_def] Theorem - - ⊢ (∀key. lookup_raw key [] = NONE) ∧ - ∀v ls key k. - lookup_raw key ((k,v)::ls) = - if k = key then SOME v else lookup_raw key ls - - [lookup_raw_ind] Theorem - - ⊢ ∀P. (∀key. P key []) ∧ - (∀key k v ls. (k ≠ key ⇒ P key ls) ⇒ P key ((k,v)::ls)) ⇒ - ∀v v1. P v v1 - - [nth_def] Theorem - - ⊢ ∀ls i. - nth ls i = - case ls of - ListCons x tl => - if u32_to_int i = 0 then Return x - else do i0 <- u32_sub i (int_to_u32 1); nth tl i0 od - | ListNil => Fail Failure - - [nth_def_loop] Theorem - - ⊢ ∀ls i. (∀n. ¬nth_fuel_P ls i n) ⇒ nth ls i = nth_expand nth ls i - - [nth_def_terminates] Theorem - - ⊢ ∀ls i. (∃n. nth_fuel_P ls i n) ⇒ nth ls i = nth_expand nth ls i - - [nth_fuel_P_mono] Theorem - - ⊢ ∀n m ls i. - n ≤ m ⇒ nth_fuel_P ls i n ⇒ nth_fuel n ls i = nth_fuel m ls i - - [nth_fuel_def] Theorem - - ⊢ ∀n ls i. - nth_fuel n ls i = - case n of - 0 => Loop - | SUC n' => - case ls of - ListCons x tl => - if u32_to_int i = 0 then Return x - else - do i0 <- u32_sub i (int_to_u32 1); nth_fuel n' tl i0 od - | ListNil => Fail Failure - - [nth_fuel_ind] Theorem - - ⊢ ∀P. (∀n ls i. - (∀n' x tl i0. - n = SUC n' ∧ ls = ListCons x tl ∧ u32_to_int i ≠ 0 ⇒ - P n' tl i0) ⇒ - P n ls i) ⇒ - ∀v v1 v2. P v v1 v2 - - [nth_fuel_least_success_mono] Theorem - - ⊢ ∀n ls i. - $LEAST (nth_fuel_P ls i) ≤ n ⇒ - nth_fuel n ls i = nth_fuel ($LEAST (nth_fuel_P ls i)) ls i - - [nth_fuel_mono] Theorem - - ⊢ ∀n m ls i. - n ≤ m ⇒ - if is_loop (nth_fuel n ls i) then T - else nth_fuel n ls i = nth_fuel m ls i - - [num2error_11] Theorem - - ⊢ ∀r r'. r < 1 ⇒ r' < 1 ⇒ (num2error r = num2error r' ⇔ r = r') - - [num2error_ONTO] Theorem - - ⊢ ∀a. ∃r. a = num2error r ∧ r < 1 - - [num2error_error2num] Theorem - - ⊢ ∀a. num2error (error2num a) = a - - [num2error_thm] Theorem - - ⊢ num2error 0 = Failure - - [result_11] Theorem - - ⊢ (∀a a'. Return a = Return a' ⇔ a = a') ∧ - ∀a a'. Fail a = Fail a' ⇔ a = a' - - [result_Axiom] Theorem - - ⊢ ∀f0 f1 f2. ∃fn. - (∀a. fn (Return a) = f0 a) ∧ (∀a. fn (Fail a) = f1 a) ∧ - fn Loop = f2 - - [result_case_cong] Theorem - - ⊢ ∀M M' f f1 v. - M = M' ∧ (∀a. M' = Return a ⇒ f a = f' a) ∧ - (∀a. M' = Fail a ⇒ f1 a = f1' a) ∧ (M' = Loop ⇒ v = v') ⇒ - result_CASE M f f1 v = result_CASE M' f' f1' v' - - [result_case_eq] Theorem - - ⊢ result_CASE x f f1 v = v' ⇔ - (∃a. x = Return a ∧ f a = v') ∨ (∃e. x = Fail e ∧ f1 e = v') ∨ - x = Loop ∧ v = v' - - [result_distinct] Theorem - - ⊢ (∀a' a. Return a ≠ Fail a') ∧ (∀a. Return a ≠ Loop) ∧ - ∀a. Fail a ≠ Loop - - [result_induction] Theorem - - ⊢ ∀P. (∀a. P (Return a)) ∧ (∀e. P (Fail e)) ∧ P Loop ⇒ ∀r. P r - - [result_nchotomy] Theorem - - ⊢ ∀rr. (∃a. rr = Return a) ∨ (∃e. rr = Fail e) ∨ rr = Loop - - [test2_11] Theorem - - ⊢ (∀a a'. Variant1_2 a = Variant1_2 a' ⇔ a = a') ∧ - ∀a a'. Variant2_2 a = Variant2_2 a' ⇔ a = a' - - [test2_Axiom] Theorem - - ⊢ ∀f0 f1. ∃fn. - (∀a. fn (Variant1_2 a) = f0 a) ∧ ∀a. fn (Variant2_2 a) = f1 a - - [test2_case_cong] Theorem - - ⊢ ∀M M' f f1. - M = M' ∧ (∀a. M' = Variant1_2 a ⇒ f a = f' a) ∧ - (∀a. M' = Variant2_2 a ⇒ f1 a = f1' a) ⇒ - test2_CASE M f f1 = test2_CASE M' f' f1' - - [test2_case_eq] Theorem - - ⊢ test2_CASE x f f1 = v ⇔ - (∃T'. x = Variant1_2 T' ∧ f T' = v) ∨ - ∃T'. x = Variant2_2 T' ∧ f1 T' = v - - [test2_distinct] Theorem - - ⊢ ∀a' a. Variant1_2 a ≠ Variant2_2 a' - - [test2_induction] Theorem - - ⊢ ∀P. (∀T. P (Variant1_2 T)) ∧ (∀T. P (Variant2_2 T)) ⇒ ∀t. P t - - [test2_nchotomy] Theorem - - ⊢ ∀tt. (∃T. tt = Variant1_2 T) ∨ ∃T. tt = Variant2_2 T - - [test_11] Theorem - - ⊢ (∀a a'. Variant1 a = Variant1 a' ⇔ a = a') ∧ - ∀a a'. Variant2 a = Variant2 a' ⇔ a = a' - - [test_Axiom] Theorem - - ⊢ ∀f0 f1. ∃fn. - (∀a. fn (Variant1 a) = f0 a) ∧ ∀a. fn (Variant2 a) = f1 a - - [test_case_cong] Theorem - - ⊢ ∀M M' f f1. - M = M' ∧ (∀a. M' = Variant1 a ⇒ f a = f' a) ∧ - (∀a. M' = Variant2 a ⇒ f1 a = f1' a) ⇒ - test_CASE M f f1 = test_CASE M' f' f1' - - [test_case_eq] Theorem - - ⊢ test_CASE x f f1 = v ⇔ - (∃b. x = Variant1 b ∧ f b = v) ∨ ∃a. x = Variant2 a ∧ f1 a = v - - [test_distinct] Theorem - - ⊢ ∀a' a. Variant1 a ≠ Variant2 a' - - [test_induction] Theorem - - ⊢ ∀P. (∀b. P (Variant1 b)) ∧ (∀a. P (Variant2 a)) ⇒ ∀t. P t - - [test_nchotomy] Theorem - - ⊢ ∀tt. (∃b. tt = Variant1 b) ∨ ∃a. tt = Variant2 a - - -*) -end |