Replace (commented) cheat with ... throughout

There are semantic checks that none of the most important
theorems depend on any cheats. However, when searching the
code base it was easy to find cheats. To make it clear that
these are unimportant cheats, I've replaced each of them
with "...".

basis/ArrayProofScript.sml

@@ -536,7 +536,7 @@ Theorem array_foldli_aux_spec
       >-(xapp \\ xsimpl \\ instantiate \\ qexists_tac `EL n a` \\ fs[LIST_REL_EL_EQN])
     \\ first_x_assum(qspecl_then [`a`, `n + 1`] mp_tac) \\ rw[]
     \\ xapp \\ xsimpl \\ instantiate \\ rw[mllistTheory.foldli_def, mllistTheory.foldli_aux_def, DROP_EL_CONS]
-    \\ cheat (*How to deal with foldli_aux as it has nothing proved about it *)
+    \\ ... (*How to deal with foldli_aux as it has nothing proved about it *)
 );
 
 Theorem array_foldli_spec
@@ -564,12 +564,12 @@ Theorem array_foldl_aux_spec
     \\ xlet `POSTv n1. & NUM (n + 1) n1 * ARRAY av vs`
       >-(xapp \\ xsimpl \\ qexists_tac `&n` \\ fs[NUM_def, integerTheory.INT_ADD])
     \\ xlet `POSTv res. & A (f init b) res * ARRAY av vs`
-      >-(cheat (*xapp*))
+      >-(... (*xapp*))
     \\ xlet `POSTv val. & (val = EL n vs) * ARRAY av vs`
       >-(xapp \\ xsimpl \\ imp_res_tac LIST_REL_LENGTH \\ fs[NUM_def, INT_def] \\ rfs[])
     \\ Induct_on `LENGTH a - n`
       >-(rw[] \\ imp_res_tac LIST_REL_LENGTH \\ fs[NUM_def, INT_def] \\ rfs[])
-    \\ rw[] \\ cheat (*xapp*)
+    \\ rw[] \\ ... (*xapp*)
 );
 
 Theorem array_foldl_spec
@@ -613,7 +613,7 @@ Theorem array_foldri_aux_spec
     \\ xlet `POSTv res. & (A (f n (EL n a) init) res) * ARRAY av vs`
         >-(xapp \\ xsimpl \\ instantiate \\ qexists_tac`EL n a` \\ fs[LIST_REL_EL_EQN])
     \\ xapp \\ xsimpl \\ instantiate \\ fs[TAKE_EL_SNOC, ADD1] (*need something similar to FOLDR SNOC*)
-    \\ cheat
+    \\ ...
 );
 
 Theorem array_foldri_spec

basis/basis_ffiScript.sml

@@ -255,7 +255,7 @@ Theorem extract_stdo_extract_fs
     \\ CASE_TAC \\ fs[]
     \\ simp[ALIST_FUPDKEY_ALOOKUP]
 
-    \\ cheat)
+    \\ ...)
   \\ qpat_x_assum`_ = SOME _`mp_tac
   \\ simp[option_caseeq,pair_caseeq]
   \\ qhdtm_x_assum`stdo`mp_tac
@@ -314,7 +314,7 @@ Theorem extract_stdout_intro
   \\ rw[]
   \\ Induct_on`io_events`
   \\ rw[extract_fs_def]
-  >- cheat
+  >- ...
   \\ Cases_on`h` \\ fs[extract_fs_def]
   \\ rw[] \\ fs[]
   \\ pop_assum mp_tac \\ CASE_TAC

candle/standard/monadic/holKernelProofScript.sml

@@ -3047,7 +3047,7 @@ Theorem inst_aux_thm
      env = []
      ==>
      inst_aux env tyin tm s <> (Failure (Clash f),t)`
-  (cheat
+  (...
   );
 
 Theorem inst_not_clash[simp]

candle/standard/syntax/holConservativeScript.sml

@@ -5,6 +5,8 @@ open preamble holSyntaxLibTheory holSyntaxTheory holSyntaxExtraTheory
 
 val _ = new_theory "holConservative";
 
+(*
+
 (* Theorems that should probably be proved elsewhere (perhaps some already are) *)
 
 val CLOSED_INST = Q.prove (
@@ -35,7 +37,7 @@ Theorem term_image_term_union
   hypset_ok h2
   ⇒
   term_image f (term_union h1 h2) = term_union (term_image f h1) (term_image f h2)`
- (cheat);
+ (...);
 
 Theorem term_image_term_image
 `!f g h.
@@ -44,7 +46,7 @@ Theorem term_image_term_image
   simp[Once term_image_def,SimpRHS] >>
   BasicProvers.CASE_TAC >- simp[] >> fs[] >> rw[] >>
   (* likely not true without some hypset_ok hypotheses *)
-  cheat)
+  ...)
 
 val term_image_term_remove = Q.prove (
 `!x f tm tms.
@@ -292,7 +294,7 @@ val remove_const_inst = Q.prove (
   remove_const tys consts (INST tyin tm) = INST tyin (remove_const tys consts tm)`,
  Induct_on `tm` >>
  rw [remove_const_def] >>
- cheat);
+ ...);
 
 val RACONV_REFL2 = Q.prove (
 `!tms tm. EVERY (\(x,y). (x ≠ y) ⇒ ~VFREE_IN x tm ∧ ~VFREE_IN y tm) tms ⇒ RACONV tms (tm,tm)`,
@@ -312,7 +314,7 @@ val RACONV_REFL2 = Q.prove (
      metis_tac [])
  >- (fs [EVERY_MEM, LAMBDA_PROD, FORALL_PROD] >>
      metis_tac [])
- >- cheat);
+ >- ...);
 
 val remove_const_raconv = Q.prove (
 `!tms tm. RACONV tms tm ⇒
@@ -336,7 +338,7 @@ val remove_const_raconv = Q.prove (
      `CLOSED (INST x'' x')` by metis_tac [CLOSED_INST] >>
      fs [EVERY_MEM, CLOSED_def, LAMBDA_PROD, FORALL_PROD] >>
      rw [] >>
-     `(?x y. p_1 = Var x y) ∧ (?x y. p_2 = Var x y)` by cheat >>
+     `(?x y. p_1 = Var x y) ∧ (?x y. p_2 = Var x y)` by ... >>
      metis_tac [])
  >- rw [Once RACONV_cases]
  >- rw [Once RACONV_cases]);
@@ -351,7 +353,7 @@ val remove_const_vsubst = Q.prove (
 `!tys consts tm.
   remove_const tys consts (VSUBST ilist tm) =
   VSUBST (MAP (λ(x,y). (remove_const tys consts x, y)) ilist) (remove_const tys consts tm)`,
- cheat);
+ ...);
 
 val welltyped_remove_const = Q.prove (
 `!tys consts tm.
@@ -366,7 +368,7 @@ val use_const_spec = Q.prove (
   ⇒
   (thyof ctxt,[]) |-
   remove_const (tysof ctxt) consts (VSUBST (MAP (λ(s,t). (Const s (typeof t),Var s (typeof t))) consts) p)`,
- cheat);
+ ...);
 
 val remove_const_old_axiom = Q.prove (
 `!ctxt consts tm.
@@ -481,8 +483,8 @@ val update_conservative = Q.prove (
          imp_res_tac term_image_term_remove >>
          metis_tac [MEM_term_union, hypset_ok_term_union, hypset_ok_term_image,
                     hypset_ok_term_remove, ACONV_TRANS, remove_const_aconv])
-     >- cheat
-     >- cheat)
+     >- ...
+     >- ...)
  >- (rw [Once proves_cases] >>
      ntac 4 disj2_tac >>
      disj1_tac >>
@@ -567,4 +569,6 @@ val update_conservative = Q.prove (
          rw [term_image_def] >>
          metis_tac [remove_const_old_axiom])));
 
+*)
+
 val _ = export_theory ();

characteristic/cfNormaliseScript.sml

@@ -276,6 +276,7 @@ val strip_annot_exp_def = tDefine"strip_annot_exp"`
                                  | INR (INR (INR funs)) => funs_size funs)` >>
    srw_tac [ARITH_ss] [size_abbrevs, astTheory.exp_size_def]);
 
+(*
 val norm_def = tDefine "norm" `
   norm (is_named: bool) (as_value: bool) (ns: string list) (Lit l) = (Lit l, ns, ([]: (string # exp) list)) /\
   norm is_named as_value ns (Var (Short name)) = (Var (Short name), name::ns, []) /\
@@ -382,9 +383,10 @@ val norm_def = tDefine "norm" `
   protect_letrec_branch is_named ns branch =
     (let (branch_e', ns) = protect is_named ns (SND (SND branch)) in
      ((FST branch, FST (SND branch), branch_e'), ns))`
- cheat;
+ (...);
 (* TODO: prove the termination of [norm]. This is probably a bit tricky and
    requires refactoring the way [norm] is defined. *)
+*)
 
 val full_normalise_def = Define `
   full_normalise ns e = FST (protect T ns (strip_annot_exp e))`;

compiler/backend/ag32/proofs/ag32_basis_ffiProofScript.sml

@@ -7120,7 +7120,7 @@ Theorem ag32_interference_implemented
   \\ impl_tac >- fs[]
   (*
   \\ Cases_on`EL ffi_index ffi_names = "exit"` \\ fs[]
-  >- cheat (* remove exit from the list ? or implement it *)
+  >- ... (* remove exit from the list ? or implement it *)
   *)
   \\ Cases_on`EL ffi_index ffi_names = ""` \\ fs[]
   >- ffi_tac ag32_ffi_interfer_ ``ag32_ffi__code``

compiler/backend/proofs/backendProofScript.sml

@@ -1278,17 +1278,17 @@ Theorem compile_correct
             strip_tac
             \\ first_x_assum drule
             \\ simp[]
-            \\ cheat (* oracle labels... *) )
+            \\ ... (* oracle labels... *) )
           \\ disj1_tac
           \\ fs[Abbr`p7`]
-          \\ cheat (* get_code_labels range...  *) )
+          \\ ... (* get_code_labels range...  *) )
         \\ qspec_then`ppg`mp_tac get_labels_MAP_prog_to_section_SUBSET_code_labels
         \\ simp[SUBSET_DEF]
         \\ strip_tac
         \\ gen_tac \\ strip_tac
         \\ first_x_assum drule
         \\ strip_tac \\ rw[]
-        \\ cheat (* referenced labels are present (for oracle) *) *))
+        \\ ... (* referenced labels are present (for oracle) *) *))
       \\ fs[Abbr`stack_oracle`,Abbr`word_oracle`,Abbr`data_oracle`,Abbr`lab_oracle`] >>
       simp[Abbr`co`, Abbr`co3`] \\
       rpt(pairarg_tac \\ fs[]) \\

compiler/backend/proofs/clos_callProofScript.sml

@@ -4235,7 +4235,7 @@ Theorem ALOOKUP_make_gs
   \\ fs [MEM_MAP,FLOOKUP_FUNION]
   \\ qexists_tac `k'` \\ fs []
   \\ rveq \\ fs []
-  \\ cheat (* this proof needs a slightly different approach *));
+  \\ ... (* this proof needs a slightly different approach *));
 *)
 
 Theorem FST_THE_make_gs
@@ -4483,7 +4483,7 @@ val pure_code_locs = Q.store_thm("pure_code_locs", (* DUPLCATED! clos_annotate *
   \\ Q.ISPEC_THEN`es`mp_tac code_locs_map
   \\ disch_then(qspec_then`I`mp_tac)
   \\ simp[FLAT_EQ_NIL, EVERY_MAP, EVERY_MEM]
-  \\ cheat);
+  \\ ...);
 
 Theorem call_dests_code_list_SUBSET
   `!xs n g.
@@ -4519,7 +4519,7 @@ Theorem calls_locs
       set (code_locs call_code) ∪ set (code_locs (MAP (SND ∘ SND) (SND g1))) =
       set (code_locs known_code) ∪ set (code_locs (MAP (SND ∘ SND) (SND g)))`
 
-  (cheat);
+  (...);
 
 (*
 

compiler/backend/proofs/clos_knownProofScript.sml

@@ -5349,7 +5349,7 @@ Theorem compile_locs
   \\ drule (GEN_ALL known_app_call_dests)
   \\ disch_then(fn th => assume_tac (SPEC``SOME T`` th) \\ assume_tac (SPEC``SOME F`` th))
   \\ fs[] \\ rfs[]
-  \\ cheat);
+  \\ ...);
 *)
 
 val _ = export_theory();

compiler/backend/proofs/clos_to_bvlProofScript.sml

@@ -6630,8 +6630,8 @@ Theorem compile_common_semantics
          \\ simp[clos_knownProofTheory.known_co_def]
          \\ TOP_CASE_TAC \\ simp[backendPropsTheory.FST_state_co] \\ rw[] )
        \\ pop_assum SUBST_ALL_TAC
-       \\ cheat )
-    \\ cheat (* syntactic properties of clos_call *)*))
+       \\ ... )
+    \\ ... (* syntactic properties of clos_call *)*))
   \\ disch_then(assume_tac o SYM) \\ fs[]
   \\ fs[FUPDATE_LIST_alist_to_fmap]
   \\ drule clos_callProofTheory.compile_ALL_DISTINCT
@@ -7734,12 +7734,12 @@ Theorem compile_semantics
       \\ simp[]
       \\ simp[all_distinct_count_list] )
     \\ `ALL_DISTINCT (MAP FST (SND (SND pp)) ++ code_locs (MAP (SND o SND) (SND (SND pp))))`
-    by cheat
+    by ...
     \\ pop_assum mp_tac
     \\ simp[ALL_DISTINCT_APPEND]
     \\ strip_tac
-    \\ cheat )
-  \\ cheat (* many syntactic properties of oracle *)*));
+    \\ ... )
+  \\ ... (* many syntactic properties of oracle *)*));
 
 Theorem assign_get_code_label_compile_op
   `closLang$assign_get_code_label (compile_op op) = case some n. op = Label n of SOME n => {n} | _ => {}`

compiler/backend/proofs/stack_to_labProofScript.sml

@@ -3419,16 +3419,6 @@ val init_stubs_labels = Q.prove(`
   EVERY (λp. get_code_labels p SUBSET (set [(1n,0n);(start,0n)])) (MAP SND (init_stubs ggc mh k start))`,
   rpt(EVAL_TAC>>rw[]>>fs[]));
 
-(* stack_alloc -- this seems strange... *)
-val get_code_labels_comp = Q.prove(
-  `!n m p pp mm.
-  comp n m p = (pp,mm) ⇒
-  get_code_labels pp SUBSET
-    (gc_stub_location,0) INSERT
-    set
-      (MAP (λi. (n,i+mm)) (COUNT_LIST (mm-m)))
-     ∪ get_code_labels p`, cheat);
-
 (* stack_names *)
 val get_code_labels_comp = Q.prove(
   `!f p. get_code_labels (comp f p) = get_code_labels p`,

compiler/inference/proofs/inferCompleteScript.sml

@@ -1396,7 +1396,7 @@ Theorem infer_ds_complete
     \\ qexists_tac`i` \\ simp[]
     \\ pop_assum(qspec_then`GENLIST Infer_Tvar_db p_1`mp_tac)
     \\ simp[infer_deBruijn_subst_id2]
-    \\ cheat )
+    \\ ... )
   *)
   \\ rw[]
   \\ drule (CONJUNCT2 infer_d_complete_canon)

examples/diffScript.sml

@@ -1144,7 +1144,7 @@ Theorem patch_diff2_cancel
    this property is false as stated; prove some appropriate weakening
 Theorem diff_patch_cancel
   `patch_alg patch l = SOME r ==> diff_alg l r = patch`
-  (cheat);
+  (...);
  *)
 
 (* The diff is optimal, in the sense that the number of line changes it

translator/ml_progScript.sml

@@ -923,7 +923,7 @@ Theorem lookup_var_merge_env
     (Cases_on`nsLookup e2.v (Short v1)`>>
     fs[namespacePropsTheory.nsLookup_nsAppend_none,
        namespacePropsTheory.nsLookup_nsAppend_some,namespaceTheory.id_to_mods_def])
-  \\ cheat (* TODO *)));
+  \\ ... (* TODO *)));
 *)
 
 val _ = export_theory();

translator/monadic/cfMonadLib.sml

@@ -162,15 +162,15 @@ val ffi = ``p:'ffi ffi_proj``
 val spec1 = Q.prove (
   `ArrowP ro (STATE_REF, ^ffi) (PURE NUM)
           (ArrowM ro (STATE_REF, ^ffi) (PURE NUM) (MONAD NUM UNIT_TYPE)) f1 f1_v`,
-  cheat);
+  ...);
 
 val spec2 = Q.prove (
   `PRECONDITION (f1_side x y st)
    ==>
    ArrowP ro (STATE_REF, ^ffi) (PURE (Eq NUM x))
           (ArrowM ro (STATE_REF, ^ffi) (EqSt (PURE (Eq NUM y)) st)
             (MONAD NUM UNIT_TYPE)) f1 f1_v`,
-  cheat)
+  ...)
 
 mk_app_of_ArrowP spec1
 mk_app_of_ArrowP spec2