/-
Copyright (c) 2022 Alex J. Best. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Alex J. Best
-/
import Lean
import Mathlib.Lean.Expr.Basic

/-!
# The `generalize_proofs` tactic

Generalize any proofs occuring in the goal or in chosen hypotheses, replacing them by
named hypotheses so that they can be referred to later in the proof easily.
Commonly useful when dealing with functions like `Classical.choose` that produce data from proofs.

For example:
```lean
example : List.nthLe [1, 2] 1 dec_trivial = 2 := by
  -- ⊢ [1, 2].nthLe 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nthLe 1 h = 2
```
-/

namespace Mathlib.Tactic.GeneralizeProofs
open Lean Meta Elab Parser.Tactic Elab.Tactic

/- The following set up are the visit function are based on the file
Lean.Meta.AbstractNestedProofs in core -/

/-- State for the generalize proofs tactic, contains the remaining names to be used and the
list of generalizations so far -/
structure 
State: List (TSyntax `Lean.binderIdent) → Array GeneralizeArg → State
State where
  /-- The user provided names, may be anonymous -/
  
nextIdx: State → List (TSyntax `Lean.binderIdent)
nextIdx : 
List: Type ?u.4 → Type ?u.4
List (
TSyntax: SyntaxNodeKinds → Type
TSyntax ``
binderIdent: ParserDescr
binderIdent)
  /-- The generalizations made so far -/
  
curIdx: State → Array GeneralizeArg
curIdx : 
Array: Type ?u.88 → Type ?u.88
Array 
GeneralizeArg: Type
GeneralizeArg := 
#[]: Array ?m.90
#[]

/-- Monad used by the `generalizeProofs` tactic, carries an expr cache and state with
names to use and previous generalizations -/
abbrev 
M: Type → Type
M := 
MonadCacheT: {ω : Type} →
  (α : Type) → Type → (m : Type → Type) → [inst : STWorld ω m] → [inst : BEq α] → [inst : Hashable α] → Type → Type
MonadCacheT 
ExprStructEq: Type
ExprStructEq 
Expr: Type
Expr $ StateRefT 
State: Type
State 
MetaM: Type → Type
MetaM

/-- generalize the given e -/
private def 
mkGen: Expr → M Unit
mkGen (
e: Expr
e : 
Expr: Type
Expr) : 
M: Type → Type
M 
Unit: Type
Unit := do
  let 
s: ?m.967
s ← 
get: {σ : outParam (Type ?u.703)} → {m : Type ?u.703 → Type ?u.702} → [self : MonadState σ m] → m σ
get
  let 
t: ?m.970
t ← match 
s: ?m.967
s.
nextIdx: State → List (TSyntax `Lean.binderIdent)
nextIdx with
  | [] => 
mkFreshUserName: Name → CoreM Name
mkFreshUserName
mkFreshUserName `h: M (?m.974 y✝)
 
`h: Name
`h
  | 
n: TSyntax `Lean.binderIdent
n :: 
rest: List (TSyntax `Lean.binderIdent)
rest =>
    
modify: {σ : Type ?u.1263} → {m : Type ?u.1263 → Type ?u.1262} → [inst : MonadState σ m] → (σ → σ) → m PUnit
modify fun 
s: ?m.1297
s ↦ { 
s: ?m.1297
s with nextIdx := 
rest: List (TSyntax `Lean.binderIdent)
rest }
    match 
n: TSyntax `Lean.binderIdent
n with
    | `(
binderIdent: ParserDescr
binderIdent| $
s: ?m.1639
s:ident) => 
pure: {f : Type ?u.1683 → Type ?u.1682} → [self : Pure f] → {α : Type ?u.1683} → α → f α
pure
pure s.getId: M (?m.974 y✝)
 
s: ?m.1639
s
pure s.getId: M (?m.974 y✝)
.
getId: Ident → Name
getId
    | _ => 
mkFreshUserName: Name → CoreM Name
mkFreshUserName
mkFreshUserName `h: M (?m.974 y✝)
 
`h: Name
`h
  
modify: {σ : Type ?u.2056} → {m : Type ?u.2056 → Type ?u.2055} → [inst : MonadState σ m] → (σ → σ) → m PUnit
modify fun 
s: ?m.2090
s ↦ { 
s: ?m.2090
s with curIdx := 
s: ?m.2090
s.
curIdx: State → Array GeneralizeArg
curIdx.
push: {α : Type ?u.2413} → Array α → α → Array α
push ⟨
e: Expr
e, 
t: ?m.970
t, 
none: {α : Type ?u.2504} → Option α
none⟩ }

/-- Recursively generalize proofs occuring in e -/
partial def 
visit: Expr → M Expr
visit (
e: Expr
e : 
Expr: Type
Expr) : 
M: Type → Type
M 
Expr: Type
Expr := do
  if 
e: Expr
e.
isAtomic: Expr → Bool
isAtomic then
    
pure: {f : Type ?u.7821 → Type ?u.7820} → [self : Pure f] → {α : Type ?u.7821} → α → f α
pure 
e: Expr
e
  else
    let 
visitBinders: Array Expr → M Expr → M Expr
visitBinders (
xs: Array Expr
xs : 
Array: Type ?u.7902 → Type ?u.7902
Array 
Expr: Type
Expr) (
k: M Expr
k : 
M: Type → Type
M 
Expr: Type
Expr) : 
M: Type → Type
M 
Expr: Type
Expr := do
      let 
localInstances: ?m.8063
localInstances ← 
getLocalInstances: MetaM LocalInstances
getLocalInstances
      let mut 
lctx: ?m.8134
lctx ← 
getLCtx: {m : Type → Type} → [self : MonadLCtx m] → m LocalContext
getLCtx
      for 
x: ?m.8236
x in 
xs: Array Expr
xs do
        let 
xFVarId: ?m.8245
xFVarId := 
x: ?m.8236
x.
fvarId!: Expr → FVarId
fvarId!
        let 
localDecl: ?m.8300
localDecl ← 
xFVarId: ?m.8245
xFVarId.
getDecl: FVarId → MetaM LocalDecl
getDecl
        let 
type: ?m.8354
type      ← 
visit: Expr → M Expr
visit 
localDecl: ?m.8300
localDecl.
type: LocalDecl → Expr
type
        let 
localDecl: ?m.8357
localDecl := 
localDecl: ?m.8300
localDecl.
setType: LocalDecl → Expr → LocalDecl
setType 
type: ?m.8354
type
        let 
localDecl: ?m.8364
localDecl ← match 
localDecl: ?m.8357
localDecl.
value?: LocalDecl → Option Expr
value? with
           | 
some: {α : Type ?u.8376} → α → Option α
some 
value: Expr
value => let 
value: ?m.8442
value ← 
visit: Expr → M Expr
visit 
value: Expr
value; 
pure: {f : Type ?u.8481 → Type ?u.8480} → [self : Pure f] → {α : Type ?u.8481} → α → f α
pure <| 
localDecl: ?m.8357
localDecl.
setValue: LocalDecl → Expr → LocalDecl
setValue 
value: ?m.8442
value
           | 
none: {α : Type ?u.7916} → Option α
none       => 
pure: {f : Type ?u.8619 → Type ?u.8618} → [self : Pure f] → {α : Type ?u.8619} → α → f α
pure 
localDecl: ?m.8357
localDecl
        
lctx: LocalContext
lctx := 
lctx: LocalContext
lctx.
modifyLocalDecl: LocalContext → FVarId → (LocalDecl → LocalDecl) → LocalContext
modifyLocalDecl 
xFVarId: ?m.8245
xFVarId fun 
_: ?m.8745
_ ↦ 
localDecl: ?m.8368 lctx
localDecl
      
withLCtx: {n : Type → Type ?u.9053} →
  [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → LocalContext → LocalInstances → n α → n α
withLCtx 
lctx: ?m.9051
lctx 
localInstances: ?m.8063
localInstances 
k: M Expr
k
    
checkCache: {α β : Type} → {m : Type → Type} → [inst : MonadCache α β m] → [inst : Monad m] → α → (Unit → m β) → m β
checkCache (
e: Expr
e : 
ExprStructEq: Type
ExprStructEq) fun 
_: ?m.9383
_ ↦ do
      if 
(← AbstractNestedProofs.isNonTrivialProof e): ?m.9532
(← 
AbstractNestedProofs.isNonTrivialProof: Expr → MetaM Bool
AbstractNestedProofs.isNonTrivialProof
(← AbstractNestedProofs.isNonTrivialProof e): ?m.9532
 
e: Expr
e
(← AbstractNestedProofs.isNonTrivialProof e): ?m.9532
) then
        
mkGen: Expr → M Unit
mkGen 
e: Expr
e
        return 
e: Expr
e
      else match 
e: Expr
e with
        | 
.lam: Name → Expr → Expr → BinderInfo → Expr
.lam ..      => 
lambdaLetTelescope: {n : Type → Type ?u.9722} →
  [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → Expr → (Array Expr → Expr → n α) → n α
lambdaLetTelescope 
e: Expr
e fun 
xs: ?m.9763
xs 
b: ?m.9766
b ↦ 
visitBinders: Array Expr → M Expr → M Expr
visitBinders 
xs: ?m.9763
xs do
          
mkLambdaFVars: Array Expr → Expr → optParam Bool false → optParam Bool true → optParam BinderInfo BinderInfo.implicit → MetaM Expr
mkLambdaFVars 
xs: ?m.9763
xs 
(← visit b): ?m.9831
(← 
visit: Expr → M Expr
visit
(← visit b): ?m.9831
 
b: ?m.9766
b
(← visit b): ?m.9831
) (usedLetOnly := 
false: Bool
false)
        | 
.letE: Name → Expr → Expr → Expr → Bool → Expr
.letE ..     => 
lambdaLetTelescope: {n : Type → Type ?u.9940} →
  [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → Expr → (Array Expr → Expr → n α) → n α
lambdaLetTelescope 
e: Expr
e fun 
xs: ?m.9981
xs 
b: ?m.9984
b ↦ 
visitBinders: Array Expr → M Expr → M Expr
visitBinders 
xs: ?m.9981
xs do
          
mkLambdaFVars: Array Expr → Expr → optParam Bool false → optParam Bool true → optParam BinderInfo BinderInfo.implicit → MetaM Expr
mkLambdaFVars 
xs: ?m.9981
xs 
(← visit b): ?m.10049
(← 
visit: Expr → M Expr
visit
(← visit b): ?m.10049
 
b: ?m.9984
b
(← visit b): ?m.10049
) (usedLetOnly := 
false: Bool
false)
        | 
.forallE: Name → Expr → Expr → BinderInfo → Expr
.forallE ..  => 
forallTelescope: {n : Type → Type ?u.10150} →
  [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → Expr → (Array Expr → Expr → n α) → n α
forallTelescope 
e: Expr
e fun 
xs: ?m.10191
xs 
b: ?m.10194
b ↦ 
visitBinders: Array Expr → M Expr → M Expr
visitBinders 
xs: ?m.10191
xs do
          
mkForallFVars: Array Expr → Expr → optParam Bool false → optParam Bool true → optParam BinderInfo BinderInfo.implicit → MetaM Expr
mkForallFVars 
xs: ?m.10191
xs 
(← visit b): ?m.10259
(← 
visit: Expr → M Expr
visit
(← visit b): ?m.10259
 
b: ?m.10194
b
(← visit b): ?m.10259
)
        | 
.mdata: MData → Expr → Expr
.mdata _ 
b: Expr
b   => return 
e: Expr
e.
updateMData!: Expr → Expr → Expr
updateMData! 
(← visit b): ?m.10373
(← 
visit: Expr → M Expr
visit
(← visit b): ?m.10373
 
b: Expr
b
(← visit b): ?m.10373
)
        | 
.proj: Name → Nat → Expr → Expr
.proj _ _ 
b: Expr
b  => return 
e: Expr
e.
updateProj!: Expr → Expr → Expr
updateProj! 
(← visit b): ?m.10487
(← 
visit: Expr → M Expr
visit
(← visit b): ?m.10487
 
b: Expr
b
(← visit b): ?m.10487
)
        | 
.app: Expr → Expr → Expr
.app ..      => 
e: Expr
e.
withApp: {α : Sort ?u.10545} → Expr → (Expr → Array Expr → α) → α
withApp fun 
f: ?m.10551
f 
args: ?m.10554
args ↦ return 
mkAppN: Expr → Array Expr → Expr
mkAppN 
f: ?m.10551
f 
(← args.mapM visit): ?m.10650
(← 
args: ?m.10554
args
(← args.mapM visit): ?m.10650
.
mapM: {α : Type ?u.10599} →
  {β : Type ?u.10598} → {m : Type ?u.10598 → Type ?u.10597} → [inst : Monad m] → (α → m β) → Array α → m (Array β)
mapM
(← args.mapM visit): ?m.10650
 
visit: Expr → M Expr
visit
(← args.mapM visit): ?m.10650
)
        | _            => 
pure: {f : Type ?u.10712 → Type ?u.10711} → [self : Pure f] → {α : Type ?u.10712} → α → f α
pure 
e: Expr
e

/--
Generalize proofs in the goal, naming them with the provided list.

For example:
```lean
example : List.nthLe [1, 2] 1 dec_trivial = 2 := by
  -- ⊢ [1, 2].nthLe 1 _ = 2
  generalize_proofs h,
  -- h : 1 < [1, 2].length
  -- ⊢ [1, 2].nthLe 1 h = 2
```
-/
elab (name := 
generalizeProofs: ParserDescr
generalizeProofs) "generalize_proofs"
    
hs: ?m.32233
hs:(
ppSpace: Parser.Parser
ppSpace (
colGt: optParam String "checkColGt" → Parser.Parser
colGt 
binderIdent: ParserDescr
binderIdent))* 
loc: ?m.32217
loc:(
ppSpace: Parser.Parser
ppSpace 
location: ParserDescr
location)? : 
tactic: Parser.Category
tactic => do
  let 
ou: ?m.32292
ou := if 
loc: ?m.32217
loc.
isSome: {α : Type ?u.32293} → Option α → Bool
isSome then
    match 
expandLocation: Syntax → Location
expandLocation 
loc: ?m.32217
loc.
get!: {α : Type ?u.32387} → [inst : Inhabited α] → Option α → α
get! with
    | 
.wildcard: Location
.wildcard => 
#[]: Array ?m.34292
#[]
    | 
.targets: Array Syntax → Bool → Location
.targets 
t: Array Syntax
t _ => 
t: Array Syntax
t
  else 
#[]: Array ?m.32487
#[]
  let 
fvs: ?m.32551
fvs ← 
getFVarIds: Array Syntax → TacticM (Array FVarId)
getFVarIds 
ou: ?m.32292
ou
  let 
goal: ?m.32599
goal ← 
getMainGoal: TacticM MVarId
getMainGoal
  let 
ty: ?m.32939
ty ← 
instantiateMVars: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → Expr → m Expr
instantiateMVars 
(← goal.getType): ?m.32822
(← 
goal: ?m.32599
goal
(← goal.getType): ?m.32822
.
getType: MVarId → MetaM Expr
getType
(← goal.getType): ?m.32822
)
  let (_, ⟨_, 
out: Array GeneralizeArg
out⟩) ← 
GeneralizeProofs.visit: Expr → M Expr
GeneralizeProofs.visit 
ty: ?m.32939
ty |>.
run: {ω α β : Type} →
  {m : Type → Type} →
    [inst : STWorld ω m] →
      [inst_1 : BEq α] →
        [inst_2 : Hashable α] →
          [inst_3 : MonadLiftT (ST ω) m] → [inst_4 : Monad m] → {σ : Type} → MonadCacheT α β m σ → m σ
run.
run: {ω σ : Type} →
  {m : Type → Type} → [inst : Monad m] → [inst : MonadLiftT (ST ω) m] → {α : Type} → StateRefT' ω σ m α → σ → m (α × σ)
run { nextIdx := 
hs: ?m.32233
hs.
toList: {α : Type ?u.33450} → Array α → List α
toList }
  let (_, 
fvarIds: Array FVarId
fvarIds, 
goal: MVarId
goal) ← 
goal: ?m.32599
goal.
generalizeHyp: MVarId →
  Array GeneralizeArg →
    optParam (Array FVarId) #[] → optParam FVarSubst { map := ∅ } → MetaM (FVarSubst × Array FVarId × MVarId)
generalizeHyp 
out: Array GeneralizeArg
out 
fvs: ?m.32551
fvs
  for 
h: ?m.33722
h in 
hs: ?m.32233
hs, 
fvar: FVarId
fvar in 
fvarIds: Array FVarId
fvarIds do
    
goal: MVarId
goal.
withContext: {n : Type → Type ?u.33889} → [inst : MonadControlT MetaM n] → [inst : Monad n] → {α : Type} → MVarId → n α → n α
withContext <| (
Expr.fvar: FVarId → Expr
Expr.fvar 
fvar: FVarId
fvar).
addLocalVarInfoForBinderIdent: Expr → TSyntax `Lean.binderIdent → TermElabM Unit
addLocalVarInfoForBinderIdent 
h: ?m.33722
h
  
replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal [
goal: MVarId
goal]