diff options
Diffstat (limited to 'backends/hol4')
| -rw-r--r-- | backends/hol4/TestTheory.sig | 839 | ||||
| -rw-r--r-- | backends/hol4/divDefExampleScript.sml | 418 | ||||
| -rw-r--r-- | backends/hol4/divDefExampleTheory.sig | 188 | ||||
| -rw-r--r-- | backends/hol4/divDefLib.sig | 98 | ||||
| -rw-r--r-- | backends/hol4/divDefLib.sml | 1789 | ||||
| -rw-r--r-- | backends/hol4/divDefLibExampleScript.sml | 29 | ||||
| -rw-r--r-- | backends/hol4/divDefNoFixLib.sig | 99 | ||||
| -rw-r--r-- | backends/hol4/divDefNoFixLib.sml | 1203 | ||||
| -rw-r--r-- | backends/hol4/divDefNoFixLibTestScript.sml (renamed from backends/hol4/testDivDefScript.sml) | 4 | ||||
| -rw-r--r-- | backends/hol4/divDefNoFixLibTestTheory.sig (renamed from backends/hol4/testDivDefTheory.sig) | 6 | ||||
| -rw-r--r-- | backends/hol4/divDefProto2TestScript.sml | 23 | ||||
| -rw-r--r-- | backends/hol4/divDefProto2Theory.sig | 334 | ||||
| -rw-r--r-- | backends/hol4/divDefProtoScript.sml | 252 | ||||
| -rw-r--r-- | backends/hol4/divDefProtoTheory.sig | 220 | ||||
| -rw-r--r-- | backends/hol4/divDefScript.sml (renamed from backends/hol4/divDefProto2Script.sml) | 329 | ||||
| -rw-r--r-- | backends/hol4/divDefTheory.sig | 187 |
16 files changed, 2938 insertions, 3080 deletions
diff --git a/backends/hol4/TestTheory.sig b/backends/hol4/TestTheory.sig deleted file mode 100644 index 552662b8..00000000 --- a/backends/hol4/TestTheory.sig +++ /dev/null @@ -1,839 +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_fail_mono : 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_fail_mono] Theorem - - ⊢ ∀n ls i. n < $LEAST (nth_fuel_P ls i) ⇒ nth_fuel n ls i = Loop - - [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 diff --git a/backends/hol4/divDefExampleScript.sml b/backends/hol4/divDefExampleScript.sml new file mode 100644 index 00000000..338385ab --- /dev/null +++ b/backends/hol4/divDefExampleScript.sml @@ -0,0 +1,418 @@ +(* Manually written examples of how to use the fixed-point operator from divDefScript *) + +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib +open divDefTheory + +val _ = new_theory "divDefExample" + +(* Rewrite the goal once, and on the left part of the goal seen as an application *) +fun pure_once_rewrite_left_tac ths = + CONV_TAC (PATH_CONV "l" (PURE_ONCE_REWRITE_CONV ths)) + +(*============================================= + * Example 1: nth (simply recursive function) + *=============================================*) + +Datatype: + list_t = + ListCons 't list_t + | ListNil +End + +(* We want to use the fixed-point operator ‘fix’ to define a function ‘nth’ + which satisfies the following equation: *) + +val nth_qt = ‘ + 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 +’ + +(* When generating a recursive definition, we apply a fixed-point operator to a + non-recursive function *body*, in which the recursive calls are handled to + a continuation. In case we define a group of mutually recursive + definitions, we generate *one* single body for the whole group of definitions. + It works as follows. + + The input of the body is an enumeration: we start by branching over this input such + that every branch corresponds to one function in the mutually recursive group. + Whenever we make a recursive call, we wrap the input parameters into the proper + variant before calling the continuation: in effect this allows us to choose + the function from the group which gets evaluated. + + Moreover, because of constraints on the way the fixed-point operator is defined, + the input of the body must have the same type as its output: we also + store the outputs of the functions in this big enumeration. + + In order to make this work, we need to shape the body so that: + - input values (at call sites) and output values (when returning) are properly + injected into the enumeration + - whenever we get an output value (which is an enumeration) from a recursive + call, we extract the value from the proper variant of the enumeration + + We encode the enumeration with a nested sum type, whose constructors + are ‘INL’ and ‘INR’. + + In the case of ‘nth’, we generate the encoding below, with the following + peculiarities: + - the input type is ‘: ('t list_t # u32) + 't’ the same as the output type + (modulo the ‘:result’). ‘:'t list_t # u32’ is for the input value, while + ‘t’ is for the output. + *) + +val nth_body_def = Define ‘ + nth_body + (* The continuation is used for the recursive calls - this is required + by the fixed-point operator *) + (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result) + + (* The input. Its type is: nth input type + nth output type *) + (x : (('t list_t # u32) + 't)) : + + (* The output type is the same as the input type - this constraint + comes from limitations in the way we can define the fixed-point + operator inside the HOL logic *) + (('t list_t # u32) + 't) result = + + (* Destruct the input. We need this to call the proper function in case + of mutually recursive definitions, but also to eliminate arguments + which correspond to the output value (the input type is the same + as the output type). *) + case x of + | INL x => ( (* Input case: normal function call *) + (* Body of nth *) + let (ls, i) = x in + case ls of + | ListCons x tl => + if u32_to_int i = (0:int) + then Return (INR x) + else + do + i0 <- u32_sub i (int_to_u32 1); + (* Recursive call: we call the continuation. + + We must wrap the input (here, in INL) then extract the + proper output (this last part is really important in + case of mutually recursive definitions). + *) + x <- (case f (INL (tl, i0)) of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + case r of + | INL _ => Fail Failure + | INR x => Return x); + + (* Wrap the return value *) + Return (INR x) + od + | ListNil => Fail Failure) + | INR _ => (* Output case: invalid, we fail *) + Fail Failure +’ + +(* Then, we prove that the body we just defined satisfies the validity property + required by the fixed-point theorem. + + Remark: + We first prove the theorem with ‘SUC (SUC n)’ where ‘n’ is a variable + to prevent this quantity from being rewritten to 2 during the proofs. *) +Theorem nth_body_is_valid_aux: + is_valid_fp_body (SUC (SUC n)) nth_body +Proof + pure_once_rewrite_tac [is_valid_fp_body_def] >> + gen_tac >> + (* Expand *) + fs [nth_body_def, bind_def] >> + (* Simply explore all paths *) + Cases_on ‘x’ >> fs [] >> + Cases_on ‘x'’ >> fs [] >> + Cases_on ‘q’ >> fs [] >> + Cases_on ‘u32_to_int r = 0’ >> fs [] >> + Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >> + fs [case_result_switch_eq] >> + (* Recursive call *) + disj2_tac >> + qexists ‘\g x. case case x of INL v => Fail Failure | INR x => Return x of + Return x => Return (INR x) + | Fail e => Fail e + | Diverge => Diverge’ >> + qexists ‘INL (l, a)’ >> + conj_tac + >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >> + gen_tac >> + (* Explore all paths *) + Cases_on ‘g (INL (l,a))’ >> fs [] >> + Cases_on ‘a'’ >> fs [] +QED + +Theorem nth_body_is_valid: + is_valid_fp_body (SUC (SUC 0)) nth_body +Proof + irule nth_body_is_valid_aux +QED + +(* We can now define ‘nth’ in terms of the fixed-point operator applied to ‘nth_body’. + + Important points: + - we apply ‘fix’ to ‘fix_body’ + - we wrap the input to take the proper branch (‘INL (ls, i)’) + - we extract the output to have a function with the proper output type + + This definition satisfies the equation we want (see next theorem). *) +val nth_raw_def = Define ‘ + nth (ls : 't list_t) (i : u32) = + case fix nth_body (INL (ls, i)) of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + case r of + | INL _ => Fail Failure + | INR x => Return x +’ + +(* We finally prove the target unfolding equation for ‘nth’ *) +Theorem nth_def: + ∀ls i. 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 +Proof + rpt strip_tac >> + (* Expand the raw definition *) + pure_rewrite_tac [nth_raw_def] >> + (* Use the fixed-point equality - the rewrite must only be applied *on the left* of the equality, in the goal *) + pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >> + (* Expand the body definition *) + pure_rewrite_tac [nth_body_def] >> + (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *) + fs [bind_def] >> + Cases_on ‘ls’ >> fs [] >> + Cases_on ‘u32_to_int i = 0’ >> fs [] >> + Cases_on ‘u32_sub i (int_to_u32 1)’ >> fs [] >> + Cases_on ‘fix nth_body (INL (l,a))’ >> fs [] >> + Cases_on ‘a'’ >> fs [] +QED + +(*=======================================================* + * Example 2: even, odd (mutually recursive definitions) + *=======================================================*) + +(* We consider the following group of mutually recursive definitions: *) + +val even_odd_qt = Defn.parse_quote ‘ + (even (i : int) : bool result = if i = 0 then Return T else odd (i - 1)) /\ + (odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)) +’ + +(* Similarly to ‘nth’, we need to introduce a body on which to apply the + fixed-point operator. Here, the body is slightly more complex because + we have mutually recursive functions. + + In particular, the input/output types is a sum of 4 types: + input of even + output of even + input of odd + output of odd + + That is: ‘: int + bool + int + bool’ + + As a consequence, the body is a case with 4 branches. + *) + +val even_odd_body_def = Define ‘ + even_odd_body + (* The body takes a continuation - required by the fixed-point operator *) + (f : (int + bool + int + bool) -> (int + bool + int + bool) result) + + (* The type of the input is: + input of even + output of even + input of odd + output of odd *) + (x : int + bool + int + bool) : + + (* The output type is the same as the input type - this constraint + comes from limitations in the way we can define the fixed-point + operator inside the HOL logic *) + (int + bool + int + bool) result = + + (* Case disjunction over the input, in order to figure out which + function from the group is actually called (even, or odd). *) + case x of + | INL i => (* Input of even *) + (* Body of even *) + if i = 0 then Return (INR (INL T)) + else + (* Recursive calls are calls to the continuation f, wrapped + in the proper variant: here we call odd *) + (case f (INR (INR (INL (i - 1)))) of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + (* Extract the proper value from the enumeration: here, the + call is tail-call so this is not really necessary, but we + might need to retrieve the output of the call to odd, which + is a boolean, and do something more complex with it. *) + case r of + | INL _ => Fail Failure + | INR (INL _) => Fail Failure + | INR (INR (INL _)) => Fail Failure + | INR (INR (INR b)) => (* Extract the output of odd *) + (* Return: inject into the variant for the output of even *) + Return (INR (INL b)) + ) + | INR (INL _) => (* Output of even *) + (* We must ignore this one *) + Fail Failure + | INR (INR (INL i)) => + (* Body of odd *) + if i = 0 then Return (INR (INR (INR F))) + else + (* Call to even *) + (case f (INL (i - 1)) of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + (* Extract the proper value from the enumeration *) + case r of + | INL _ => Fail Failure + | INR (INL b) => (* Extract the output of even *) + (* Return: inject into the variant for the output of odd *) + Return (INR (INR (INR b))) + | INR (INR (INL _)) => Fail Failure + | INR (INR (INR _)) => Fail Failure + ) + | INR (INR (INR _)) => (* Output of odd *) + (* We must ignore this one *) + Fail Failure +’ + +(* We then prove that this body satisfies the validity condition *) +Theorem even_odd_body_is_valid_aux: + is_valid_fp_body (SUC (SUC n)) even_odd_body +Proof + pure_once_rewrite_tac [is_valid_fp_body_def] >> + gen_tac >> + (* Expand *) + fs [even_odd_body_def, bind_def] >> + (* Explore the body *) + Cases_on ‘x’ >> fs [] + >-( + Cases_on ‘x' = 0’ >> fs [] >> + (* Recursive call *) + disj2_tac >> + qexists ‘\g x. case x of + | INL v => Fail Failure + | INR (INL v2) => Fail Failure + | INR (INR (INL v4)) => Fail Failure + | INR (INR (INR b)) => Return (INR (INL b))’ >> + qexists ‘INR (INR (INL (x' − 1)))’ >> + conj_tac + >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >> + fs []) >> + Cases_on ‘y’ >> fs [] >> + Cases_on ‘y'’ >> fs [] >> + Cases_on ‘x = 0’ >> fs [] >> + (* Recursive call *) + disj2_tac >> + qexists ‘\g x. case x of + INL v => Fail Failure + | INR (INL b) => Return (INR (INR (INR b))) + | INR (INR v3) => Fail Failure’ >> + qexists ‘INL (x − 1)’ >> + conj_tac + >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >> + fs [] +QED + +Theorem even_odd_body_is_valid: + is_valid_fp_body (SUC (SUC 0)) even_odd_body +Proof + irule even_odd_body_is_valid_aux +QED + +(* We finally introduce the definitions for even and odd *) +val even_raw_def = Define ‘ + even (i : int) = + case fix even_odd_body (INL i) of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + case r of + | INL _ => Fail Failure + | INR (INL b) => Return b + | INR (INR (INL b)) => Fail Failure + | INR (INR (INR _)) => Fail Failure +’ + +val odd_raw_def = Define ‘ + odd (i : int) = + case fix even_odd_body (INR (INR (INL i))) of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + case r of + | INL _ => Fail Failure + | INR (INL _) => Fail Failure + | INR (INR (INL _)) => Fail Failure + | INR (INR (INR b)) => Return b +’ + +Theorem even_def: + ∀i. even (i : int) : bool result = + if i = 0 then Return T else odd (i - 1) +Proof + gen_tac >> + (* Expand the definition *) + pure_once_rewrite_tac [even_raw_def] >> + (* Use the fixed-point equality *) + pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >> + (* Expand the body definition *) + pure_rewrite_tac [even_odd_body_def] >> + (* Expand all the definitions from the group *) + pure_rewrite_tac [even_raw_def, odd_raw_def] >> + (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *) + fs [bind_def] >> + Cases_on ‘i = 0’ >> fs [] >> + Cases_on ‘fix even_odd_body (INR (INR (INL (i − 1))))’ >> fs [] >> + Cases_on ‘a’ >> fs [] >> + Cases_on ‘y’ >> fs [] >> + Cases_on ‘y'’ >> fs [] +QED + +Theorem odd_def: + ∀i. odd (i : int) : bool result = + if i = 0 then Return F else even (i - 1) +Proof + gen_tac >> + (* Expand the definition *) + pure_once_rewrite_tac [odd_raw_def] >> + (* Use the fixed-point equality *) + pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >> + (* Expand the body definition *) + pure_rewrite_tac [even_odd_body_def] >> + (* Expand all the definitions from the group *) + pure_rewrite_tac [even_raw_def, odd_raw_def] >> + (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *) + fs [bind_def] >> + Cases_on ‘i = 0’ >> fs [] >> + Cases_on ‘fix even_odd_body (INL (i − 1))’ >> fs [] >> + Cases_on ‘a’ >> fs [] >> + Cases_on ‘y’ >> fs [] +QED + +val _ = export_theory () diff --git a/backends/hol4/divDefExampleTheory.sig b/backends/hol4/divDefExampleTheory.sig new file mode 100644 index 00000000..29e98856 --- /dev/null +++ b/backends/hol4/divDefExampleTheory.sig @@ -0,0 +1,188 @@ +signature divDefExampleTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val even_odd_body_def : thm + val list_t_TY_DEF : thm + val list_t_case_def : thm + val list_t_size_def : thm + val nth_body_def : thm + + (* Theorems *) + val datatype_list_t : thm + val even_def : thm + val even_odd_body_is_valid : thm + val even_odd_body_is_valid_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 nth_body_is_valid : thm + val nth_body_is_valid_aux : thm + val nth_def : thm + val odd_def : thm + + val divDefExample_grammars : type_grammar.grammar * term_grammar.grammar +(* + [divDef] Parent theory of "divDefExample" + + [even_odd_body_def] Definition + + ⊢ ∀f x. + even_odd_body f x = + case x of + INL 0 => Return (INR (INL T)) + | INL i => + (case f (INR (INR (INL (i − 1)))) of + Return (INL v) => Fail Failure + | Return (INR (INL v2)) => Fail Failure + | Return (INR (INR (INL v4))) => Fail Failure + | Return (INR (INR (INR b))) => Return (INR (INL b)) + | Fail e => Fail e + | Diverge => Diverge) + | INR (INL v8) => Fail Failure + | INR (INR (INL 0)) => Return (INR (INR (INR F))) + | INR (INR (INL i')) => + (case f (INL (i' − 1)) of + Return (INL v) => Fail Failure + | Return (INR (INL b)) => Return (INR (INR (INR b))) + | Return (INR (INR v3)) => Fail Failure + | Fail e => Fail e + | Diverge => Diverge) + | INR (INR (INR v11)) => 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 + + [nth_body_def] Definition + + ⊢ ∀f x. + nth_body f x = + case x of + INL x => + (let + (ls,i) = x + in + case ls of + ListCons x tl => + if u32_to_int i = 0 then Return (INR x) + else + do + i0 <- u32_sub i (int_to_u32 1); + x <- + case f (INL (tl,i0)) of + Return (INL v) => Fail Failure + | Return (INR x) => Return x + | Fail e => Fail e + | Diverge => Diverge; + Return (INR x) + od + | ListNil => Fail Failure) + | INR v3 => Fail Failure + + [datatype_list_t] Theorem + + ⊢ DATATYPE (list_t ListCons ListNil) + + [even_def] Theorem + + ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1) + + [even_odd_body_is_valid] Theorem + + ⊢ is_valid_fp_body (SUC (SUC 0)) even_odd_body + + [even_odd_body_is_valid_aux] Theorem + + ⊢ is_valid_fp_body (SUC (SUC n)) even_odd_body + + [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 + + [nth_body_is_valid] Theorem + + ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body + + [nth_body_is_valid_aux] Theorem + + ⊢ is_valid_fp_body (SUC (SUC n)) nth_body + + [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 + + [odd_def] Theorem + + ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1) + + +*) +end diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig index d63d7771..51a09b9c 100644 --- a/backends/hol4/divDefLib.sig +++ b/backends/hol4/divDefLib.sig @@ -1,93 +1,19 @@ -signature divDefLib = -sig - include Abbrev - - (* Define a (group of mutually recursive) function(s) which uses an error - monad and is potentially divergent. - - We encode divergence in such a way that we don't have to prove that the - functions we define terminate *upon defining them*, and can do those proofs - in an extrinsic way later. It works as follows. - - Let's say you want to define the following “even” and “odd” functions - which operate on *integers*: - - {[ - even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\ - - odd (i : int) : bool result = if i = 0 then Return F else even (i - 1) - ]} - - It is easy to prove that the functions terminate provided the input is >= 0, - but it would require to be able to define those functions in the first place! - - {!DefineDev} consequently does the following. +(* This library implements an automated method, DefineDiv, which generates + definitions by means of the fixed-point operator ‘fix’ introduced in + ‘divDefScript’. - It first defines versions of “even” and “odd” which use fuel: - {[ - even___fuel (n : num) (i : int) : bool result = - case n of 0 => Diverge - | SUC m => if i = 0 then Return T else odd___fuel m (i - 1) /\ + For examples of how to use the fixed-point operator step by step on + hand-written examples, see divDefExampleTheory. - odd___fuel (n : num) (i : int) : bool result = - case n of 0 => Diverge - | SUC m => if i = 0 then Return F else even___fuel m (i - 1) - ]} + The current file is organized so as to follow the steps detailed in + divDefExampleTheory. - Those functions trivially terminate. + For examples of how to use DefiveDiv, see divDefLibExampleScript. + *) - Then, provided we have the following auxiliary definition: - {[ - is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F - ]} - - we can define the following predicates, which tell us whether “even___fuel” - and “odd___fuel” terminate on some given inputs: - {[ - even___P i n = ~(is_diverge (even___fuel n i)) /\ - - odd___P i n = ~(is_diverge (odd___fuel n i)) - ]} - - We can finally define “even” and “odd” as follows. We use the excluded - middle to test whether there exists some fuel on which the function - terminates: if there exists such fuel, we call the "___fuel" versions - of “even” and “odd” with it (we use the least upper bound, to be more - precise). Otherwise, we simply return “Diverge”. - {[ - even i = - if (?n. even___P i n) then even___fuel ($LEAST (even___P i)) i - else Diverge /\ - - odd i = - if (?n. odd___P i n) then odd___fuel ($LEAST (odd___P i)) i - else Diverge - ]} - - The definitions above happen to satisfy the rewriting theorem we want: - {[ - even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\ - - odd (i : int) : bool result = if i = 0 then Return F else even (i - 1) - ]} - - Moreover, if we prove a lemma which states that they don't evaluate to - “Diverge” on some given inputs (trivial recursion if we take “i >= 0” - and reuse the rewriting theorem just above), then we effectively proved - that the functions terminate on those inputs. +signature divDefLib = +sig + include Abbrev - Remark: - ======= - {!DefineDiv} introduces all the auxiliary definitions we need and - automatically performs the proofs. A crucial intermediate lemma - we need in order to establish the last theorem is that the "___fuel" - versions of the functions are monotonic in the fuel. - More precisely: - {[ - !n m. n <= m ==> - (!ls i. even___P ls i n ==> even___fuel n ls i n = even___fuel m ls i n) /\ - (!ls i. odd___P ls i n ==> odd___fuel n ls i n = odd___fuel m ls i n) - ]} - *) val DefineDiv : term quotation -> thm list end diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml index 59c1edaf..3e2d7c04 100644 --- a/backends/hol4/divDefLib.sml +++ b/backends/hol4/divDefLib.sml @@ -1,5 +1,3 @@ -(* This file implements utilities to define potentially diverging functions *) - structure divDefLib :> divDefLib = struct @@ -8,1196 +6,889 @@ open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory open primitivesLib +open divDefTheory -val case_result_same_eq = prove ( - “!(r : 'a result). - (case r of - Return x => Return x - | Fail e => Fail e - | Diverge => Diverge) = r”, - rw [] >> CASE_TAC) - -(* -val ty = id_ty -strip_arrows ty -*) +val dbg = ref false +fun print_dbg s = if (!dbg) then print s else () -(* TODO: move *) -fun list_mk_arrow (tys : hol_type list) (ret_ty : hol_type) : hol_type = - foldr (fn (ty, aty) => ty --> aty) ret_ty tys +val result_ty = “:'a result” +val error_ty = “:error” +val alpha_ty = “:'a” +val num_ty = “:num” -(* TODO: move *) -fun strip_arrows (ty : hol_type) : hol_type list * hol_type = - let - val (ty0, ty1) = dom_rng ty - val (tys, ret) = strip_arrows ty1 - in - (ty0::tys, ret) - end - handle HOL_ERR _ => ([], ty) +val zero_num_tm = “0:num” +val suc_tm = “SUC” -(* Small utilities *) -val current_goal : term option ref = ref NONE +val return_tm = “Return : 'a -> 'a result” +val fail_tm = “Fail : error -> 'a result” +val fail_failure_tm = “Fail Failure : 'a result” +val diverge_tm = “Diverge : 'a result” -(* Save a goal in {!current_goal} then prove it. +val fix_tm = “fix” +val is_valid_fp_body_tm = “is_valid_fp_body” - This way if the proof fails we can easily retrieve the goal for debugging - purposes. - *) -fun save_goal_and_prove (g, tac) : thm = +fun mk_result (ty : hol_type) : hol_type = Type.type_subst [ alpha_ty |-> ty ] result_ty +fun dest_result (ty : hol_type) : hol_type = let - val _ = current_goal := SOME g + val {Args=out_ty, Thy=thy, Tyop=tyop} = dest_thy_type ty in - prove (g, tac) + if thy = "primitives" andalso tyop = "result" then hd out_ty + else failwith "dest_result: not a result" end - - -(*val def_qt = ‘ -(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 num_zero_tm = “0:num” -val num_suc_tm = “SUC: num -> num” -val num_ty = “:num” - -val fuel_def_suffix = "___fuel" (* TODO: name collisions *) -val fuel_var_name = "$n" (* TODO: name collisions *) -val fuel_var = mk_var (fuel_var_name, num_ty) -val fuel_var0 = fuel_var -val fuel_var1 = mk_var ("$m", “:num”) (* TODO: name collisions *) -val fuel_vars_le = “^fuel_var0 <= ^fuel_var1” -val fuel_predicate_suffix = "___P" (* TODO: name collisions *) -val expand_suffix = "___E" (* TODO: name collisions *) +fun mk_return (x : term) : term = mk_icomb (return_tm, x) +fun mk_fail (ty : hol_type) (e : term) : term = mk_comb (inst [ alpha_ty |-> ty ] fail_tm, e) +fun mk_fail_failure (ty : hol_type) : term = inst [ alpha_ty |-> ty ] fail_failure_tm +fun mk_diverge (ty : hol_type) : term = inst [ alpha_ty |-> ty ] diverge_tm -val bool_ty = “:bool” +fun mk_suc (n : term) = mk_comb (suc_tm, n) -val alpha_tyvar : hol_type = “:'a” -val beta_tyvar : hol_type = “:'b” - -val is_diverge_tm = “is_diverge: 'a result -> bool” -val diverge_tm = “Diverge : 'a result” +fun enumerate (ls : 'a list) : (int * 'a) list = + zip (List.tabulate (List.length ls, fn i => i)) ls -val least_tm = “$LEAST” -val le_tm = (fst o strip_comb) “x:num <= y:num” -val true_tm = “T” -val false_tm = “F” +(*=============================================================================* + * + * Generate the (non-recursive) body to give to the fixed-point operator + * + * ============================================================================*) -val measure_tm = “measure: ('a -> num) -> 'a -> 'a -> bool” - -fun mk_diverge_tm (ty : hol_type) : term = - let - val diverge_ty = mk_thy_type {Thy="primitives", Tyop="result", Args = [ty] } - val diverge_tm = mk_thy_const { Thy="primitives", Name="Diverge", Ty=diverge_ty } - in - diverge_tm - end +(* Small helper to generate wrappers of the shape: ‘INL x’, ‘INR (INL x)’, etc. + Note that we should have: ‘length before_tys + 1 + length after tys >= 2’ -(* Small utility: we sometimes need to generate a termination measure for - the fuel definitions. + Ex.: + ==== + The enumeration has type: “: 'a + 'b + 'c + 'd”. + We want to generate the variant which injects “x:'c” into this enumeration. - We derive a measure for a type which is simply the sum of the tuples - of the input types of the functions. - - For instance, for even and odd we have: + We need to split the list of types into: {[ - even___fuel : num -> int -> bool result - odd___fuel : num -> int -> bool result + before_tys = [“:'a”, “'b”] + tm = “x: 'c” + after_tys = [“:'d”] ]} - So the type would be: + The function will generate: {[ - (num # int) + (num # int) + INR (INR (INL x) : 'a + 'b + 'c + 'd ]} - Note that generally speaking we expect a type of the shape (the “:num” - on the left is for the fuel): - {[ - (num # ...) + (num # ...) + ... + (num # ...) - ]} + (* Debug *) + val before_tys = [“:'a”, “:'b”, “:'c”] + val tm = “x:'d” + val after_tys = [“:'e”, “:'f”] - The decreasing measure is simply given by a function which matches over - its argument to return the fuel, whatever the case. + val before_tys = [“:'a”, “:'b”, “:'c”] + val tm = “x:'d” + val after_tys = [] + + mk_inl_inr_wrapper before_tys tm after_tys *) -fun mk_termination_measure_from_ty (ty : hol_type) : term = +fun list_mk_inl_inr (before_tys : hol_type list) (tm : term) (after_tys : hol_type list) : + term = let - val dtys = map pairSyntax.strip_prod (sumSyntax.strip_sum ty) - (* For every tuple, create a match to extract the num *) - fun mk_case_of_tuple (tys : hol_type list) : (term * term) = - case tys of - [] => failwith "mk_termination_measure_from_ty: empty list of types" - | [num_ty] => - (* No need for a case *) - let val var = genvar num_ty in (var, var) end - | num_ty :: rem_tys => + val (before_tys, pat) = + if after_tys = [] + then let - val scrut_var = genvar (pairSyntax.list_mk_prod tys) - val var = genvar num_ty - val rem_var = genvar (pairSyntax.list_mk_prod rem_tys) - val pats = [(pairSyntax.mk_pair (var, rem_var), var)] - val case_tm = TypeBase.mk_case (scrut_var, pats) + val just_before_ty = List.last before_tys + val before_tys = List.take (before_tys, List.length before_tys - 1) + val pat = sumSyntax.mk_inr (tm, just_before_ty) in - (scrut_var, case_tm) + (before_tys, pat) end - val tuple_cases = map mk_case_of_tuple dtys - - (* For every sum, create a match to extract one of the tuples *) - fun mk_sum_case ((tuple_var, tuple_case), (nvar, case_end)) = - let - val left_pat = sumSyntax.mk_inl (tuple_var, type_of nvar) - val right_pat = sumSyntax.mk_inr (nvar, type_of tuple_var) - val scrut = genvar (sumSyntax.mk_sum (type_of tuple_var, type_of nvar)) - val pats = [(left_pat, tuple_case), (right_pat, case_end)] - val case_tm = TypeBase.mk_case (scrut, pats) - in - (scrut, case_tm) - end - val tuple_cases = rev tuple_cases - val (nvar, case_end) = hd tuple_cases - val tuple_cases = tl tuple_cases - val (scrut, case_tm) = foldl mk_sum_case (nvar, case_end) tuple_cases - - (* Create the function *) - val abs_tm = mk_abs (scrut, case_tm) - - (* Add the “measure term” *) - val tm = inst [alpha_tyvar |-> type_of scrut] measure_tm - val tm = mk_comb (tm, abs_tm) + else (before_tys, sumSyntax.mk_inl (tm, sumSyntax.list_mk_sum after_tys)) + val pat = foldr (fn (ty, pat) => sumSyntax.mk_inr (pat, ty)) pat before_tys in - tm + pat end -(* -val ty = “: (num # 'a) + (num # 'b) + (num # 'c)” - -val tys = hd dtys -val num_ty::rem_tys = tys - -val (tuple_var, tuple_case) = hd tuple_cases -*) - -(* Get the smallest id which make the names unique (or to be more precise: - such that the names don't correspond to already defined constants). - - We do this for {!mk_fuel_defs}: for some reason, the termination proof - fails if we try to reuse the same names as before. +(* This function wraps a term into the proper variant of the input/output + sum. + + Ex.: + ==== + For the input of the first function, we generate: ‘INL x’ + For the output of the first function, we generate: ‘INR (INL x)’ + For the input of the 2nd function, we generate: ‘INR (INR (INL x))’ + etc. + + If ‘is_input’ is true: we are wrapping an input. Otherwise we are wrapping + an output. + + (* Debug *) + val tys = [(“:'a”, “:'b”), (“:'c”, “:'d”), (“:'e”, “:'f”)] + val j = 1 + val tm = “x:'c” + val tm = “y:'d” + val is_input = true *) -fun get_smallest_unique_id_for_names (names : string list) : string = +fun inject_in_param_sum (tys : (hol_type * hol_type) list) (j : int) (is_input : bool) + (tm : term) : term = let - (* Not trying to be smart here *) - val i : int option ref = ref NONE - fun get_i () = case !i of NONE => "" | SOME i => int_to_string i - fun incr_i () = - i := (case !i of NONE => SOME 0 | SOME i => SOME (i+1)) - val continue = ref true - fun name_is_ok (name : string) : bool = - not (is_const (Parse.parse_in_context [] [QUOTE (name ^ get_i ())])) - handle HOL_ERR _ => false - val _ = - while !continue do ( - let val _ = (continue := not (forall name_is_ok names)) in - if !continue then incr_i () else () end - ) + fun flatten ls = List.concat (map (fn (x, y) => [x, y]) ls) + val before_tys = flatten (List.take (tys, j)) + val (input_ty, output_ty) = List.nth (tys, j) + val after_tys = flatten (List.drop (tys, j + 1)) + val (before_tys, after_tys) = + if is_input then (before_tys, output_ty :: after_tys) + else (before_tys @ [input_ty], after_tys) in - get_i () + list_mk_inl_inr before_tys tm after_tys end -fun mk_fuel_defs (def_tms : term list) : thm list = - let - (* Retrieve the identifiers. +(* Remark: the order of the branches when creating matches is important. + For instance, in the case of ‘result’ it must be: ‘Return’, ‘Fail’, ‘Diverge’. - Ex.: def_tm = “even (n : int) : bool result = if i = 0 then Return T else odd (i - 1))” - We want to retrive: id = “even” - *) - val ids = map (fst o strip_comb o lhs) def_tms - - (* In the definitions, replace the identifiers by new identifiers which use - fuel. - - Ex.: - def_fuel_tm = “ - even___fuel (fuel : nat) (n : int) : result bool = - case fuel of 0 => Diverge - | SUC fuel' => - if i = 0 then Return T else odd_fuel fuel' (i - 1))” - *) - val names = map ((fn s => s ^ fuel_def_suffix) o fst o dest_var) ids - val index = get_smallest_unique_id_for_names names - fun mk_fuel_id (id : term) : term = - let - val (id_str, ty) = dest_var id - (* Note: we use symbols forbidden in the generation of code to - prevent name collisions *) - val fuel_id_str = id_str ^ fuel_def_suffix ^ index - val fuel_id = mk_var (fuel_id_str, num_ty --> ty) - in fuel_id end - val fuel_ids = map mk_fuel_id ids - - val fuel_ids_with_fuel0 = map (fn id => mk_comb (id, fuel_var0)) fuel_ids - val fuel_ids_with_fuel1 = map (fn id => mk_comb (id, fuel_var1)) fuel_ids - - (* Recurse through the terms and replace the calls *) - val rwr_thms0 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel0) - val rwr_thms1 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel1) - - fun mk_fuel_tm (def_tm : term) : term = - let - val (tm0, tm1) = dest_eq def_tm - val tm0 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms0)) tm0 - val tm1 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms1)) tm1 - in mk_eq (tm0, tm1) end - val fuel_tms = map mk_fuel_tm def_tms - - (* Add the case over the fuel *) - fun add_fuel_case (tm : term) : term = - let - val (f, body) = dest_eq tm - (* Create the “Diverge” term with the proper type *) - val body_ty = type_of body - val return_ty = - case (snd o dest_type) body_ty of [ty] => ty - | _ => failwith "unexpected" - val diverge_tm = mk_diverge_tm return_ty - (* Create the “SUC fuel” term *) - val suc_tm = mk_comb (num_suc_tm, fuel_var1) - val fuel_tm = - TypeBase.mk_case (fuel_var0, [(num_zero_tm, diverge_tm), (suc_tm, body)]) - in mk_eq (f, fuel_tm) end - val fuel_tms = map add_fuel_case fuel_tms - - (* Define the auxiliary definitions which use fuel *) - val fuel_defs_conj = list_mk_conj fuel_tms - (* The definition name *) - val def_name = (fst o dest_var o hd) fuel_ids - (* The tactic to prove the termination *) - val rty = ref “:bool” (* This is useful for debugging *) - fun prove_termination_tac (asms, g) = - let - val r_tm = (fst o dest_exists) g - val _ = rty := type_of r_tm - val ty = (hd o snd o dest_type) (!rty) - val m_tm = mk_termination_measure_from_ty ty - in - WF_REL_TAC ‘^m_tm’ (asms, g) - end - - (* Define the fuel definitions *) - (* - val temp_def = Hol_defn def_name ‘^fuel_defs_conj’ - Defn.tgoal temp_def - *) - val fuel_defs = tDefine def_name ‘^fuel_defs_conj’ prove_termination_tac - in - CONJUNCTS fuel_defs - end - -(* -val (fuel_tms, fuel_defs) = mk_fuel_defs def_tms -val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs) -val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms) -*) - -fun mk_is_diverge_tm (fuel_tm : term) : term = - case snd (dest_type (type_of fuel_tm)) of - [ret_ty] => mk_comb (inst [alpha_tyvar |-> ret_ty] is_diverge_tm, fuel_tm) - | _ => failwith "mk_is_diverge_tm: unexpected" - -fun mk_fuel_predicate_defs (def_tm, fuel_def_tm) : thm = + For the purpose of stability and maintainability, we introduce this small helper + which reorders the cases in a pattern before actually creating the case + expression. + *) +fun unordered_mk_case (scrut: term, pats: (term * term) list) : term = let - (* From [even i] create the term [even_P i n], where [n] is the fuel *) - val (id, args) = (strip_comb o lhs) def_tm - val (id_str, id_ty) = dest_var id - val (tys, ret_ty) = strip_arrows id_ty - val tys = append tys [num_ty] - val pred_ty = list_mk_arrow tys bool_ty - val pred_id = mk_var (id_str ^ fuel_predicate_suffix, pred_ty) - val pred_tm = list_mk_comb (pred_id, append args [fuel_var]) - - (* Create the term ~is_diverge (even_fuel n i) *) - val fuel_tm = lhs fuel_def_tm - val not_is_diverge_tm = mk_neg (mk_is_diverge_tm fuel_tm) - - (* Create the term: even_P i n = ~(is_diverge (even_fuel n i) *) - val pred_def_tm = mk_eq (pred_tm, not_is_diverge_tm) + (* Retrieve the constructors *) + val cl = TypeBase.constructors_of (type_of scrut) + (* Retrieve the names of the constructors *) + val names = map (fst o dest_const) cl + (* Use those to reorder the patterns *) + fun is_pat (name : string) (pat, _) = + let + val app = (fst o strip_comb) pat + val app_name = (fst o dest_const) app + in + app_name = name + end + val pats = map (fn name => valOf (List.find (is_pat name) pats)) names in - (* Create the definition *) - Define ‘^pred_def_tm’ + (* Create the case *) + TypeBase.mk_case (scrut, pats) end -(* -val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms) - -val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms) -*) +(* Wrap a term of type “:'a result” into a ‘case of’ which matches over + the result. -(* Tactic which makes progress in a proof by making a case disjunction (we use - this to explore all the paths in a function body). *) -fun case_progress (asms, g) = - let - val scrut = (strip_all_cases_get_scrutinee o lhs) g - in Cases_on ‘^scrut’ (asms, g) end + Ex.: + ==== + {[ + f x -(* Prove the fuel monotonicity properties. + ~~> - We want to prove a theorem of the shape: - {[ - !n m. - (!i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i) /\ - (!i. n <= m ==> odd___P i n ==> odd___fuel n i = odd___fuel m i) + case f x of + | Fail e => Fail e + | Diverge => Diverge + | Return y => ... (* The branch content is generated by the continuation *) ]} -*) -fun prove_fuel_mono (pred_defs : thm list) (fuel_defs : thm list) : thm = - let - val pred_tms = map (lhs o snd o strip_forall o concl) pred_defs - val fuel_tms = map (lhs o snd o strip_forall o concl) fuel_defs - val pred_fuel_tms = zip pred_tms fuel_tms - (* Create a set containing the names of all the functions in the recursive group *) - val rec_fun_set = - Redblackset.fromList const_name_compare (map get_fun_name_from_app fuel_tms) - (* Small tactic which rewrites the occurrences of recursive calls *) - fun rewrite_rec_call (asms, g) = - let - val scrut = (strip_all_cases_get_scrutinee o lhs) g - val fun_id = get_fun_name_from_app scrut (* This can fail *) - in - (* Check if the function is part of the group we are considering *) - if Redblackset.member (rec_fun_set, fun_id) then - let - (* Yes: use the induction hypothesis *) - fun apply_ind_hyp (ind_th : thm) : tactic = - let - val th = SPEC_ALL ind_th - val th_pat = (lhs o snd o strip_imp o concl) th - val (var_s, ty_s) = match_term th_pat scrut - (* Note that in practice the type instantiation should be empty *) - val th = INST var_s (INST_TYPE ty_s th) - in - assume_tac th - end - in - (last_assum apply_ind_hyp >> fs []) (asms, g) - end - else all_tac (asms, g) - end - handle HOL_ERR _ => all_tac (asms, g) - (* Generate terms of the shape: - !i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i - *) - fun mk_fuel_eq_tm (pred_tm, fuel_tm) : term = - let - (* Retrieve the variables which are not the fuel - for the quantifiers *) - val vars = (tl o snd o strip_comb) fuel_tm - (* Introduce the fuel term which uses “m” *) - val m_fuel_tm = subst [fuel_var0 |-> fuel_var1] fuel_tm - (* Introduce the equality *) - val fuel_eq_tm = mk_eq (fuel_tm, m_fuel_tm) - (* Introduce the implication with the _P pred *) - val fuel_eq_tm = mk_imp (pred_tm, fuel_eq_tm) - (* Introduce the “n <= m ==> ...” implication *) - val fuel_eq_tm = mk_imp (fuel_vars_le, fuel_eq_tm) - (* Quantify *) - val fuel_eq_tm = list_mk_forall (vars, fuel_eq_tm) - in - fuel_eq_tm - end - val fuel_eq_tms = map mk_fuel_eq_tm pred_fuel_tms - (* Create the conjunction *) - val fuel_eq_tms = list_mk_conj fuel_eq_tms - (* Qantify over the fuels *) - val fuel_eq_tms = list_mk_forall ([fuel_var0, fuel_var1], fuel_eq_tms) - (* The tactics for the proof *) - val prove_tac = - Induct_on ‘^fuel_var0’ >-( - (* The ___P predicates are false: n is 0 *) - fs pred_defs >> - fs [is_diverge_def] >> - pure_once_rewrite_tac fuel_defs >> fs []) >> - (* Introduce n *) - gen_tac >> - (* Introduce m *) - Cases_on ‘^fuel_var1’ >-( - (* Contradiction: SUC n < 0 *) - rw [] >> exfalso >> int_tac) >> - fs pred_defs >> - fs [is_diverge_def] >> - pure_once_rewrite_tac fuel_defs >> fs [bind_def] >> - (* Introduce in the context *) - rpt gen_tac >> - (* Split the goals - note that we prove one big goal for all the functions at once *) - rpt strip_tac >> - (* Instantiate the assumption: !m. n <= m ==> ~(...) - with the proper m. - *) - last_x_assum imp_res_tac >> - (* Make sure the induction hypothesis is always the last assumption *) - last_x_assum assume_tac >> - (* Split the goals *) - rpt strip_tac >> fs [case_result_same_eq] >> - (* Explore all the paths *) - rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq]) - in - (* Prove *) - save_goal_and_prove (fuel_eq_tms, prove_tac) - end -(* -val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs + ‘gen_ret_branch’ is a *continuation* which generates the content of the + ‘Return’ branch (i.e., the content of the ‘...’ in the example above). + It receives as input the value contained by the ‘Return’ (i.e., the variable + ‘y’ in the example above). -set_goal ([], fuel_eq_tms) -*) + Remark.: the type of the term generated by ‘gen_ret_branch’ must have + the type ‘result’, but it can change the content of the result (i.e., + if ‘scrut’ has type ‘:'a result’, we can change the type of the wrapped + expression to ‘:'b result’). -(* Prove the property about the least upper bound. + (* Debug *) + val scrut = “x: int result” + fun gen_ret_branch x = mk_return x - We want to prove theorems of the shape: - {[ - (!n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i) - ]} - {[ - (!n i. $LEAST (odd___P i) <= n ==> odd___fuel n i = odd___fuel ($LEAST (odd___P i)) i) - ]} + val scrut = “x: int result” + fun gen_ret_branch _ = “Return T” - TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms) -*) -fun prove_least_fuel_mono (pred_defs : thm list) (fuel_mono_thm : thm) : thm list = + mk_result_case scrut gen_ret_branch + *) +fun mk_result_case (scrut : term) (gen_ret_branch : term -> term) : term = let - val thl = (CONJUNCTS o SPECL [fuel_var0, fuel_var1]) fuel_mono_thm - fun mk_least_fuel_thm (pred_def, mono_thm) : thm = - let - (* Retrieve the predicate, without the fuel *) - val pred_tm = (lhs o snd o strip_forall o concl) pred_def - val (pred_tm, args) = strip_comb pred_tm - val args = rev (tl (rev args)) - val pred_tm = list_mk_comb (pred_tm, args) - (* Add $LEAST *) - val least_pred_tm = mk_comb (least_tm, pred_tm) - (* Specialize all *) - val vars = (fst o strip_forall o concl) mono_thm - val th = SPECL vars mono_thm - (* Substitute in the mono theorem *) - val th = INST [fuel_var0 |-> least_pred_tm] th - (* Symmetrize the equality *) - val th = PURE_ONCE_REWRITE_RULE [EQ_SYM_EQ] th - (* Quantify *) - val th = GENL (fuel_var1 :: vars) th - in - th - end + val scrut_ty = dest_result (type_of scrut) + (* Return branch *) + val ret_var = genvar scrut_ty + val ret_pat = mk_return ret_var + val ret_br = gen_ret_branch ret_var + val ret_ty = dest_result (type_of ret_br) + (* Failure branch *) + val fail_var = genvar error_ty + val fail_pat = mk_fail scrut_ty fail_var + val fail_br = mk_fail ret_ty fail_var + (* Diverge branch *) + val div_pat = mk_diverge scrut_ty + val div_br = mk_diverge ret_ty in - map mk_least_fuel_thm (zip pred_defs thl) + unordered_mk_case (scrut, [(ret_pat, ret_br), (fail_pat, fail_br), (div_pat, div_br)]) end -(* -val (pred_def, mono_thm) = hd (zip pred_defs thl) -*) +(* Generate a ‘case ... of’ over a sum type. -(* Prove theorems of the shape: + Ex.: + ==== + If the scrutinee is: “x : 'a + 'b + 'c” (i.e., the tys list is: [“:'a”, “:b”, “:c”]), + we generate: {[ - !n i. even___P i n ==> $LEAST (even___P i) <= n + case x of + | INL y0 => ... (* Branch of index 0 *) + | INR (INL y1) => ... (* Branch of index 1 *) + | INR (INR (INL y2)) => ... (* Branch of index 2 *) + | INR (INR (INR y3)) => ... (* Branch of index 3 *) ]} - TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms) + The content of the branches is generated by the ‘gen_branch’ continuation, + which receives as input the index of the branch as well as the variable + introduced by the pattern (in the example above: ‘y0’ for the branch 0, + ‘y1’ for the branch 1, etc.) + + (* Debug *) + val tys = [“:'a”, “:'b”] + val scrut = mk_var ("x", sumSyntax.list_mk_sum tys) + fun gen_branch i (x : term) = “F” + + val tys = [“:'a”, “:'b”, “:'c”, “:'d”] + val scrut = mk_var ("x", sumSyntax.list_mk_sum tys) + fun gen_branch i (x : term) = if type_of x = “:'c” then mk_return x else mk_fail_failure “:'c” + + list_mk_sum_case scrut tys gen_branch *) -fun prove_least_pred_thms (pred_defs : thm list) : thm list = +(* For debugging *) +val list_mk_sum_case_case = ref (“T”, [] : (term * term) list) +(* +val (scrut, [(pat1, br1), (pat2, br2)]) = !list_mk_sum_case_case +*) +fun list_mk_sum_case (scrut : term) (tys : hol_type list) + (gen_branch : int -> term -> term) : term = let - fun prove_least_pred_thm (pred_def : thm) : thm = + (* Create the cases. Note that without sugar, the match actually looks like this: + {[ + case x of + | INL y0 => ... (* Branch of index 0 *) + | INR x1 + case x1 of + | INL y1 => ... (* Branch of index 1 *) + | INR x2 => + case x2 of + | INL y2 => ... (* Branch of index 2 *) + | INR y3 => ... (* Branch of index 3 *) + ]} + *) + fun create_case (j : int) (scrut : term) (tys : hol_type list) : term = let - val pred_tm = (lhs o snd o strip_forall o concl) pred_def - val (pred_no_fuel_tm, args) = strip_comb pred_tm - val args = rev (tl (rev args)) - val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args) - (* Make the “$LEAST (even___P i)” term *) - val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm) - (* Make the inequality *) - val tm = list_mk_comb (le_tm, [least_pred_tm, fuel_var0]) - (* Add the implication *) - val tm = mk_imp (pred_tm, tm) - (* Quantify *) - val tm = list_mk_forall (args, tm) - val tm = mk_forall (fuel_var0, tm) - (* Prove *) - val prove_tac = - rpt gen_tac >> - disch_tac >> - (* Use the "fundamental" property about $LEAST *) - qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >> - (* Prove the premise *) - pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >> - rw [] >> - (* Finish the proof by contraposition *) - spose_not_then assume_tac >> - fs [not_le_eq_gt] + val _ = print_dbg ("list_mk_sum_case: " ^ + String.concatWith ", " (map type_to_string tys) ^ "\n") in - save_goal_and_prove (tm, prove_tac) + case tys of + [] => failwith "tys is too short" + | [ ty ] => + (* Last element: no match to perform *) + gen_branch j scrut + | ty1 :: tys => + (* Not last: we create a pattern: + {[ + case scrut of + | INL pat_var1 => ... (* Branch of index i *) + | INR pat_var2 => + ... (* Generate this term recursively *) + ]} + *) + let + (* INL branch *) + val after_ty = sumSyntax.list_mk_sum tys + val pat_var1 = genvar ty1 + val pat1 = sumSyntax.mk_inl (pat_var1, after_ty) + val br1 = gen_branch j pat_var1 + (* INR branch *) + val pat_var2 = genvar after_ty + val pat2 = sumSyntax.mk_inr (pat_var2, ty1) + val br2 = create_case (j+1) pat_var2 tys + val _ = print_dbg ("list_mk_sum_case: assembling:\n" ^ + term_to_string scrut ^ ",\n" ^ + "[(" ^ term_to_string pat1 ^ ",\n " ^ term_to_string br1 ^ "),\n\n" ^ + " (" ^ term_to_string pat2 ^ ",\n " ^ term_to_string br2 ^ ")]\n\n") + val case_elems = (scrut, [(pat1, br1), (pat2, br2)]) + val _ = list_mk_sum_case_case := case_elems + in + (* Put everything together *) + TypeBase.mk_case case_elems + end end in - map prove_least_pred_thm pred_defs + create_case 0 scrut tys end +(* Generate a ‘case ... of’ to select the input/output of the ith variant of + the param enumeration. -(* -val least_pred_thms = prove_least_pred_thms pred_defs - -val least_pred_thm = hd least_pred_thms -*) - -(* Prove theorems of the shape: - + Ex.: + ==== + There are two functions in the group, and we select the input of the function of index 1: {[ - !n i. even___P i n ==> even___P i ($LEAST (even___P i)) + case x of + | INL _ => Fail Failure (* Input of function of index 0 *) + | INR (INL _) => Fail Failure (* Output of function of index 0 *) + | INR (INR (INL y)) => Return y (* Input of the function of index 1: select this one *) + | INR (INR (INR _)) => Fail Failure (* Output of the function of index 1 *) ]} -*) -fun prove_pred_n_imp_pred_least_thms (pred_defs : thm list) : thm list = - let - fun prove_pred_n_imp_pred_least (pred_def : thm) : thm = - let - val pred_tm = (lhs o snd o strip_forall o concl) pred_def - val (pred_no_fuel_tm, args) = strip_comb pred_tm - val args = rev (tl (rev args)) - val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args) - (* Make the “$LEAST (even___P i)” term *) - val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm) - (* Make the “even___P i ($LEAST (even___P i))” *) - val tm = subst [fuel_var0 |-> least_pred_tm] pred_tm - (* Add the implication *) - val tm = mk_imp (pred_tm, tm) - (* Quantify *) - val tm = list_mk_forall (args, tm) - val tm = mk_forall (fuel_var0, tm) - (* The proof tactic *) - val prove_tac = - rpt gen_tac >> - disch_tac >> - (* Use the "fundamental" property about $LEAST *) - qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >> - (* Prove the premise *) - pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >> - rw [] - in - save_goal_and_prove (tm, prove_tac) - end - in - map prove_pred_n_imp_pred_least pred_defs - end -(* -val (pred_def, mono_thm) = hd (zip pred_defs thl) -val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_defs fuel_mono_thm + (* Debug *) + val tys = [(“:'a”, “:'b”)] + val scrut = “x : 'a + 'b” + val fi = 0 + val is_input = true -val least_fuel_mono_thm = hd least_fuel_mono_thms -*) + val tys = [(“:'a”, “:'b”), (“:'c”, “:'d”)] + val scrut = “x : 'a + 'b + 'c + 'd” + val fi = 1 + val is_input = false -(* Define the "raw" definitions: + val scrut = mk_var ("x", sumSyntax.list_mk_sum (flatten tys)) - {[ - even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge - ]} + list_mk_case_select scrut tys fi is_input *) -fun define_raw_defs (def_tms : term list) (pred_defs : thm list) (fuel_defs : thm list) : thm list = +fun list_mk_case_sum_select (scrut : term) (tys : (hol_type * hol_type) list) + (fi : int) (is_input : bool) : term = let - fun define_raw_def (def_tm, (pred_def, fuel_def)) : thm = - let - val app = lhs def_tm - val pred_tm = (lhs o snd o strip_forall o concl) pred_def - (* Make the “?n. even___P i n” term *) - val exists_fuel_tm = mk_exists (fuel_var0, pred_tm) - (* Make the “even___fuel ($LEAST (even___P i)) i” term *) - val fuel_tm = (lhs o snd o strip_forall o concl) fuel_def - val (pred_tm, args) = strip_comb pred_tm - val args = rev (tl (rev args)) - val pred_tm = list_mk_comb (pred_tm, args) - val least_pred_tm = mk_comb (least_tm, pred_tm) - val fuel_tm = subst [fuel_var0 |-> least_pred_tm] fuel_tm - (* Create the Diverge term *) - val ret_ty = (hd o snd o dest_type) (type_of app) - (* Create the “if then else” *) - val body = TypeBase.mk_case (exists_fuel_tm, [(true_tm, fuel_tm), (false_tm, mk_diverge_tm ret_ty)]) - (* *) - val raw_def_tm = mk_eq (app, body) - in - Define ‘^raw_def_tm’ - end + (* The index of the element in the enumeration that we will select *) + val i = 2 * fi + (if is_input then 0 else 1) + (* Flatten the types and numerotate them *) + fun flatten ls = List.concat (map (fn (x, y) => [x, y]) ls) + val tys = flatten tys + (* Get the return type *) + val ret_ty = List.nth (tys, i) + (* The continuation which will generate the content of the branches *) + fun gen_branch j var = if j = i then mk_return var else mk_fail_failure ret_ty in - map define_raw_def (zip def_tms (zip pred_defs fuel_defs)) + (* Generate the ‘case ... of’ *) + list_mk_sum_case scrut tys gen_branch end -(* -val raw_defs = define_raw_defs def_tms pred_defs fuel_defs +(* Generate a ‘case ... of’ to select the input/output of the ith variant of + the param enumeration. + + Ex.: + ==== + There are two functions in the group, and we select the input of the function of index 1: + {[ + case x of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + case r of + | INL _ => Fail Failure (* Input of function of index 0 *) + | INR (INL _) => Fail Failure (* Output of function of index 0 *) + | INR (INR (INL y)) => Return y (* Input of the function of index 1: select this one *) + | INR (INR (INR _)) => Fail Failure (* Output of the function of index 1 *) + ]} *) +fun mk_case_select_result_sum (scrut : term) (tys : (hol_type * hol_type) list) + (fi : int) (is_input : bool) : term = + (* We match over the result, then over the enumeration *) + mk_result_case scrut (fn x => list_mk_case_sum_select x tys fi is_input) -(* Prove theorems of the shape: +(* Generate a body for the fixed-point operator from a quoted group of mutually + recursive definitions. - !n i. even___P i n ==> even___fuel n i = even i + See TODO for detailed explanations: from the quoted equations for ‘nth’ + (or for [‘even’, ‘odd’]) we generate the body ‘nth_body’ (or ‘even_odd_body’, + respectively). *) -fun prove_pred_imp_fuel_eq_raw_defs - (pred_defs : thm list) - (fuel_def_tms : term list) - (least_fuel_mono_thms : thm list) - (least_pred_thms : thm list) - (pred_n_imp_pred_least_thms : thm list) - (raw_defs : thm list) : - thm list = +fun mk_body (fnames : string list) (in_out_tys : (hol_type * hol_type) list) + (def_tms : term list) : term = let - fun prove_thm (pred_def, - (fuel_def_tm, - (least_fuel_mono_thm, - (least_pred_thm, - (pred_n_imp_pred_least_thm, raw_def))))) : thm = - let - (* Generate: “even___P i n” *) - val pred_tm = (lhs o snd o strip_forall o concl) pred_def - val (pred_no_fuel_tm, args) = strip_comb pred_tm - val args = rev (tl (rev args)) - (* Generate: “even___fuel n i” *) - val fuel_tm = lhs fuel_def_tm - (* Generate: “even i” *) - val raw_def_tm = (lhs o snd o strip_forall o concl) raw_def - (* Generate: “even___fuel n i = even i” *) - val tm = mk_eq (fuel_tm, raw_def_tm) - (* Add the implication *) - val tm = mk_imp (pred_tm, tm) - (* Quantify *) - val tm = list_mk_forall (args, tm) - val tm = mk_forall (fuel_var0, tm) - (* Prove *) - val prove_tac = - rpt gen_tac >> - strip_tac >> - fs raw_defs >> - (* Case on ‘?n. even___P i n’ *) - CASE_TAC >> fs [] >> - (* Use the monotonicity property *) - irule least_fuel_mono_thm >> - imp_res_tac pred_n_imp_pred_least_thm >> fs [] >> - irule least_pred_thm >> fs [] - in - save_goal_and_prove (tm, prove_tac) - end - in - map prove_thm (zip pred_defs (zip fuel_def_tms (zip least_fuel_mono_thms - (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_defs))))) - end + val fnames_set = Redblackset.fromList String.compare fnames + + (* Compute a map from function name to function index *) + val fnames_map = Redblackmap.fromList String.compare + (map (fn (x, y) => (y, x)) (enumerate fnames)) + + (* Compute the input/output type, that we dub the "parameter type" *) + fun flatten ls = List.concat (map (fn (x, y) => [x, y]) ls) + val param_type = sumSyntax.list_mk_sum (flatten in_out_tys) + + (* Introduce a variable for the confinuation *) + val fcont = genvar (param_type --> mk_result param_type) + + (* In the function equations, replace all the recursive calls with calls to the continuation. + + When replacing a recursive call, we have to do two things: + - we need to inject the input parameters into the parameter type + Ex.: + - ‘nth tl i’ becomes ‘f (INL (tl, i))’ where ‘f’ is the continuation + - ‘even i’ becomes ‘f (INL i)’ where ‘f’ is the continuation + - we need to wrap the the call to the continuation into a ‘case ... of’ + to extract its output (we need to make sure that the transformation + preserves the type of the expression!) + Ex.: ‘nth tl i’ becomes: + {[ + case f (INL (tl, i)) of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + case r of + | INL _ => Fail Failure + | INR x => Return (INR x) + ]} + *) + (* For debugging *) + val replace_rec_calls_rec_call_tm = ref “T” + fun replace_rec_calls (fnames_set : string Redblackset.set) (tm : term) : term = + let + val _ = print_dbg ("replace_rec_calls: original expression:\n" ^ + term_to_string tm ^ "\n\n") + val ntm = + case dest_term tm of + VAR (name, ty) => + (* Check that this is not one of the functions in the group - remark: + we could handle that by introducing lambdas. + *) + if Redblackset.member (fnames_set, name) + then failwith ("mk_body: not well-formed definition: found " ^ name ^ + " in an improper position") + else tm + | CONST _ => tm + | LAMB (x, tm) => + let + (* The variable might shadow one of the functions *) + val fnames_set = Redblackset.delete (fnames_set, (fst o dest_var) x) + (* Update the term in the lambda *) + val tm = replace_rec_calls fnames_set tm + in + (* Reconstruct *) + mk_abs (x, tm) + end + | COMB (_, _) => + let + (* Completely destruct the application, check if this is a recursive call *) + val (app, args) = strip_comb tm + val is_rec_call = Redblackset.member (fnames_set, (fst o dest_var) app) + handle HOL_ERR _ => false + (* Whatever the case, apply the transformation to all the inputs *) + val args = map (replace_rec_calls fnames_set) args + in + (* If this is not a recursive call: apply the transformation to all the + terms. Otherwise, replace. *) + if not is_rec_call then list_mk_comb (replace_rec_calls fnames_set app, args) + else + (* Rec call: replace *) + let + val _ = replace_rec_calls_rec_call_tm := tm + (* First, find the index of the function *) + val fname = (fst o dest_var) app + val fi = Redblackmap.find (fnames_map, fname) + (* Inject the input values into the param type *) + val input = pairSyntax.list_mk_pair args + val input = inject_in_param_sum in_out_tys fi true input + (* Create the recursive call *) + val call = mk_comb (fcont, input) + (* Wrap the call into a ‘case ... of’ to extract the output *) + val call = mk_case_select_result_sum call in_out_tys fi false + in + (* Return *) + call + end + end + val _ = print_dbg ("replace_rec_calls: new expression:\n" ^ term_to_string ntm ^ "\n\n") + in + ntm + end + handle HOL_ERR e => + let + val _ = print_dbg ("replace_rec_calls: failed on:\n" ^ term_to_string tm ^ "\n\n") + in + raise (HOL_ERR e) + end + fun replace_rec_calls_in_eq (eq : term) : term = + let + val (l, r) = dest_eq eq + in + mk_eq (l, replace_rec_calls fnames_set r) + end + val def_tms_with_fcont = map replace_rec_calls_in_eq def_tms -(* -val pred_imp_fuel_eq_raw_defs = - prove_pred_imp_fuel_eq_raw_defs - pred_defs fuel_def_tms least_fuel_mono_thms least_pred_thms - pred_n_imp_pred_least_thms raw_defs - *) + (* Wrap all the function bodies to inject their result into the param type. + We collect the function inputs at the same time, because they will be + grouped into a tuple that we will have to deconstruct. + *) + fun inject_body_to_enums (i : int, def_eq : term) : term list * term = + let + val (l, body) = dest_eq def_eq + val (_, args) = strip_comb l + (* We have the deconstruct the result, then, in the ‘Return’ branch, + properly wrap the returned value *) + val body = mk_result_case body (fn x => mk_return (inject_in_param_sum in_out_tys i false x)) + in + (args, body) + end + val def_tms_inject = map inject_body_to_enums (enumerate def_tms_with_fcont) -(* Generate "expand" definitions of the following shape (we use them to - hide the raw function bodies, to control the rewritings): + (* Currify the body inputs. - {[ - even___expand even odd i : bool result = - if i = 0 then Return T else odd (i - 1) - ]} + For instance, if the body has inputs: ‘x’, ‘y’; we return the following: + {[ + (‘z’, ‘case z of (x, y) => ... (* body *) ’) + ]} + where ‘z’ is fresh. - {[ - odd___expand even odd i : bool result = - if i = 0 then Return F else even (i - 1) - ]} + We return: (curried input, body). - *) -fun gen_expand_defs (def_tms : term list) = - let - (* Generate the variables for “even”, “odd”, etc. *) - val fun_vars = map (fst o strip_comb o lhs) def_tms - val fun_tys = map type_of fun_vars - (* Generate the expansion *) - fun mk_def (def_tm : term) : thm = - let - val (exp_fun, args) = (strip_comb o lhs) def_tm - val (exp_fun_str, exp_fun_ty) = dest_var exp_fun - val exp_fun_str = exp_fun_str ^ expand_suffix - val exp_fun_ty = list_mk_arrow fun_tys exp_fun_ty - val exp_fun = mk_var (exp_fun_str, exp_fun_ty) - val exp_fun = list_mk_comb (exp_fun, fun_vars) - val exp_fun = list_mk_comb (exp_fun, args) - val tm = mk_eq (exp_fun, rhs def_tm) - in - Define ‘^tm’ - end + (* Debug *) + val body = “(x:'a, y:'b, z:'c)” + val args = [“x:'a”, “y:'b”, “z:'c”] + currify_body_inputs (args, body) + *) + fun currify_body_inputs (args : term list, body : term) : term * term = + let + fun mk_curry (args : term list) (body : term) : term * term = + case args of + [] => failwith "no inputs" + | [x] => (x, body) + | x1 :: args => + let + val (x2, body) = mk_curry args body + val scrut = genvar (pairSyntax.list_mk_prod (map type_of (x1 :: args))) + val pat = pairSyntax.mk_pair (x1, x2) + val br = body + in + (scrut, TypeBase.mk_case (scrut, [(pat, br)])) + end + in + mk_curry args body + end + val def_tms_currified = map currify_body_inputs def_tms_inject + + (* Group all the functions into a single body, with an outer ‘case .. of’ + which selects the appropriate body depending on the input *) + val param_ty = sumSyntax.list_mk_sum (flatten in_out_tys) + val input = genvar param_ty + fun mk_mut_rec_body_branch (i : int) (patvar : term) : term = + (* Case disjunction on whether the branch is for an input value (in + which case we call the proper body) or an output value (in which + case we return ‘Fail ...’ *) + if i mod 2 = 0 then + let + val fi = i div 2 + val (x, def_tm) = List.nth (def_tms_currified, fi) + (* The variable in the pattern and the variable expected by the + body may not be the same: we introduce a let binding *) + val def_tm = mk_let (mk_abs (x, def_tm), patvar) + in + def_tm + end + else + (* Output value: fail *) + mk_fail_failure param_ty + val mut_rec_body = list_mk_sum_case input (flatten in_out_tys) mk_mut_rec_body_branch + + + (* Abstract away the parameters to produce the final body of the fixed point *) + val mut_rec_body = list_mk_abs ([fcont, input], mut_rec_body) in - map mk_def def_tms + mut_rec_body end -(* -val def_tm = hd def_tms +(*=============================================================================* + * + * Prove that the body satisfies the validity condition + * + * ============================================================================*) -val expand_defs = gen_expand_defs def_tms -*) - -(* Small utility: - - Return the list: - {[ - (“even___P i n”, “even i = even___expand even odd i”), - ... - ]} - - *) -fun mk_termination_diverge_tms - (def_tms : term list) - (pred_defs : thm list) - (raw_defs : thm list) - (expand_defs : thm list) : - (term * term) list = +(* Tactic to prove that a body is valid: perform one step. *) +fun prove_body_is_valid_tac_step (asms, g) = let - (* Create the substitution for the "expand" functions: + (* The goal has the shape: {[ - even -> even - odd -> odd - ... - ]} - - where on the left we have *variables* and on the right we have - the "raw" definitions. + (∀g h. ... g x = ... h x) ∨ + ∃h y. is_valid_fp_body n h ∧ ∀g. ... g x = ... od + ]} + *) + (* Retrieve the scrutinee in the goal (‘x’). + There are two cases: + - either the function has the shape: + {[ + (λ(y,z). ...) x + ]} + in which case we need to destruct ‘x’ + - or we have a normal ‘case ... of’ *) - fun mk_fun_subst (def_tm, raw_def) = + val body = (lhs o snd o strip_forall o fst o dest_disj) g + val scrut = let - val var = (fst o strip_comb o lhs) def_tm - val f = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def + val (app, x) = dest_comb body + val (app, _) = dest_comb app + val {Name=name, Thy=thy, Ty = _ } = dest_thy_const app in - (var |-> f) + if thy = "pair" andalso name = "UNCURRY" then x else failwith "not a curried argument" end - val fun_subst = map mk_fun_subst (zip def_tms raw_defs) - - fun mk_tm (pred_def, (raw_def, expand_def)) : - term * term = + handle HOL_ERR _ => strip_all_cases_get_scrutinee body + (* Retrieve the first quantified continuations from the goal (‘g’) *) + val qc = (hd o fst o strip_forall o fst o dest_disj) g + (* Check if the scrutinee is a recursive call *) + val (scrut_app, _) = strip_comb scrut + val _ = print_dbg ("prove_body_is_valid_step: Scrutinee: " ^ term_to_string scrut ^ "\n") + (* For the recursive calls: *) + fun step_rec () = let - (* “even___P i n” *) - val pred_tm = (lhs o snd o strip_forall o concl) pred_def - (* “even i = even___expand even odd i” *) - val expand_tm = (lhs o snd o strip_forall o concl) expand_def - val expand_tm = subst fun_subst expand_tm - val fun_tm = (lhs o snd o strip_forall o concl) raw_def - val fun_eq_tm = mk_eq (fun_tm, expand_tm) - in (pred_tm, fun_eq_tm) end + val _ = print_dbg ("prove_body_is_valid_step: rec call\n") + (* We need to instantiate the ‘h’ existantially quantified function *) + (* First, retrieve the body of the function: it is given by the ‘Return’ branch *) + val (_, _, branches) = TypeBase.dest_case body + (* Find the branch corresponding to the return *) + val ret_branch = List.find (fn (pat, _) => + let + val {Name=name, Thy=thy, Ty = _ } = (dest_thy_const o fst o strip_comb) pat + in + thy = "primitives" andalso name = "Return" + end) branches + val var = (hd o snd o strip_comb o fst o valOf) ret_branch + val br = (snd o valOf) ret_branch + (* Abstract away the input variable introduced by the pattern and the continuation ‘g’ *) + val h = list_mk_abs ([qc, var], br) + val _ = print_dbg ("prove_body_is_valid_step: h: " ^ term_to_string h ^ "\n") + (* Retrieve the input parameter ‘x’ *) + val input = (snd o dest_comb) scrut + val _ = print_dbg ("prove_body_is_valid_step: y: " ^ term_to_string input ^ "\n") + in + ((* Choose the right possibility (this is a recursive call) *) + disj2_tac >> + (* Instantiate the quantifiers *) + qexists ‘^h’ >> + qexists ‘^input’ >> + (* Unfold the predicate once *) + pure_once_rewrite_tac [is_valid_fp_body_def] >> + (* We have two subgoals: + - we have to prove that ‘h’ is valid + - we have to finish the proof of validity for the current body + *) + conj_tac >> fs [case_result_switch_eq]) + end in - map mk_tm (zip pred_defs (zip raw_defs expand_defs)) + (* If recursive call: special treatment. Otherwise, we do a simple disjunction *) + (if term_eq scrut_app qc then step_rec () + else (Cases_on ‘^scrut’ >> fs [case_result_switch_eq])) (asms, g) end -(* -val term_div_tms = - mk_termination_diverge_tms pred_defs raw_defs expand_defs -*) +(* Tactic to prove that a body is valid *) +fun prove_body_is_valid_tac (body_def : thm option) : tactic = + let val body_def_thm = case body_def of SOME th => [th] | NONE => [] + in + pure_once_rewrite_tac [is_valid_fp_body_def] >> gen_tac >> + (* Expand *) + fs body_def_thm >> + fs [bind_def, case_result_switch_eq] >> + (* Explore the body *) + rpt prove_body_is_valid_tac_step + end -(* Prove the termination lemmas: - - {[ - !i. - (?n. even___P i n) ==> - even i = even___expand even odd i - ]} - *) -fun prove_termination_thms - (term_div_tms : (term * term) list) - (fuel_defs : thm list) - (pred_defs : thm list) - (raw_defs : thm list) - (expand_defs : thm list) - (pred_n_imp_pred_least_thms : thm list) - (pred_imp_fuel_eq_raw_defs : thm list) - : thm list = +(* Prove that a body satisfies the validity condition of the fixed point *) +fun prove_body_is_valid (body : term) : thm = let - (* Create a map from functions in the recursive group to lemmas - to apply *) - fun mk_rec_fun_eq_pair (fuel_def, eq_th) = - let - val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def - in - (rfun, eq_th) - end - val rec_fun_eq_map = - Redblackmap.fromList const_name_compare ( - map mk_rec_fun_eq_pair - (zip fuel_defs pred_imp_fuel_eq_raw_defs)) - - (* Small tactic which rewrites the recursive calls *) - fun rewrite_rec_call (asms, g) = - let - val scrut = (strip_all_cases_get_scrutinee o lhs) g - val fun_id = get_fun_name_from_app scrut (* This can fail *) - (* This can raise an exception - hence the handle at the end - of the function *) - val eq_th = Redblackmap.find (rec_fun_eq_map, fun_id) - val eq_th = (UNDISCH_ALL o SPEC_ALL) eq_th - (* Match the theorem *) - val eq_th_tm = (lhs o concl) eq_th - val (var_s, ty_s) = match_term eq_th_tm scrut - val eq_th = INST var_s (INST_TYPE ty_s eq_th) - val eq_th = thm_to_conj_implies eq_th - (* Some tactics *) - val premise_tac = fs pred_defs >> fs [is_diverge_def] - in - (* Apply the theorem, prove the premise, and rewrite *) - (prove_premise_then premise_tac assume_tac eq_th >> fs []) (asms, g) - end handle NotFound => all_tac (asms, g) - | HOL_ERR _ => all_tac (asms, g) (* Getting the function name can also fail *) - - fun prove_one ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) : - thm = - let - (* “?n. even___P i n” *) - val pred_tm = mk_exists (fuel_var0, pred_tm) - (* “even i = even___expand even odd i” *) - val tm = fun_eq_tm - (* Add the implication *) - val tm = mk_imp (pred_tm, tm) - (* Quantify *) - val (_, args) = strip_comb (lhs fun_eq_tm) - val tm = list_mk_forall (args, tm) - - (* Prove *) - val prove_tac = - rpt gen_tac >> - disch_tac >> - - (* Expand the raw definition and get rid of the ‘?n ...’ *) - pure_once_rewrite_tac raw_defs >> - pure_asm_rewrite_tac [] >> - - (* Simplify *) - fs [] >> - - (* Prove that: “even___P i $(LEAST ...)” *) - imp_res_tac pred_n_imp_pred_least_thm >> - - (* We don't need the ‘even___P i n’ assumption anymore: we have a more - precise one with the least upper bound *) - last_x_assum ignore_tac >> - - (* Expand *) - fs pred_defs >> - fs [is_diverge_def] >> - fs expand_defs >> - - (* We need to be a bit careful when expanding the definitions which use fuel: - it can make the simplifier loop. *) - rpt (pop_assum mp_tac) >> - pure_once_rewrite_tac fuel_defs >> - rpt disch_tac >> + (* Explore the body and count the number of occurrences of nested recursive + calls so that we can properly instantiate the ‘N’ argument of ‘is_valid_fp_body’. + + We first retrieve the name of the continuation parameter. + Rem.: we generated fresh names so that, for instance, the continuation name + doesn't collide with other names. Because of this, we don't need to look for + collisions when exploring the body (and in the worst case, we would cound + an overapproximation of the number of recursive calls, which is perfectly + valid). + *) + val fcont = (hd o fst o strip_abs) body + val fcont_name = (fst o dest_var) fcont + fun max x y = if x > y then x else y + fun count_body_rec_calls (body : term) : int = + case dest_term body of + VAR (name, _) => if name = fcont_name then 1 else 0 + | CONST _ => 0 + | COMB (x, y) => max (count_body_rec_calls x) (count_body_rec_calls y) + | LAMB (_, x) => count_body_rec_calls x + val num_rec_calls = count_body_rec_calls body + + (* Generate the term ‘SUC (SUC ... (SUC n))’ where ‘n’ is a fresh variable. + + Remark: we first prove ‘is_valid_fp_body (SUC ... n) body’ then substitue + ‘n’ with ‘0’ to prevent the quantity from being rewritten to a bit + representation, which would prevent unfolding of the ‘is_valid_fp_body’. + *) + val nvar = genvar num_ty + (* Rem.: we stack num_rec_calls + 1 occurrences of ‘SUC’ (and the + 1 is important) *) + fun mk_n i = if i = 0 then mk_suc nvar else mk_suc (mk_n (i-1)) + val n_tm = mk_n num_rec_calls - (* Expand the binds *) - fs [bind_def, case_result_same_eq] >> + (* Generate the lemma statement *) + val is_valid_tm = list_mk_icomb (is_valid_fp_body_tm, [n_tm, body]) + val is_valid_thm = prove (is_valid_tm, prove_body_is_valid_tac NONE) - (* Explore all the paths by doing case disjunctions *) - rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq]) - in - save_goal_and_prove (tm, prove_tac) - end + (* Replace ‘nvar’ with ‘0’ *) + val is_valid_thm = INST [nvar |-> zero_num_tm] is_valid_thm in - map prove_one - (zip term_div_tms pred_n_imp_pred_least_thms) + is_valid_thm end -(* -val termination_thms = - prove_termination_thms term_div_tms fuel_defs pred_defs - raw_defs expand_defs pred_n_imp_pred_least_thms - pred_imp_fuel_eq_raw_defs - -val ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) = hd (zip term_div_tms pred_n_imp_pred_least_thms) -set_goal ([], tm) -*) - -(* Prove the divergence lemmas: - - {[ - !i. - (!n. ~even___P i n) ==> - (!n. ~even___P i (SUC n)) ==> - even i = even___expand even odd i - ]} +(*=============================================================================* + * + * Generate the definitions with the fixed-point operator + * + * ============================================================================*) - Note that the shape of the theorem is very precise: this helps for the proof. - Also, by correctly ordering the assumptions, we make sure that by rewriting - we don't convert one of the two to “T”. - *) -fun prove_divergence_thms - (term_div_tms : (term * term) list) - (fuel_defs : thm list) - (pred_defs : thm list) - (raw_defs : thm list) - (expand_defs : thm list) - : thm list = +(* Generate the raw definitions by using the grouped definition body and the + fixed point operator *) +fun mk_raw_defs (in_out_tys : (hol_type * hol_type) list) + (def_tms : term list) (body_is_valid : thm) : thm list = let - (* Create a set containing the names of all the functions in the recursive group *) - fun get_rec_fun_id (fuel_def : thm) = - (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def - val rec_fun_set = - Redblackset.fromList const_name_compare ( - map get_rec_fun_id raw_defs) - - (* Small tactic which rewrites the recursive calls *) - fun rewrite_rec_call (asms, g) = - let - val scrut = (strip_all_cases_get_scrutinee o lhs) g - val fun_id = get_fun_name_from_app scrut (* This can fail *) - in - (* Check if the function is part of the group we are considering *) - if Redblackset.member (rec_fun_set, fun_id) then - let - (* Create a subgoal “odd i = Diverge” *) - val ret_ty = (hd o snd o dest_type o type_of) scrut - val g = mk_eq (scrut, mk_diverge_tm ret_ty) - - (* Create a subgoal: “?n. odd___P i n”. - - It is a bit cumbersome because we have to lookup the proper - predicate (from “odd” we need to lookup “odd___P”) and we - may have to perform substitutions... We hack a bit by using - a conversion to rewrite “odd i” to a term which contains - the “?n. odd___P i n” we are looking for. - *) - val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs scrut) - val (_, exists_g, _) = TypeBase.dest_case exists_g - (* The tactic to prove the subgoal *) - val prove_sg_tac = - pure_rewrite_tac raw_defs >> - Cases_on ‘^exists_g’ >> pure_asm_rewrite_tac [] >> fs [] >> - (* There must only remain the positive case (i.e., “?n. ...”): - we have a contradiction *) - exfalso >> - (* The end of the proof is done by opening the definitions *) - pop_assum mp_tac >> - fs pred_defs >> fs [is_diverge_def] - in - (SUBGOAL_THEN g assume_tac >- prove_sg_tac >> fs []) (asms, g) - end - else all_tac (asms, g) (* Nothing to do *) - end handle HOL_ERR _ => all_tac (asms, g) - - fun prove_one (pred_tm, fun_eq_tm) : - thm = - let - (* “!n. ~even___P i n” *) - val neg_pred_tm = mk_neg pred_tm - val pred_tm = mk_forall (fuel_var0, neg_pred_tm) - val pred_suc_tm = subst [fuel_var0 |-> numSyntax.mk_suc fuel_var0] neg_pred_tm - val pred_suc_tm = mk_forall (fuel_var0, pred_suc_tm) - - (* “even i = even___expand even odd i” *) - val tm = fun_eq_tm + (* Retrieve the body *) + val body = (List.last o snd o strip_comb o concl) body_is_valid - (* Add the implications *) - val tm = list_mk_imp ([pred_tm, pred_suc_tm], tm) + (* Create the term ‘fix body’ *) + val fixed_body = mk_icomb (fix_tm, body) - (* Quantify *) - val (_, args) = strip_comb (lhs fun_eq_tm) - val tm = list_mk_forall (args, tm) + (* For every function in the group, generate the equation that we will + use as definition. In particular: + - add the properly injected input ‘x’ to ‘fix body’ (ex.: for ‘nth ls i’ + we add the input ‘INL (ls, i)’) + - wrap ‘fix body x’ into a case disjunction to extract the relevant output - (* Prove *) - val prove_tac = - rpt gen_tac >> - - pure_rewrite_tac raw_defs >> - rpt disch_tac >> + For instance, in the case of ‘nth ls i’: + {[ + nth (ls : 't list_t) (i : u32) = + case fix nth_body (INL (ls, i)) of + | Fail e => Fail e + | Diverge => Diverge + | Return r => + case r of + | INL _ => Fail Failure + | INR x => Return x + ]} + *) + fun mk_def_eq (i : int, def_tm : term) : term = + let + (* Retrieve the lhs of the original definition equation, and in + particular the inputs *) + val def_lhs = lhs def_tm + val args = (snd o strip_comb) def_lhs - (* This allows to simplify the “?n. even___P i n” *) - fs [] >> - (* We don't need the last assumption anymore *) - last_x_assum ignore_tac >> + (* Inject the inputs into the param type *) + val input = pairSyntax.list_mk_pair args + val input = inject_in_param_sum in_out_tys i true input - (* Expand *) - fs pred_defs >> fs [is_diverge_def] >> - fs expand_defs >> + (* Compose*) + val def_rhs = mk_comb (fixed_body, input) - (* We need to be a bit careful when expanding the definitions which use fuel: - it can make the simplifier loop. - *) - pop_assum mp_tac >> - pure_once_rewrite_tac fuel_defs >> - rpt disch_tac >> fs [bind_def, case_result_same_eq] >> + (* Wrap in the case disjunction *) + val def_rhs = mk_case_select_result_sum def_rhs in_out_tys i false - (* Evaluate all the paths *) - rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq]) + (* Create the equation *) + val def_eq_tm = mk_eq (def_lhs, def_rhs) in - save_goal_and_prove (tm, prove_tac) + def_eq_tm end + val raw_def_tms = map mk_def_eq (enumerate def_tms) + + (* Generate the definitions *) + val raw_defs = map (fn tm => Define ‘^tm’) raw_def_tms in - map prove_one term_div_tms + raw_defs end -(* -val (pred_tm, fun_eq_tm) = hd term_div_tms -set_goal ([], tm) - -val divergence_thms = - prove_divergence_thms - term_div_tms - fuel_defs - pred_defs - raw_defs - expand_defs -*) +(*=============================================================================* + * + * Prove that the definitions satisfy the target equations + * + * ============================================================================*) -(* Prove the final lemmas: +(* Tactic which makes progress in a proof by making a case disjunction (we use + this to explore all the paths in a function body). *) +fun case_progress (asms, g) = + let + val scrut = (strip_all_cases_get_scrutinee o lhs) g + in Cases_on ‘^scrut’ (asms, g) end - {[ - !i. even i = even___expand even odd i - ]} +(* Prove the final equation, that we will use as definition. *) +fun prove_def_eq_tac + (current_raw_def : thm) (all_raw_defs : thm list) (is_valid : thm) + (body_def : thm option) : tactic = + let + val body_def_thm = case body_def of SOME th => [th] | NONE => [] + in + rpt gen_tac >> + (* Expand the definition *) + pure_once_rewrite_tac [current_raw_def] >> + (* Use the fixed-point equality *) + pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq is_valid] >> + (* Expand the body definition *) + pure_rewrite_tac body_def_thm >> + (* Expand all the definitions from the group *) + pure_rewrite_tac all_raw_defs >> + (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *) + fs [bind_def] >> + rpt (case_progress >> fs []) + end - Note that the shape of the theorem is very precise: this helps for the proof. - Also, by correctly ordering the assumptions, we make sure that by rewriting - we don't convert one of the two to “T”. - *) -fun prove_final_eqs - (term_div_tms : (term * term) list) - (termination_thms : thm list) - (divergence_thms : thm list) - (raw_defs : thm list) - : thm list = +(* Prove the final equations that we will give to the user as definitions *) +fun prove_def_eqs (body_is_valid : thm) (def_tms : term list) (raw_defs : thm list) : thm list= let - fun prove_one ((pred_tm, fun_eq_tm), (termination_thm, divergence_thm)) : thm = + val defs_tgt_raw = zip def_tms raw_defs + (* Substitute the function variables with the constants introduced in the raw + definitions *) + fun compute_fsubst (def_tm, raw_def) : {redex: term, residue: term} = + let + val (fvar, _) = (strip_comb o lhs) def_tm + val fconst = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def + in + (fvar |-> fconst) + end + val fsubst = map compute_fsubst defs_tgt_raw + val defs_tgt_raw = map (fn (x, y) => (subst fsubst x, y)) defs_tgt_raw + + fun prove_def_eq (def_tm, raw_def) : thm = let - val (_, args) = strip_comb (lhs fun_eq_tm) - val g = list_mk_forall (args, fun_eq_tm) - (* We make a case disjunction of the subgoal: “exists n. even___P i n” *) - val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs (lhs fun_eq_tm)) - val (_, exists_g, _) = TypeBase.dest_case exists_g - val prove_tac = - rpt gen_tac >> - Cases_on ‘^exists_g’ - >-( (* Termination *) - irule termination_thm >> pure_asm_rewrite_tac []) - (* Divergence *) - >> irule divergence_thm >> fs [] - + (* Quantify the parameters *) + val (_, params) = (strip_comb o lhs) def_tm + val def_eq_tm = list_mk_forall (params, def_tm) + (* Prove *) + val def_eq = prove (def_eq_tm, prove_def_eq_tac raw_def raw_defs body_is_valid NONE) in - save_goal_and_prove (g, prove_tac) - end + def_eq + end + val def_eqs = map prove_def_eq defs_tgt_raw in - map prove_one (zip term_div_tms (zip termination_thms divergence_thms)) + def_eqs end -(* -val termination_thm = hd termination_thms -val divergence_thm = hd divergence_thms -set_goal ([], g) -*) +(*=============================================================================* + * + * The final DefineDiv function + * + * ============================================================================*) -(* The final function: define potentially diverging functions in an error monad *) fun DefineDiv (def_qt : term quotation) = let - (* Parse the definitions. - - Example: - {[ - (even (i : int) : bool result = if i = 0 then Return T else odd (i - 1)) /\ - (odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)) - ]} - *) + (* Parse the definitions *) val def_tms = (strip_conj o list_mk_conj o rev) (Defn.parse_quote def_qt) - (* Generate definitions which use some fuel - - Example: - {[ - even___fuel n i = - case fuel of - 0 => Diverge - | SUC fuel => - if i = 0 then Return T else odd_fuel (i - 1)) - ]} - *) - val fuel_defs = mk_fuel_defs def_tms - - (* Generate the predicate definitions. - - {[ even___P n i = = ~is_diverge (even___fuel n i) ]} - *) - val fuel_def_tms = map (snd o strip_forall o concl) fuel_defs - val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms) - - (* Prove the monotonicity property for the fuel, all at once - - *) - val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs - - (* Prove the individual fuel functions - TODO: update - - {[ - !n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i - ]} - *) - val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_mono_thm - - (* - {[ - !n i. even___P i n ==> $LEAST (even___P i) <= n - ]} - *) - val least_pred_thms = prove_least_pred_thms pred_defs - - (* - {[ - !n i. even___P i n ==> even___P i ($LEAST (even___P i)) - ]} - *) - val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_defs - - (* - "Raw" definitions: - - {[ - even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge - ]} - *) - val raw_defs = define_raw_defs def_tms pred_defs fuel_defs - - (* - !n i. even___P i n ==> even___fuel n i = even i - *) - val pred_imp_fuel_eq_raw_defs = - prove_pred_imp_fuel_eq_raw_defs - pred_defs fuel_def_tms least_fuel_mono_thms - least_pred_thms pred_n_imp_pred_least_thms raw_defs - - (* "Expand" definitions *) - val expand_defs = gen_expand_defs def_tms - - (* Small utility *) - val term_div_tms = mk_termination_diverge_tms def_tms pred_defs raw_defs expand_defs - - (* Termination theorems *) - val termination_thms = - prove_termination_thms term_div_tms fuel_defs pred_defs - raw_defs expand_defs pred_n_imp_pred_least_thms pred_imp_fuel_eq_raw_defs + (* Compute the names and the input/output types of the functions *) + fun compute_names_in_out_tys (tm : term) : string * (hol_type * hol_type) = + let + val app = lhs tm + val name = (fst o dest_var o fst o strip_comb) app + val out_ty = dest_result (type_of app) + val input_tys = pairSyntax.list_mk_prod (map type_of ((snd o strip_comb) app)) + in + (name, (input_tys, out_ty)) + end + val (fnames, in_out_tys) = unzip (map compute_names_in_out_tys def_tms) - (* Divergence theorems *) - val divergence_thms = - prove_divergence_thms term_div_tms fuel_defs pred_defs raw_defs expand_defs + (* Generate the body to give to the fixed-point operator *) + val body = mk_body fnames in_out_tys def_tms - (* Final theorems: + (* Prove that the body satisfies the validity property required by the fixed point *) + val body_is_valid = prove_body_is_valid body + + (* Generate the definitions for the various functions by using the fixed point + and the body *) + val raw_defs = mk_raw_defs in_out_tys def_tms body_is_valid - {[ - ∀i. even i = even___E even odd i, - ⊢ ∀i. odd i = odd___E even odd i - ]} - *) - val final_eqs = prove_final_eqs term_div_tms termination_thms divergence_thms raw_defs - val final_eqs = map (PURE_REWRITE_RULE expand_defs) final_eqs + (* Prove the final equations *) + val def_eqs = prove_def_eqs body_is_valid def_tms raw_defs in - (* We return the final equations, which act as rewriting theorems *) - final_eqs + def_eqs end end diff --git a/backends/hol4/divDefLibExampleScript.sml b/backends/hol4/divDefLibExampleScript.sml new file mode 100644 index 00000000..c4a57783 --- /dev/null +++ b/backends/hol4/divDefLibExampleScript.sml @@ -0,0 +1,29 @@ +(* Examples which use divDefLib.DefineDiv *) + +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib +open divDefTheory divDefLib + +val [even_def, odd_def] = DefineDiv ‘ + (even (i : int) : bool result = + if i = 0 then Return T else odd (i - 1)) /\ + (odd (i : int) : bool result = + if i = 0 then Return F else even (i - 1)) +’ + +val [nth_def] = DefineDiv ‘ + 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 +’ diff --git a/backends/hol4/divDefNoFixLib.sig b/backends/hol4/divDefNoFixLib.sig new file mode 100644 index 00000000..eefc6ff7 --- /dev/null +++ b/backends/hol4/divDefNoFixLib.sig @@ -0,0 +1,99 @@ +(* **DEPRECATED**: see divDefLib + + This library defines an older version of DefineDiv, which doesn't use + fixed-point operator and thus relies on more complex meta functions. + + Define a (group of mutually recursive) function(s) which uses an error + monad and is potentially divergent. + + We encode divergence in such a way that we don't have to prove that the + functions we define terminate *upon defining them*, and can do those proofs + in an extrinsic way later. It works as follows. + + Let's say you want to define the following “even” and “odd” functions + which operate on *integers*: + + {[ + even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\ + + odd (i : int) : bool result = if i = 0 then Return F else even (i - 1) + ]} + + It is easy to prove that the functions terminate provided the input is >= 0, + but it would require to be able to define those functions in the first place! + + {!DefineDev} consequently does the following. + + It first defines versions of “even” and “odd” which use fuel: + {[ + even___fuel (n : num) (i : int) : bool result = + case n of 0 => Diverge + | SUC m => if i = 0 then Return T else odd___fuel m (i - 1) /\ + + odd___fuel (n : num) (i : int) : bool result = + case n of 0 => Diverge + | SUC m => if i = 0 then Return F else even___fuel m (i - 1) + ]} + + Those functions trivially terminate. + + Then, provided we have the following auxiliary definition: + {[ + is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F + ]} + + we can define the following predicates, which tell us whether “even___fuel” + and “odd___fuel” terminate on some given inputs: + {[ + even___P i n = ~(is_diverge (even___fuel n i)) /\ + + odd___P i n = ~(is_diverge (odd___fuel n i)) + ]} + + We can finally define “even” and “odd” as follows. We use the excluded + middle to test whether there exists some fuel on which the function + terminates: if there exists such fuel, we call the "___fuel" versions + of “even” and “odd” with it (we use the least upper bound, to be more + precise). Otherwise, we simply return “Diverge”. + {[ + even i = + if (?n. even___P i n) then even___fuel ($LEAST (even___P i)) i + else Diverge /\ + + odd i = + if (?n. odd___P i n) then odd___fuel ($LEAST (odd___P i)) i + else Diverge + ]} + + The definitions above happen to satisfy the rewriting theorem we want: + {[ + even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\ + + odd (i : int) : bool result = if i = 0 then Return F else even (i - 1) + ]} + + Moreover, if we prove a lemma which states that they don't evaluate to + “Diverge” on some given inputs (trivial recursion if we take “i >= 0” + and reuse the rewriting theorem just above), then we effectively proved + that the functions terminate on those inputs. + + Remark: + ======= + {!DefineDiv} introduces all the auxiliary definitions we need and + automatically performs the proofs. A crucial intermediate lemma + we need in order to establish the last theorem is that the "___fuel" + versions of the functions are monotonic in the fuel. + More precisely: + {[ + !n m. n <= m ==> + (!ls i. even___P ls i n ==> even___fuel n ls i n = even___fuel m ls i n) /\ + (!ls i. odd___P ls i n ==> odd___fuel n ls i n = odd___fuel m ls i n) + ]} + *) + +signature divDefNoFixLib = +sig + include Abbrev + + val DefineDiv : term quotation -> thm list +end diff --git a/backends/hol4/divDefNoFixLib.sml b/backends/hol4/divDefNoFixLib.sml new file mode 100644 index 00000000..59319e6a --- /dev/null +++ b/backends/hol4/divDefNoFixLib.sml @@ -0,0 +1,1203 @@ +(* **DEPRECATED**: see divDefLib *) + +structure divDefNoFixLib :> divDefNoFixLib = +struct + +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib + +val case_result_same_eq = prove ( + “!(r : 'a result). + (case r of + Return x => Return x + | Fail e => Fail e + | Diverge => Diverge) = r”, + rw [] >> CASE_TAC) + +(* +val ty = id_ty +strip_arrows ty +*) + +(* TODO: move *) +fun list_mk_arrow (tys : hol_type list) (ret_ty : hol_type) : hol_type = + foldr (fn (ty, aty) => ty --> aty) ret_ty tys + +(* TODO: move *) +fun strip_arrows (ty : hol_type) : hol_type list * hol_type = + let + val (ty0, ty1) = dom_rng ty + val (tys, ret) = strip_arrows ty1 + in + (ty0::tys, ret) + end + handle HOL_ERR _ => ([], ty) + +(* Small utilities *) +val current_goal : term option ref = ref NONE + +(* Save a goal in {!current_goal} then prove it. + + This way if the proof fails we can easily retrieve the goal for debugging + purposes. + *) +fun save_goal_and_prove (g, tac) : thm = + let + val _ = current_goal := SOME g + in + prove (g, tac) + end + + +(*val def_qt = ‘ +(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 num_zero_tm = “0:num” +val num_suc_tm = “SUC: num -> num” +val num_ty = “:num” + +val fuel_def_suffix = "___fuel" (* TODO: name collisions *) +val fuel_var_name = "$n" (* TODO: name collisions *) +val fuel_var = mk_var (fuel_var_name, num_ty) +val fuel_var0 = fuel_var +val fuel_var1 = mk_var ("$m", “:num”) (* TODO: name collisions *) +val fuel_vars_le = “^fuel_var0 <= ^fuel_var1” + +val fuel_predicate_suffix = "___P" (* TODO: name collisions *) +val expand_suffix = "___E" (* TODO: name collisions *) + +val bool_ty = “:bool” + +val alpha_tyvar : hol_type = “:'a” +val beta_tyvar : hol_type = “:'b” + +val is_diverge_tm = “is_diverge: 'a result -> bool” +val diverge_tm = “Diverge : 'a result” + +val least_tm = “$LEAST” +val le_tm = (fst o strip_comb) “x:num <= y:num” +val true_tm = “T” +val false_tm = “F” + +val measure_tm = “measure: ('a -> num) -> 'a -> 'a -> bool” + +fun mk_diverge_tm (ty : hol_type) : term = + let + val diverge_ty = mk_thy_type {Thy="primitives", Tyop="result", Args = [ty] } + val diverge_tm = mk_thy_const { Thy="primitives", Name="Diverge", Ty=diverge_ty } + in + diverge_tm + end + +(* Small utility: we sometimes need to generate a termination measure for + the fuel definitions. + + We derive a measure for a type which is simply the sum of the tuples + of the input types of the functions. + + For instance, for even and odd we have: + {[ + even___fuel : num -> int -> bool result + odd___fuel : num -> int -> bool result + ]} + + So the type would be: + {[ + (num # int) + (num # int) + ]} + + Note that generally speaking we expect a type of the shape (the “:num” + on the left is for the fuel): + {[ + (num # ...) + (num # ...) + ... + (num # ...) + ]} + + The decreasing measure is simply given by a function which matches over + its argument to return the fuel, whatever the case. + *) +fun mk_termination_measure_from_ty (ty : hol_type) : term = + let + val dtys = map pairSyntax.strip_prod (sumSyntax.strip_sum ty) + (* For every tuple, create a match to extract the num *) + fun mk_case_of_tuple (tys : hol_type list) : (term * term) = + case tys of + [] => failwith "mk_termination_measure_from_ty: empty list of types" + | [num_ty] => + (* No need for a case *) + let val var = genvar num_ty in (var, var) end + | num_ty :: rem_tys => + let + val scrut_var = genvar (pairSyntax.list_mk_prod tys) + val var = genvar num_ty + val rem_var = genvar (pairSyntax.list_mk_prod rem_tys) + val pats = [(pairSyntax.mk_pair (var, rem_var), var)] + val case_tm = TypeBase.mk_case (scrut_var, pats) + in + (scrut_var, case_tm) + end + val tuple_cases = map mk_case_of_tuple dtys + + (* For every sum, create a match to extract one of the tuples *) + fun mk_sum_case ((tuple_var, tuple_case), (nvar, case_end)) = + let + val left_pat = sumSyntax.mk_inl (tuple_var, type_of nvar) + val right_pat = sumSyntax.mk_inr (nvar, type_of tuple_var) + val scrut = genvar (sumSyntax.mk_sum (type_of tuple_var, type_of nvar)) + val pats = [(left_pat, tuple_case), (right_pat, case_end)] + val case_tm = TypeBase.mk_case (scrut, pats) + in + (scrut, case_tm) + end + val tuple_cases = rev tuple_cases + val (nvar, case_end) = hd tuple_cases + val tuple_cases = tl tuple_cases + val (scrut, case_tm) = foldl mk_sum_case (nvar, case_end) tuple_cases + + (* Create the function *) + val abs_tm = mk_abs (scrut, case_tm) + + (* Add the “measure term” *) + val tm = inst [alpha_tyvar |-> type_of scrut] measure_tm + val tm = mk_comb (tm, abs_tm) + in + tm + end + +(* +val ty = “: (num # 'a) + (num # 'b) + (num # 'c)” + +val tys = hd dtys +val num_ty::rem_tys = tys + +val (tuple_var, tuple_case) = hd tuple_cases +*) + +(* Get the smallest id which make the names unique (or to be more precise: + such that the names don't correspond to already defined constants). + + We do this for {!mk_fuel_defs}: for some reason, the termination proof + fails if we try to reuse the same names as before. + *) +fun get_smallest_unique_id_for_names (names : string list) : string = + let + (* Not trying to be smart here *) + val i : int option ref = ref NONE + fun get_i () = case !i of NONE => "" | SOME i => int_to_string i + fun incr_i () = + i := (case !i of NONE => SOME 0 | SOME i => SOME (i+1)) + val continue = ref true + fun name_is_ok (name : string) : bool = + not (is_const (Parse.parse_in_context [] [QUOTE (name ^ get_i ())])) + handle HOL_ERR _ => false + val _ = + while !continue do ( + let val _ = (continue := not (forall name_is_ok names)) in + if !continue then incr_i () else () end + ) + in + get_i () + end + +fun mk_fuel_defs (def_tms : term list) : thm list = + let + (* Retrieve the identifiers. + + Ex.: def_tm = “even (n : int) : bool result = if i = 0 then Return T else odd (i - 1))” + We want to retrive: id = “even” + *) + val ids = map (fst o strip_comb o lhs) def_tms + + (* In the definitions, replace the identifiers by new identifiers which use + fuel. + + Ex.: + def_fuel_tm = “ + even___fuel (fuel : nat) (n : int) : result bool = + case fuel of 0 => Diverge + | SUC fuel' => + if i = 0 then Return T else odd_fuel fuel' (i - 1))” + *) + val names = map ((fn s => s ^ fuel_def_suffix) o fst o dest_var) ids + val index = get_smallest_unique_id_for_names names + fun mk_fuel_id (id : term) : term = + let + val (id_str, ty) = dest_var id + (* Note: we use symbols forbidden in the generation of code to + prevent name collisions *) + val fuel_id_str = id_str ^ fuel_def_suffix ^ index + val fuel_id = mk_var (fuel_id_str, num_ty --> ty) + in fuel_id end + val fuel_ids = map mk_fuel_id ids + + val fuel_ids_with_fuel0 = map (fn id => mk_comb (id, fuel_var0)) fuel_ids + val fuel_ids_with_fuel1 = map (fn id => mk_comb (id, fuel_var1)) fuel_ids + + (* Recurse through the terms and replace the calls *) + val rwr_thms0 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel0) + val rwr_thms1 = map (ASSUME o mk_eq) (zip ids fuel_ids_with_fuel1) + + fun mk_fuel_tm (def_tm : term) : term = + let + val (tm0, tm1) = dest_eq def_tm + val tm0 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms0)) tm0 + val tm1 = (rhs o concl o (PURE_REWRITE_CONV rwr_thms1)) tm1 + in mk_eq (tm0, tm1) end + val fuel_tms = map mk_fuel_tm def_tms + + (* Add the case over the fuel *) + fun add_fuel_case (tm : term) : term = + let + val (f, body) = dest_eq tm + (* Create the “Diverge” term with the proper type *) + val body_ty = type_of body + val return_ty = + case (snd o dest_type) body_ty of [ty] => ty + | _ => failwith "unexpected" + val diverge_tm = mk_diverge_tm return_ty + (* Create the “SUC fuel” term *) + val suc_tm = mk_comb (num_suc_tm, fuel_var1) + val fuel_tm = + TypeBase.mk_case (fuel_var0, [(num_zero_tm, diverge_tm), (suc_tm, body)]) + in mk_eq (f, fuel_tm) end + val fuel_tms = map add_fuel_case fuel_tms + + (* Define the auxiliary definitions which use fuel *) + val fuel_defs_conj = list_mk_conj fuel_tms + (* The definition name *) + val def_name = (fst o dest_var o hd) fuel_ids + (* The tactic to prove the termination *) + val rty = ref “:bool” (* This is useful for debugging *) + fun prove_termination_tac (asms, g) = + let + val r_tm = (fst o dest_exists) g + val _ = rty := type_of r_tm + val ty = (hd o snd o dest_type) (!rty) + val m_tm = mk_termination_measure_from_ty ty + in + WF_REL_TAC ‘^m_tm’ (asms, g) + end + + (* Define the fuel definitions *) + (* + val temp_def = Hol_defn def_name ‘^fuel_defs_conj’ + Defn.tgoal temp_def + *) + val fuel_defs = tDefine def_name ‘^fuel_defs_conj’ prove_termination_tac + in + CONJUNCTS fuel_defs + end + +(* +val (fuel_tms, fuel_defs) = mk_fuel_defs def_tms +val fuel_def_tms = map (snd o strip_forall) ((strip_conj o concl) fuel_defs) +val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms) +*) + +fun mk_is_diverge_tm (fuel_tm : term) : term = + case snd (dest_type (type_of fuel_tm)) of + [ret_ty] => mk_comb (inst [alpha_tyvar |-> ret_ty] is_diverge_tm, fuel_tm) + | _ => failwith "mk_is_diverge_tm: unexpected" + +fun mk_fuel_predicate_defs (def_tm, fuel_def_tm) : thm = + let + (* From [even i] create the term [even_P i n], where [n] is the fuel *) + val (id, args) = (strip_comb o lhs) def_tm + val (id_str, id_ty) = dest_var id + val (tys, ret_ty) = strip_arrows id_ty + val tys = append tys [num_ty] + val pred_ty = list_mk_arrow tys bool_ty + val pred_id = mk_var (id_str ^ fuel_predicate_suffix, pred_ty) + val pred_tm = list_mk_comb (pred_id, append args [fuel_var]) + + (* Create the term ~is_diverge (even_fuel n i) *) + val fuel_tm = lhs fuel_def_tm + val not_is_diverge_tm = mk_neg (mk_is_diverge_tm fuel_tm) + + (* Create the term: even_P i n = ~(is_diverge (even_fuel n i) *) + val pred_def_tm = mk_eq (pred_tm, not_is_diverge_tm) + in + (* Create the definition *) + Define ‘^pred_def_tm’ + end + +(* +val (def_tm, fuel_def_tm) = hd (zip def_tms fuel_def_tms) + +val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms) +*) + +(* Tactic which makes progress in a proof by making a case disjunction (we use + this to explore all the paths in a function body). *) +fun case_progress (asms, g) = + let + val scrut = (strip_all_cases_get_scrutinee o lhs) g + in Cases_on ‘^scrut’ (asms, g) end + +(* Prove the fuel monotonicity properties. + + We want to prove a theorem of the shape: + {[ + !n m. + (!i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i) /\ + (!i. n <= m ==> odd___P i n ==> odd___fuel n i = odd___fuel m i) + ]} +*) +fun prove_fuel_mono (pred_defs : thm list) (fuel_defs : thm list) : thm = + let + val pred_tms = map (lhs o snd o strip_forall o concl) pred_defs + val fuel_tms = map (lhs o snd o strip_forall o concl) fuel_defs + val pred_fuel_tms = zip pred_tms fuel_tms + (* Create a set containing the names of all the functions in the recursive group *) + val rec_fun_set = + Redblackset.fromList const_name_compare (map get_fun_name_from_app fuel_tms) + (* Small tactic which rewrites the occurrences of recursive calls *) + fun rewrite_rec_call (asms, g) = + let + val scrut = (strip_all_cases_get_scrutinee o lhs) g + val fun_id = get_fun_name_from_app scrut (* This can fail *) + in + (* Check if the function is part of the group we are considering *) + if Redblackset.member (rec_fun_set, fun_id) then + let + (* Yes: use the induction hypothesis *) + fun apply_ind_hyp (ind_th : thm) : tactic = + let + val th = SPEC_ALL ind_th + val th_pat = (lhs o snd o strip_imp o concl) th + val (var_s, ty_s) = match_term th_pat scrut + (* Note that in practice the type instantiation should be empty *) + val th = INST var_s (INST_TYPE ty_s th) + in + assume_tac th + end + in + (last_assum apply_ind_hyp >> fs []) (asms, g) + end + else all_tac (asms, g) + end + handle HOL_ERR _ => all_tac (asms, g) + (* Generate terms of the shape: + !i. n <= m ==> even___P i n ==> even___fuel n i = even___fuel m i + *) + fun mk_fuel_eq_tm (pred_tm, fuel_tm) : term = + let + (* Retrieve the variables which are not the fuel - for the quantifiers *) + val vars = (tl o snd o strip_comb) fuel_tm + (* Introduce the fuel term which uses “m” *) + val m_fuel_tm = subst [fuel_var0 |-> fuel_var1] fuel_tm + (* Introduce the equality *) + val fuel_eq_tm = mk_eq (fuel_tm, m_fuel_tm) + (* Introduce the implication with the _P pred *) + val fuel_eq_tm = mk_imp (pred_tm, fuel_eq_tm) + (* Introduce the “n <= m ==> ...” implication *) + val fuel_eq_tm = mk_imp (fuel_vars_le, fuel_eq_tm) + (* Quantify *) + val fuel_eq_tm = list_mk_forall (vars, fuel_eq_tm) + in + fuel_eq_tm + end + val fuel_eq_tms = map mk_fuel_eq_tm pred_fuel_tms + (* Create the conjunction *) + val fuel_eq_tms = list_mk_conj fuel_eq_tms + (* Qantify over the fuels *) + val fuel_eq_tms = list_mk_forall ([fuel_var0, fuel_var1], fuel_eq_tms) + (* The tactics for the proof *) + val prove_tac = + Induct_on ‘^fuel_var0’ >-( + (* The ___P predicates are false: n is 0 *) + fs pred_defs >> + fs [is_diverge_def] >> + pure_once_rewrite_tac fuel_defs >> fs []) >> + (* Introduce n *) + gen_tac >> + (* Introduce m *) + Cases_on ‘^fuel_var1’ >-( + (* Contradiction: SUC n < 0 *) + rw [] >> exfalso >> int_tac) >> + fs pred_defs >> + fs [is_diverge_def] >> + pure_once_rewrite_tac fuel_defs >> fs [bind_def] >> + (* Introduce in the context *) + rpt gen_tac >> + (* Split the goals - note that we prove one big goal for all the functions at once *) + rpt strip_tac >> + (* Instantiate the assumption: !m. n <= m ==> ~(...) + with the proper m. + *) + last_x_assum imp_res_tac >> + (* Make sure the induction hypothesis is always the last assumption *) + last_x_assum assume_tac >> + (* Split the goals *) + rpt strip_tac >> fs [case_result_same_eq] >> + (* Explore all the paths *) + rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq]) + in + (* Prove *) + save_goal_and_prove (fuel_eq_tms, prove_tac) + end + +(* +val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs + +set_goal ([], fuel_eq_tms) +*) + +(* Prove the property about the least upper bound. + + We want to prove theorems of the shape: + {[ + (!n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i) + ]} + {[ + (!n i. $LEAST (odd___P i) <= n ==> odd___fuel n i = odd___fuel ($LEAST (odd___P i)) i) + ]} + + TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms) +*) +fun prove_least_fuel_mono (pred_defs : thm list) (fuel_mono_thm : thm) : thm list = + let + val thl = (CONJUNCTS o SPECL [fuel_var0, fuel_var1]) fuel_mono_thm + fun mk_least_fuel_thm (pred_def, mono_thm) : thm = + let + (* Retrieve the predicate, without the fuel *) + val pred_tm = (lhs o snd o strip_forall o concl) pred_def + val (pred_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + val pred_tm = list_mk_comb (pred_tm, args) + (* Add $LEAST *) + val least_pred_tm = mk_comb (least_tm, pred_tm) + (* Specialize all *) + val vars = (fst o strip_forall o concl) mono_thm + val th = SPECL vars mono_thm + (* Substitute in the mono theorem *) + val th = INST [fuel_var0 |-> least_pred_tm] th + (* Symmetrize the equality *) + val th = PURE_ONCE_REWRITE_RULE [EQ_SYM_EQ] th + (* Quantify *) + val th = GENL (fuel_var1 :: vars) th + in + th + end + in + map mk_least_fuel_thm (zip pred_defs thl) + end + +(* +val (pred_def, mono_thm) = hd (zip pred_defs thl) +*) + +(* Prove theorems of the shape: + + {[ + !n i. even___P i n ==> $LEAST (even___P i) <= n + ]} + + TODO: merge with other functions? (prove_pred_imp_fuel_eq_raw_thms) + *) +fun prove_least_pred_thms (pred_defs : thm list) : thm list = + let + fun prove_least_pred_thm (pred_def : thm) : thm = + let + val pred_tm = (lhs o snd o strip_forall o concl) pred_def + val (pred_no_fuel_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args) + (* Make the “$LEAST (even___P i)” term *) + val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm) + (* Make the inequality *) + val tm = list_mk_comb (le_tm, [least_pred_tm, fuel_var0]) + (* Add the implication *) + val tm = mk_imp (pred_tm, tm) + (* Quantify *) + val tm = list_mk_forall (args, tm) + val tm = mk_forall (fuel_var0, tm) + (* Prove *) + val prove_tac = + rpt gen_tac >> + disch_tac >> + (* Use the "fundamental" property about $LEAST *) + qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >> + (* Prove the premise *) + pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >> + rw [] >> + (* Finish the proof by contraposition *) + spose_not_then assume_tac >> + fs [not_le_eq_gt] + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_least_pred_thm pred_defs + end + + +(* +val least_pred_thms = prove_least_pred_thms pred_defs + +val least_pred_thm = hd least_pred_thms +*) + +(* Prove theorems of the shape: + + {[ + !n i. even___P i n ==> even___P i ($LEAST (even___P i)) + ]} +*) +fun prove_pred_n_imp_pred_least_thms (pred_defs : thm list) : thm list = + let + fun prove_pred_n_imp_pred_least (pred_def : thm) : thm = + let + val pred_tm = (lhs o snd o strip_forall o concl) pred_def + val (pred_no_fuel_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + val pred_no_fuel_tm = list_mk_comb (pred_no_fuel_tm, args) + (* Make the “$LEAST (even___P i)” term *) + val least_pred_tm = mk_comb (least_tm, pred_no_fuel_tm) + (* Make the “even___P i ($LEAST (even___P i))” *) + val tm = subst [fuel_var0 |-> least_pred_tm] pred_tm + (* Add the implication *) + val tm = mk_imp (pred_tm, tm) + (* Quantify *) + val tm = list_mk_forall (args, tm) + val tm = mk_forall (fuel_var0, tm) + (* The proof tactic *) + val prove_tac = + rpt gen_tac >> + disch_tac >> + (* Use the "fundamental" property about $LEAST *) + qspec_assume ‘^pred_no_fuel_tm’ whileTheory.LEAST_EXISTS_IMP >> + (* Prove the premise *) + pop_assum sg_premise_tac >- (exists_tac fuel_var0 >> fs []) >> + rw [] + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_pred_n_imp_pred_least pred_defs + end + +(* +val (pred_def, mono_thm) = hd (zip pred_defs thl) +val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_defs fuel_mono_thm + +val least_fuel_mono_thm = hd least_fuel_mono_thms +*) + +(* Define the "raw" definitions: + + {[ + even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge + ]} + *) +fun define_raw_defs (def_tms : term list) (pred_defs : thm list) (fuel_defs : thm list) : thm list = + let + fun define_raw_def (def_tm, (pred_def, fuel_def)) : thm = + let + val app = lhs def_tm + val pred_tm = (lhs o snd o strip_forall o concl) pred_def + (* Make the “?n. even___P i n” term *) + val exists_fuel_tm = mk_exists (fuel_var0, pred_tm) + (* Make the “even___fuel ($LEAST (even___P i)) i” term *) + val fuel_tm = (lhs o snd o strip_forall o concl) fuel_def + val (pred_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + val pred_tm = list_mk_comb (pred_tm, args) + val least_pred_tm = mk_comb (least_tm, pred_tm) + val fuel_tm = subst [fuel_var0 |-> least_pred_tm] fuel_tm + (* Create the Diverge term *) + val ret_ty = (hd o snd o dest_type) (type_of app) + (* Create the “if then else” *) + val body = TypeBase.mk_case (exists_fuel_tm, [(true_tm, fuel_tm), (false_tm, mk_diverge_tm ret_ty)]) + (* *) + val raw_def_tm = mk_eq (app, body) + in + Define ‘^raw_def_tm’ + end + in + map define_raw_def (zip def_tms (zip pred_defs fuel_defs)) + end + +(* +val raw_defs = define_raw_defs def_tms pred_defs fuel_defs + *) + +(* Prove theorems of the shape: + + !n i. even___P i n ==> even___fuel n i = even i + *) +fun prove_pred_imp_fuel_eq_raw_defs + (pred_defs : thm list) + (fuel_def_tms : term list) + (least_fuel_mono_thms : thm list) + (least_pred_thms : thm list) + (pred_n_imp_pred_least_thms : thm list) + (raw_defs : thm list) : + thm list = + let + fun prove_thm (pred_def, + (fuel_def_tm, + (least_fuel_mono_thm, + (least_pred_thm, + (pred_n_imp_pred_least_thm, raw_def))))) : thm = + let + (* Generate: “even___P i n” *) + val pred_tm = (lhs o snd o strip_forall o concl) pred_def + val (pred_no_fuel_tm, args) = strip_comb pred_tm + val args = rev (tl (rev args)) + (* Generate: “even___fuel n i” *) + val fuel_tm = lhs fuel_def_tm + (* Generate: “even i” *) + val raw_def_tm = (lhs o snd o strip_forall o concl) raw_def + (* Generate: “even___fuel n i = even i” *) + val tm = mk_eq (fuel_tm, raw_def_tm) + (* Add the implication *) + val tm = mk_imp (pred_tm, tm) + (* Quantify *) + val tm = list_mk_forall (args, tm) + val tm = mk_forall (fuel_var0, tm) + (* Prove *) + val prove_tac = + rpt gen_tac >> + strip_tac >> + fs raw_defs >> + (* Case on ‘?n. even___P i n’ *) + CASE_TAC >> fs [] >> + (* Use the monotonicity property *) + irule least_fuel_mono_thm >> + imp_res_tac pred_n_imp_pred_least_thm >> fs [] >> + irule least_pred_thm >> fs [] + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_thm (zip pred_defs (zip fuel_def_tms (zip least_fuel_mono_thms + (zip least_pred_thms (zip pred_n_imp_pred_least_thms raw_defs))))) + end + +(* +val pred_imp_fuel_eq_raw_defs = + prove_pred_imp_fuel_eq_raw_defs + pred_defs fuel_def_tms least_fuel_mono_thms least_pred_thms + pred_n_imp_pred_least_thms raw_defs + *) + + +(* Generate "expand" definitions of the following shape (we use them to + hide the raw function bodies, to control the rewritings): + + {[ + even___expand even odd i : bool result = + if i = 0 then Return T else odd (i - 1) + ]} + + {[ + odd___expand even odd i : bool result = + if i = 0 then Return F else even (i - 1) + ]} + + *) +fun gen_expand_defs (def_tms : term list) = + let + (* Generate the variables for “even”, “odd”, etc. *) + val fun_vars = map (fst o strip_comb o lhs) def_tms + val fun_tys = map type_of fun_vars + (* Generate the expansion *) + fun mk_def (def_tm : term) : thm = + let + val (exp_fun, args) = (strip_comb o lhs) def_tm + val (exp_fun_str, exp_fun_ty) = dest_var exp_fun + val exp_fun_str = exp_fun_str ^ expand_suffix + val exp_fun_ty = list_mk_arrow fun_tys exp_fun_ty + val exp_fun = mk_var (exp_fun_str, exp_fun_ty) + val exp_fun = list_mk_comb (exp_fun, fun_vars) + val exp_fun = list_mk_comb (exp_fun, args) + val tm = mk_eq (exp_fun, rhs def_tm) + in + Define ‘^tm’ + end + in + map mk_def def_tms + end + +(* +val def_tm = hd def_tms + +val expand_defs = gen_expand_defs def_tms +*) + +(* Small utility: + + Return the list: + {[ + (“even___P i n”, “even i = even___expand even odd i”), + ... + ]} + + *) +fun mk_termination_diverge_tms + (def_tms : term list) + (pred_defs : thm list) + (raw_defs : thm list) + (expand_defs : thm list) : + (term * term) list = + let + (* Create the substitution for the "expand" functions: + {[ + even -> even + odd -> odd + ... + ]} + + where on the left we have *variables* and on the right we have + the "raw" definitions. + *) + fun mk_fun_subst (def_tm, raw_def) = + let + val var = (fst o strip_comb o lhs) def_tm + val f = (fst o strip_comb o lhs o snd o strip_forall o concl) raw_def + in + (var |-> f) + end + val fun_subst = map mk_fun_subst (zip def_tms raw_defs) + + fun mk_tm (pred_def, (raw_def, expand_def)) : + term * term = + let + (* “even___P i n” *) + val pred_tm = (lhs o snd o strip_forall o concl) pred_def + (* “even i = even___expand even odd i” *) + val expand_tm = (lhs o snd o strip_forall o concl) expand_def + val expand_tm = subst fun_subst expand_tm + val fun_tm = (lhs o snd o strip_forall o concl) raw_def + val fun_eq_tm = mk_eq (fun_tm, expand_tm) + in (pred_tm, fun_eq_tm) end + in + map mk_tm (zip pred_defs (zip raw_defs expand_defs)) + end + +(* +val term_div_tms = + mk_termination_diverge_tms pred_defs raw_defs expand_defs +*) + +(* Prove the termination lemmas: + + {[ + !i. + (?n. even___P i n) ==> + even i = even___expand even odd i + ]} + *) +fun prove_termination_thms + (term_div_tms : (term * term) list) + (fuel_defs : thm list) + (pred_defs : thm list) + (raw_defs : thm list) + (expand_defs : thm list) + (pred_n_imp_pred_least_thms : thm list) + (pred_imp_fuel_eq_raw_defs : thm list) + : thm list = + let + (* Create a map from functions in the recursive group to lemmas + to apply *) + fun mk_rec_fun_eq_pair (fuel_def, eq_th) = + let + val rfun = (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def + in + (rfun, eq_th) + end + val rec_fun_eq_map = + Redblackmap.fromList const_name_compare ( + map mk_rec_fun_eq_pair + (zip fuel_defs pred_imp_fuel_eq_raw_defs)) + + (* Small tactic which rewrites the recursive calls *) + fun rewrite_rec_call (asms, g) = + let + val scrut = (strip_all_cases_get_scrutinee o lhs) g + val fun_id = get_fun_name_from_app scrut (* This can fail *) + (* This can raise an exception - hence the handle at the end + of the function *) + val eq_th = Redblackmap.find (rec_fun_eq_map, fun_id) + val eq_th = (UNDISCH_ALL o SPEC_ALL) eq_th + (* Match the theorem *) + val eq_th_tm = (lhs o concl) eq_th + val (var_s, ty_s) = match_term eq_th_tm scrut + val eq_th = INST var_s (INST_TYPE ty_s eq_th) + val eq_th = thm_to_conj_implies eq_th + (* Some tactics *) + val premise_tac = fs pred_defs >> fs [is_diverge_def] + in + (* Apply the theorem, prove the premise, and rewrite *) + (prove_premise_then premise_tac assume_tac eq_th >> fs []) (asms, g) + end handle NotFound => all_tac (asms, g) + | HOL_ERR _ => all_tac (asms, g) (* Getting the function name can also fail *) + + fun prove_one ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) : + thm = + let + (* “?n. even___P i n” *) + val pred_tm = mk_exists (fuel_var0, pred_tm) + (* “even i = even___expand even odd i” *) + val tm = fun_eq_tm + (* Add the implication *) + val tm = mk_imp (pred_tm, tm) + (* Quantify *) + val (_, args) = strip_comb (lhs fun_eq_tm) + val tm = list_mk_forall (args, tm) + + (* Prove *) + val prove_tac = + rpt gen_tac >> + disch_tac >> + + (* Expand the raw definition and get rid of the ‘?n ...’ *) + pure_once_rewrite_tac raw_defs >> + pure_asm_rewrite_tac [] >> + + (* Simplify *) + fs [] >> + + (* Prove that: “even___P i $(LEAST ...)” *) + imp_res_tac pred_n_imp_pred_least_thm >> + + (* We don't need the ‘even___P i n’ assumption anymore: we have a more + precise one with the least upper bound *) + last_x_assum ignore_tac >> + + (* Expand *) + fs pred_defs >> + fs [is_diverge_def] >> + fs expand_defs >> + + (* We need to be a bit careful when expanding the definitions which use fuel: + it can make the simplifier loop. *) + rpt (pop_assum mp_tac) >> + pure_once_rewrite_tac fuel_defs >> + rpt disch_tac >> + + (* Expand the binds *) + fs [bind_def, case_result_same_eq] >> + + (* Explore all the paths by doing case disjunctions *) + rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq]) + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_one + (zip term_div_tms pred_n_imp_pred_least_thms) + end + +(* +val termination_thms = + prove_termination_thms term_div_tms fuel_defs pred_defs + raw_defs expand_defs pred_n_imp_pred_least_thms + pred_imp_fuel_eq_raw_defs + +val ((pred_tm, fun_eq_tm), pred_n_imp_pred_least_thm) = hd (zip term_div_tms pred_n_imp_pred_least_thms) +set_goal ([], tm) +*) + +(* Prove the divergence lemmas: + + {[ + !i. + (!n. ~even___P i n) ==> + (!n. ~even___P i (SUC n)) ==> + even i = even___expand even odd i + ]} + + Note that the shape of the theorem is very precise: this helps for the proof. + Also, by correctly ordering the assumptions, we make sure that by rewriting + we don't convert one of the two to “T”. + *) +fun prove_divergence_thms + (term_div_tms : (term * term) list) + (fuel_defs : thm list) + (pred_defs : thm list) + (raw_defs : thm list) + (expand_defs : thm list) + : thm list = + let + (* Create a set containing the names of all the functions in the recursive group *) + fun get_rec_fun_id (fuel_def : thm) = + (get_fun_name_from_app o lhs o snd o strip_forall o concl) fuel_def + val rec_fun_set = + Redblackset.fromList const_name_compare ( + map get_rec_fun_id raw_defs) + + (* Small tactic which rewrites the recursive calls *) + fun rewrite_rec_call (asms, g) = + let + val scrut = (strip_all_cases_get_scrutinee o lhs) g + val fun_id = get_fun_name_from_app scrut (* This can fail *) + in + (* Check if the function is part of the group we are considering *) + if Redblackset.member (rec_fun_set, fun_id) then + let + (* Create a subgoal “odd i = Diverge” *) + val ret_ty = (hd o snd o dest_type o type_of) scrut + val g = mk_eq (scrut, mk_diverge_tm ret_ty) + + (* Create a subgoal: “?n. odd___P i n”. + + It is a bit cumbersome because we have to lookup the proper + predicate (from “odd” we need to lookup “odd___P”) and we + may have to perform substitutions... We hack a bit by using + a conversion to rewrite “odd i” to a term which contains + the “?n. odd___P i n” we are looking for. + *) + val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs scrut) + val (_, exists_g, _) = TypeBase.dest_case exists_g + (* The tactic to prove the subgoal *) + val prove_sg_tac = + pure_rewrite_tac raw_defs >> + Cases_on ‘^exists_g’ >> pure_asm_rewrite_tac [] >> fs [] >> + (* There must only remain the positive case (i.e., “?n. ...”): + we have a contradiction *) + exfalso >> + (* The end of the proof is done by opening the definitions *) + pop_assum mp_tac >> + fs pred_defs >> fs [is_diverge_def] + in + (SUBGOAL_THEN g assume_tac >- prove_sg_tac >> fs []) (asms, g) + end + else all_tac (asms, g) (* Nothing to do *) + end handle HOL_ERR _ => all_tac (asms, g) + + fun prove_one (pred_tm, fun_eq_tm) : + thm = + let + (* “!n. ~even___P i n” *) + val neg_pred_tm = mk_neg pred_tm + val pred_tm = mk_forall (fuel_var0, neg_pred_tm) + val pred_suc_tm = subst [fuel_var0 |-> numSyntax.mk_suc fuel_var0] neg_pred_tm + val pred_suc_tm = mk_forall (fuel_var0, pred_suc_tm) + + (* “even i = even___expand even odd i” *) + val tm = fun_eq_tm + + (* Add the implications *) + val tm = list_mk_imp ([pred_tm, pred_suc_tm], tm) + + (* Quantify *) + val (_, args) = strip_comb (lhs fun_eq_tm) + val tm = list_mk_forall (args, tm) + + (* Prove *) + val prove_tac = + rpt gen_tac >> + + pure_rewrite_tac raw_defs >> + rpt disch_tac >> + + (* This allows to simplify the “?n. even___P i n” *) + fs [] >> + (* We don't need the last assumption anymore *) + last_x_assum ignore_tac >> + + (* Expand *) + fs pred_defs >> fs [is_diverge_def] >> + fs expand_defs >> + + (* We need to be a bit careful when expanding the definitions which use fuel: + it can make the simplifier loop. + *) + pop_assum mp_tac >> + pure_once_rewrite_tac fuel_defs >> + rpt disch_tac >> fs [bind_def, case_result_same_eq] >> + + (* Evaluate all the paths *) + rpt (rewrite_rec_call >> case_progress >> fs [case_result_same_eq]) + in + save_goal_and_prove (tm, prove_tac) + end + in + map prove_one term_div_tms + end + +(* +val (pred_tm, fun_eq_tm) = hd term_div_tms +set_goal ([], tm) + +val divergence_thms = + prove_divergence_thms + term_div_tms + fuel_defs + pred_defs + raw_defs + expand_defs +*) + +(* Prove the final lemmas: + + {[ + !i. even i = even___expand even odd i + ]} + + Note that the shape of the theorem is very precise: this helps for the proof. + Also, by correctly ordering the assumptions, we make sure that by rewriting + we don't convert one of the two to “T”. + *) +fun prove_final_eqs + (term_div_tms : (term * term) list) + (termination_thms : thm list) + (divergence_thms : thm list) + (raw_defs : thm list) + : thm list = + let + fun prove_one ((pred_tm, fun_eq_tm), (termination_thm, divergence_thm)) : thm = + let + val (_, args) = strip_comb (lhs fun_eq_tm) + val g = list_mk_forall (args, fun_eq_tm) + (* We make a case disjunction of the subgoal: “exists n. even___P i n” *) + val exists_g = (rhs o concl) (PURE_REWRITE_CONV raw_defs (lhs fun_eq_tm)) + val (_, exists_g, _) = TypeBase.dest_case exists_g + val prove_tac = + rpt gen_tac >> + Cases_on ‘^exists_g’ + >-( (* Termination *) + irule termination_thm >> pure_asm_rewrite_tac []) + (* Divergence *) + >> irule divergence_thm >> fs [] + + in + save_goal_and_prove (g, prove_tac) + end + in + map prove_one (zip term_div_tms (zip termination_thms divergence_thms)) + end + +(* +val termination_thm = hd termination_thms +val divergence_thm = hd divergence_thms +set_goal ([], g) +*) + +(* The final function: define potentially diverging functions in an error monad *) +fun DefineDiv (def_qt : term quotation) = + let + (* Parse the definitions. + + Example: + {[ + (even (i : int) : bool result = if i = 0 then Return T else odd (i - 1)) /\ + (odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)) + ]} + *) + val def_tms = (strip_conj o list_mk_conj o rev) (Defn.parse_quote def_qt) + + (* Generate definitions which use some fuel + + Example: + {[ + even___fuel n i = + case fuel of + 0 => Diverge + | SUC fuel => + if i = 0 then Return T else odd_fuel (i - 1)) + ]} + *) + val fuel_defs = mk_fuel_defs def_tms + + (* Generate the predicate definitions. + + {[ even___P n i = = ~is_diverge (even___fuel n i) ]} + *) + val fuel_def_tms = map (snd o strip_forall o concl) fuel_defs + val pred_defs = map mk_fuel_predicate_defs (zip def_tms fuel_def_tms) + + (* Prove the monotonicity property for the fuel, all at once + + *) + val fuel_mono_thm = prove_fuel_mono pred_defs fuel_defs + + (* Prove the individual fuel functions - TODO: update + + {[ + !n i. $LEAST (even___P i) <= n ==> even___fuel n i = even___fuel ($LEAST (even___P i)) i + ]} + *) + val least_fuel_mono_thms = prove_least_fuel_mono pred_defs fuel_mono_thm + + (* + {[ + !n i. even___P i n ==> $LEAST (even___P i) <= n + ]} + *) + val least_pred_thms = prove_least_pred_thms pred_defs + + (* + {[ + !n i. even___P i n ==> even___P i ($LEAST (even___P i)) + ]} + *) + val pred_n_imp_pred_least_thms = prove_pred_n_imp_pred_least_thms pred_defs + + (* + "Raw" definitions: + + {[ + even i = if (?n. even___P i n) then even___P ($LEAST (even___P i)) i else Diverge + ]} + *) + val raw_defs = define_raw_defs def_tms pred_defs fuel_defs + + (* + !n i. even___P i n ==> even___fuel n i = even i + *) + val pred_imp_fuel_eq_raw_defs = + prove_pred_imp_fuel_eq_raw_defs + pred_defs fuel_def_tms least_fuel_mono_thms + least_pred_thms pred_n_imp_pred_least_thms raw_defs + + (* "Expand" definitions *) + val expand_defs = gen_expand_defs def_tms + + (* Small utility *) + val term_div_tms = mk_termination_diverge_tms def_tms pred_defs raw_defs expand_defs + + (* Termination theorems *) + val termination_thms = + prove_termination_thms term_div_tms fuel_defs pred_defs + raw_defs expand_defs pred_n_imp_pred_least_thms pred_imp_fuel_eq_raw_defs + + (* Divergence theorems *) + val divergence_thms = + prove_divergence_thms term_div_tms fuel_defs pred_defs raw_defs expand_defs + + (* Final theorems: + + {[ + ∀i. even i = even___E even odd i, + ⊢ ∀i. odd i = odd___E even odd i + ]} + *) + val final_eqs = prove_final_eqs term_div_tms termination_thms divergence_thms raw_defs + val final_eqs = map (PURE_REWRITE_RULE expand_defs) final_eqs + in + (* We return the final equations, which act as rewriting theorems *) + final_eqs + end + +end diff --git a/backends/hol4/testDivDefScript.sml b/backends/hol4/divDefNoFixLibTestScript.sml index 4a87895f..b2a4d607 100644 --- a/backends/hol4/testDivDefScript.sml +++ b/backends/hol4/divDefNoFixLibTestScript.sml @@ -2,9 +2,9 @@ open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib divDefLib +open primitivesLib divDefNoFixLib -val _ = new_theory "testDivDef" +val _ = new_theory "divDefNoFixLibTest" val def_qt = ‘ (even (i : int) : bool result = diff --git a/backends/hol4/testDivDefTheory.sig b/backends/hol4/divDefNoFixLibTestTheory.sig index a3ce2255..999cf543 100644 --- a/backends/hol4/testDivDefTheory.sig +++ b/backends/hol4/divDefNoFixLibTestTheory.sig @@ -1,4 +1,4 @@ -signature testDivDefTheory = +signature divDefNoFixLibTestTheory = sig type thm = Thm.thm @@ -40,9 +40,9 @@ sig val nth_mut_fwd___fuel_def : thm val nth_mut_fwd___fuel_ind : thm - val testDivDef_grammars : type_grammar.grammar * term_grammar.grammar + val divDefNoFixLibTest_grammars : type_grammar.grammar * term_grammar.grammar (* - [primitives] Parent theory of "testDivDef" + [primitives] Parent theory of "divDefNoFixLibTest" [even___E_def] Definition diff --git a/backends/hol4/divDefProto2TestScript.sml b/backends/hol4/divDefProto2TestScript.sml index 39719b65..bc9ea9a7 100644 --- a/backends/hol4/divDefProto2TestScript.sml +++ b/backends/hol4/divDefProto2TestScript.sml @@ -57,29 +57,6 @@ fun prove_valid_case_progress val (asms, g) = top_goal () *) -(* TODO: move *) -(* This theorem is important to shape the goal when proving that a body - satifies the fixed point validity property. - - Importantly: this theorem relies on the fact that errors are just transmitted - to the caller (in particular, without modification). - *) -Theorem case_result_switch_eq: - (case (case x of Return y => f y | Fail e => Fail e | Diverge => Diverge) of - | Return y => g y - | Fail e => Fail e - | Diverge => Diverge) = - (case x of - | Return y => - (case f y of - | Return y => g y - | Fail e => Fail e - | Diverge => Diverge) - | Fail e => Fail e - | Diverge => Diverge) -Proof - Cases_on ‘x’ >> fs [] -QED (* Tactic to prove that a body is valid: perform one step. *) fun prove_body_is_valid_tac_step (asms, g) = diff --git a/backends/hol4/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig deleted file mode 100644 index 77d5631e..00000000 --- a/backends/hol4/divDefProto2Theory.sig +++ /dev/null @@ -1,334 +0,0 @@ -signature divDefProto2Theory = -sig - type thm = Thm.thm - - (* Definitions *) - val even_odd_body_def : thm - val fix_def : thm - val fix_fuel_P_def : thm - val fix_fuel_def : thm - val is_valid_fp_body_def : thm - val list_t_TY_DEF : thm - val list_t_case_def : thm - val list_t_size_def : thm - val nth_body_def : thm - - (* Theorems *) - val datatype_list_t : thm - val even_def : thm - val even_odd_body_is_valid : thm - val even_odd_body_is_valid_aux : thm - val fix_fixed_diverges : thm - val fix_fixed_eq : thm - val fix_fixed_terminates : thm - val fix_fuel_P_least : thm - val fix_fuel_compute : thm - val fix_fuel_eq_fix : thm - val fix_fuel_mono : thm - val fix_fuel_mono_aux : thm - val fix_fuel_mono_least : thm - val fix_fuel_not_diverge_eq_fix : thm - val fix_fuel_not_diverge_eq_fix_aux : thm - val fix_not_diverge_implies_fix_fuel : thm - val fix_not_diverge_implies_fix_fuel_aux : thm - val is_valid_fp_body_compute : 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 nth_body_is_valid : thm - val nth_body_is_valid_aux : thm - val nth_def : thm - val odd_def : thm - - val divDefProto2_grammars : type_grammar.grammar * term_grammar.grammar -(* - [primitives] Parent theory of "divDefProto2" - - [even_odd_body_def] Definition - - ⊢ ∀f x. - even_odd_body f x = - case x of - INL 0 => Return (INR (INR T)) - | INL i => - (case f (INR (INL (i − 1))) of - Return (INL v) => Fail Failure - | Return (INR (INL v2)) => Fail Failure - | Return (INR (INR b)) => Return (INR (INR b)) - | Fail e => Fail e - | Diverge => Diverge) - | INR (INL 0) => Return (INR (INR F)) - | INR (INL i) => - (case f (INL (i − 1)) of - Return (INL v) => Fail Failure - | Return (INR (INL v2)) => Fail Failure - | Return (INR (INR b)) => Return (INR (INR b)) - | Fail e => Fail e - | Diverge => Diverge) - | INR (INR v5) => Fail Failure - - [fix_def] Definition - - ⊢ ∀f x. - fix f x = - if ∃n. fix_fuel_P f x n then - fix_fuel ($LEAST (fix_fuel_P f x)) f x - else Diverge - - [fix_fuel_P_def] Definition - - ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x) - - [fix_fuel_def] Definition - - ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ - ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x - - [is_valid_fp_body_def] Definition - - ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧ - ∀n f. - is_valid_fp_body (SUC n) f ⇔ - ∀x. (∀g h. f g x = f h x) ∨ - ∃h y. - is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od - - [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 - - [nth_body_def] Definition - - ⊢ ∀f x. - nth_body f x = - case x of - INL x => - (let - (ls,i) = x - in - case ls of - ListCons x tl => - if u32_to_int i = 0 then Return (INR x) - else - do - i0 <- u32_sub i (int_to_u32 1); - r <- f (INL (tl,i0)); - case r of - INL v => Fail Failure - | INR i1 => Return (INR i1) - od - | ListNil => Fail Failure) - | INR v2 => Fail Failure - - [datatype_list_t] Theorem - - ⊢ DATATYPE (list_t ListCons ListNil) - - [even_def] Theorem - - ⊢ ∀i. even i = if i = 0 then Return T else odd (i − 1) - - [even_odd_body_is_valid] Theorem - - ⊢ is_valid_fp_body (SUC (SUC 0)) even_odd_body - - [even_odd_body_is_valid_aux] Theorem - - ⊢ is_valid_fp_body (SUC (SUC n)) even_odd_body - - [fix_fixed_diverges] Theorem - - ⊢ ∀N f. - is_valid_fp_body N f ⇒ - ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x - - [fix_fixed_eq] Theorem - - ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x - - [fix_fixed_terminates] Theorem - - ⊢ ∀N f. - is_valid_fp_body N f ⇒ - ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x - - [fix_fuel_P_least] Theorem - - ⊢ ∀f n x. - fix_fuel n f x ≠ Diverge ⇒ - fix_fuel_P f x ($LEAST (fix_fuel_P f x)) - - [fix_fuel_compute] Theorem - - ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ - (∀n f x. - fix_fuel (NUMERAL (BIT1 n)) f x = - f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧ - ∀n f x. - fix_fuel (NUMERAL (BIT2 n)) f x = - f (fix_fuel (NUMERAL (BIT1 n)) f) x - - [fix_fuel_eq_fix] Theorem - - ⊢ ∀N f. - is_valid_fp_body N f ⇒ - ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix f x - - [fix_fuel_mono] Theorem - - ⊢ ∀N f. - is_valid_fp_body N f ⇒ - ∀n x. - fix_fuel_P f x n ⇒ ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x - - [fix_fuel_mono_aux] Theorem - - ⊢ ∀n N M g f. - is_valid_fp_body M f ⇒ - is_valid_fp_body N g ⇒ - ∀x. ¬is_diverge (g (fix_fuel n f) x) ⇒ - ∀m. n ≤ m ⇒ g (fix_fuel n f) x = g (fix_fuel m f) x - - [fix_fuel_mono_least] Theorem - - ⊢ ∀N f. - is_valid_fp_body N f ⇒ - ∀n x. - fix_fuel_P f x n ⇒ - fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x - - [fix_fuel_not_diverge_eq_fix] Theorem - - ⊢ ∀N f. - is_valid_fp_body N f ⇒ - ∀n x. - f (fix_fuel n f) x ≠ Diverge ⇒ f (fix f) x = f (fix_fuel n f) x - - [fix_fuel_not_diverge_eq_fix_aux] Theorem - - ⊢ ∀N M g f. - is_valid_fp_body M f ⇒ - is_valid_fp_body N g ⇒ - ∀n x. - g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x - - [fix_not_diverge_implies_fix_fuel] Theorem - - ⊢ ∀N f. - is_valid_fp_body N f ⇒ - ∀x. f (fix f) x ≠ Diverge ⇒ ∃n. f (fix f) x = f (fix_fuel n f) x - - [fix_not_diverge_implies_fix_fuel_aux] Theorem - - ⊢ ∀N M g f. - is_valid_fp_body M f ⇒ - is_valid_fp_body N g ⇒ - ∀x. g (fix f) x ≠ Diverge ⇒ - ∃n. g (fix f) x = g (fix_fuel n f) x ∧ - ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x - - [is_valid_fp_body_compute] Theorem - - ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧ - (∀n f. - is_valid_fp_body (NUMERAL (BIT1 n)) f ⇔ - ∀x. (∀g h. f g x = f h x) ∨ - ∃h y. - is_valid_fp_body (NUMERAL (BIT1 n) − 1) h ∧ - ∀g. f g x = do z <- g y; h g z od) ∧ - ∀n f. - is_valid_fp_body (NUMERAL (BIT2 n)) f ⇔ - ∀x. (∀g h. f g x = f h x) ∨ - ∃h y. - is_valid_fp_body (NUMERAL (BIT1 n)) h ∧ - ∀g. f g x = do z <- g y; h g z od - - [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 - - [nth_body_is_valid] Theorem - - ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body - - [nth_body_is_valid_aux] Theorem - - ⊢ is_valid_fp_body (SUC (SUC n)) nth_body - - [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 - - [odd_def] Theorem - - ⊢ ∀i. odd i = if i = 0 then Return F else even (i − 1) - - -*) -end diff --git a/backends/hol4/divDefProtoScript.sml b/backends/hol4/divDefProtoScript.sml deleted file mode 100644 index 6280fa7e..00000000 --- a/backends/hol4/divDefProtoScript.sml +++ /dev/null @@ -1,252 +0,0 @@ -(* Prototype: divDefLib but with general combinators *) - -open HolKernel boolLib bossLib Parse -open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory - -open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory -open primitivesLib - -val _ = new_theory "divDefProto" - -(* - * Test with a general validity predicate. - * - * TODO: this works! Cleanup. - *) -val fix_fuel_def = Define ‘ - (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧ - (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x) -’ - -val fix_fuel_P_def = Define ‘ - fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x)) -’ - -val fix_def = Define ‘ - fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = - if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge -’ - -val is_valid_fp_body_def = Define ‘ - is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) = - ∀x. (∀g h. f g x = f h x) ∨ (∃ y. ∀g. f g x = g y) -’ - -Theorem fix_fuel_mono: - ∀f. is_valid_fp_body f ⇒ - ∀n x. fix_fuel_P f x n ⇒ - ∀ m. n ≤ m ⇒ - fix_fuel n f x = fix_fuel m f x -Proof - ntac 2 strip_tac >> - Induct_on ‘n’ >> rpt strip_tac - >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> - Cases_on ‘m’ >- int_tac >> fs [] >> - fs [is_valid_fp_body_def] >> - fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> - - (* Use the validity property *) - last_x_assum (qspec_assume ‘x’) >> - (* This makes a case disjunction on the validity property *) - rw [] - >-((* Case 1: the continuation doesn't matter *) fs []) >> - (* Case 2: the continuation *does* matter (i.e., there is a recursive call *) - (* Instantiate the validity property with the different continuations *) - first_assum (qspec_assume ‘fix_fuel n f’) >> - first_assum (qspec_assume ‘fix_fuel n' f’) >> - last_assum (qspec_assume ‘y’) >> - fs [] -QED - -(* TODO: remove? *) -Theorem fix_fuel_mono_least: - ∀f. is_valid_fp_body f ⇒ - ∀n x. fix_fuel_P f x n ⇒ - fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x -Proof - rw [] >> - pure_once_rewrite_tac [EQ_SYM_EQ] >> - irule fix_fuel_mono >> fs [] >> - (* Use the "fundamental" property about $LEAST *) - qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >> - (* Prove the premise *) - pop_assum sg_premise_tac >- metis_tac [] >> fs [] >> - spose_not_then assume_tac >> - fs [not_le_eq_gt] -QED - -Theorem fix_fixed_diverges: - ∀f. is_valid_fp_body f ⇒ ∀x. ~(∃ n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x -Proof - rw [fix_def] >> - (* Case disjunction on the validity hypothesis *) - fs [is_valid_fp_body_def] >> - last_x_assum (qspec_assume ‘x’) >> - rw [] - >- ( - last_assum (qspec_assume ‘SUC n’) >> - fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> - first_assum (qspecl_assume [‘fix f’, ‘fix_fuel n f’]) >> - Cases_on ‘f (fix_fuel n f) x’ >> fs [] - ) >> - first_assum (qspec_assume ‘fix f’) >> fs [] >> - fs [fix_def] >> - (* Case disjunction on the ‘∃n. ...’ *) - rw [] >> - (* Use the hypothesis that there is no fuel s.t. ... *) - last_assum (qspec_assume ‘SUC n’) >> - fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> - first_assum (qspec_assume ‘fix_fuel n f’) >> - Cases_on ‘fix_fuel n f y’ >> fs [] -QED - -(* TODO: I think we can merge this with the theorem below *) -Theorem fix_fixed_termination_rec_case_aux: - ∀x y n m. - is_valid_fp_body f ⇒ - (∀g. f g x = g y) ⇒ - fix_fuel_P f x n ⇒ - fix_fuel_P f y m ⇒ - fix_fuel n f x = fix_fuel m f y -Proof - rw [] >> - Cases_on ‘n’ >- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> - pure_asm_rewrite_tac [fix_fuel_def] >> - sg ‘fix_fuel_P f y n'’ >- rfs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> - imp_res_tac fix_fuel_mono_least >> - fs [] -QED - -Theorem fix_fixed_termination_rec_case: - ∀ x y n m. - is_valid_fp_body f ⇒ - (∀g. f g x = g y) ⇒ - fix_fuel_P f x n ⇒ - fix_fuel_P f y m ⇒ - fix_fuel ($LEAST (fix_fuel_P f x)) f x = - fix_fuel ($LEAST (fix_fuel_P f y)) f y -Proof - rw [] >> - imp_res_tac fix_fuel_mono_least >> - irule fix_fixed_termination_rec_case_aux >> - fs [] >> - (* TODO: factorize *) - qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >> - pop_assum sg_premise_tac >- metis_tac [] >> - qspec_assume ‘fix_fuel_P f y’ whileTheory.LEAST_EXISTS_IMP >> - pop_assum sg_premise_tac >- metis_tac [] >> - rw [] -QED - -Theorem fix_fixed_terminates: - ∀f. is_valid_fp_body f ⇒ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x -Proof - rpt strip_tac >> - (* Case disjunction on the validity hypothesis - we don't want to consume it *) - last_assum mp_tac >> - pure_rewrite_tac [is_valid_fp_body_def] >> rpt strip_tac >> - pop_assum (qspec_assume ‘x’) >> - rw [] - >-( (* No recursive call *) - fs [fix_def] >> rw [] >> fs [] >> - imp_res_tac fix_fuel_mono_least >> - Cases_on ‘$LEAST (fix_fuel_P f x)’ >> fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] - ) >> - (* There exists a recursive call *) - SUBGOAL_THEN “∃m. fix_fuel_P f y m” assume_tac >-( - Cases_on ‘n’ >> - fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> - metis_tac [] - ) >> - fs [fix_def] >> rw [] >> fs [] >> - irule fix_fixed_termination_rec_case >> - fs [] >> - metis_tac [] -QED - -Theorem fix_fixed_eq: - ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x -Proof - rw [] >> - Cases_on ‘∃n. fix_fuel_P f x n’ - >- (irule fix_fixed_terminates >> metis_tac []) >> - irule fix_fixed_diverges >> - fs [] -QED - -(* Testing on an example *) -Datatype: - list_t = - ListCons 't list_t - | ListNil -End - -val nth_body_def = Define ‘ - nth_body (f : ('t list_t # u32) -> 't result) (x : ('t list_t # u32)) : 't result = - let (ls, i) = x in - 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); - f (tl, i0) - od - | ListNil => Fail Failure -’ - -(* TODO: move *) -Theorem is_valid_suffice: - ∃y. ∀g. g x = g y -Proof - metis_tac [] -QED - -(* The general proof of is_valid_fp_body *) -Theorem nth_body_is_valid: - is_valid_fp_body nth_body -Proof - pure_rewrite_tac [is_valid_fp_body_def] >> - gen_tac >> - (* TODO: automate this *) - Cases_on ‘x’ >> fs [] >> - (* Expand *) - fs [nth_body_def, bind_def] >> - (* Explore all paths *) - Cases_on ‘q’ >> fs [is_valid_suffice] >> - Cases_on ‘u32_to_int r = 0’ >> fs [is_valid_suffice] >> - Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [is_valid_suffice] -QED - -val nth_raw_def = Define ‘ - nth (ls : 't list_t) (i : u32) = fix nth_body (ls, i) -’ - -Theorem nth_def: - ∀ls i. 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 -Proof - rpt strip_tac >> - (* Expand the raw definition *) - pure_rewrite_tac [nth_raw_def] >> - (* Use the fixed-point equality *) - sg ‘fix nth_body (ls,i) = nth_body (fix nth_body) (ls,i)’ - >- simp_tac bool_ss [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >> - pure_asm_rewrite_tac [] >> - (* Expand the body definition *) - qspecl_assume [‘fix nth_body’, ‘(ls, i)’] nth_body_def >> - pure_asm_rewrite_tac [LET_THM] >> - simp_tac arith_ss [] -QED - -val _ = export_theory () diff --git a/backends/hol4/divDefProtoTheory.sig b/backends/hol4/divDefProtoTheory.sig deleted file mode 100644 index e74c2fd4..00000000 --- a/backends/hol4/divDefProtoTheory.sig +++ /dev/null @@ -1,220 +0,0 @@ -signature divDefProtoTheory = -sig - type thm = Thm.thm - - (* Definitions *) - val fix_def : thm - val fix_fuel_P_def : thm - val fix_fuel_def : thm - val is_valid_fp_body_def : thm - val list_t_TY_DEF : thm - val list_t_case_def : thm - val list_t_size_def : thm - val nth_body_def : thm - - (* Theorems *) - val datatype_list_t : thm - val fix_fixed_diverges : thm - val fix_fixed_eq : thm - val fix_fixed_terminates : thm - val fix_fixed_termination_rec_case : thm - val fix_fixed_termination_rec_case_aux : thm - val fix_fuel_compute : thm - val fix_fuel_mono : thm - val fix_fuel_mono_least : thm - val is_valid_suffice : 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 nth_body_is_valid : thm - val nth_def : thm - - val divDefProto_grammars : type_grammar.grammar * term_grammar.grammar -(* - [primitives] Parent theory of "divDefProto" - - [fix_def] Definition - - ⊢ ∀f x. - fix f x = - if ∃n. fix_fuel_P f x n then - fix_fuel ($LEAST (fix_fuel_P f x)) f x - else Diverge - - [fix_fuel_P_def] Definition - - ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x) - - [fix_fuel_def] Definition - - ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ - ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x - - [is_valid_fp_body_def] Definition - - ⊢ ∀f. is_valid_fp_body f ⇔ - ∀x. (∀g h. f g x = f h x) ∨ ∃y. ∀g. f g x = g y - - [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 - - [nth_body_def] Definition - - ⊢ ∀f x. - nth_body f x = - (let - (ls,i) = x - in - 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); f (tl,i0) od - | ListNil => Fail Failure) - - [datatype_list_t] Theorem - - ⊢ DATATYPE (list_t ListCons ListNil) - - [fix_fixed_diverges] Theorem - - ⊢ ∀f. is_valid_fp_body f ⇒ - ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x - - [fix_fixed_eq] Theorem - - ⊢ ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x - - [fix_fixed_terminates] Theorem - - ⊢ ∀f. is_valid_fp_body f ⇒ - ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x - - [fix_fixed_termination_rec_case] Theorem - - ⊢ ∀x y n m. - is_valid_fp_body f ⇒ - (∀g. f g x = g y) ⇒ - fix_fuel_P f x n ⇒ - fix_fuel_P f y m ⇒ - fix_fuel ($LEAST (fix_fuel_P f x)) f x = - fix_fuel ($LEAST (fix_fuel_P f y)) f y - - [fix_fixed_termination_rec_case_aux] Theorem - - ⊢ ∀x y n m. - is_valid_fp_body f ⇒ - (∀g. f g x = g y) ⇒ - fix_fuel_P f x n ⇒ - fix_fuel_P f y m ⇒ - fix_fuel n f x = fix_fuel m f y - - [fix_fuel_compute] Theorem - - ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ - (∀n f x. - fix_fuel (NUMERAL (BIT1 n)) f x = - f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧ - ∀n f x. - fix_fuel (NUMERAL (BIT2 n)) f x = - f (fix_fuel (NUMERAL (BIT1 n)) f) x - - [fix_fuel_mono] Theorem - - ⊢ ∀f. is_valid_fp_body f ⇒ - ∀n x. - fix_fuel_P f x n ⇒ - ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x - - [fix_fuel_mono_least] Theorem - - ⊢ ∀f. is_valid_fp_body f ⇒ - ∀n x. - fix_fuel_P f x n ⇒ - fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x - - [is_valid_suffice] Theorem - - ⊢ ∃y. ∀g. g x = g y - - [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 - - [nth_body_is_valid] Theorem - - ⊢ is_valid_fp_body nth_body - - [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 - - -*) -end diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefScript.sml index 9efe835b..c742fb1f 100644 --- a/backends/hol4/divDefProto2Script.sml +++ b/backends/hol4/divDefScript.sml @@ -1,4 +1,11 @@ -(* Prototype: divDefLib but with general combinators *) +(* This file introduces a fixed-point operator to define potentially diverging + functions so that the user doesn't have to prove termination at *definition time* + but can prove it in an extrinsic manner. + + See divDefLib for a library which uses this fixed-point operator in an automated + manner, and divDefExampleScript for hand-written and well commented examples of + how to use it. + *) open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory @@ -6,27 +13,34 @@ open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory open primitivesLib -val _ = new_theory "divDefProto2" +val _ = new_theory "divDef" -(* - * Test with a general validity predicate. - * - * TODO: this works! Cleanup. - *) +(*====================== + * Fixed-point operator + *======================*) + +(* An auxiliary operator which uses some fuel *) val fix_fuel_def = Define ‘ (fix_fuel (0 : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧ (fix_fuel (SUC n) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = f (fix_fuel n f) x) ’ +(* An auxiliary predicate *) val fix_fuel_P_def = Define ‘ fix_fuel_P f x n = ~(is_diverge (fix_fuel n f x)) ’ +(* The fixed point operator *) val fix_def = Define ‘ fix (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge ’ +(* A validity condition. + + If a function body ‘f’ satisfies this condition, then we have the fixed point + equation ‘fix f = f (fix f)’ (see [fix_fixed_eq]). + *) val is_valid_fp_body_def = Define ‘ (is_valid_fp_body (0 : num) (f : ('a -> 'a result) -> 'a -> 'a result) = F) ∧ @@ -35,9 +49,11 @@ val is_valid_fp_body_def = Define ‘ (∃ h y. is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od)) ’ - +(*====================== + * Lemmas + *======================*) (* Auxiliary lemma. - We generalize the goal of fix_fuel_mono in the case the fuel is non-empty + We generalize the goal of [fix_fuel_mono] in the case the fuel is non-empty (this allows us to unfold definitions like ‘fix_fuel’ once, and reveal a first intermediate function). @@ -93,6 +109,7 @@ Proof gvs [] QED +(* ‘fix_fuel’ is monotonous over the fuel *) Theorem fix_fuel_mono: ∀N f. is_valid_fp_body N f ⇒ ∀n x. fix_fuel_P f x n ⇒ @@ -108,7 +125,6 @@ Proof gvs [fix_fuel_def] QED -(* TODO: remove? *) Theorem fix_fuel_mono_least: ∀N f. is_valid_fp_body N f ⇒ ∀n x. fix_fuel_P f x n ⇒ @@ -149,7 +165,11 @@ Proof rw [] QED -(* If ‘g (fix f) x’ doesn't diverge, we can exhibit some fuel *) +(* If ‘g (fix f) x’ doesn't diverge, we can write it in terms of ‘g (fix_fuel n f)’ + for some fuel ‘n’. + + This is an auxiliary lemma used to prove [fix_not_diverge_implies_fix_fuel] + *) Theorem fix_not_diverge_implies_fix_fuel_aux: ∀N M g f. is_valid_fp_body M f ⇒ is_valid_fp_body N g ⇒ @@ -215,7 +235,8 @@ Proof first_x_assum (fn th => assume_tac (GSYM th)) >> fs [] QED -(* If ‘g (fix f) x’ doesn't diverge, we can exhibit some fuel *) +(* If ‘g (fix f) x’ doesn't diverge, we can write it in terms of ‘g (fix_fuel n f)’ + for some fuel ‘n’. *) Theorem fix_not_diverge_implies_fix_fuel: ∀N f. is_valid_fp_body N f ⇒ ∀x. f (fix f) x ≠ Diverge ⇒ @@ -224,6 +245,7 @@ Proof metis_tac [fix_not_diverge_implies_fix_fuel_aux] QED +(* ‘fix’ satisfies the fixed point equation in case the evaluation diverges *) Theorem fix_fixed_diverges: ∀N f. is_valid_fp_body N f ⇒ ∀x. ~(∃ n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x Proof @@ -272,6 +294,7 @@ Proof metis_tac [fix_fuel_not_diverge_eq_fix_aux] QED +(* ‘fix’ satisfies the fixed point equation in case the evaluation terminates *) Theorem fix_fixed_terminates: ∀N f. is_valid_fp_body N f ⇒ ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x Proof @@ -287,6 +310,7 @@ Proof Cases_on ‘f (fix_fuel n'' f) x’ >> fs [] >> metis_tac [] QED +(* The final fixed point equation *) Theorem fix_fixed_eq: ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x Proof @@ -295,272 +319,33 @@ Proof >- (irule fix_fixed_terminates >> metis_tac []) >> irule fix_fixed_diverges >> metis_tac [] -QED - -(*====================== - * Example 1: nth - *======================*) -Datatype: - list_t = - ListCons 't list_t - | ListNil -End - -(* We use this version of the body to prove that the body is valid *) -val nth_body_def = Define ‘ - nth_body (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result) - (x : (('t list_t # u32) + 't)) : - (('t list_t # u32) + 't) result = - (* Destruct the input. We need this to call the proper function in case - of mutually recursive definitions, but also to eliminate arguments - which correspond to the output value (the input type is the same - as the output type). *) - case x of - | INL x => ( - let (ls, i) = x in - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return (INR x) - else - do - i0 <- u32_sub i (int_to_u32 1); - r <- f (INL (tl, i0)); - (* Eliminate the invalid outputs. This is not necessary here, - but it is in the case of non tail call recursive calls. *) - case r of - | INL _ => Fail Failure - | INR i1 => Return (INR i1) - od - | ListNil => Fail Failure) - | INR _ => Fail Failure -’ - -(* We first prove the theorem with ‘SUC (SUC n)’ where ‘n’ is a variable - to prevent this quantity from being rewritten to 2 *) -Theorem nth_body_is_valid_aux: - is_valid_fp_body (SUC (SUC n)) nth_body -Proof - pure_once_rewrite_tac [is_valid_fp_body_def] >> - gen_tac >> - (* TODO: automate this *) - Cases_on ‘x’ >> fs [] >> - (* Expand *) - fs [nth_body_def, bind_def] >> - (* Explore all paths *) - Cases_on ‘x'’ >> fs [] >> - Cases_on ‘q’ >> fs [] >> - Cases_on ‘u32_to_int r = 0’ >> fs [] >> - Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] >> - disj2_tac >> - (* This is hard *) - qexists ‘\g x. case x of | INL _ => Fail Failure | INR i1 => Return (INR i1)’ >> - qexists ‘INL (l, a)’ >> - conj_tac - >-( - (* Prove that the body of h is valid *) - pure_once_rewrite_tac [is_valid_fp_body_def] >> - (* *) - fs []) >> - gen_tac >> - (* Explore all paths *) - Cases_on ‘g (INL (l,a))’ >> fs [] >> - Cases_on ‘a'’ >> fs [] -QED - -Theorem nth_body_is_valid: - is_valid_fp_body (SUC (SUC 0)) nth_body -Proof - irule nth_body_is_valid_aux QED -val nth_raw_def = Define ‘ - nth (ls : 't list_t) (i : u32) = - case fix nth_body (INL (ls, i)) of - | Fail e => Fail e - | Diverge => Diverge - | Return r => - case r of - | INL _ => Fail Failure - | INR x => Return x -’ - -(* Rewrite the goal once, and on the left part of the goal seen as an application *) -fun pure_once_rewrite_left_tac ths = - CONV_TAC (PATH_CONV "l" (PURE_ONCE_REWRITE_CONV ths)) +(*=============================== + * Utilities for the automation + *===============================*) -Theorem nth_def: - ∀ls i. 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 -Proof - rpt strip_tac >> - (* Expand the raw definition *) - pure_rewrite_tac [nth_raw_def] >> - (* Use the fixed-point equality - the rewrite must only be applied *on the left* of the equality, in the goal *) - pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq nth_body_is_valid] >> - (* Expand the body definition *) - pure_rewrite_tac [nth_body_def] >> - (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *) - fs [bind_def] >> - Cases_on ‘ls’ >> fs [] >> - Cases_on ‘u32_to_int i = 0’ >> fs [] >> - Cases_on ‘u32_sub i (int_to_u32 1)’ >> fs [] >> - Cases_on ‘fix nth_body (INL (l,a))’ >> fs [] >> - Cases_on ‘a'’ >> fs [] -QED - -(*====================== - * Example 2: even, odd - *======================*) +(* This theorem is important to shape the goal when proving that a body + satifies the fixed point validity property. -val even_odd_body_def = Define ‘ - even_odd_body - (f : (int + int + bool) -> (int + int + bool) result) - (x : int + int + bool) : (int + int + bool) result = - case x of - | INL i => - (* Even *) - if i = 0 then Return (INR (INR T)) - else - (case f (INR (INL (i - 1))) of - | Fail e => Fail e - | Diverge => Diverge - | Return r => - (* Eliminate the unwanted results *) - case r of - | INL _ => Fail Failure - | INR (INL _) => Fail Failure - | INR (INR b) => Return (INR (INR b)) - ) - | INR x => - case x of - | INL i => - (* Odd *) - if i = 0 then Return (INR (INR F)) - else - (case f (INL (i - 1)) of - | Fail e => Fail e - | Diverge => Diverge - | Return r => - (* Eliminate the unwanted results *) - case r of - | INL _ => Fail Failure - | INR (INL _) => Fail Failure - | INR (INR b) => Return (INR (INR b)) - ) - | INR _ => - (* This case is for the return value *) - Fail Failure -’ - -Theorem even_odd_body_is_valid_aux: - is_valid_fp_body (SUC (SUC n)) even_odd_body + Important: this theorem (and its usafe) relies on the fact that errors are just + transmitted to the caller (in particular, without modification). + *) +Theorem case_result_switch_eq: + (case (case x of Return y => f y | Fail e => Fail e | Diverge => Diverge) of + | Return y => g y + | Fail e => Fail e + | Diverge => Diverge) = + (case x of + | Return y => + (case f y of + | Return y => g y + | Fail e => Fail e + | Diverge => Diverge) + | Fail e => Fail e + | Diverge => Diverge) Proof - pure_once_rewrite_tac [is_valid_fp_body_def] >> - gen_tac >> - (* Expand *) - fs [even_odd_body_def, bind_def] >> - (* TODO: automate this *) Cases_on ‘x’ >> fs [] - >-( - Cases_on ‘x' = 0’ >> fs [] >> - (* Recursive call *) - disj2_tac >> - qexists ‘\g x. case x of | INL _ => Fail Failure | INR (INL _) => Fail Failure | INR (INR i1) => Return (INR (INR i1))’ >> - qexists ‘INR (INL (x' − 1))’ >> - conj_tac - >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >> - fs []) >> - Cases_on ‘y’ >> fs [] >> - Cases_on ‘x = 0’ >> fs [] >> - (* Recursive call *) - disj2_tac >> - qexists ‘\g x. case x of | INL _ => Fail Failure | INR (INL _) => Fail Failure | INR (INR i1) => Return (INR (INR i1))’ >> - qexists ‘INL (x − 1)’ >> - conj_tac - >-(pure_once_rewrite_tac [is_valid_fp_body_def] >> fs []) >> - fs [] -QED - -Theorem even_odd_body_is_valid: - is_valid_fp_body (SUC (SUC 0)) even_odd_body -Proof - irule even_odd_body_is_valid_aux -QED - -val even_raw_def = Define ‘ - even (i : int) = - case fix even_odd_body (INL i) of - | Fail e => Fail e - | Diverge => Diverge - | Return r => - case r of - | INL _ => Fail Failure - | INR (INL _) => Fail Failure - | INR (INR b) => Return b -’ - -val odd_raw_def = Define ‘ - odd (i : int) = - case fix even_odd_body (INR (INL i)) of - | Fail e => Fail e - | Diverge => Diverge - | Return r => - case r of - | INL _ => Fail Failure - | INR (INL _) => Fail Failure - | INR (INR b) => Return b -’ - -Theorem even_def: - ∀i. even (i : int) : bool result = - if i = 0 then Return T else odd (i - 1) -Proof - gen_tac >> - (* Expand the definition *) - pure_once_rewrite_tac [even_raw_def] >> - (* Use the fixed-point equality *) - pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >> - (* Expand the body definition *) - pure_rewrite_tac [even_odd_body_def] >> - (* Expand all the definitions from the group *) - pure_rewrite_tac [even_raw_def, odd_raw_def] >> - (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *) - fs [bind_def] >> - Cases_on ‘i = 0’ >> fs [] >> - Cases_on ‘fix even_odd_body (INR (INL (i − 1)))’ >> fs [] >> - Cases_on ‘a’ >> fs [] >> - Cases_on ‘y’ >> fs [] -QED - -Theorem odd_def: - ∀i. odd (i : int) : bool result = - if i = 0 then Return F else even (i - 1) -Proof - gen_tac >> - (* Expand the definition *) - pure_once_rewrite_tac [odd_raw_def] >> - (* Use the fixed-point equality *) - pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq even_odd_body_is_valid] >> - (* Expand the body definition *) - pure_rewrite_tac [even_odd_body_def] >> - (* Expand all the definitions from the group *) - pure_rewrite_tac [even_raw_def, odd_raw_def] >> - (* Explore all the paths - maybe we can be smarter, but this is fast and really easy *) - fs [bind_def] >> - Cases_on ‘i = 0’ >> fs [] >> - Cases_on ‘fix even_odd_body (INL (i − 1))’ >> fs [] >> - Cases_on ‘a’ >> fs [] >> - Cases_on ‘y’ >> fs [] QED val _ = export_theory () diff --git a/backends/hol4/divDefTheory.sig b/backends/hol4/divDefTheory.sig new file mode 100644 index 00000000..15592052 --- /dev/null +++ b/backends/hol4/divDefTheory.sig @@ -0,0 +1,187 @@ +signature divDefTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val fix_def : thm + val fix_fuel_P_def : thm + val fix_fuel_def : thm + val is_valid_fp_body_def : thm + + (* Theorems *) + val case_result_switch_eq : thm + val fix_fixed_diverges : thm + val fix_fixed_eq : thm + val fix_fixed_terminates : thm + val fix_fuel_P_least : thm + val fix_fuel_compute : thm + val fix_fuel_eq_fix : thm + val fix_fuel_mono : thm + val fix_fuel_mono_aux : thm + val fix_fuel_mono_least : thm + val fix_fuel_not_diverge_eq_fix : thm + val fix_fuel_not_diverge_eq_fix_aux : thm + val fix_not_diverge_implies_fix_fuel : thm + val fix_not_diverge_implies_fix_fuel_aux : thm + val is_valid_fp_body_compute : thm + + val divDef_grammars : type_grammar.grammar * term_grammar.grammar +(* + [primitives] Parent theory of "divDef" + + [fix_def] Definition + + ⊢ ∀f x. + fix f x = + if ∃n. fix_fuel_P f x n then + fix_fuel ($LEAST (fix_fuel_P f x)) f x + else Diverge + + [fix_fuel_P_def] Definition + + ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x) + + [fix_fuel_def] Definition + + ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ + ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x + + [is_valid_fp_body_def] Definition + + ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧ + ∀n f. + is_valid_fp_body (SUC n) f ⇔ + ∀x. (∀g h. f g x = f h x) ∨ + ∃h y. + is_valid_fp_body n h ∧ ∀g. f g x = do z <- g y; h g z od + + [case_result_switch_eq] Theorem + + ⊢ (case + case x of + Return y => f y + | Fail e => Fail e + | Diverge => Diverge + of + Return y => g y + | Fail e => Fail e + | Diverge => Diverge) = + case x of + Return y => + (case f y of + Return y => g y + | Fail e => Fail e + | Diverge => Diverge) + | Fail e => Fail e + | Diverge => Diverge + + [fix_fixed_diverges] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀x. ¬(∃n. fix_fuel_P f x n) ⇒ fix f x = f (fix f) x + + [fix_fixed_eq] Theorem + + ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix f x = f (fix f) x + + [fix_fixed_terminates] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀x n. fix_fuel_P f x n ⇒ fix f x = f (fix f) x + + [fix_fuel_P_least] Theorem + + ⊢ ∀f n x. + fix_fuel n f x ≠ Diverge ⇒ + fix_fuel_P f x ($LEAST (fix_fuel_P f x)) + + [fix_fuel_compute] Theorem + + ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧ + (∀n f x. + fix_fuel (NUMERAL (BIT1 n)) f x = + f (fix_fuel (NUMERAL (BIT1 n) − 1) f) x) ∧ + ∀n f x. + fix_fuel (NUMERAL (BIT2 n)) f x = + f (fix_fuel (NUMERAL (BIT1 n)) f) x + + [fix_fuel_eq_fix] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀n x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix f x + + [fix_fuel_mono] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀n x. + fix_fuel_P f x n ⇒ ∀m. n ≤ m ⇒ fix_fuel n f x = fix_fuel m f x + + [fix_fuel_mono_aux] Theorem + + ⊢ ∀n N M g f. + is_valid_fp_body M f ⇒ + is_valid_fp_body N g ⇒ + ∀x. ¬is_diverge (g (fix_fuel n f) x) ⇒ + ∀m. n ≤ m ⇒ g (fix_fuel n f) x = g (fix_fuel m f) x + + [fix_fuel_mono_least] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀n x. + fix_fuel_P f x n ⇒ + fix_fuel n f x = fix_fuel ($LEAST (fix_fuel_P f x)) f x + + [fix_fuel_not_diverge_eq_fix] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀n x. + f (fix_fuel n f) x ≠ Diverge ⇒ f (fix f) x = f (fix_fuel n f) x + + [fix_fuel_not_diverge_eq_fix_aux] Theorem + + ⊢ ∀N M g f. + is_valid_fp_body M f ⇒ + is_valid_fp_body N g ⇒ + ∀n x. + g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x + + [fix_not_diverge_implies_fix_fuel] Theorem + + ⊢ ∀N f. + is_valid_fp_body N f ⇒ + ∀x. f (fix f) x ≠ Diverge ⇒ ∃n. f (fix f) x = f (fix_fuel n f) x + + [fix_not_diverge_implies_fix_fuel_aux] Theorem + + ⊢ ∀N M g f. + is_valid_fp_body M f ⇒ + is_valid_fp_body N g ⇒ + ∀x. g (fix f) x ≠ Diverge ⇒ + ∃n. g (fix f) x = g (fix_fuel n f) x ∧ + ∀m. n ≤ m ⇒ g (fix_fuel m f) x = g (fix_fuel n f) x + + [is_valid_fp_body_compute] Theorem + + ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧ + (∀n f. + is_valid_fp_body (NUMERAL (BIT1 n)) f ⇔ + ∀x. (∀g h. f g x = f h x) ∨ + ∃h y. + is_valid_fp_body (NUMERAL (BIT1 n) − 1) h ∧ + ∀g. f g x = do z <- g y; h g z od) ∧ + ∀n f. + is_valid_fp_body (NUMERAL (BIT2 n)) f ⇔ + ∀x. (∀g h. f g x = f h x) ∨ + ∃h y. + is_valid_fp_body (NUMERAL (BIT1 n)) h ∧ + ∀g. f g x = do z <- g y; h g z od + + +*) +end |