From 74e8e6b80b31b1df9123fbec9a7f910a68a0b1cd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 15 May 2023 12:01:48 +0200
Subject: Introduce fix_exec, an executable version of fix

---
 backends/hol4/divDefLib.sig            |  5 +++-
 backends/hol4/divDefLib.sml            | 23 +++++++++------
 backends/hol4/divDefScript.sml         | 52 ++++++++++++++++++++++++++++++++--
 backends/hol4/divDefTheory.sig         | 22 ++++++++++++++
 backends/hol4/primitivesBaseTacLib.sml |  1 +
 5 files changed, 90 insertions(+), 13 deletions(-)

(limited to 'backends')

diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig
index df879b4b..0de88db5 100644
--- a/backends/hol4/divDefLib.sig
+++ b/backends/hol4/divDefLib.sig
@@ -34,7 +34,10 @@
 
    Remark: "Partial recursive functions in higher-order logic", Alexander Krauss,
    introduces an interesting approach by means of an inductive. It could be
-   interesting to try and compare.
+   interesting to try and compare. One advantage of the current approach, though,
+   is that it is compatible with an "execution" through [EVAL]. But if we manage
+   to make [EVAL] use arbitrary rewriting theorems, then it doesn't make a
+   difference.
  *)
 
 signature divDefLib =
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index f53ef6f8..78e664e6 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -24,7 +24,12 @@ val fail_tm = “Fail : error -> 'a result”
 val fail_failure_tm = “Fail Failure : 'a result”
 val diverge_tm = “Diverge : 'a result”
 
+(* Switch to use ‘fix_exec’ (leading to executable definitions) and ‘fix’ (non
+   executable) *)
+val use_fix_exec = ref true
+
 val fix_tm = “fix”
+val fix_exec_tm = “fix_exec”
 val is_valid_fp_body_tm = “is_valid_fp_body”
 
 fun mk_result (ty : hol_type) : hol_type = Type.type_subst [ alpha_ty |-> ty ] result_ty
@@ -744,8 +749,8 @@ fun mk_raw_defs (in_out_tys : (hol_type * hol_type) list)
     (* Retrieve the body *)
     val body = (List.last o snd o strip_comb o concl) body_is_valid
 
-    (* Create the term ‘fix body’ *)
-    val fixed_body = mk_icomb (fix_tm, body)
+    (* Create the term ‘fix_exec body’ *)
+    val fixed_body = mk_icomb (if !use_fix_exec then fix_exec_tm else fix_tm, body)
 
     (* For every function in the group, generate the equation that we will
        use as definition. In particular:
@@ -814,12 +819,13 @@ fun prove_def_eq_tac
   (body_def : thm option) : tactic =
   let
     val body_def_thm = case body_def of SOME th => [th] | NONE => []
+    val fix_eq = if !use_fix_exec then fix_exec_fixed_eq else fix_fixed_eq
   in
     rpt gen_tac >>
     (* Expand the definition *)
     pure_once_rewrite_tac [current_raw_def] >>
     (* Use the fixed-point equality *)
-    pure_once_rewrite_left_tac [HO_MATCH_MP fix_fixed_eq is_valid] >>
+    pure_once_rewrite_left_tac [HO_MATCH_MP fix_eq is_valid] >>
     (* Expand the body definition *)
     pure_rewrite_tac body_def_thm >>
     (* Expand all the definitions from the group *)
@@ -896,13 +902,12 @@ fun DefineDiv (def_qt : term quotation) =
     (* Prove the final equations *)
     val def_eqs = prove_def_eqs body_is_valid def_tms raw_defs
 
-    (* Save the final equations as definitions.
-
-       Note that because we use the same names, doing this overrides the "raw"
-       definitions, which are then forgotten, which means we don't need to
-       manually delete them.
-     *)
+    (* Save the final equations as definitions. *)
     val thm_names = map (fn x => x ^ "_def") fnames
+    (* Because [store_definition] overrides existing names, it seems that in
+       practice we don't really need to  delete the previous definitions
+       (we still do it: it doesn't cost much). *)
+    val _ = map delete_binding thm_names
     val _ = map store_definition (zip thm_names def_eqs)
   in
     def_eqs
diff --git a/backends/hol4/divDefScript.sml b/backends/hol4/divDefScript.sml
index b80aa2bf..cc745e5d 100644
--- a/backends/hol4/divDefScript.sml
+++ b/backends/hol4/divDefScript.sml
@@ -36,6 +36,22 @@ Definition fix_def:
     if (∃ n. fix_fuel_P f x n) then fix_fuel ($LEAST (fix_fuel_P f x)) f x else Diverge
 End
 
+(* An "executable" fixed point operator - useful for unit tests: we first test
+   if ‘fix_fuel_P f x’ is true for a high quantity of fuel, otherwise we use
+   ‘fix’ (which is not executable).
+
+   We prove later that, under some constraints: ‘∀n. fix_nexec n f = fix f’
+ *)
+Definition fix_nexec_def:
+  fix_nexec (n : num) (f : ('a -> 'b result) -> 'a -> 'b result) (x : 'a) : 'b result =
+    if (fix_fuel_P f x n) then fix_fuel n f x else fix f x
+End
+
+(* We fix a quantity of fuel for ’fix_nexec *)
+Definition fix_exec_def:
+  fix_exec = fix_nexec 1000000
+End
+
 (* A validity condition.
 
    If a function body ‘f’ satisfies this condition, then we have the fixed point
@@ -50,9 +66,9 @@ Definition is_valid_fp_body_def:
                   ∀g. f g x = do z <- g y; h g z od))
 End
 
-(*======================
- * Lemmas
- *======================*)
+(*=====================================*
+ * Lemmas about ‘fix_fuel’ and ‘fix’
+ *=====================================*)
 (* Auxiliary lemma.
    We generalize the goal of [fix_fuel_mono] in the case the fuel is non-empty
    (this allows us to unfold definitions like ‘fix_fuel’ once, and reveal
@@ -322,6 +338,36 @@ Proof
   metis_tac []
 QED
 
+(*===============================
+ * Lemmas about ‘fix_exec’
+ *===============================*)
+
+(* Prove that ‘fix_nexec’ is equivalent to ‘fix’ *)
+Theorem fix_nexec_eq_fix:
+  ∀ N f n. is_valid_fp_body N f ⇒ fix_nexec n f = fix f
+Proof
+  rw [] >>
+  rpt (irule EQ_EXT >> gen_tac) >>
+  fs [fix_nexec_def, fix_def] >>
+  top_case_tac >>
+  case_tac >> fs [] >>
+  (* Use the properties of the least upper bound *)
+  qspec_assume ‘fix_fuel_P f x’ whileTheory.LEAST_EXISTS_IMP >>
+  pop_assum sg_premise_tac >- metis_tac [] >> fs [] >>
+  (* Use the monotonicity property *)
+  irule fix_fuel_mono_least >> metis_tac []
+QED
+
+(* Prove the fixed point property for ‘fix_exec’ *)
+Theorem fix_exec_fixed_eq:
+  ∀N f. is_valid_fp_body N f ⇒ ∀x. fix_exec f x = f (fix_exec f) x
+Proof
+  rw [fix_exec_def] >>
+  imp_res_tac fix_nexec_eq_fix >> fs [] >>
+  irule fix_fixed_eq >> fs [] >> metis_tac []
+QED
+
+
 (*===============================
  * Utilities for the automation
  *===============================*)
diff --git a/backends/hol4/divDefTheory.sig b/backends/hol4/divDefTheory.sig
index 15592052..ec69c44f 100644
--- a/backends/hol4/divDefTheory.sig
+++ b/backends/hol4/divDefTheory.sig
@@ -4,12 +4,15 @@ sig
   
   (*  Definitions  *)
     val fix_def : thm
+    val fix_exec_def : thm
     val fix_fuel_P_def : thm
     val fix_fuel_def : thm
+    val fix_nexec_def : thm
     val is_valid_fp_body_def : thm
   
   (*  Theorems  *)
     val case_result_switch_eq : thm
+    val fix_exec_fixed_eq : thm
     val fix_fixed_diverges : thm
     val fix_fixed_eq : thm
     val fix_fixed_terminates : thm
@@ -21,6 +24,7 @@ sig
     val fix_fuel_mono_least : thm
     val fix_fuel_not_diverge_eq_fix : thm
     val fix_fuel_not_diverge_eq_fix_aux : thm
+    val fix_nexec_eq_fix : thm
     val fix_not_diverge_implies_fix_fuel : thm
     val fix_not_diverge_implies_fix_fuel_aux : thm
     val is_valid_fp_body_compute : thm
@@ -37,6 +41,10 @@ sig
             fix_fuel ($LEAST (fix_fuel_P f x)) f x
           else Diverge
    
+   [fix_exec_def]  Definition
+      
+      ⊢ fix_exec = fix_nexec 1000000
+   
    [fix_fuel_P_def]  Definition
       
       ⊢ ∀f x n. fix_fuel_P f x n ⇔ ¬is_diverge (fix_fuel n f x)
@@ -46,6 +54,12 @@ sig
       ⊢ (∀f x. fix_fuel 0 f x = Diverge) ∧
         ∀n f x. fix_fuel (SUC n) f x = f (fix_fuel n f) x
    
+   [fix_nexec_def]  Definition
+      
+      ⊢ ∀n f x.
+          fix_nexec n f x =
+          if fix_fuel_P f x n then fix_fuel n f x else fix f x
+   
    [is_valid_fp_body_def]  Definition
       
       ⊢ (∀f. is_valid_fp_body 0 f ⇔ F) ∧
@@ -75,6 +89,10 @@ sig
         | Fail e => Fail e
         | Diverge => Diverge
    
+   [fix_exec_fixed_eq]  Theorem
+      
+      ⊢ ∀N f. is_valid_fp_body N f ⇒ ∀x. fix_exec f x = f (fix_exec f) x
+   
    [fix_fixed_diverges]  Theorem
       
       ⊢ ∀N f.
@@ -151,6 +169,10 @@ sig
           ∀n x.
             g (fix_fuel n f) x ≠ Diverge ⇒ g (fix f) x = g (fix_fuel n f) x
    
+   [fix_nexec_eq_fix]  Theorem
+      
+      ⊢ ∀N f n. is_valid_fp_body N f ⇒ fix_nexec n f = fix f
+   
    [fix_not_diverge_implies_fix_fuel]  Theorem
       
       ⊢ ∀N f.
diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 78822abe..133f6a99 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -25,6 +25,7 @@ val exfalso : tactic =
   SUBGOAL_THEN “F” (fn th => ASSUME_TAC th >> fs[])
 
 val case_tac = CASE_TAC
+val top_case_tac = BasicProvers.TOP_CASE_TAC
 val try_tac = TRY
 val first_tac = FIRST
 val map_first_tac = MAP_FIRST
-- 
cgit v1.2.3