From e696e6d07d1c22e49491d6df59b2d4f96b681201 Mon Sep 17 00:00:00 2001
From: Hrutvik Kanabar <hrutvikkanabar@yahoo.co.uk>
Date: Thu, 7 Dec 2023 09:19:39 +0000
Subject: [PATCH] Fixes for `OPTREL` changes in HOL (probably
 HOL-Theorem-Prover/HOL@f0a4649)

---
 .../backend/passes/proofs/env_to_state_2ProofScript.sml   | 1 -
 .../backend/passes/proofs/state_app_unitProofScript.sml   | 2 --
 typing/pure_typingPropsScript.sml                         | 8 +++-----
 3 files changed, 3 insertions(+), 8 deletions(-)

diff --git a/compiler/backend/passes/proofs/env_to_state_2ProofScript.sml b/compiler/backend/passes/proofs/env_to_state_2ProofScript.sml
index fd7aaa3c..6529c6da 100644
--- 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
index bc1d5644..68b21da7 100644
--- 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
index 37a4ce3e..fd151f88 100644
--- 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[]
     >- (