Write some tests for divDefProto2Script.sml

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