/-
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
import Mathlib.Lean.Meta

/-!
# `rfl` tactic extension for reflexive relations

This extends the `rfl` tactic so that it works on any reflexive relation,
provided the reflexivity lemma has been marked as `@[refl]`.
-/

namespace Mathlib.Tactic

open Lean Meta

/-- Environment extensions for `refl` lemmas -/
initialize 
reflExt: SimpleScopedEnvExtension (Name × Array (DiscrTree.Key true)) (DiscrTree Name true)
reflExt :
    
SimpleScopedEnvExtension: Type → Type → Type
SimpleScopedEnvExtension (
Name: Type
Name × 
Array: Type ?u.559 → Type ?u.559
Array (
DiscrTree.Key: Bool → Type
DiscrTree.Key 
true: Bool
true)) (
DiscrTree: Type → Bool → Type
DiscrTree 
Name: Type
Name 
true: Bool
true) ←
  
registerSimpleScopedEnvExtension: {α σ : Type} → SimpleScopedEnvExtension.Descr α σ → IO (SimpleScopedEnvExtension α σ)
registerSimpleScopedEnvExtension {
    addEntry := fun 
dt: ?m.39
dt (
n: Name
n, 
ks: Array (DiscrTree.Key true)
ks) ↦ 
dt: ?m.39
dt.
insertCore: {α : Type} → {s : Bool} → [inst : BEq α] → DiscrTree α s → Array (DiscrTree.Key s) → α → DiscrTree α s
insertCore 
ks: Array (DiscrTree.Key true)
ks 
n: Name
n
    initial := 
{}: DiscrTree ?m.171 ?m.172
{}
  }

initialize 
registerBuiltinAttribute: AttributeImpl → IO Unit
registerBuiltinAttribute {
  name := 
`refl: Name
`refl
  descr := 
"reflexivity relation": String
"reflexivity relation"
  add := fun 
decl: ?m.619
decl 
_: ?m.622
_ 
kind: ?m.625
kind ↦ 
MetaM.run': {α : Type} →
  MetaM α →
    optParam Context
        {
          config :=
            { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false,
              isDefEqStuckEx := false, transparency := TransparencyMode.default, zetaNonDep := true, trackZeta := false,
              unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true,
              etaStruct := EtaStructMode.all },
          lctx :=
            {
              fvarIdToDecl :=
                { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              decls :=
                { root := PersistentArrayNode.node (Array.mkEmpty (USize.toNat PersistentArray.branching)),
                  tail := Array.mkEmpty (USize.toNat PersistentArray.branching), size := 0,
                  shift := PersistentArray.initShift, tailOff := 0 } },
          localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } →
      optParam State
          {
            mctx :=
              { depth := 0, levelAssignDepth := 0, mvarCounter := 0,
                lDepth := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                decls := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                userNames :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                lAssignment :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                eAssignment :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                dAssignment :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 } },
            cache :=
              {
                inferType :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                funInfo := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                synthInstance :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                whnfDefault :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                whnfAll := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                defEq := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 } },
            zetaFVarIds := ∅,
            postponed :=
              { root := PersistentArrayNode.node (Array.mkEmpty (USize.toNat PersistentArray.branching)),
                tail := Array.mkEmpty (USize.toNat PersistentArray.branching), size := 0,
                shift := PersistentArray.initShift, tailOff := 0 } } →
        CoreM α
MetaM.run' do
    let 
declTy: ?m.929
declTy := 
(← getConstInfo decl): ?m.926
(← 
getConstInfo: {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m ConstantInfo
getConstInfo
(← getConstInfo decl): ?m.926
 
decl: ?m.619
decl
(← getConstInfo decl): ?m.926
).
type: ConstantInfo → Expr
type
    let (_, _, 
targetTy: Expr
targetTy) ← 
withReducible: {n : Type → Type ?u.968} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → n α
withReducible <| 
forallMetaTelescopeReducing: Expr →
  optParam (Option Nat) none → optParam MetavarKind MetavarKind.natural → MetaM (Array Expr × Array BinderInfo × Expr)
forallMetaTelescopeReducing 
declTy: ?m.929
declTy
    let 
fail: ?m.1121
fail := throwError
      "@[refl] attribute only applies to lemmas proving x ∼ x, got {
declTy: ?m.929
declTy}"
    let 
.app: Expr → Expr → Expr
.app (
.app: Expr → Expr → Expr
.app 
rel: Expr
rel 
lhs: Expr
lhs) 
rhs: Expr
rhs := 
targetTy: Expr
targetTy | 
fail: ?m.1121
fail
    unless ← 
withNewMCtxDepth: {n : Type → Type ?u.1388} →
  [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → n α → optParam Bool false → n α
withNewMCtxDepth <| 
isDefEq: Expr → Expr → MetaM Bool
isDefEq 
lhs: Expr
lhs 
rhs: Expr
rhs do 
fail: ?m.1121
fail
    let 
key: ?m.1765
key ← 
DiscrTree.mkPath: {s : Bool} → Expr → MetaM (Array (DiscrTree.Key s))
DiscrTree.mkPath 
rel: Expr
rel
    
reflExt: SimpleScopedEnvExtension (Name × Array (DiscrTree.Key true)) (DiscrTree Name true)
reflExt.
add: {m : Type → Type} →
  {α β σ : Type} →
    [inst : Monad m] →
      [inst : MonadResolveName m] →
        [inst : MonadEnv m] → ScopedEnvExtension α β σ → β → optParam AttributeKind AttributeKind.global → m Unit
add (
decl: ?m.619
decl, 
key: ?m.1765
key) 
kind: ?m.625
kind
}

open Elab Tactic

/-- `MetaM` version of the `rfl` 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 
_root_.Lean.MVarId.rfl: MVarId → MetaM Unit
_root_.Lean.MVarId.rfl (
goal: MVarId
goal : 
MVarId: Type
MVarId) : 
MetaM: Type → Type
MetaM 
Unit: Type
Unit := do
  let 
.app: Expr → Expr → Expr
.app (
.app: Expr → Expr → Expr
.app 
rel: Expr
rel _) _ ← 
whnfR: Expr → MetaM Expr
whnfR <|← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars <|← 
goal: MVarId
goal.
getType: MVarId → MetaM Expr
getType
    | throwError "reflexivity lemmas only apply to binary relations, not
      {
indentExpr: Expr → MessageData
indentExpr 
(← goal.getType): ?m.9236
(← 
goal: MVarId
goal
(← goal.getType): ?m.9236
.
getType: MVarId → MetaM Expr
getType
(← goal.getType): ?m.9236
)}"
  let 
s: ?m.6530
s ← 
saveState: {s : outParam Type} → {m : Type → Type} → [self : MonadBacktrack s m] → m s
saveState
  let mut 
ex?: ?m.8321
ex? := 
none: {α : Type ?u.6534} → Option α
none
  for 
lem: ?m.6767
lem in ← (
reflExt: SimpleScopedEnvExtension (Name × Array (DiscrTree.Key true)) (DiscrTree Name true)
reflExt.
getState: {σ α β : Type} → [inst : Inhabited σ] → ScopedEnvExtension α β σ → Environment → σ
getState 
(← getEnv): ?m.6582
(← 
getEnv: {m : Type → Type} → [self : MonadEnv m] → m Environment
getEnv
(← getEnv): ?m.6582
)).
getMatch: {α : Type} → {s : Bool} → DiscrTree α s → Expr → MetaM (Array α)
getMatch 
rel: Expr
rel do
    try
      let 
gs: ?m.6939
gs ← 
goal: MVarId
goal.
apply: MVarId →
  Expr →
    optParam ApplyConfig
        { newGoals := ApplyNewGoals.nonDependentFirst, synthAssignedInstances := true, approx := true } →
      MetaM (List MVarId)
apply 
(← mkConstWithFreshMVarLevels lem): ?m.6882
(← 
mkConstWithFreshMVarLevels: Name → MetaM Expr
mkConstWithFreshMVarLevels
(← mkConstWithFreshMVarLevels lem): ?m.6882
 
lem: ?m.6767
lem
(← mkConstWithFreshMVarLevels lem): ?m.6882
)
      if 
gs: ?m.6939
gs.
isEmpty: {α : Type ?u.6941} → List α → Bool
isEmpty then return 
(): Unit
() else
        
logError: {m : Type → Type} →
  [inst : Monad m] → [inst : MonadLog m] → [inst : AddMessageContext m] → [inst : MonadOptions m] → MessageData → m Unit
logError <| 
MessageData.tagged: Name → MessageData → MessageData
MessageData.tagged 
`Tactic.unsolvedGoals: Name
`Tactic.unsolvedGoals <| m!"unsolved goals\n
          {
goalsToMessageData: List MVarId → MessageData
goalsToMessageData 
gs: ?m.6939
gs}"
    catch 
e: ?m.7376
e =>
      
ex?: ?m.7425
ex? := 
ex?: ?m.6781
ex? <|> (
some: {α : Type ?u.7429} → α → Option α
some (← 
saveState: {s : outParam Type} → {m : Type → Type} → [self : MonadBacktrack s m] → m s
saveState, 
e: ?m.7376
e)) -- stash the first failure of `apply`
    
s: ?m.6530
s.
restore: Meta.SavedState → MetaM Unit
restore
  if let 
some: {α : Type ?u.8538} → α → Option α
some (
sErr: Meta.SavedState
sErr, 
e: Exception
e) := 
ex?: ?m.8321
ex? then
    
sErr: Meta.SavedState
sErr.
restore: Meta.SavedState → MetaM Unit
restore
    
throw: {ε : outParam (Type ?u.8629)} →
  {m : Type ?u.8628 → Type ?u.8627} → [self : MonadExcept ε m] → {α : Type ?u.8628} → ε → m α
throw 
e: Exception
e
  else
    
throwError "rfl failed, no lemma with @[refl] applies": ?m.8866 ?m.8867
throwError
throwError "rfl failed, no lemma with @[refl] applies": ?m.8866 ?m.8867
 "rfl failed, no lemma with @[refl] applies"

/--
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].
-/
elab_rules : tactic
| `(tactic| rfl) => 
withMainContext: {α : Type} → TacticM α → TacticM α
withMainContext do 
liftMetaFinishingTactic: (MVarId → MetaM Unit) → TacticM Unit
liftMetaFinishingTactic (·.
rfl: MVarId → MetaM Unit
rfl)