-
Notifications
You must be signed in to change notification settings - Fork 314
/
Rfl.lean
72 lines (64 loc) · 2.81 KB
/
Rfl.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
72
/-
Copyright (c) 2022 Newell Jensen. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Newell Jensen
-/
import Lean.Meta.Tactic.Subst
import Std.Tactic.Relation.Rfl
/-!
# `Lean.MVarId.liftReflToEq`
Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
If this can't be done, returns the original `MVarId`.
-/
namespace Mathlib.Tactic
open Lean Meta Elab Tactic Std.Tactic
/--
This tactic applies to a goal whose target has the form `x ~ x`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute [refl].
-/
def rflTac : TacticM Unit :=
withMainContext do liftMetaFinishingTactic (·.applyRfl)
/-- If `e` is the form `@R .. x y`, where `R` is a reflexive
relation, return `some (R, x, y)`.
As a special case, if `e` is `@HEq α a β b`, return ``some (`HEq, a, b)``. -/
def _root_.Lean.Expr.relSidesIfRefl? (e : Expr) : MetaM (Option (Name × Expr × Expr)) := do
if let some (_, lhs, rhs) := e.eq? then
return (``Eq, lhs, rhs)
if let some (lhs, rhs) := e.iff? then
return (``Iff, lhs, rhs)
if let some (_, lhs, _, rhs) := e.heq? then
return (``HEq, lhs, rhs)
if let .app (.app rel lhs) rhs := e then
unless (← (reflExt.getState (← getEnv)).getMatch rel reflExt.config).isEmpty do
match rel.getAppFn.constName? with
| some n => return some (n, lhs, rhs)
| none => return none
return none
/-- Helper theorem for `Lean.MVar.liftReflToEq`. -/
private theorem rel_of_eq_and_refl {α : Sort _} {R : α → α → Prop}
{x y : α} (hxy : x = y) (h : R x x) : R x y :=
hxy ▸ h
/--
Convert a goal of the form `x ~ y` into the form `x = y`, where `~` is a reflexive
relation, that is, a relation which has a reflexive lemma tagged with the attribute `[refl]`.
If this can't be done, returns the original `MVarId`.
-/
def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
mvarId.checkNotAssigned `liftReflToEq
let .app (.app rel _) _ ← withReducible mvarId.getType' | return mvarId
if rel.isAppOf `Eq then
-- No need to lift Eq to Eq
return mvarId
for lem in ← (Std.Tactic.reflExt.getState (← getEnv)).getMatch rel Std.Tactic.reflExt.config do
let res ← observing? do
-- First create an equality relating the LHS and RHS
-- and reduce the goal to proving that LHS is related to LHS.
let [mvarIdEq, mvarIdR] ← mvarId.apply (← mkConstWithFreshMVarLevels ``rel_of_eq_and_refl)
| failure
-- Then fill in the proof of the latter by reflexivity.
let [] ← mvarIdR.apply (← mkConstWithFreshMVarLevels lem) | failure
return mvarIdEq
if let some mvarIdEq := res then
return mvarIdEq
return mvarId