summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2023-07-20 15:46:11 +0200
committerSon Ho2023-07-20 15:46:11 +0200
commite58872aa4dc31f0819fe17b13e6b7e4b0d9635c8 (patch)
tree8e10b3dced080a71f0ae6f352aa4b3b1a32cc00e /backends
parent03492250b45855fe9db5e0a28a96166607cd84a1 (diff)
Make progress on some of the hashmap proofs
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Utils.lean30
1 files changed, 22 insertions, 8 deletions
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