From e58872aa4dc31f0819fe17b13e6b7e4b0d9635c8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 20 Jul 2023 15:46:11 +0200
Subject: Make progress on some of the hashmap proofs

---
 backends/lean/Base/Utils.lean | 30 ++++++++++++++++++++++--------
 1 file changed, 22 insertions(+), 8 deletions(-)

(limited to 'backends/lean/Base')

diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 44590176..f014e112 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -326,14 +326,6 @@ def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do
     | some _ => pure ()
     | none => firstTac tacl -/
 
--- Split the goal if it is a conjunction
-def splitConjTarget : TacticM Unit := do
-  withMainContext do
-  let and_intro := Expr.const ``And.intro []
-  let mvarIds' ← _root_.Lean.MVarId.apply (← getMainGoal) and_intro
-  Term.synthesizeSyntheticMVarsNoPostponing
-  replaceMainGoal mvarIds'
-
 -- Taken from Lean.Elab.evalAssumption
 def assumptionTac : TacticM Unit :=
   liftMetaTactic fun mvarId => do mvarId.assumption; pure []
@@ -349,6 +341,24 @@ def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do
   if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1))
   else pure (e, none)
 
+-- Split the goal if it is a conjunction
+def splitConjTarget : TacticM Unit := do
+  withMainContext do
+  let g ← getMainTarget
+  -- The tactic was initially implemened with `_root_.Lean.MVarId.apply`
+  -- but it tended to mess the goal by unfolding terms, even when it failed
+  let (l, r) ← optSplitConj g
+  match r with
+  | none => do throwError "The goal is not a conjunction"
+  | some r => do
+    let lmvar ← mkFreshExprSyntheticOpaqueMVar l
+    let rmvar ← mkFreshExprSyntheticOpaqueMVar r
+    let and_intro ← mkAppM ``And.intro #[lmvar, rmvar]
+    let g ← getMainGoal
+    g.assign and_intro
+    let goals ← getUnsolvedGoals
+    setGoals (lmvar.mvarId! :: rmvar.mvarId! :: goals)
+
 -- Destruct an equaliy and return the two sides
 def destEq (e : Expr) : MetaM (Expr × Expr) := do
   e.withApp fun f args =>
@@ -520,6 +530,10 @@ elab "split_all_exists " n:ident : tactic => do
   let fvar := mkFVar decl.fvarId
   splitAllExistsTac fvar [] (fun _ _ => pure ())
 
+elab "split_target_conjs" : tactic =>
+  withMainContext do
+  repeatTac splitConjTarget
+
 example (h : a ∧ b) : a := by
   split_all_exists h
   split_conj h
-- 
cgit v1.2.3