/-
Copyright (c) 2022 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean.Meta.Tactic.Congr
import Std.Tactic.RCases
import Std.Tactic.Ext

/-! # `congr with` tactic, `rcongr` tactic -/

namespace Std.Tactic
open Lean Meta Elab Tactic Std.Tactic

/--
Apply congruence (recursively) to goals of the form `⊢ f as = f bs` and `⊢ HEq (f as) (f bs)`.
* `congr n` controls the depth of the recursive applications.
  This is useful when `congr` is too aggressive in breaking down the goal.
  For example, given `⊢ f (g (x + y)) = f (g (y + x))`,
  `congr` produces the goals `⊢ x = y` and `⊢ y = x`,
  while `congr 2` produces the intended `⊢ x + y = y + x`.
* If, at any point, a subgoal matches a hypothesis then the subgoal will be closed.
* You can use `congr with p (: n)?` to call `ext p (: n)?` to all subgoals generated by `congr`.
  For example, if the goal is `⊢ f '' s = g '' s` then `congr with x` generates the goal
  `x : α ⊢ f x = g x`.
-/
syntax (name := congrWith: ParserDescr
congrWith) "congr" (ppSpace: Parser.Parser
ppSpace colGt: optParam String "checkColGt" → Parser.Parser
colGt num: Parser.Parser
num)?
  " with " (colGt: optParam String "checkColGt" → Parser.Parser
colGt rintroPat: Parser.Category
rintroPat)* (" : " num: Parser.Parser
num)? : tactic: Parser.Category
tactic

macro_rules
  | `(tactic| congr $(depth: ?m.430
depth)? with $ps: ?m.423
ps* $[: $n: ?m.149 x✝
n]?) =>
    `(tactic| congr $(depth: ?m.430
depth)? <;> ext $ps: ?m.423
ps* $[: $n: ?m.149 x✝
n]?)

/--
Recursive core of `rcongr`. Calls `ext pats <;> congr` and then itself recursively,
unless `ext pats <;> congr` made no progress.
-/
partial def rcongrCore: MVarId → List (TSyntax `rcasesPat) → Array MVarId → TermElabM (Array MVarId)
rcongrCore (g: MVarId
g : MVarId: Type
MVarId) (pats: List (TSyntax `rcasesPat)
pats : List: Type ?u.3818 → Type ?u.3818
List (TSyntax: SyntaxNodeKinds → Type
TSyntax `rcasesPat: Name
`rcasesPat))
    (acc: Array MVarId
acc : Array: Type ?u.3902 → Type ?u.3902
Array MVarId: Type
MVarId) : TermElabM: Type → Type
TermElabM (Array: Type ?u.3905 → Type ?u.3905
Array MVarId: Type
MVarId) := do
  let mut acc: ?m.3939
acc := acc: Array MVarId
acc
  for (g: MVarId
g, qs: List (TSyntax `rcasesPat)
qs) in ← Ext.extCore: MVarId →
  List (TSyntax `rcasesPat) →
    optParam Nat 1000000 → optParam Bool true → TermElabM (Array (MVarId × List (TSyntax `rcasesPat)))
Ext.extCore g: MVarId
g pats: List (TSyntax `rcasesPat)
pats (failIfUnchanged := false: Bool
false) do
    let s: ?m.4191
s ← saveState: {s : outParam Type} → {m : Type → Type} → [self : MonadBacktrack s m] → m s
saveState
    let gs: ?m.4361
gs ← g: MVarId
g.congrN: MVarId → optParam Nat 1000000 → optParam Bool true → optParam Bool true → MetaM (List MVarId)
congrN 1000000: ?m.4245
1000000
    if ← not: Bool → Bool
not <$> g: MVarId
g.isAssigned: {m : Type → Type} → [inst : Monad m] → [inst : MonadMCtx m] → MVarId → m Bool
isAssigned <||> gs: ?m.4361
gs.anyM: {m : Type → Type ?u.4537} → [inst : Monad m] → {α : Type ?u.4536} → (α → m Bool) → List α → m Bool
anyM fun g': ?m.4568
g' => return (← g'.getType): ?m.4613
(← g': ?m.4568
g'(← g'.getType): ?m.4613
.getType: MVarId → MetaM Expr
getType(← g'.getType): ?m.4613
).eqv: Expr → Expr → Bool
eqv (← g.getType): ?m.4667
(← g: MVarId
g(← g.getType): ?m.4667
.getType: MVarId → MetaM Expr
getType(← g.getType): ?m.4667
) then
      s: ?m.4191
s.restore: Term.SavedState → optParam Bool false → TermElabM Unit
restore
      acc: ?m.4139
acc := acc: ?m.4139
acc.push: {α : Type ?u.4905} → Array α → α → Array α
push g: MVarId
g
    else
      for g: ?m.5149
g in gs: ?m.4361
gs do
        acc: ?m.5211
acc ← rcongrCore: MVarId → List (TSyntax `rcasesPat) → Array MVarId → TermElabM (Array MVarId)
rcongrCore g: ?m.5149
g qs: List (TSyntax `rcasesPat)
qs acc: ?m.5155
acc
  pure: {f : Type ?u.5636 → Type ?u.5635} → [self : Pure f] → {α : Type ?u.5636} → α → f α
pure acc: ?m.5633
acc

/--
Repeatedly apply `congr` and `ext`, using the given patterns as arguments for `ext`.

There are two ways this tactic stops:
* `congr` fails (makes no progress), after having already applied `ext`.
* `congr` canceled out the last usage of `ext`. In this case, the state is reverted to before
  the `congr` was applied.

For example, when the goal is
```
⊢ (λ x, f x + 3) '' s = (λ x, g x + 3) '' s
```
then `rcongr x` produces the goal
```
x : α ⊢ f x = g x
```
This gives the same result as `congr; ext x; congr`.

In contrast, `congr` would produce
```
⊢ (λ x, f x + 3) = (λ x, g x + 3)
```
and `congr with x` (or `congr; ext x`) would produce
```
x : α ⊢ f x + 3 = g x + 3
```
-/
elab (name := rcongr: ParserDescr
rcongr) "rcongr" ps: ?m.10592
ps:(ppSpace: Parser.Parser
ppSpace colGt: optParam String "checkColGt" → Parser.Parser
colGt rintroPat: Parser.Category
rintroPat)* : tactic: Parser.Category
tactic => do
  let gs: ?m.10853
gs ← rcongrCore: MVarId → List (TSyntax `rcasesPat) → Array MVarId → TermElabM (Array MVarId)
rcongrCore (← getMainGoal): ?m.10668
(← getMainGoal: TacticM MVarId
getMainGoal(← getMainGoal): ?m.10668
) (RCases.expandRIntroPats: Array (TSyntax `rintroPat) →
  optParam (Array (TSyntax `rcasesPat)) #[] → optParam (Option Term) none → Array (TSyntax `rcasesPat)
RCases.expandRIntroPats ps: ?m.10592
ps).toList: {α : Type ?u.10726} → Array α → List α
toList #[]: Array ?m.10740
#[]
  replaceMainGoal: List MVarId → TacticM Unit
replaceMainGoal gs: ?m.10853
gs.toList: {α : Type ?u.10864} → Array α → List α
toList