-
Notifications
You must be signed in to change notification settings - Fork 335
/
Refl.lean
71 lines (62 loc) · 2.51 KB
/
Refl.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
/-
Copyright (c) 2022 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
import Lean.Meta.Reduce
import Lean.Meta.Tactic.Util
import Lean.Meta.Tactic.Apply
namespace Lean.Meta
private def useKernel (lhs rhs : Expr) : MetaM Bool := do
if lhs.hasFVar || lhs.hasMVar || rhs.hasFVar || rhs.hasMVar then
return false
else
return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all
/--
Close given goal using `Eq.refl`.
-/
def _root_.Lean.MVarId.refl (mvarId : MVarId) : MetaM Unit := do
mvarId.withContext do
mvarId.checkNotAssigned `refl
let targetType ← mvarId.getType'
unless targetType.isAppOfArity ``Eq 3 do
throwTacticEx `rfl mvarId m!"equality expected{indentExpr targetType}"
let lhs ← instantiateMVars targetType.appFn!.appArg!
let rhs ← instantiateMVars targetType.appArg!
let success ← if (← useKernel lhs rhs) then
ofExceptKernelException (Kernel.isDefEq (← getEnv) {} lhs rhs)
else
isDefEq lhs rhs
unless success do
throwTacticEx `rfl mvarId m!"equality lhs{indentExpr lhs}\nis not definitionally equal to rhs{indentExpr rhs}"
let us := targetType.getAppFn.constLevels!
let α := targetType.appFn!.appFn!.appArg!
mvarId.assign (mkApp2 (mkConst ``Eq.refl us) α lhs)
@[deprecated MVarId.refl]
def refl (mvarId : MVarId) : MetaM Unit := do
mvarId.refl
@[deprecated MVarId.refl]
def _root_.Lean.MVarId.applyRefl (mvarId : MVarId) (msg : MessageData := "refl failed") : MetaM Unit :=
try mvarId.refl catch _ => throwError msg
/--
Try to apply `heq_of_eq`. If successful, then return new goal, otherwise return `mvarId`.
-/
def _root_.Lean.MVarId.heqOfEq (mvarId : MVarId) : MetaM MVarId :=
mvarId.withContext do
let some [mvarId] ← observing? do mvarId.apply (mkConst ``heq_of_eq [← mkFreshLevelMVar]) | return mvarId
return mvarId
/--
Try to apply `eq_of_heq`. If successful, then return new goal, otherwise return `mvarId`.
-/
def _root_.Lean.MVarId.eqOfHEq (mvarId : MVarId) : MetaM MVarId :=
mvarId.withContext do
let some [mvarId] ← observing? do mvarId.apply (mkConst ``eq_of_heq [← mkFreshLevelMVar]) | return mvarId
return mvarId
/--
Close given goal using `HEq.refl`.
-/
def _root_.Lean.MVarId.hrefl (mvarId : MVarId) : MetaM Unit := do
mvarId.withContext do
let some [] ← observing? do mvarId.apply (mkConst ``HEq.refl [← mkFreshLevelMVar])
| throwTacticEx `hrefl mvarId ""
end Lean.Meta