Fixes for OPTREL changes in HOL (probably HOL-Theorem-Prover/HOL@f0…

…a4649)
CakeML · Dec 8, 2023 · e696e6d · e696e6d
1 parent 9d1a9e8
commit e696e6d
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 8 deletions.
diff --git a/compiler/backend/passes/proofs/env_to_state_2ProofScript.sml b/compiler/backend/passes/proofs/env_to_state_2ProofScript.sml
@@ -697,7 +697,6 @@ Proof
           OPTREL (λ(a,x) (b,y). a = b ∧ clean x y) te
             (case d of NONE => NONE | SOME (d',e) => SOME (d',to_state e))’ by
      (Cases_on ‘d’ \\ fs []
-      >- (rpt $ qexists_tac ‘NONE’ \\ fs [])
       \\ fs [] \\ rename [‘xx = (_,_)’]
       \\ PairCases_on ‘xx’ \\ fs [OPTREL_SOME,PULL_EXISTS,EXISTS_PROD]
       \\ rpt $ first_assum $ irule_at Any

diff --git a/compiler/backend/passes/proofs/state_app_unitProofScript.sml b/compiler/backend/passes/proofs/state_app_unitProofScript.sml
@@ -208,7 +208,6 @@ Proof
            OPTREL (λ(a,x) (b,y). a = b ∧ rel1 x y) tt
              (OPTION_MAP (λ(alts,e). (MAP (explode ## I) alts,exp_of e)) se)’ by
    (Cases_on ‘te’ \\ Cases_on ‘se’ \\ gvs []
-    >- (qexists_tac ‘NONE’ \\ fs [])
     \\ gvs [UNCURRY]
     \\ Q.REFINE_EXISTS_TAC ‘SOME (_,_)’
     \\ fs [] \\ rpt $ first_x_assum $ irule_at Any)
@@ -633,7 +632,6 @@ Proof
   \\ ‘∃tt. OPTREL (λ(a,x) (b,y). a = b ∧ cexp1_rel x y) x tt ∧
            OPTREL (λ(a,x) (b,x1). a = b ∧ NRC cexp1_rel k x x1) tt x1’ by
    (Cases_on ‘x’ \\ Cases_on ‘x1’ \\ fs []
-    >- (qexists_tac ‘NONE’ \\ fs [])
     \\ Cases_on ‘x’ \\ Cases_on ‘x'’ \\ gvs []
     \\ Q.REFINE_EXISTS_TAC ‘SOME (_,_)’ \\ fs []
     \\ first_x_assum $ irule_at Any \\ fs [])

diff --git a/typing/pure_typingPropsScript.sml b/typing/pure_typingPropsScript.sml
@@ -1870,8 +1870,7 @@ Proof
   pop_assum mp_tac >> once_rewrite_tac[type_tcexp_cases] >>
   rw[] >> gvs[LIST_REL_EL_EQN, EL_MAP]
   >- (
-    Cases_on `usopt2` >> gvs[OPTREL_THM] >> disj1_tac >>
-    gvs[MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD] >>
+    disj1_tac >> gvs[MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD] >>
     gvs[GSYM LAMBDA_PROD, GSYM FST_THM] >>
     `MAP FST css1 = MAP FST css2` by (
       gvs[MAP_EQ_EVERY2, LIST_REL_EL_EQN] >> rw[] >>
@@ -1881,12 +1880,11 @@ Proof
     first_x_assum drule >> rw[]
     )
   >- (
-    Cases_on `usopt2` >> gvs[OPTREL_THM] >> disj1_tac >>
-    rpt (pairarg_tac >> gvs[]) >>
+    disj1_tac >> rpt (pairarg_tac >> gvs[]) >>
     rpt $ first_x_assum $ irule_at Any >> simp[]
     )
   >- (
-    Cases_on `usopt2` >> gvs[OPTREL_THM] >> ntac 2 disj2_tac >> disj1_tac >>
+    ntac 2 disj2_tac >> disj1_tac >>
     simp[MAP_MAP_o, combinTheory.o_DEF, LAMBDA_PROD] >>
     simp[GSYM LAMBDA_PROD, GSYM FST_THM] >> rw[]
     >- (