Remove val foo = Q.prove(..) automatically

Note we only remove instances where foo contains the result of
Q.prove, not a modified version through use of |>.

import os
import re
import sys

def match_comment_parens(s, start_idx):
    if s[start_idx:start_idx + 2] == '(*':
        paren_count = 0
        comment_content = ""
        for i, char in enumerate(s[start_idx:], start=start_idx):
            if char == '(' and s[i + 1] == '*':
                paren_count += 1
            elif char == '*' and i + 1 < len(s) and s[i + 1] == ')':
                paren_count -= 1
                comment_content += char
                if paren_count == 0:
                    comment_content += ")"
                    i += 1
                    while i + 1 < len(s) and s[i + 1].isspace():
                        i += 1
                        comment_content += s[i]
                    return comment_content, i + 1
            comment_content += char
        return None
    return "", start_idx

def transform_definition(s):
    done_before = 0

    pattern = re.compile(r"\nval[ \t]+([a-zA-Z0-9][a-zA-Z0-9_']*)\s*=\s*Q.prove\s*")

    match = pattern.search(s, done_before)

    while match:
        re_start, re_end = match.span()

        comment_parens, comment_end = match_comment_parens(s, re_end)

        if s[comment_end] == '(':
            paren_count = 0
            paren_content = ""
            for i, char in enumerate(s[comment_end:]):
                if char == '(':
                    paren_count += 1
                elif char == ')':
                    paren_count -= 1
                paren_content += char
                if paren_count == 0:
                    break
            paren_length = len(paren_content)
            paren_content = paren_content[1:paren_length-1]

            match2 = re.search(r"\s*(?:`|‘)([^`’]*?)(?:`|’)\s*,(.*)", paren_content, re.DOTALL)

            if match2:
                if comment_parens == "":
                    replacement = f"\nTriviality {match.group(1)}:\n  {match2.group(1).strip()}\nProof\n  {match2.group(2).strip()}\nQED"
                else:
                    replacement = f"\n{comment_parens}Triviality {match.group(1)}:\n  {match2.group(1).strip()}\nProof\n  {match2.group(2).strip()}\nQED"
                if comment_end + paren_length < len(s) and s[comment_end + paren_length] == ';':
                    s = s[:re_start] + replacement + s[comment_end+paren_length+1:]
                elif comment_end + paren_length + 1< len(s) and s[(comment_end + paren_length):(comment_end + paren_length+2)] == "\n\n":
                    s = s[:re_start] + replacement + s[comment_end+paren_length:]
                else:
                    done_before = comment_end + paren_length
            else:
                done_before = comment_end
        else:
            done_before = comment_end

        match = pattern.search(s, done_before)

    return s

def process_sml_file(filepath):
    with open(filepath, 'r') as file:
        content = file.read()

    transformed_content = transform_definition(content)

    with open(filepath, 'w') as file:
        file.write(transformed_content)

def find_and_transform_sml_files(directory):
    for root, _, files in os.walk(directory):
        for file in files:
            if (file.endswith("Script.sml")):
                    filepath = os.path.join(root, file)
                    print(f"Processing file: {filepath}")
                    process_sml_file(filepath)

if __name__ == "__main__":
    if len(sys.argv) != 2:
        print("Usage: python script.py <directory>")
        sys.exit(1)

    directory_to_search = sys.argv[1]

    if not os.path.isdir(directory_to_search):
        print(f"Error: {directory_to_search} is not a valid directory.")
        sys.exit(1)

    find_and_transform_sml_files(directory_to_search)

Author: dnezam

basis/ArrayProofScript.sml

@@ -153,9 +153,11 @@ QED
 val eq_v_thm = fetch "mlbasicsProg" "eq_v_thm"
 val eq_num_v_thm = MATCH_MP (DISCH_ALL eq_v_thm) (EqualityType_NUM_BOOL |> CONJUNCT1)
 
-val num_eq_thm = Q.prove(
-  `!n nv x xv. NUM n nv /\ NUM x xv ==> (n = x <=> nv = xv)`,
-  metis_tac[EqualityType_NUM_BOOL, EqualityType_def]);
+Triviality num_eq_thm:
+  !n nv x xv. NUM n nv /\ NUM x xv ==> (n = x <=> nv = xv)
+Proof
+  metis_tac[EqualityType_NUM_BOOL, EqualityType_def]
+QED
 
 Theorem array_tabulate_spec:
    !n nv f fv (A: 'a -> v -> bool).
@@ -251,27 +253,29 @@ val res = max_print_depth := 100
 *)
 
 
-val less_than_length_thm = Q.prove (
-  `!xs n. (n < LENGTH xs) ==> (?ys z zs. (xs = ys ++ z::zs) /\ (LENGTH ys = n))`,
+Triviality less_than_length_thm:
+  !xs n. (n < LENGTH xs) ==> (?ys z zs. (xs = ys ++ z::zs) /\ (LENGTH ys = n))
+Proof
   rw[] \\
   qexists_tac`TAKE n xs` \\
   rw[] \\
   qexists_tac`HD (DROP n xs)` \\
   qexists_tac`TL (DROP n xs)` \\
   Cases_on`DROP n xs` \\ fs[] \\
   metis_tac[TAKE_DROP,APPEND_ASSOC,CONS_APPEND]
-);
+QED
 
 
-val lupdate_breakdown_thm = Q.prove(
-  `!l val n. n < LENGTH l
-    ==> LUPDATE val n l = TAKE n l ++ [val] ++ DROP (n + 1) l`,
-    rw[] \\ drule less_than_length_thm
+Triviality lupdate_breakdown_thm:
+  !l val n. n < LENGTH l
+    ==> LUPDATE val n l = TAKE n l ++ [val] ++ DROP (n + 1) l
+Proof
+  rw[] \\ drule less_than_length_thm
     \\ rw[] \\ simp_tac std_ss [TAKE_LENGTH_APPEND, GSYM APPEND_ASSOC, GSYM CONS_APPEND]
     \\simp_tac std_ss [DROP_APPEND2]
     \\ simp_tac std_ss [GSYM CONS_APPEND]
     \\ EVAL_TAC \\ rw[lupdate_append2]
-);
+QED
 
 Theorem array_copy_aux_spec:
    !src n srcv dstv di div nv max maxv bfr mid afr.
@@ -462,16 +466,18 @@ Proof
   rw [NUM_def]
 QED
 
-val list_rel_take_thm = Q.prove(
-  `!A xs ys n.
-      LIST_REL A xs ys ==> LIST_REL A (TAKE n xs) (TAKE n ys)`,
-    Induct_on `xs` \\ Induct_on `ys` \\ rw[LIST_REL_def, TAKE_def]
-);
+Triviality list_rel_take_thm:
+  !A xs ys n.
+      LIST_REL A xs ys ==> LIST_REL A (TAKE n xs) (TAKE n ys)
+Proof
+  Induct_on `xs` \\ Induct_on `ys` \\ rw[LIST_REL_def, TAKE_def]
+QED
 
-val drop_pre_length_thm = Q.prove(
-  `!l. l <> [] ==> (DROP (LENGTH l - 1) l) = [(EL (LENGTH l - 1) l)]`,
+Triviality drop_pre_length_thm:
+  !l. l <> [] ==> (DROP (LENGTH l - 1) l) = [(EL (LENGTH l - 1) l)]
+Proof
   rw[] \\ Induct_on `l` \\ rw[DROP, LENGTH, DROP_EL_CONS, DROP_LENGTH_NIL]
-);
+QED
 
 (*
 Definition ARRAY_TYPE_def:

basis/ListProgScript.sml

@@ -431,11 +431,13 @@ Definition AUPDATE_def:
 End
 val AUPDATE_eval = translate AUPDATE_def;
 
-val FMAP_EQ_ALIST_UPDATE = Q.prove(
-  `FMAP_EQ_ALIST f l ==> FMAP_EQ_ALIST (FUPDATE f (x,y)) (AUPDATE l (x,y))`,
+Triviality FMAP_EQ_ALIST_UPDATE:
+  FMAP_EQ_ALIST f l ==> FMAP_EQ_ALIST (FUPDATE f (x,y)) (AUPDATE l (x,y))
+Proof
   SIMP_TAC (srw_ss()) [FMAP_EQ_ALIST_def,AUPDATE_def,ALOOKUP_def,FUN_EQ_THM,
     finite_mapTheory.FLOOKUP_DEF,finite_mapTheory.FAPPLY_FUPDATE_THM]
-  THEN METIS_TAC []);
+  THEN METIS_TAC []
+QED
 
 val Eval_FUPDATE = Q.prove(
   `!v. ((LIST_TYPE (PAIR_TYPE a b) -->
@@ -473,22 +475,28 @@ val _ = next_ml_names := ["every","every"];
 val _ = translate AEVERY_AUX_def;
 val AEVERY_eval = translate AEVERY_def;
 
-val AEVERY_AUX_THM = Q.prove(
-  `!l aux P. AEVERY_AUX aux P l <=>
-              !x y. (ALOOKUP l x = SOME y) /\ ~(MEM x aux) ==> P (x,y)`,
+Triviality AEVERY_AUX_THM:
+  !l aux P. AEVERY_AUX aux P l <=>
+              !x y. (ALOOKUP l x = SOME y) /\ ~(MEM x aux) ==> P (x,y)
+Proof
   Induct
   THEN FULL_SIMP_TAC std_ss [ALOOKUP_def,AEVERY_AUX_def,FORALL_PROD,
     MEM,GSYM MEMBER_INTRO] THEN REPEAT STRIP_TAC
-  THEN SRW_TAC [] [] THEN METIS_TAC [SOME_11]);
+  THEN SRW_TAC [] [] THEN METIS_TAC [SOME_11]
+QED
 
-val AEVERY_THM = Q.prove(
-  `AEVERY P l <=> !x y. (ALOOKUP l x = SOME y) ==> P (x,y)`,
-  SIMP_TAC (srw_ss()) [AEVERY_def,AEVERY_AUX_THM]);
+Triviality AEVERY_THM:
+  AEVERY P l <=> !x y. (ALOOKUP l x = SOME y) ==> P (x,y)
+Proof
+  SIMP_TAC (srw_ss()) [AEVERY_def,AEVERY_AUX_THM]
+QED
 
-val AEVERY_EQ_FEVERY = Q.prove(
-  `FMAP_EQ_ALIST f l ==> (AEVERY P l <=> FEVERY P f)`,
+Triviality AEVERY_EQ_FEVERY:
+  FMAP_EQ_ALIST f l ==> (AEVERY P l <=> FEVERY P f)
+Proof
   FULL_SIMP_TAC std_ss [FMAP_EQ_ALIST_def,FEVERY_DEF,AEVERY_THM]
-  THEN FULL_SIMP_TAC std_ss [FLOOKUP_DEF]);
+  THEN FULL_SIMP_TAC std_ss [FLOOKUP_DEF]
+QED
 
 val Eval_FEVERY = Q.prove(
   `!v. (((PAIR_TYPE (a:'a->v->bool) (b:'b->v->bool) --> BOOL) -->
@@ -509,16 +517,20 @@ Definition AMAP_def:
 End
 val AMAP_eval = translate AMAP_def;
 
-val ALOOKUP_AMAP = Q.prove(
-  `!l. ALOOKUP (AMAP f l) a =
-        case ALOOKUP l a of NONE => NONE | SOME x => SOME (f x)`,
+Triviality ALOOKUP_AMAP:
+  !l. ALOOKUP (AMAP f l) a =
+        case ALOOKUP l a of NONE => NONE | SOME x => SOME (f x)
+Proof
   Induct THEN SIMP_TAC std_ss [AMAP_def,ALOOKUP_def,FORALL_PROD]
-  THEN SRW_TAC [] []);
+  THEN SRW_TAC [] []
+QED
 
-val FMAP_EQ_ALIST_o_f = Q.prove(
-  `FMAP_EQ_ALIST m l ==> FMAP_EQ_ALIST (x o_f m) (AMAP x l)`,
+Triviality FMAP_EQ_ALIST_o_f:
+  FMAP_EQ_ALIST m l ==> FMAP_EQ_ALIST (x o_f m) (AMAP x l)
+Proof
   SIMP_TAC std_ss [FMAP_EQ_ALIST_def,FUN_EQ_THM,FLOOKUP_DEF,
-    o_f_DEF,ALOOKUP_AMAP] THEN REPEAT STRIP_TAC THEN SRW_TAC [] []);
+    o_f_DEF,ALOOKUP_AMAP] THEN REPEAT STRIP_TAC THEN SRW_TAC [] []
+QED
 
 val Eval_o_f = Q.prove(
   `!v. (((b --> c) --> LIST_TYPE (PAIR_TYPE (a:'a->v->bool) (b:'b->v->bool)) -->
@@ -567,17 +579,21 @@ Definition ADEL_def:
 End
 val ADEL_eval = translate ADEL_def;
 
-val ALOOKUP_ADEL = Q.prove(
-  `!l a x. ALOOKUP (ADEL l a) x = if x = a then NONE else ALOOKUP l x`,
+Triviality ALOOKUP_ADEL:
+  !l a x. ALOOKUP (ADEL l a) x = if x = a then NONE else ALOOKUP l x
+Proof
   Induct THEN SRW_TAC [] [ALOOKUP_def,ADEL_def] THEN Cases_on `h`
-  THEN SRW_TAC [] [ALOOKUP_def,ADEL_def]);
+  THEN SRW_TAC [] [ALOOKUP_def,ADEL_def]
+QED
 
-val FMAP_EQ_ALIST_ADEL = Q.prove(
-  `!x l. FMAP_EQ_ALIST x l ==>
-          FMAP_EQ_ALIST (x \\ a) (ADEL l a)`,
+Triviality FMAP_EQ_ALIST_ADEL:
+  !x l. FMAP_EQ_ALIST x l ==>
+          FMAP_EQ_ALIST (x \\ a) (ADEL l a)
+Proof
   FULL_SIMP_TAC std_ss [FMAP_EQ_ALIST_def,ALOOKUP_def,fmap_domsub,FUN_EQ_THM]
   THEN REPEAT STRIP_TAC THEN SRW_TAC [] [ALOOKUP_ADEL,FLOOKUP_DEF,DRESTRICT_DEF]
-  THEN FULL_SIMP_TAC std_ss []);
+  THEN FULL_SIMP_TAC std_ss []
+QED
 
 val Eval_fmap_domsub = Q.prove(
   `!v. ((LIST_TYPE (PAIR_TYPE a b) --> a -->

basis/RatProgScript.sml

@@ -52,10 +52,11 @@ val _ = add_type_inv ``REAL_TYPE`` ``:rational``;
 
 (* transfer *)
 
-val RAT_RAT = Q.prove(
-  `(!r1. real_of_rat (f1 r1) = f2 (real_of_rat r1)) ==>
+Triviality RAT_RAT:
+  (!r1. real_of_rat (f1 r1) = f2 (real_of_rat r1)) ==>
    !v. (RAT_TYPE --> RAT_TYPE) f1 v ==>
-       (REAL_TYPE --> REAL_TYPE) f2 v`,
+       (REAL_TYPE --> REAL_TYPE) f2 v
+Proof
   strip_tac
   \\ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
                           FORALL_PROD] \\ rw []
@@ -64,12 +65,14 @@ val RAT_RAT = Q.prove(
                      mp_then.mp_then (mp_then.Pos hd)
                                     (qspec_then ‘R’ strip_assume_tac))
   \\ fs [] \\ asm_exists_tac \\ fs []
-  \\ fs [] \\ asm_exists_tac \\ fs []);
+  \\ fs [] \\ asm_exists_tac \\ fs []
+QED
 
-val RAT_RAT_RAT = Q.prove(
-  `(!r1 r2. real_of_rat (f1 r1 r2) = f2 (real_of_rat r1) (real_of_rat r2)) ==>
+Triviality RAT_RAT_RAT:
+  (!r1 r2. real_of_rat (f1 r1 r2) = f2 (real_of_rat r1) (real_of_rat r2)) ==>
    !v. (RAT_TYPE --> RAT_TYPE --> RAT_TYPE) f1 v ==>
-       (REAL_TYPE --> REAL_TYPE --> REAL_TYPE) f2 v`,
+       (REAL_TYPE --> REAL_TYPE --> REAL_TYPE) f2 v
+Proof
   strip_tac
   \\ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
                           FORALL_PROD] \\ rw []
@@ -81,12 +84,14 @@ val RAT_RAT_RAT = Q.prove(
   \\ rw [] \\ first_x_assum drule
   \\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
   \\ disch_then (qspec_then `refs2` mp_tac)
-  \\ strip_tac \\ rpt (asm_exists_tac \\ fs []));
+  \\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
+QED
 
-val RAT_RAT_BOOL = Q.prove(
-  `(!r1 r2. f1 r1 r2 <=> f2 (real_of_rat r1) (real_of_rat r2)) ==>
+Triviality RAT_RAT_BOOL:
+  (!r1 r2. f1 r1 r2 <=> f2 (real_of_rat r1) (real_of_rat r2)) ==>
    !v. (RAT_TYPE --> RAT_TYPE --> BOOL) f1 v ==>
-       (REAL_TYPE --> REAL_TYPE --> BOOL) f2 v`,
+       (REAL_TYPE --> REAL_TYPE --> BOOL) f2 v
+Proof
   strip_tac
   \\ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
                           FORALL_PROD] \\ rw []
@@ -98,23 +103,28 @@ val RAT_RAT_BOOL = Q.prove(
   \\ rw [] \\ first_x_assum drule
   \\ qmatch_goalsub_rename_tac `(empty_state with refs := refs2)`
   \\ disch_then (qspec_then `refs2` mp_tac)
-  \\ strip_tac \\ rpt (asm_exists_tac \\ fs []));
+  \\ strip_tac \\ rpt (asm_exists_tac \\ fs [])
+QED
 
-val RAT_BOOL = Q.prove(
-  `(!r1. (f1 r1) = f2 (real_of_rat r1)) ==>
+Triviality RAT_BOOL:
+  (!r1. (f1 r1) = f2 (real_of_rat r1)) ==>
    !v. (RAT_TYPE --> BOOL) f1 v ==>
-       (REAL_TYPE --> BOOL) f2 v`,
+       (REAL_TYPE --> BOOL) f2 v
+Proof
   strip_tac
   \\ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
-                          FORALL_PROD] \\ rw []);
+                          FORALL_PROD] \\ rw []
+QED
 
-val RAT_INT = Q.prove(
-  `(!r1. (f1 r1) = f2 (real_of_rat r1)) ==>
+Triviality RAT_INT:
+  (!r1. (f1 r1) = f2 (real_of_rat r1)) ==>
    !v. (RAT_TYPE --> INT) f1 v ==>
-       (REAL_TYPE --> INT) f2 v`,
+       (REAL_TYPE --> INT) f2 v
+Proof
   strip_tac
   \\ SIMP_TAC (srw_ss()) [Arrow_def,AppReturns_def,REAL_TYPE_def,PULL_EXISTS,
-                          FORALL_PROD] \\ rw []);
+                          FORALL_PROD] \\ rw []
+QED
 
 
 (* -- *)
@@ -362,8 +372,9 @@ Proof
          arithmeticTheory.NOT_ZERO_LT_ZERO])
 QED
 
-val INT_NEG_DIV_FACTOR = Q.prove(
-  ‘0 < (x:num) ==> (-&(x * y):int / &x = -&y)’,
+Triviality INT_NEG_DIV_FACTOR:
+  0 < (x:num) ==> (-&(x * y):int / &x = -&y)
+Proof
   strip_tac >> qspec_then ‘&x’ mp_tac integerTheory.INT_DIVISION >>
   simp[] >> disch_then (qspec_then ‘-&(x * y)’ strip_assume_tac) >>
   map_every qabbrev_tac [`D:int = -&(x * y)`, `q = D / &x`, `r = D % &x`] >>
@@ -388,7 +399,8 @@ val INT_NEG_DIV_FACTOR = Q.prove(
   >- (rename [‘q + &y = 0’] >> disch_then kall_tac >>
       ‘q + &y + -&y = -&y’ by metis_tac [integerTheory.INT_ADD_LID] >>
       metis_tac[integerTheory.INT_ADD_ASSOC, integerTheory.INT_ADD_RID,
-                integerTheory.INT_ADD_RINV]))
+                integerTheory.INT_ADD_RINV])
+QED
 
 val PAIR_TYPE_IMP_RAT_TYPE = prove(
   ``r = rat_of_int m / & n /\ n <> 0 ==>
@@ -424,9 +436,11 @@ End
 val _ = next_ml_names := ["+"];
 val pair_add_v_thm = translate pair_add_def;
 
-val abs_rat_ONTO = Q.prove(
-  ‘!r. ?f. abs_rat f = r’,
-  gen_tac >> qexists_tac ‘rep_rat r’ >> simp[rat_type_thm]);
+Triviality abs_rat_ONTO:
+  !r. ?f. abs_rat f = r
+Proof
+  gen_tac >> qexists_tac ‘rep_rat r’ >> simp[rat_type_thm]
+QED
 
 val Eval_RAT_ADD = Q.prove(
   `!v.