diff options
| -rw-r--r-- | backends/hol4/divDefProtoScript.sml | 773 | ||||
| -rw-r--r-- | backends/hol4/divDefProtoTheory.sig | 210 |
2 files changed, 983 insertions, 0 deletions
diff --git a/backends/hol4/divDefProtoScript.sml b/backends/hol4/divDefProtoScript.sml new file mode 100644 index 00000000..64d4b9f0 --- /dev/null +++ b/backends/hol4/divDefProtoScript.sml @@ -0,0 +1,773 @@ +(* 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: + ∀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 >> + 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 + +(************************** FAILED TESTS *) + +(* +Datatype: + fresult = FReturn 'b | FFail error | FRec 'a +End + +(* TODO: monad converter from fresult to result + rewrite rules *) +val fres_to_res_def = Define ‘ + fres_to_res (f : 'a -> 'b result) (r : ('a, 'b) fresult) : 'b result = + case r of + | FReturn x => Return x + | FFail e => Fail e + | FRec y => f y +’ + +val fixa_fuel_def = Define ‘ + (fixa_fuel (0 : num) (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result = Diverge) ∧ + (fixa_fuel (SUC n) (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result = + fres_to_res (fixa_fuel n f) (f x)) +’ + +val fixa_fuel_P_def = Define ‘ + fixa_fuel_P f x n = ~(is_diverge (fixa_fuel n f x)) +’ + +val fixa_def = Define ‘ + fixa (f : 'a -> ('a, 'b) fresult) (x : 'a) : 'b result = + if (∃ n. fixa_fuel_P f x n) then fixa_fuel ($LEAST (fixa_fuel_P f x)) f x else Diverge +’ + +Theorem fixa_fuel_mono: + ∀n m. n <= m ⇒ (∀f x. fixa_fuel_P f x n ⇒ fixa_fuel n f x = fixa_fuel m f x) +Proof + Induct_on ‘n’ >> rpt strip_tac + >- (fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def]) >> + Cases_on ‘m’ >- int_tac >> fs [] >> + last_x_assum imp_res_tac >> + fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def] >> + Cases_on ‘f x’ >> fs [] +QED + +(* TODO: remove ? *) +Theorem fixa_fuel_P_least: + ∀f x n. fixa_fuel_P f x n ⇒ fixa_fuel_P f x ($LEAST (fixa_fuel_P f x)) +Proof + rw [] >> + (* Use the "fundamental" property about $LEAST *) + qspec_assume ‘fixa_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >> + (* Prove the premise *) + pop_assum sg_premise_tac >- metis_tac [] >> + rw [] +QED + +Theorem fixa_fuel_mono_least: + ∀n f x. fixa_fuel_P f x n ⇒ fixa_fuel n f x = fixa_fuel ($LEAST (fixa_fuel_P f x)) f x +Proof + rw [] >> + (* Use the "fundamental" property about $LEAST *) + qspec_assume ‘fixa_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >> + (* Prove the premise *) + pop_assum sg_premise_tac >- metis_tac [] >> + (* Prove that $LEAST ... ≤ n *) + sg ‘n >= $LEAST (fixa_fuel_P f x)’ >-( + spose_not_then assume_tac >> + fs [not_ge_eq_lt]) >> + pure_once_rewrite_tac [EQ_SYM_EQ] >> + irule fixa_fuel_mono >> + fs [] +QED + +Theorem fixa_fixed_eq: + ∀f x. fixa f x = fres_to_res (fixa f) (f x) +Proof + rw [fixa_def, fres_to_res_def] + >- ( + (* Termination case *) + imp_res_tac fixa_fuel_P_least >> + Cases_on ‘$LEAST (fixa_fuel_P f x)’ >> + fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def] >> + Cases_on ‘f x’ >> fs [] >> + rw [] >> fs [] >> + irule fixa_fuel_mono_least >> + fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def]) >> + (* Divergence case *) + fs [fres_to_res_def] >> + sg ‘∀n. ~(fixa_fuel_P f x (SUC n))’ >- fs [] >> + Cases_on ‘f x’ >> fs [] >> + fs [fixa_fuel_P_def, is_diverge_def, fixa_fuel_def, fres_to_res_def] >> + rw [] +QED + +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 +’ + +Theorem fixa_fuel_eq_fix_fuel: + ∀n (f : 'a -> ('a, 'b) fresult) (x : 'a). + fixa_fuel n f x = fix_fuel n (\g y. fres_to_res g (f y)) x +Proof + Induct_on ‘n’ >> rw [fixa_fuel_def, fix_fuel_def, fres_to_res_def] +QED + +Theorem fixa_fuel_P_eq_fix_fuel_P: + ∀(f : 'a -> ('a, 'b) fresult) (x : 'a). + fixa_fuel_P f x = fix_fuel_P (\g y. fres_to_res g (f y)) x +Proof + rw [] >> irule EQ_EXT >> rw [] >> + qspecl_assume [‘x'’, ‘f’, ‘x’] fixa_fuel_eq_fix_fuel >> + fs [fixa_fuel_P_def, fix_fuel_P_def] +QED + +Theorem fixa_fuel_eq_fix_fuel: + ∀(f : 'a -> ('a, 'b) fresult) (x : 'a). + fixa f x = fix (\g y. fres_to_res g (f y)) x +Proof + rw [fixa_def, fix_def, fixa_fuel_P_eq_fix_fuel_P, fixa_fuel_eq_fix_fuel] +QED + +(* + The annoying thing is that to make this work, we need to rewrite the + body by swapping matches, which is not easy to automate. +*) + +(* +f x = + case _ of + | _ => Fail e + | _ => Return x + | _ => f y + +f x (g : ('a, 'b) result => 'c) + +f x (fres_to_res g) = f x g + +*) + +(* +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 is_valid_FP_body_def = Define ‘ + is_valid_FP_body (f : (('a, 'b) fresult -> 'c) -> ('a, 'b) fresult -> 'c) = + ∃ (fa: (('a, 'b) fresult -> ('a, 'b) fresult) -> ('a, 'b) fresult -> ('a, 'b) fresult). + ∀ (g : ('a, 'b) fresult -> 'c) x. + f g x = g (fa (\x. x) x) + +val fix_fuel_def = Define ‘ + (fix_fuel (0 : num) (f : (('a, 'b) fresult -> 'b result) -> ('a, 'b) fresult -> 'b result) (x : ('a, 'b) fresult) : 'b result = Diverge) ∧ + (fix_fuel (SUC n) (f : (('a, 'b) fresult -> 'b result) -> ('a, 'b) fresult -> 'b result) (x : ('a, 'b) fresult) : '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 x : 'b result = + if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge + + +Theorem fix_fuel_mono: + ∀f. is_valid_FP_body f ⇒ + ∀n m. n <= m ⇒ (∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x) +Proof + strip_tac >> strip_tac >> + Induct_on ‘n’ >> rpt strip_tac + >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + Cases_on ‘m’ >- int_tac >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + fs [is_valid_FP_body] >> + last_x_assum (qspec_assume ‘fix_fuel n f’) >> + fs [] +QED + +’*) + +(* + * Test with a validity predicate which gives monotonicity. + + TODO: not enough to prove the fixed-point equation. + *) +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 +’ + +Theorem fix_eq: + fix f = \x. if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge +Proof + irule EQ_EXT >> fs [fix_def] +QED + +val is_valid_fp_body_def = Define ‘ + is_valid_fp_body (f : ('a -> 'b result) -> 'a -> 'b result) = + ∀n m. n ≤ m ⇒ ∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x +’ + +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 [] >> + (* 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 [] >> + (* Prove that $LEAST ... ≤ n *) + sg ‘n >= $LEAST (fix_fuel_P f x)’ >-( + spose_not_then assume_tac >> + fs [not_ge_eq_lt]) >> + pure_once_rewrite_tac [EQ_SYM_EQ] >> + (* Finish by using the monotonicity property *) + fs [is_valid_fp_body_def] +QED + + +(* TODO: remove ? *) +Theorem fix_fuel_P_least: + ∀f x n. fix_fuel_P f x n ⇒ fix_fuel_P f x ($LEAST (fix_fuel_P f x)) +Proof + rw [] >> + (* 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 [] >> + rw [] +QED + +(*Theorem test: + fix_fuel_P f x (SUC n) ⇒ + (∀m. n ≤ m ⇒ f (fix_fuel n f) x = f (fix_fuel m f) x) ⇒ + f (fix_fuel n f) x = f (fix f) x +Proof + rw [] >> + spose_not_then assume_tac >> + fs [fix_eq] +*) +Theorem fix_fixed_eq: + ∀f. is_valid_fp_body f ⇒ ∀x. fix f x = f (fix f) x +Proof + rw [fix_def] >> CASE_TAC >> fs [] + >- ( + (* Termination case *) + sg ‘$LEAST (fix_fuel_P f x) <= n’ >- cheat >> + imp_res_tac fix_fuel_P_least >> + Cases_on ‘$LEAST (fix_fuel_P f x)’ >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + Cases_on ‘n’ >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + (* Use the validity assumption *) + fs [is_valid_fp_body_def] >> + +(* last_x_assum imp_res_tac >> *) + last_assum (qspecl_assume [‘SUC n'’, ‘SUC n''’]) >> fs [] >> + pop_assum imp_res_tac >> + pop_assum (qspec_assume ‘x’) >> + pop_assum sg_premise_tac >- fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + + fs [fix_fuel_def] >> + + + fs [fix_fuel_P_def] >> + rfs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + + fs [fix_eq] >> + + Cases_on ‘fix_fuel n' f x’ >> fs [] >> + last_assum (qspecl_then [‘n'’, ‘’ + f (fix_fuel n' f) x >> + + Cases_on ‘f x’ >> fs [] >> + rw [] >> fs [] >> + irule fix_fuel_mono_least >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> + (* Divergence case *) + fs [fres_to_res_def] >> + sg ‘∀n. ~(fix_fuel_P f x (SUC n))’ >- fs [] >> + Cases_on ‘f x’ >> fs [] >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + rw [] +QED + + +(* A slightly weaker and more precise validity criteria. + + We simply extracted the part of the inductive proof that we can't prove without + knowing ‘f’. + *) +val is_valid_fp_body_weak_def = Define ‘ + is_valid_fp_body_weak f = + ∀n m x. + ((∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x) ⇒ + n ≤ m ⇒ + fix_fuel_P f x (SUC n) ⇒ + fix_fuel (SUC n) f x = fix_fuel (SUC m) f x) +’ + +Theorem is_valid_fp_body_weak_imp_is_valid: + ∀f. is_valid_fp_body_weak f ⇒ is_valid_fp_body f +Proof + rpt strip_tac >> fs [is_valid_fp_body_def] >> + Induct_on ‘n’ >- fs [fix_fuel_P_def, fix_fuel_def, is_diverge_def] >> + Cases_on ‘m’ >> fs [] >> + fs [is_valid_fp_body_weak_def] +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) +’ + +(* The general proof of is_valid_fp_body. We isolate a more precise property below. *) +Theorem nth_body_is_valid: + is_valid_fp_body nth_body +Proof + pure_rewrite_tac [is_valid_fp_body_def] >> + Induct_on ‘n’ >- fs [fix_fuel_P_def, fix_fuel_def, is_diverge_def] >> + Cases_on ‘m’ >- fs [] >> + rpt strip_tac >> + (* TODO: here *) + last_assum imp_res_tac >> + (* TODO: here? *) + fs [fix_fuel_def, nth_body_def, fix_fuel_P_def, is_diverge_def, bind_def] >> + Cases_on ‘x’ >> fs [] >> (* TODO: automate this *) + (* Explore all paths *) + Cases_on ‘q’ >> fs [] >> + Cases_on ‘u32_to_int r = 0’ >> fs [] >> + Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] +QED + + +Theorem nth_body_is_valid_weak: + is_valid_fp_body_weak nth_body +Proof + pure_rewrite_tac [is_valid_fp_body_weak_def] >> + rpt strip_tac >> + (* TODO: automate this - we may need to destruct a variable number of times *) + Cases_on ‘x’ >> fs [] >> + (* Expand all *) + fs [fix_fuel_def, nth_body_def, fix_fuel_P_def, is_diverge_def, bind_def] >> + (* Explore all paths *) + Cases_on ‘q’ >> fs [] >> + Cases_on ‘u32_to_int r = 0’ >> fs [] >> + Cases_on ‘u32_sub r (int_to_u32 1)’ >> fs [] +QED + +(* + * Test with a more general validity predicate. + *) +(* We need to control the way calls to the continuation are performed, so + that we can inspect the inputs (otherwise we can't prove anything). + *) +val is_valid_FP_body_def = Define ‘ + is_valid_FP_body (f : (('a, 'b) fresult -> 'c) -> 'a -> 'c) = + ∃ (fa: (('a, 'b) fresult -> ('a, 'b) fresult) -> 'a -> ('a, 'b) fresult). + ∀ (g : ('a, 'b) fresult -> 'c) x. + f g x = g (fa (\x. x) x) +’ + + +val fix_fuel_def = Define ‘ + (fix_fuel (0 : num) (f : (('a, 'b) fresult -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = Diverge) ∧ + (fix_fuel (SUC n) (f : (('a, 'b) fresult -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result = + f (fres_to_res (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 x : 'b result = + if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge +’ + +Theorem fix_fuel_mono: + ∀f. is_valid_FP_body f ⇒ + ∀n m. n <= m ⇒ (∀x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x) +Proof + strip_tac >> strip_tac >> + Induct_on ‘n’ >> rpt strip_tac + >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def, fres_to_res_def] >> + Cases_on ‘m’ >- int_tac >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + fs [is_valid_FP_body_def, fres_to_res_def] >> + CASE_TAC >> + last_x_assum (qspec_assume ‘fres_to_res (fix_fuel n f)’) >> + fs [fres_to_res_def] +QED + +(* Tests *) + + + +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_body_def = Define ‘ + nth_body (f : ('t list_t # u32, 't) fresult -> 'c) (ls : 't list_t, i : u32) : 'c = + case ls of + | ListCons x tl => + if u32_to_int i = (0:int) + then f (FReturn x) + else + do + i0 <- u32_sub i (int_to_u32 1); + f (FRec (tl, i0)) + od + | ListNil => f (FFail Failure) +’ + +Theorem nth_body_is_valid_FP_body: + is_valid_FP_body nth_body +Proof + fs [is_valid_FP_body_def] >> + exists_tac “nth_body” >> +QED + +“nth_body” + +(* TODO: abbreviation for ‘(\g y. fres_to_res g (f y))’ *) +Theorem fix_fixed_eq: + ∀f x. fix (\g y. fres_to_res g (f y)) x = + (f x) + fres_to_res (\g y. fres_to_res g (f y)) + + + +(* +TODO: can't prove that + +Theorem fix_fuel_mono: + ∀n m. n <= m ⇒ (∀f x. fix_fuel_P f x n ⇒ fix_fuel n f x = fix_fuel m f x) +Proof + Induct_on ‘n’ >> rpt strip_tac + >- (fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def]) >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + Cases_on ‘m’ >- int_tac >> + fs [fix_fuel_P_def, is_diverge_def, fix_fuel_def] >> + + sg ‘fix_fuel n f = fix_fuel n' f’ >> + + last_x_assum imp_res_tac >> + pop_assum (qspecl_assume [‘x’, ‘f’]) >> + +Theorem fix_def_eq: + ∀f x. fix f x = f (fix f) x +Proof + +*) +*) + + +val _ = export_theory () diff --git a/backends/hol4/divDefProtoTheory.sig b/backends/hol4/divDefProtoTheory.sig new file mode 100644 index 00000000..6e4e5950 --- /dev/null +++ b/backends/hol4/divDefProtoTheory.sig @@ -0,0 +1,210 @@ +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_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_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 |