(* -------------------------------------------------------------------------- *) (* This is an example demonstrating the benefits of using the SMT solver *) (* Yices through HolSmtLib. The binary search always splits the array in the *) (* middle. This middle is calculated by *) (* *) (* m := l + ((r - l) DIV 2) *) (* *) (* The boundary checks need to prove l <= m /\ m <= r provided l <= r *) (* The HOL internal procedures have trouble with DIV and need user *) (* interaction. Yices proves this automatically. *) (* -------------------------------------------------------------------------- *) (******************************************************************************) (* Boilerplate *) (******************************************************************************) (* load the libries use (Globals.HOLDIR ^ "/examples/separationLogic/src/holfoot/header.sml") *) HOL_Interactive.toggle_quietdec(); open listTheory rich_listTheory pred_setTheory sortingTheory ConseqConv boolSimps open relationTheory HolSmtLib generalHelpersTheory; HOL_Interactive.toggle_quietdec(); (******************************************************************************) (* Lemmata *) (******************************************************************************) val SORTED_EL = prove ( ``!R l n1 n2. transitive R /\ SORTED R l /\ (n2 < LENGTH l) /\ (n1 < n2) ==> (R (EL n1 l) (EL n2 l))``, GEN_TAC THEN Induct_on `l` THEN1 ( SIMP_TAC list_ss [SORTED_DEF] ) THEN Cases_on `n1` THEN Cases_on `n2` THEN REPEAT STRIP_TAC THEN FULL_SIMP_TAC list_ss [] THEN ( METIS_TAC[SORTED_EQ, EL_IS_EL] )); val SORTED_EL_LESS_EQ = prove ( ``!l:num list n1 n2. SORTED $<= l /\ (n1 < LENGTH l) /\ (n2 < LENGTH l) /\ ((EL n1 l) < (EL n2 l)) ==> (n1 < n2)``, REPEAT STRIP_TAC THEN MP_TAC (Q.SPECL [`l`, `n2`, `n1`] (ISPEC ``($<=):num -> num -> bool`` SORTED_EL)) THEN ASM_SIMP_TAC arith_ss [transitive_def] THEN `~(n1 = n2)` by METIS_TAC[prim_recTheory.LESS_REFL] THEN DECIDE_TAC); val TAKE_ID = prove ( ``(!n l. (FIRSTN n l = l) = (n >= LENGTH l))``, Induct_on `l` THEN Cases_on `n` THEN ( ASM_SIMP_TAC list_ss [] )); val DROP_NIL = prove ( ``(!n l. (BUTFIRSTN n l = []) = (n >= LENGTH l))``, Induct_on `l` THEN Cases_on `n` THEN ( ASM_SIMP_TAC list_ss [] )); val SORTED_TAKE_DROP = prove ( ``(!R (l:'a list) n. SORTED R l ==> SORTED R (BUTFIRSTN n l)) /\ (!R (l:'a list) n. SORTED R l ==> SORTED R (FIRSTN n l))``, SIMP_TAC std_ss [GSYM FORALL_AND_THM, GSYM IMP_CONJ_THM] THEN GEN_TAC THEN Induct_on `l` THEN ( SIMP_TAC list_ss [SORTED_DEF] ) THEN Cases_on `n` THEN ( SIMP_TAC list_ss [SORTED_DEF] ) THEN GEN_TAC THEN STRIP_TAC THEN `SORTED R l` by ALL_TAC THEN1 ( Cases_on `l` THEN FULL_SIMP_TAC std_ss [SORTED_DEF] ) THEN FULL_SIMP_TAC std_ss [] THEN Cases_on `n'` THEN1 ( SIMP_TAC list_ss [SORTED_DEF] ) THEN Cases_on `l` THEN ( FULL_SIMP_TAC list_ss [SORTED_DEF] ) THEN Q.PAT_ASSUM `!n. X n` (MP_TAC o Q.SPEC `SUC n`) THEN SIMP_TAC list_ss []); (******************************************************************************) (* Just the shape works automatically *) (******************************************************************************) (*turn yices on*) set_trace "holfoot use Yices" 1; (*verbose off*) set_trace "HolSmtLib" 0; val file = concat [examplesDir, "/automatic/binary_search-shape.dsf"]; val _ = holfoot_auto_verify_spec file; (* see what happens without yices (it fails) *) (* val _ = set_trace "holfoot use Yices" 0; (*turn yices off*) val thm = holfoot_auto_verify_spec file *) (******************************************************************************) (* Verify the fully functional spec now *) (******************************************************************************) val _ = set_trace "holfoot use Yices" 0; (*turn yices off again*) val file_full = concat [examplesDir, "/interactive/binary_search-full.dsf"]; (* holfoot_set_goal file_full *) val binsearch_full_TAC = HF_SOLVE_TAC THEN REPEAT STRIP_TAC THENL [ HF_VC_TAC THEN YICES_TAC, HF_VC_TAC THEN DEPTH_CONSEQ_CONV_TAC (K EXISTS_EQ___CONSEQ_CONV) THEN SIMP_TAC (std_ss++EQUIV_EXTRACT_ss) [] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC arith_ss [] THEN REPEAT STRIP_TAC THEN MP_TAC (Q.SPECL [`data'`, `m_const`, `i`] SORTED_EL_LESS_EQ) THEN ASM_SIMP_TAC arith_ss [], HF_VC_TAC THEN DEPTH_CONSEQ_CONV_TAC (K EXISTS_EQ___CONSEQ_CONV) THEN SIMP_TAC (std_ss++EQUIV_EXTRACT_ss) [] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC arith_ss [] THEN REPEAT STRIP_TAC THEN MP_TAC (Q.SPECL [`data'`, `i`, `m_const`] SORTED_EL_LESS_EQ) THEN ASM_SIMP_TAC arith_ss [], HF_VC_TAC THEN Q.EXISTS_TAC `m_const` THEN ASM_SIMP_TAC arith_ss [], HF_VC_TAC THEN CONJ_TAC THEN1 ( METIS_TAC[MEM_EL] ) THEN HF_CONTINUE_TAC THEN HF_VC_TAC THEN REPEAT STRIP_TAC THEN ( FULL_SIMP_TAC arith_ss [IS_BOOL_TO_NUM_def, BOOL_TO_NUM_REWRITE] ) THEN CCONTR_TAC THEN FULL_SIMP_TAC arith_ss [] ]; val _ = holfoot_tac_verify_spec file_full NONE [("binsearch", binsearch_full_TAC)]; (******************************************************************************) (* Verify the fully functional spec with loopspec *) (******************************************************************************) set_trace "holfoot use Yices" 0; (*turn yices off*) val file_loopspec = concat [examplesDir, "/interactive/binary_search-full-loopspec.dsf"]; (* holfoot_set_goal file_loopspec *) val binsearch_loopspec_TAC = HF_SOLVE_TAC THEN SIMP_TAC (std_ss++CONJ_ss) [IS_BOOL_TO_NUM_REWRITE, SORTED_TAKE_DROP, BOOL_TO_NUM_REWRITE] THEN HF_SOLVE_TAC THEN REPEAT STRIP_TAC THENL [ `old_r - old_l = 0` by DECIDE_TAC THEN xHF_CONTINUE_TAC [use_asms] THEN HF_VC_TAC THEN FULL_SIMP_TAC std_ss [IS_BOOL_TO_NUM_def, BOOL_TO_NUM_REWRITE], HF_VC_TAC THEN YICES_TAC, HF_VC_TAC THEN FULL_SIMP_TAC arith_ss [MIN_EQ] THEN ASM_SIMP_TAC (list_ss++CONJ_ss) [MEM_EL, EL_BUTFIRSTN] THEN EQ_TAC THEN STRIP_TAC THEN1 ( Q.EXISTS_TAC `m_const + (n+1) - old_l` THEN ASM_SIMP_TAC arith_ss [] ) THEN MP_TAC (Q.SPECL [`data'`, `m_const-old_l`, `n`] SORTED_EL_LESS_EQ) THEN ASM_SIMP_TAC arith_ss [] THEN STRIP_TAC THEN Q.EXISTS_TAC `((n - 1) + old_l) - m_const` THEN ASM_SIMP_TAC arith_ss [], HF_VC_TAC THEN ASM_SIMP_TAC (list_ss++CONJ_ss) [MEM_EL, EL_FIRSTN] THEN DEPTH_CONSEQ_CONV_TAC (K EXISTS_EQ___CONSEQ_CONV) THEN SIMP_TAC (std_ss++EQUIV_EXTRACT_ss) [] THEN REPEAT STRIP_TAC THEN EQ_TAC THEN ASM_SIMP_TAC arith_ss [] THEN REPEAT STRIP_TAC THEN MP_TAC (Q.SPECL [`data'`, `n`, `m_const - old_l`] SORTED_EL_LESS_EQ) THEN ASM_SIMP_TAC arith_ss [], HF_VC_TAC THEN SIMP_TAC std_ss [MEM_EL] THEN Q.EXISTS_TAC `m_const - old_l` THEN ASM_SIMP_TAC arith_ss [] ]; val _ = holfoot_tac_verify_spec file_loopspec NONE [("binsearch", binsearch_loopspec_TAC)]