diff options
| -rw-r--r-- | backends/hol4/divDefLib.sig | 93 | ||||
| -rw-r--r-- | backends/hol4/divDefLib.sml | 98 | ||||
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 3 | ||||
| -rw-r--r-- | backends/hol4/primitivesTheory.sig | 6 | ||||
| -rw-r--r-- | backends/hol4/testDivDefScript.sml | 87 | ||||
| -rw-r--r-- | backends/hol4/testDivDefTheory.sig | 380 |
6 files changed, 577 insertions, 90 deletions
diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig new file mode 100644 index 00000000..d63d7771 --- /dev/null +++ b/backends/hol4/divDefLib.sig @@ -0,0 +1,93 @@ +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. + + 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) + ]} + *) + val DefineDiv : term quotation -> thm list +end diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml index 3ecb32df..59c1edaf 100644 --- a/backends/hol4/divDefLib.sml +++ b/backends/hol4/divDefLib.sml @@ -1,21 +1,21 @@ (* This file implements utilities to define potentially diverging functions *) +structure divDefLib :> divDefLib = +struct + open HolKernel boolLib bossLib Parse open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory open primitivesLib -(* TODO: move *) -Theorem case_result_same_eq: - !(r : 'a result). +val case_result_same_eq = prove ( + “!(r : 'a result). (case r of Return x => Return x | Fail e => Fail e - | Diverge => Diverge) = r -Proof - rw [] >> CASE_TAC -QED + | Diverge => Diverge) = r”, + rw [] >> CASE_TAC) (* val ty = id_ty @@ -90,8 +90,6 @@ val bool_ty = “:bool” val alpha_tyvar : hol_type = “:'a” val beta_tyvar : hol_type = “:'b” -val is_diverge_def = Define ‘ - is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F’ val is_diverge_tm = “is_diverge: 'a result -> bool” val diverge_tm = “Diverge : 'a result” @@ -1202,84 +1200,4 @@ fun DefineDiv (def_qt : term quotation) = final_eqs end -(* - -val def_qt = ‘ - (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 even_def = DefineDiv def_qt - -(* Complexigying the above definition *) -val def_qt = ‘ - (even (i : int) : bool result = - if i = 0 then - do - b <- Return T; - Return b - od - else do - b <- odd (i - 1); - Return b - od - ) /\ - (odd (i : int) : bool result = - if i = 0 then - do - b <- Return F; - Return b - od - else do - b <- even (i - 1); - Return b - od) -’ - -val even_def = DefineDiv def_qt - -Datatype: - list_t = - ListCons 't list_t - | ListNil -End - -val def_qt = ‘ - nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - nth_mut_fwd tl i0 - od - | ListNil => - Fail Failure -’ - -val nth_mut_fwd_def = DefineDiv def_qt - -(* Checking what happens with non terminal calls *) -val def_qt = ‘ - nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = - case ls of - | ListCons x tl => - if u32_to_int i = (0:int) - then Return x - else - do - i0 <- u32_sub i (int_to_u32 1); - x <- nth_mut_fwd tl i0; - Return x - od - | ListNil => - Fail Failure -’ - -val nth_mut_fwd_def = DefineDiv def_qt - -*) +end diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 969e9f6e..00511f00 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -36,6 +36,9 @@ Overload monad_bind = ``bind`` Overload monad_unitbind = ``\x y. bind x (\z. y)`` Overload monad_ignore_bind = ``\x y. bind x (\z. y)`` +val is_diverge_def = Define ‘ + is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F’ + (* Allow the use of monadic syntax *) val _ = monadsyntax.enable_monadsyntax () diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig index cf550f00..fdf28172 100644 --- a/backends/hol4/primitivesTheory.sig +++ b/backends/hol4/primitivesTheory.sig @@ -86,6 +86,7 @@ sig val i8_rem_def : thm val i8_sub_def : thm val int_rem_def : thm + val is_diverge_def : thm val isize_add_def : thm val isize_div_def : thm val isize_mul_def : thm @@ -646,6 +647,11 @@ sig int_rem x y = if x ≥ 0 ∧ y ≥ 0 ∨ x < 0 ∧ y < 0 then x % y else -(x % y) + [is_diverge_def] Definition + + ⊢ ∀r. is_diverge r ⇔ + case r of Return v2 => F | Fail v3 => F | Diverge => T + [isize_add_def] Definition ⊢ ∀x y. isize_add x y = mk_isize (isize_to_int x + isize_to_int y) diff --git a/backends/hol4/testDivDefScript.sml b/backends/hol4/testDivDefScript.sml new file mode 100644 index 00000000..4a87895f --- /dev/null +++ b/backends/hol4/testDivDefScript.sml @@ -0,0 +1,87 @@ +open HolKernel boolLib bossLib Parse +open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory + +open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory +open primitivesLib divDefLib + +val _ = new_theory "testDivDef" + +val def_qt = ‘ + (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 even_def = DefineDiv def_qt + +(* Complexifying the above definition, and overriding on purpose *) +val def_qt = ‘ + (even (i : int) : bool result = + if i = 0 then + do + b <- Return T; + Return b + od + else do + b <- odd (i - 1); + Return b + od + ) /\ + (odd (i : int) : bool result = + if i = 0 then + do + b <- Return F; + Return b + od + else do + b <- even (i - 1); + Return b + od) +’ + +val even_def = DefineDiv def_qt + +Datatype: + list_t = + ListCons 't list_t + | ListNil +End + +val def_qt = ‘ + nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = + case ls of + | ListCons x tl => + if u32_to_int i = (0:int) + then Return x + else + do + i0 <- u32_sub i (int_to_u32 1); + nth_mut_fwd tl i0 + od + | ListNil => + Fail Failure +’ + +val nth_mut_fwd_def = DefineDiv def_qt + +(* Complexifying the above definition, and overriding on purpose *) +val def_qt = ‘ + nth_mut_fwd (ls : 't list_t) (i : u32) : 't result = + case ls of + | ListCons x tl => + if u32_to_int i = (0:int) + then Return x + else + do + i0 <- u32_sub i (int_to_u32 1); + x <- nth_mut_fwd tl i0; + Return x + od + | ListNil => + Fail Failure +’ + +val nth_mut_fwd_def = DefineDiv def_qt + +val _ = export_theory () diff --git a/backends/hol4/testDivDefTheory.sig b/backends/hol4/testDivDefTheory.sig new file mode 100644 index 00000000..a3ce2255 --- /dev/null +++ b/backends/hol4/testDivDefTheory.sig @@ -0,0 +1,380 @@ +signature testDivDefTheory = +sig + type thm = Thm.thm + + (* Definitions *) + val even___E_def : thm + val even___P_def : thm + val even___fuel0_def_UNION_extract0 : thm + val even___fuel0_def_UNION_extract1 : thm + val even___fuel0_def_UNION_primitive : thm + val even___fuel_def_UNION_extract0 : thm + val even___fuel_def_UNION_extract1 : thm + val even___fuel_def_UNION_primitive : thm + val even_def : thm + val list_t_TY_DEF : thm + val list_t_case_def : thm + val list_t_size_def : thm + val nth_mut_fwd___E_def : thm + val nth_mut_fwd___P_def : thm + val nth_mut_fwd_def : thm + val odd___E_def : thm + val odd___P_def : thm + val odd_def : thm + + (* Theorems *) + val datatype_list_t : thm + val even___fuel0_def : thm + val even___fuel0_ind : thm + val even___fuel_def : thm + val even___fuel_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 nth_mut_fwd___fuel0_def : thm + val nth_mut_fwd___fuel0_ind : thm + val nth_mut_fwd___fuel_def : thm + val nth_mut_fwd___fuel_ind : thm + + val testDivDef_grammars : type_grammar.grammar * term_grammar.grammar +(* + [primitives] Parent theory of "testDivDef" + + [even___E_def] Definition + + ⊢ ∀even odd i. + even___E even odd i = + if i = 0 then do b <- Return T; Return b od + else do b <- odd (i − 1); Return b od + + [even___P_def] Definition + + ⊢ ∀i $var$($n). + even___P i $var$($n) ⇔ ¬is_diverge (even___fuel0 $var$($n) i) + + [even___fuel0_def_UNION_extract0] Definition + + ⊢ ∀x x0. even___fuel0 x x0 = even___fuel0_def_UNION (INL (x,x0)) + + [even___fuel0_def_UNION_extract1] Definition + + ⊢ ∀x x0. odd___fuel0 x x0 = even___fuel0_def_UNION (INR (x,x0)) + + [even___fuel0_def_UNION_primitive] Definition + + ⊢ even___fuel0_def_UNION = + WFREC + (@R. WF R ∧ + (∀i $var$($n) $var$($m). + $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ + R (INR ($var$($m),i − 1)) (INL ($var$($n),i))) ∧ + ∀i $var$($n) $var$($m). + $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ + R (INL ($var$($m),i − 1)) (INR ($var$($n),i))) + (λeven___fuel0_def_UNION a. + case a of + INL ($var$($n),i) => + I + (case $var$($n) of + 0 => Diverge + | SUC $var$($m) => + if i = 0 then do b <- Return T; Return b od + else + do + b <- + even___fuel0_def_UNION + (INR ($var$($m),i − 1)); + Return b + od) + | INR ($var$($n'),i') => + I + (case $var$($n') of + 0 => Diverge + | SUC $var$($m) => + if i' = 0 then do b <- Return F; Return b od + else + do + b <- + even___fuel0_def_UNION (INL ($var$($m),i' − 1)); + Return b + od)) + + [even___fuel_def_UNION_extract0] Definition + + ⊢ ∀x x0. even___fuel x x0 = even___fuel_def_UNION (INL (x,x0)) + + [even___fuel_def_UNION_extract1] Definition + + ⊢ ∀x x0. odd___fuel x x0 = even___fuel_def_UNION (INR (x,x0)) + + [even___fuel_def_UNION_primitive] Definition + + ⊢ even___fuel_def_UNION = + WFREC + (@R. WF R ∧ + (∀i $var$($n) $var$($m). + $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ + R (INR ($var$($m),i − 1)) (INL ($var$($n),i))) ∧ + ∀i $var$($n) $var$($m). + $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ + R (INL ($var$($m),i − 1)) (INR ($var$($n),i))) + (λeven___fuel_def_UNION a. + case a of + INL ($var$($n),i) => + I + (case $var$($n) of + 0 => Diverge + | SUC $var$($m) => + if i = 0 then Return T + else even___fuel_def_UNION (INR ($var$($m),i − 1))) + | INR ($var$($n'),i') => + I + (case $var$($n') of + 0 => Diverge + | SUC $var$($m) => + if i' = 0 then Return F + else even___fuel_def_UNION (INL ($var$($m),i' − 1)))) + + [even_def] Definition + + ⊢ ∀i. even i = + if ∃ $var$($n). even___P i $var$($n) then + even___fuel0 ($LEAST (even___P i)) i + else Diverge + + [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_mut_fwd___E_def] Definition + + ⊢ ∀nth_mut_fwd ls i. + nth_mut_fwd___E nth_mut_fwd ls i = + case ls of + ListCons x tl => + if u32_to_int i = 0 then Return x + else + do + i0 <- u32_sub i (int_to_u32 1); + x <- nth_mut_fwd tl i0; + Return x + od + | ListNil => Fail Failure + + [nth_mut_fwd___P_def] Definition + + ⊢ ∀ls i $var$($n). + nth_mut_fwd___P ls i $var$($n) ⇔ + ¬is_diverge (nth_mut_fwd___fuel0 $var$($n) ls i) + + [nth_mut_fwd_def] Definition + + ⊢ ∀ls i. + nth_mut_fwd ls i = + if ∃ $var$($n). nth_mut_fwd___P ls i $var$($n) then + nth_mut_fwd___fuel0 ($LEAST (nth_mut_fwd___P ls i)) ls i + else Diverge + + [odd___E_def] Definition + + ⊢ ∀even odd i. + odd___E even odd i = + if i = 0 then do b <- Return F; Return b od + else do b <- even (i − 1); Return b od + + [odd___P_def] Definition + + ⊢ ∀i $var$($n). + odd___P i $var$($n) ⇔ ¬is_diverge (odd___fuel0 $var$($n) i) + + [odd_def] Definition + + ⊢ ∀i. odd i = + if ∃ $var$($n). odd___P i $var$($n) then + odd___fuel0 ($LEAST (odd___P i)) i + else Diverge + + [datatype_list_t] Theorem + + ⊢ DATATYPE (list_t ListCons ListNil) + + [even___fuel0_def] Theorem + + ⊢ (∀i $var$($n). + even___fuel0 $var$($n) i = + case $var$($n) of + 0 => Diverge + | SUC $var$($m) => + if i = 0 then do b <- Return T; Return b od + else do b <- odd___fuel0 $var$($m) (i − 1); Return b od) ∧ + ∀i $var$($n). + odd___fuel0 $var$($n) i = + case $var$($n) of + 0 => Diverge + | SUC $var$($m) => + if i = 0 then do b <- Return F; Return b od + else do b <- even___fuel0 $var$($m) (i − 1); Return b od + + [even___fuel0_ind] Theorem + + ⊢ ∀P0 P1. + (∀ $var$($n) i. + (∀ $var$($m). + $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ P1 $var$($m) (i − 1)) ⇒ + P0 $var$($n) i) ∧ + (∀ $var$($n) i. + (∀ $var$($m). + $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ P0 $var$($m) (i − 1)) ⇒ + P1 $var$($n) i) ⇒ + (∀v0 v1. P0 v0 v1) ∧ ∀v0 v1. P1 v0 v1 + + [even___fuel_def] Theorem + + ⊢ (∀i $var$($n). + even___fuel $var$($n) i = + case $var$($n) of + 0 => Diverge + | SUC $var$($m) => + if i = 0 then Return T else odd___fuel $var$($m) (i − 1)) ∧ + ∀i $var$($n). + odd___fuel $var$($n) i = + case $var$($n) of + 0 => Diverge + | SUC $var$($m) => + if i = 0 then Return F else even___fuel $var$($m) (i − 1) + + [even___fuel_ind] Theorem + + ⊢ ∀P0 P1. + (∀ $var$($n) i. + (∀ $var$($m). + $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ P1 $var$($m) (i − 1)) ⇒ + P0 $var$($n) i) ∧ + (∀ $var$($n) i. + (∀ $var$($m). + $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ P0 $var$($m) (i − 1)) ⇒ + P1 $var$($n) i) ⇒ + (∀v0 v1. P0 v0 v1) ∧ ∀v0 v1. P1 v0 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 + + [nth_mut_fwd___fuel0_def] Theorem + + ⊢ ∀ls i $var$($n). + nth_mut_fwd___fuel0 $var$($n) ls i = + case $var$($n) of + 0 => Diverge + | SUC $var$($m) => + 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); + x <- nth_mut_fwd___fuel0 $var$($m) tl i0; + Return x + od + | ListNil => Fail Failure + + [nth_mut_fwd___fuel0_ind] Theorem + + ⊢ ∀P. (∀ $var$($n) ls i. + (∀ $var$($m) x tl i0. + $var$($n) = SUC $var$($m) ∧ ls = ListCons x tl ∧ + u32_to_int i ≠ 0 ⇒ + P $var$($m) tl i0) ⇒ + P $var$($n) ls i) ⇒ + ∀v v1 v2. P v v1 v2 + + [nth_mut_fwd___fuel_def] Theorem + + ⊢ ∀ls i $var$($n). + nth_mut_fwd___fuel $var$($n) ls i = + case $var$($n) of + 0 => Diverge + | SUC $var$($m) => + case ls of + ListCons x tl => + if u32_to_int i = 0 then Return x + else + do + i0 <- u32_sub i (int_to_u32 1); + nth_mut_fwd___fuel $var$($m) tl i0 + od + | ListNil => Fail Failure + + [nth_mut_fwd___fuel_ind] Theorem + + ⊢ ∀P. (∀ $var$($n) ls i. + (∀ $var$($m) x tl i0. + $var$($n) = SUC $var$($m) ∧ ls = ListCons x tl ∧ + u32_to_int i ≠ 0 ⇒ + P $var$($m) tl i0) ⇒ + P $var$($n) ls i) ⇒ + ∀v v1 v2. P v v1 v2 + + +*) +end |