Fix errors caused by HOL deleting various quotient_*Theory

CakeML · Jul 31, 2023 · e6db84d · e6db84d
1 parent 3cf115c
commit e6db84d
Show file tree

Hide file tree

Showing 7 changed files with 14 additions and 18 deletions.
diff --git a/candle/overloading/syntax/holSyntaxExtraScript.sml b/candle/overloading/syntax/holSyntaxExtraScript.sml
@@ -6865,7 +6865,7 @@ Proof
   `!l ty1 ty2. equal_upto l ty1 ty2 ==> l = [] ==> ty1 = ty2`
     suffices_by metis_tac[]
   \\ ho_match_mp_tac equal_upto_ind \\  fs[]
-  \\ CONV_TAC(DEPTH_CONV ETA_CONV) \\ fs[quotient_listTheory.LIST_REL_EQ]
+  \\ CONV_TAC(DEPTH_CONV ETA_CONV) \\ fs[]
 
 QED
 

diff --git a/compiler/backend/proofs/backendProofScript.sml b/compiler/backend/proofs/backendProofScript.sml
@@ -485,8 +485,8 @@ Proof
   simp [keep_progs_def, FUN_EQ_THM]
 QED
 
-Triviality compile_inc_progs_defs = LIST_CONJ
-  [compile_inc_progs_def, keep_progs_T, quotient_pairTheory.PAIR_MAP_I]
+Triviality compile_inc_progs_defs =
+  LIST_CONJ [compile_inc_progs_def, keep_progs_T]
 
 Theorem cake_orac_eqs:
   state_co (\c (env_id, decs). inc_compile env_id c

diff --git a/compiler/backend/proofs/bvi_tailrecProofScript.sml b/compiler/backend/proofs/bvi_tailrecProofScript.sml
@@ -1070,7 +1070,7 @@ Proof
     \\ fs[state_rel_def] )
   \\ imp_res_tac state_rel_const
   \\ fs[case_eq_thms]
-  \\ rveq \\ fs[OPTREL_def,quotient_pairTheory.PAIR_REL_THM]
+  \\ rveq \\ fs[OPTREL_def,PAIR_REL_THM]
   \\ fs[state_rel_def]
 QED
 
@@ -1087,7 +1087,7 @@ Proof
   \\ first_x_assum(qspec_then`vs`strip_assume_tac)
   \\ fs[case_eq_thms,OPTREL_def] \\ rw[] \\ rfs[]
   \\ fs[PULL_EXISTS]
-  \\ rveq \\ fs[quotient_pairTheory.PAIR_REL]
+  \\ rveq \\ fs[PAIR_REL]
   \\ TRY(pairarg_tac \\ fs[])
   \\ imp_res_tac state_rel_const
   \\ fs[bvlSemTheory.do_app_def,case_eq_thms,bvl_to_bvi_id]

diff --git a/compiler/backend/proofs/clos_annotateProofScript.sml b/compiler/backend/proofs/clos_annotateProofScript.sml
@@ -386,7 +386,7 @@ Proof
   \\ imp_res_tac v_to_list \\ fs[] \\ rw[]
   \\ TRY (strip_tac \\ rw[])
   \\ fs[EVERY2_MAP,v_rel_Number]
-  \\ fsrw_tac[ETA_ss][EQ_SYM_EQ,quotient_listTheory.LIST_REL_EQ]
+  \\ fsrw_tac[ETA_ss][EQ_SYM_EQ]
   \\ fs[LIST_EQ_REWRITE,EL_MAP,LIST_REL_EL_EQN] \\ rfs[EL_MAP]
   \\ METIS_TAC[EL_MAP,o_DEF]
 QED
@@ -401,7 +401,7 @@ Proof
   \\ imp_res_tac v_to_list \\ fs[] \\ rw[]
   \\ TRY (strip_tac \\ rw[])
   \\ fs[EVERY2_MAP,v_rel_Number]
-  \\ fsrw_tac[ETA_ss][EQ_SYM_EQ,quotient_listTheory.LIST_REL_EQ]
+  \\ fsrw_tac[ETA_ss][EQ_SYM_EQ]
   \\ fs[LIST_EQ_REWRITE,EL_MAP,LIST_REL_EL_EQN] \\ rfs[EL_MAP]
   \\ METIS_TAC[EL_MAP,o_DEF]
 QED

diff --git a/compiler/backend/proofs/flat_patternProofScript.sml b/compiler/backend/proofs/flat_patternProofScript.sml
@@ -685,9 +685,6 @@ Theorem v_rel_l_cases = TypeBase.nchotomy_of ``: v``
 val env_rel_def = ``env_rel N env1 env2``
     |> SIMP_CONV bool_ss [v_rel_cases]
 
-val add_q = augment_srw_ss [simpLib.named_rewrites "pair_rel_thm"
-  [quotient_pairTheory.PAIR_REL_THM]];
-
 Definition install_conf_rel_def:
   install_conf_rel pat_cfg ic1 ic2 <=>
     (ic2.compile_oracle =

diff --git a/compiler/backend/proofs/source_evalProofScript.sml b/compiler/backend/proofs/source_evalProofScript.sml
@@ -126,7 +126,7 @@ Proof
   Induct
   \\ simp [FORALL_PROD, EXISTS_PROD]
   \\ rw []
-  \\ fs [namespaceTheory.nsBindList_def, quotient_pairTheory.PAIR_REL_THM]
+  \\ fs [namespaceTheory.nsBindList_def]
   \\ irule env_rel_add_nsBind
   \\ simp []
 QED
@@ -428,8 +428,7 @@ Theorem pmatch:
 Proof
   disch_tac
   \\ ho_match_mp_tac pmatch_ind
-  \\ rw [pmatch_def, match_result_rel_def,
-    quotient_pairTheory.PAIR_REL_THM]
+  \\ rw [pmatch_def, match_result_rel_def]
   \\ rveq \\ fs []
   \\ imp_res_tac v_to_env_id_SOME
   \\ fs [pmatch_def]
@@ -1010,7 +1009,7 @@ Proof
     \\ simp [build_rec_env_merge, nsAppend_to_nsBindList]
     \\ irule env_rel_add_nsBindList
     \\ simp [LIST_REL_MAP1, SIMP_RULE (bool_ss ++ ETA_ss) [] LIST_REL_MAP2]
-    \\ simp [ELIM_UNCURRY, quotient_pairTheory.PAIR_REL_THM, EVERY2_refl]
+    \\ simp [ELIM_UNCURRY, EVERY2_refl]
   )
   >~ [‘getOpClass op = Icing’]
   >- (
@@ -1141,7 +1140,7 @@ Proof
   \\ simp [build_rec_env_merge, nsAppend_to_nsBindList]
   \\ irule env_rel_add_nsBindList
   \\ simp [LIST_REL_MAP1, SIMP_RULE (bool_ss ++ ETA_ss) [] LIST_REL_MAP2]
-  \\ simp [quotient_pairTheory.PAIR_REL_THM, ELIM_UNCURRY]
+  \\ simp [ELIM_UNCURRY]
   \\ simp [GSYM pairarg_to_pair_map, ELIM_UNCURRY, EVERY2_refl]
 QED
 
@@ -1198,7 +1197,7 @@ Proof
   \\ irule env_rel_add_nsBindList
   \\ simp []
   \\ simp [LIST_REL_MAP1, SIMP_RULE (bool_ss ++ ETA_ss) [] LIST_REL_MAP2]
-  \\ simp [quotient_pairTheory.PAIR_REL_THM, ELIM_UNCURRY]
+  \\ simp [ELIM_UNCURRY]
   \\ simp [EVERY2_refl]
 QED
 

diff --git a/compiler/inference/proofs/inferPropsScript.sml b/compiler/inference/proofs/inferPropsScript.sml
@@ -4081,7 +4081,7 @@ Proof
     match_mp_tac nsAll_alist_to_ns
     \\ simp[EVERY_MAP,every_zip_snd]
     \\ imp_res_tac generalise_inf_set_tids
-    \\ fs[GSYM LIST_REL_MAP_inv_image, quotient_listTheory.LIST_REL_EQ]
+    \\ fs[GSYM LIST_REL_MAP_inv_image]
     \\ simp[GSYM (Q.ISPEC`inf_set_tids`(CONV_RULE SWAP_FORALL_CONV EVERY_MAP))]
     \\ pop_assum(assume_tac o SYM)
     \\ simp[]
@@ -4120,7 +4120,7 @@ Proof
     \\ simp[MAP2_MAP, UNCURRY, EVERY_MAP]
     \\ simp[every_zip_snd]
     \\ imp_res_tac generalise_inf_set_tids
-    \\ fs[GSYM LIST_REL_MAP_inv_image, quotient_listTheory.LIST_REL_EQ]
+    \\ fs[GSYM LIST_REL_MAP_inv_image]
     \\ simp[GSYM (Q.ISPEC`inf_set_tids`(CONV_RULE SWAP_FORALL_CONV EVERY_MAP))]
     \\ pop_assum(assume_tac o SYM)
     \\ simp[]