summaryrefslogtreecommitdiff
path: root/backends/hol4
diff options
context:
space:
mode:
authorSon Ho2023-05-12 20:17:26 +0200
committerSon HO2023-06-04 21:54:38 +0200
commit8a5c5e4ae0cab0ab627c25ece59453a8e4bd4b64 (patch)
tree2e92885f457b610d183cf2e7f18fd05c5219ba60 /backends/hol4
parentc49fd4b6230a1f926e929f133794b6f73d338077 (diff)
Cleanup the files of the HOL4 backend
Diffstat (limited to '')
-rw-r--r--backends/hol4/TestTheory.sig839
-rw-r--r--backends/hol4/divDefExampleScript.sml418
-rw-r--r--backends/hol4/divDefExampleTheory.sig188
-rw-r--r--backends/hol4/divDefLib.sig98
-rw-r--r--backends/hol4/divDefLib.sml1789
-rw-r--r--backends/hol4/divDefLibExampleScript.sml29
-rw-r--r--backends/hol4/divDefNoFixLib.sig99
-rw-r--r--backends/hol4/divDefNoFixLib.sml1203
-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.sml23
-rw-r--r--backends/hol4/divDefProto2Theory.sig334
-rw-r--r--backends/hol4/divDefProtoScript.sml252
-rw-r--r--backends/hol4/divDefProtoTheory.sig220
-rw-r--r--backends/hol4/divDefScript.sml (renamed from backends/hol4/divDefProto2Script.sml)329
-rw-r--r--backends/hol4/divDefTheory.sig187
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