diff options
| -rw-r--r-- | backends/hol4/divDefProto2Script.sml | 191 | ||||
| -rw-r--r-- | backends/hol4/divDefProto2Theory.sig | 107 |
2 files changed, 214 insertions, 84 deletions
diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefProto2Script.sml index 9da186c1..9dc43ea7 100644 --- a/backends/hol4/divDefProto2Script.sml +++ b/backends/hol4/divDefProto2Script.sml @@ -298,23 +298,9 @@ Proof metis_tac [] QED -(* - * Attempt to make the lemmas work with more general types - * (we want ‘: 'a -> 'b result’, not ‘:'a -> 'a result’). - *) -val simp_types_def = Define ‘ - simp_types (f : 'a -> 'b result) : ('a + 'b) -> ('a + 'b) result = - \x. case x of - | INL x => - (case f x of - | Fail e => Fail e - | Diverge => Diverge - | Return y => - Return (INR y)) - | INR _ => Fail Failure -’ - -(* Testing on an example *) +(*====================== + * Example 1: nth + *======================*) Datatype: list_t = ListCons 't list_t @@ -326,6 +312,10 @@ 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 @@ -337,6 +327,8 @@ val nth_body_def = Define ‘ 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) @@ -345,13 +337,6 @@ val nth_body_def = Define ‘ | INR _ => Fail Failure ’ -(* TODO: move *) -Theorem is_valid_suffice: - ∃y. ∀g. g x = g y -Proof - metis_tac [] -QED - (* 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: @@ -401,6 +386,10 @@ val nth_raw_def = Define ‘ | 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)) + Theorem nth_def: ∀ls i. nth (ls : 't list_t) (i : u32) : 't result = case ls of @@ -417,13 +406,10 @@ Proof rpt strip_tac >> (* Expand the raw definition *) pure_rewrite_tac [nth_raw_def] >> - (* Use the fixed-point equality *) - sg ‘fix nth_body (INL (ls,i)) = nth_body (fix nth_body) (INL (ls,i))’ - >- (simp_tac bool_ss [HO_MATCH_MP fix_fixed_eq nth_body_is_valid]) >> - pop_assum (fn th => pure_asm_rewrite_tac [th]) >> + (* 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 *) - qspecl_assume [‘fix nth_body’, ‘(INL (ls, i))’] nth_body_def >> - pop_assum (fn th => pure_rewrite_tac [th, LET_THM]) >> + 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 [] >> @@ -433,4 +419,149 @@ Proof Cases_on ‘a'’ >> fs [] QED +(*====================== + * Example 2: even, odd + *======================*) + +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 +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/divDefProto2Theory.sig b/backends/hol4/divDefProto2Theory.sig index 7ce4b194..77d5631e 100644 --- a/backends/hol4/divDefProto2Theory.sig +++ b/backends/hol4/divDefProto2Theory.sig @@ -3,6 +3,7 @@ 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 @@ -10,12 +11,13 @@ sig val list_t_TY_DEF : thm val list_t_case_def : thm val list_t_size_def : thm - val nth_body1_def : thm - val nth_body_valid_def : thm - val simp_types_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 @@ -30,7 +32,6 @@ sig 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 is_valid_suffice : thm val list_t_11 : thm val list_t_Axiom : thm val list_t_case_cong : thm @@ -38,14 +39,38 @@ sig val list_t_distinct : thm val list_t_induction : thm val list_t_nchotomy : thm - val nth_body_valid_eq : thm - val nth_body_valid_is_valid : 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. @@ -101,36 +126,10 @@ sig list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧ ∀f. list_t_size f ListNil = 0 - [nth_body1_def] Definition - - ⊢ ∀f x. - nth_body1 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 <- - case f (INL (tl,i0)) of - Return (INL v) => Fail Failure - | Return (INR i1) => Return i1 - | Fail e => Fail e - | Diverge => Diverge; - Return (INR r) - od - | ListNil => Fail Failure) - | INR v3 => Fail Failure - - [nth_body_valid_def] Definition + [nth_body_def] Definition ⊢ ∀f x. - nth_body_valid f x = + nth_body f x = case x of INL x => (let @@ -150,22 +149,22 @@ sig | ListNil => Fail Failure) | INR v2 => Fail Failure - [simp_types_def] Definition - - ⊢ ∀f. simp_types f = - (λx'. - case x' of - INL x => - (case f x of - Return y => Return (INR y) - | Fail e => Fail e - | Diverge => Diverge) - | INR v1 => 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. @@ -273,10 +272,6 @@ sig is_valid_fp_body (NUMERAL (BIT1 n)) h ∧ ∀g. f g x = do z <- g y; h g z od - [is_valid_suffice] Theorem - - ⊢ ∃y. ∀g. g x = g y - [list_t_11] Theorem ⊢ ∀a0 a1 a0' a1'. @@ -312,13 +307,13 @@ sig ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil - [nth_body_valid_eq] Theorem + [nth_body_is_valid] Theorem - ⊢ nth_body_valid = nth_body1 + ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body - [nth_body_valid_is_valid] Theorem + [nth_body_is_valid_aux] Theorem - ⊢ is_valid_fp_body (SUC (SUC 0)) nth_body_valid + ⊢ is_valid_fp_body (SUC (SUC n)) nth_body [nth_def] Theorem @@ -330,6 +325,10 @@ sig 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 |