From 829f098c5cfae032f897d20f691a9f1f338b15bb Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 11 May 2023 15:55:50 +0200
Subject: Update divDefProto2Script.sml

---
 backends/hol4/divDefProto2Script.sml | 71 ++++++++----------------------------
 1 file changed, 16 insertions(+), 55 deletions(-)

(limited to 'backends/hol4/divDefProto2Script.sml')

diff --git a/backends/hol4/divDefProto2Script.sml b/backends/hol4/divDefProto2Script.sml
index 074006c9..9da186c1 100644
--- a/backends/hol4/divDefProto2Script.sml
+++ b/backends/hol4/divDefProto2Script.sml
@@ -322,8 +322,8 @@ Datatype:
 End
 
 (* We use this version of the body to prove that the body is valid *)
-val nth_body_valid_def = Define ‘
-  nth_body_valid (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
+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 =
     case x of
@@ -352,15 +352,17 @@ Proof
   metis_tac []
 QED
 
-Theorem nth_body_valid_is_valid:
-  is_valid_fp_body (SUC (SUC 0)) nth_body_valid
+(* 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_valid_def, bind_def] >>
+  fs [nth_body_def, bind_def] >>
   (* Explore all paths *)
   Cases_on ‘x'’ >> fs [] >>
   Cases_on ‘q’ >> fs [] >>
@@ -373,8 +375,6 @@ Proof
   conj_tac
   >-(
     (* Prove that the body of h is valid *)
-    sg ‘1 = SUC 0’ >- fs [] >>
-    pop_assum (fn th => pure_rewrite_tac [th]) >>
     pure_once_rewrite_tac [is_valid_fp_body_def] >>
     (* *)
     fs []) >>
@@ -384,52 +384,15 @@ Proof
   Cases_on ‘a'’ >> fs []
 QED
 
-(* We prove that ‘nth_body_valid’ is equivalent to ‘nth_body’ *)
-val nth_body1_def = Define ‘
-  nth_body1 (f : (('t list_t # u32) + 't) -> (('t list_t # u32) + 't) result)
-    (x : (('t list_t # u32) + 't)) :
-    (('t list_t # u32) + 't) result =
-    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 <- case f (INL (tl, i0)) of
-               | Fail e => Fail e
-               | Diverge => Diverge
-               | Return r =>
-                 case r of
-                 | INL _ => Fail Failure
-                 | INR i1 => Return i1;
-          Return (INR r)
-          od
-      | ListNil => Fail Failure)
-    | INR _ => Fail Failure
-’
-
-Theorem nth_body_valid_eq:
-  nth_body_valid = nth_body1
+Theorem nth_body_is_valid:
+  is_valid_fp_body (SUC (SUC 0)) nth_body
 Proof
-  ntac 2 (irule EQ_EXT >> gen_tac) >>
-  pure_rewrite_tac [nth_body_valid_def, nth_body1_def, bind_def, LET_DEF] >>
-  (* TODO: automate *)
-  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 [] >>
-  Cases_on ‘x (INL (l,a))’ >> fs [] >>
-  Cases_on ‘a'’ >> fs []
+  irule nth_body_is_valid_aux
 QED
 
 val nth_raw_def = Define ‘
   nth (ls : 't list_t) (i : u32) =
-    case fix nth_body1 (INL (ls, i)) of
+    case fix nth_body (INL (ls, i)) of
     | Fail e => Fail e
     | Diverge => Diverge
     | Return r =>
@@ -455,20 +418,18 @@ Proof
   (* Expand the raw definition *)
   pure_rewrite_tac [nth_raw_def] >>
   (* Use the fixed-point equality *)
-  sg ‘fix nth_body1 (INL (ls,i)) = nth_body1 (fix nth_body1) (INL (ls,i))’
-  >- (
-    pure_rewrite_tac [GSYM nth_body_valid_eq] >>
-    simp_tac bool_ss [HO_MATCH_MP fix_fixed_eq nth_body_valid_is_valid]) >>
+  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]) >>
   (* Expand the body definition *)
-  qspecl_assume [‘fix nth_body1’, ‘(INL (ls, i))’] nth_body1_def >>
+  qspecl_assume [‘fix nth_body’, ‘(INL (ls, i))’] nth_body_def >>
   pop_assum (fn th => pure_rewrite_tac [th, LET_THM]) >>
-  (* Do we really have to explore all the paths again? If yes, nth_body1 is useless *)
+  (* 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_body1 (INL (l,a))’ >> fs [] >>
+  Cases_on ‘fix nth_body (INL (l,a))’ >> fs [] >>
   Cases_on ‘a'’ >> fs []
 QED
 
-- 
cgit v1.2.3