@@ -6,9 +6,13 @@ Authors: Lars König, Mario Carneiro, Sebastian Graf
66module
77
88prelude
9- public import Std.Tactic.Do.Syntax
10- public import Lean.Elab.Tactic.Do.ProofMode.Focus
11- public import Lean.Elab.Tactic.Meta
9+ public import Lean.Elab.Tactic.Basic
10+ public import Lean.Elab.Tactic.Do.ProofMode.MGoal
11+ import Std.Tactic.Do.Syntax
12+ import Lean.Elab.Tactic.Meta
13+ import Lean.Elab.Tactic.Do.ProofMode.Basic
14+ import Lean.Elab.Tactic.Do.ProofMode.Focus
15+ import Lean.Meta.Tactic.Rfl
1216
1317public section
1418
@@ -21,14 +25,16 @@ open Lean Elab Tactic Meta
2125-- It will provide a proof for Q ∧ H ⊢ₛ T
2226-- if `k` produces a proof for Q ⊢ₛ T that may range over a pure proof h : φ.
2327-- It calls `k` with the φ in H = ⌜φ⌝ and a proof `h : φ` thereof.
24- def mPureCore (σs : Expr) (hyp : Expr) (name : TSyntax ``binderIdent)
25- (k : Expr /-φ:Prop-/ → Expr /-h:φ-/ → MetaM (α × MGoal × Expr)) : MetaM (α × MGoal × Expr) := do
28+ def mPureCore
29+ [Monad m] [MonadControlT MetaM m] [MonadLiftT MetaM m]
30+ (σs : Expr) (hyp : Expr) (name : TSyntax ``binderIdent)
31+ (k : Expr /-φ:Prop-/ → Expr /-h:φ-/ → m (α × MGoal × Expr)) : m (α × MGoal × Expr) := do
2632 let u ← mkFreshLevelMVar
2733 let φ ← mkFreshExprMVar (mkSort .zero)
2834 let inst ← synthInstance (mkApp3 (mkConst ``IsPure [u]) σs hyp φ)
29- let (name, ref) ← getFreshHypName name
35+ let (name, ref) ← liftMetaM <| getFreshHypName name
3036 withLocalDeclD name φ fun h => do
31- addLocalVarInfo ref (← getLCtx) h φ
37+ addLocalVarInfo ref (← liftMetaM <| getLCtx) h φ
3238 let (a, goal, prf /- : goal.toExpr -/ ) ← k φ h
3339 let prf ← mkLambdaFVars #[h] prf
3440 let prf := mkApp7 (mkConst ``Pure.thm [u]) σs goal.hyps hyp goal.target φ inst prf
@@ -38,10 +44,8 @@ def mPureCore (σs : Expr) (hyp : Expr) (name : TSyntax ``binderIdent)
3844@[builtin_tactic Lean.Parser.Tactic.mpure]
3945def elabMPure : Tactic
4046 | `(tactic| mpure $hyp) => do
41- let mvar ← getMainGoal
47+ let ( mvar, goal) ← mStartMainGoal
4248 mvar.withContext do
43- let g ← instantiateMVars <| ← mvar.getType
44- let some goal := parseMGoal? g | throwError "not in proof mode"
4549 let res ← goal.focusHypWithInfo hyp
4650 let (m, _new_goal, prf) ← mPureCore goal.σs res.focusHyp (← `(binderIdent| $hyp:ident)) fun _ _ => do
4751 let goal := res.restGoal goal
@@ -52,8 +56,87 @@ def elabMPure : Tactic
5256 replaceMainGoal [m.mvarId!]
5357 | _ => throwUnsupportedSyntax
5458
55- def MGoal.triviallyPure (goal : MGoal) : OptionT MetaM Expr := do
59+ -- NB: We do not use MVarId.intro because that would mean we require all callers to supply an MVarId.
60+ -- This function only knows about the hypothesis H=⌜φ⌝ to destruct.
61+ -- It will provide a proof for Q ∧ H ⊢ₛ T
62+ -- if `k` produces a proof for Q ⊢ₛ T that may range over a pure proof h : φ.
63+ -- It calls `k` with the φ in H = ⌜φ⌝ and a proof `h : φ` thereof.
64+ def mPureIntroCore [Monad m] [MonadLiftT MetaM m]
65+ (goal : MGoal)
66+ (k : Expr /-φ:Prop-/ → m (α × Expr)) : m (α × Expr) := do
67+ let φ ← mkFreshExprMVar (mkSort .zero)
68+ let inst ← synthInstance (mkApp3 (mkConst ``IsPure [goal.u]) goal.σs goal.target φ)
69+ let (a, hφ) ← k φ
70+ let prf := mkApp6 (mkConst ``Pure.intro [goal.u]) goal.σs goal.hyps goal.target φ inst hφ
71+ return (a, prf)
72+
73+ @[builtin_tactic Lean.Parser.Tactic.mpureIntro]
74+ def elabMPureIntro : Tactic
75+ | `(tactic| mpure_intro) => do
76+ let (mvar, goal) ← mStartMainGoal
77+ mvar.withContext do
78+ let (mv, prf) ← mPureIntroCore goal fun φ => do
79+ let m ← mkFreshExprSyntheticOpaqueMVar φ (← mvar.getTag)
80+ return (m.mvarId!, m)
81+ mvar.assign prf
82+ replaceMainGoal [mv]
83+ | _ => throwUnsupportedSyntax
84+
85+ partial def _root_.Lean.MVarId.applyRflAndAndIntro (mvar : MVarId) : MetaM Unit := do
86+ -- The target might look like `(⌜?n = nₛ ∧ ?m = b⌝ s).down`, which we reduce to
87+ -- `?n = nₛ ∧ ?m = b` by `whnfD`.
88+ -- (Recall that `⌜s = 4⌝ s` is `SPred.pure (σs:=[Nat]) (s = 4) s` and `SPred.pure` is
89+ -- semi-reducible.)
90+ let ty ← whnfD (← mvar.getType)
91+ trace[Elab.Tactic.Do.spec] "whnf: {ty}"
92+ if ty.isAppOf ``True then
93+ mvar.assign (mkConst ``True.intro)
94+ else if let some (lhs, rhs) := ty.app2? ``And then
95+ let hlhs ← mkFreshExprMVar lhs
96+ let hrhs ← mkFreshExprMVar rhs
97+ applyRflAndAndIntro hlhs.mvarId!
98+ applyRflAndAndIntro hrhs.mvarId!
99+ mvar.assign (mkApp4 (mkConst ``And.intro) lhs rhs hlhs hrhs)
100+ else
101+ mvar.setType ty
102+ mvar.applyRfl
103+
104+ def MGoal.pureRflAndAndIntro (goal : MGoal) : OptionT MetaM Expr := do
105+ trace[Elab.Tactic.Do.spec] "pureRflAndAndIntro: {goal.target}"
106+ try
107+ let (_, prf) ← mPureIntroCore goal fun φ => do
108+ trace[Elab.Tactic.Do.spec] "discharge? {φ}"
109+ let m ← mkFreshExprMVar φ
110+ m.mvarId!.applyRflAndAndIntro
111+ trace[Elab.Tactic.Do.spec] "discharged: {φ}"
112+ return ((), m)
113+ return prf
114+ catch _ => failure
115+
116+ def MGoal.pureTrivial (goal : MGoal) : OptionT MetaM Expr := do
117+ try
118+ let (_, prf) ← mPureIntroCore goal fun φ => do
119+ let m ← mkFreshExprMVar φ
120+ try
121+ -- First try to use rfl and And.intro directly.
122+ -- This is more efficient than to elaborate the `trivial` tactic.
123+ m.mvarId!.applyRflAndAndIntro
124+ catch _ =>
125+ let ([], _) ← runTactic m.mvarId! (← `(tactic| trivial))
126+ | failure
127+ return ((), m)
128+ return prf
129+ catch _ => failure
130+
131+ /-
132+ def MGoal.pureRfl (goal : MGoal) : OptionT MetaM Expr := do
56133 let mv ← mkFreshExprMVar goal.toExpr
57- let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); trivial )) catch _ => failure
134+ let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); rfl )) catch _ => failure
58135 | failure
59136 return mv
137+ def MGoal.pureRfl (goal : MGoal) : OptionT MetaM Expr := do
138+ let mv ← mkFreshExprMVar goal.toExpr
139+ let ([], _) ← try runTactic mv.mvarId! (← `(tactic| apply $(mkIdent ``Std.Do.SPred.Tactic.Pure.intro); rfl)) catch _ => failure
140+ | failure
141+ return mv
142+ -/
0 commit comments