diff options
| -rw-r--r-- | backends/hol4/divDefProtoScript.sml | 525 | ||||
| -rw-r--r-- | backends/hol4/divDefProtoTheory.sig | 10 |
2 files changed, 12 insertions, 523 deletions
diff --git a/backends/hol4/divDefProtoScript.sml b/backends/hol4/divDefProtoScript.sml index 64d4b9f0..6280fa7e 100644 --- a/backends/hol4/divDefProtoScript.sml +++ b/backends/hol4/divDefProtoScript.sml @@ -101,7 +101,7 @@ Proof QED (* TODO: I think we can merge this with the theorem below *) -Theorem fix_fixed_termination_rec_case: +Theorem fix_fixed_termination_rec_case_aux: ∀x y n m. is_valid_fp_body f ⇒ (∀g. f g x = g y) ⇒ @@ -128,7 +128,7 @@ Theorem fix_fixed_termination_rec_case: Proof rw [] >> imp_res_tac fix_fuel_mono_least >> - irule fix_fixed_termination_rec_case >> + irule fix_fixed_termination_rec_case_aux >> fs [] >> (* TODO: factorize *) qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >> @@ -249,525 +249,4 @@ Proof 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 index 6e4e5950..e74c2fd4 100644 --- a/backends/hol4/divDefProtoTheory.sig +++ b/backends/hol4/divDefProtoTheory.sig @@ -18,6 +18,7 @@ sig 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 @@ -128,6 +129,15 @@ sig 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) ∧ |