Splitting conjunction / disjunction in hypotheses

Stream: lean4

[Marx]

Hey guys,
I am currently trying to write a custom tactic which splits all conjunctions and disjuncitons from a certain hypotheses into its modular parts.
My approach was to search for the desired hypotheses, create a RCases pattern (e.g. (( _ | ( (⟨ _, _ ⟩))))), parse this and replace the main goal with its context (simillar to rcases ... with ...).
While doing so, I encountered several problems:

1. I can't use Lean.Elab.Tactic.RCases.RCasesPatt.parse
2. I am not sure, what the tgtsshould look like

To solve 1., i copy pasted the required functions and definitions into my scope.
But I think i messed up either with this "implementation" of the RCasesPatt.parse or the tgts array.

Here is what I have so far:

import Lean
open Lean Elab Parser Tactic RCases

def RCasesPatt.alts' (ref : Syntax) : List/-Σ-/ RCasesPatt → RCasesPatt
  | [p] => p
  | ps  => RCasesPatt.alts ref ps

/-- Parses a `Syntax` into the `RCasesPatt` type used by the `RCases` tactic. -/
partial def RCasesPatt.parse (stx : Syntax) : MetaM RCasesPatt :=
  match stx with
  | `(rcasesPatMed| $ps:rcasesPat|*) => return RCasesPatt.alts' stx (← ps.getElems.toList.mapM (parse ·.raw))
  | `(rcasesPatLo| $pat:rcasesPatMed : $t:term) => return .typed stx (← parse pat) t
  | `(rcasesPatLo| $pat:rcasesPatMed) => parse pat
  | `(rcasesPat| _) => return .one stx `_
  | `(rcasesPat| $h:ident) => return .one h h.getId
  | `(rcasesPat| -) => return .clear stx
  | `(rcasesPat| @$pat) => return .explicit stx (← parse pat)
  | `(rcasesPat| ⟨$ps,*⟩) => return .tuple stx (← ps.getElems.toList.mapM (parse ·.raw))
  | `(rcasesPat| ($pat)) => return .paren stx (← parse pat)
  | _ => throwUnsupportedSyntax



partial def split_ands (declType : Expr) : MetaM (TSyntax `rcasesPat) := do
  let e ← Meta.whnf declType
  if e.isAppOfArity `Or 2 then
    let left ← split_ands (←Meta.whnf <| e.getArg! 0)
    let right ← split_ands (←Meta.whnf <| e.getArg! 1)
    return (←`(rcasesPat | ($left | $right)))
  if e.isAppOfArity `And 2 then
    let left ← split_ands (←Meta.whnf <| e.getArg! 0)
    let right ← split_ands (←Meta.whnf <| e.getArg! 1)
    return (←`(rcasesPat | ⟨$left , $right⟩))
  if e.isFVar then
    return (←`(rcasesPat | _))
  throwUnsupportedSyntax


elab "split_ands_in_pre" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    let ctx ← Lean.MonadLCtx.getLCtx
    let option_matching_expr ← ctx.findDeclM? fun decl: Lean.LocalDecl => do
      if decl.userName == `user_precondition then
        let type := decl.type
        let pat ← split_ands type
        let pat' ← RCasesPatt.parse pat
        return some pat'
      return none
    match option_matching_expr with
    | some e => goal.withContext do replaceMainGoal (← RCases.rcases
        #[(none, (←`(`user_precondition)))] e goal)
    | none =>
      Lean.Meta.throwTacticEx `custom_assump_2 goal
        (m!"failure")



example : ∀ (A B C D : Prop), ((D ∨ (A ∧ B) ∨ D ∧ A) ∨ A ∧ (C ∨ (D ∧ C))) → C := by
  intros A B C D
  intros user_precondition
  split_ands_in_pre -- not sure why this is happening here, ideally it should do the same as
  --   rcases user_precondition with (( _ | ( (⟨ _, _ ⟩)| (⟨ _, _ ⟩) )) | ⟨ _, ( ( _ | ⟨ _, _ ⟩ ) )⟩ )
  repeat sorry

[Marx]

After working through each step and recreating the rcases tactic, I was able to identify the source of the issue. The problem was with the tgts array: using (none, (← user_precondition)) constructed a tuple like #[(none, (Term.quotedName (name "user_precondition")))], when what was actually required was #[(none, 'user_precondition)]. To resolve this, I modified the tactic to accept the hypothesis name as an ident, and then used that identifier directly to build the array. With this change, everything now works as expected.
This is what the code now looks like:

import Lean
import Batteries.Data.UInt

open Lean Elab Parser Tactic RCases

def RCasesPatt.alts' (ref : Syntax) : List/-Σ-/ RCasesPatt → RCasesPatt
  | [p] => p
  | ps  => RCasesPatt.alts ref ps

/-- Parses a `Syntax` into the `RCasesPatt` type used by the `RCases` tactic. -/
partial def RCasesPatt.parse (stx : Syntax) : MetaM RCasesPatt :=
  match stx with
  | `(rcasesPatMed| $ps:rcasesPat|*) => return RCasesPatt.alts' stx (← ps.getElems.toList.mapM (parse ·.raw))
  | `(rcasesPatLo| $pat:rcasesPatMed : $t:term) => return .typed stx (← parse pat) t
  | `(rcasesPatLo| $pat:rcasesPatMed) => parse pat
  | `(rcasesPat| _) => return .one stx `_
  | `(rcasesPat| $h:ident) => return .one h h.getId
  | `(rcasesPat| -) => return .clear stx
  | `(rcasesPat| @$pat) => return .explicit stx (← parse pat)
  | `(rcasesPat| ⟨$ps,*⟩) => return .tuple stx (← ps.getElems.toList.mapM (parse ·.raw))
  | `(rcasesPat| ($pat)) => return .paren stx (← parse pat)
  | _ => throwUnsupportedSyntax



partial def split_ands (declType : Expr) : MetaM (TSyntax `rcasesPat) := do
  let e ← Meta.whnf declType
  if e.isAppOfArity `Or 2 then
    let left ← split_ands (←Meta.whnf <| e.getArg! 0)
    let right ← split_ands (←Meta.whnf <| e.getArg! 1)
    return (←`(rcasesPat | ($left | $right)))
  if e.isAppOfArity `And 2 then
    let left ← split_ands (←Meta.whnf <| e.getArg! 0)
    let right ← split_ands (←Meta.whnf <| e.getArg! 1)
    return (←`(rcasesPat | ⟨$left , $right⟩))
  if e.isFVar then
    return (←`(rcasesPat | _))
  throwUnsupportedSyntax


elab "split_ands_in_pre" " in " h:ident : tactic => do
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    let ctx ← Lean.MonadLCtx.getLCtx
    let option_matching_expr ← ctx.findDeclM? fun decl: Lean.LocalDecl => do
      if decl.userName == h.getId then
        let type := decl.type
        let pat ← split_ands type
        let pat' ← RCasesPatt.parse pat
        return some pat'
      return none

    match option_matching_expr with
    | some e =>
      let tgts : Array (Option Ident × Syntax) := #[(none, h)]
      let g ← getMainGoal
      g.withContext do replaceMainGoal (← RCases.rcases tgts e g)
    | none =>
      Lean.Meta.throwTacticEx `custom_assump_2 goal
        (m!"failure")

example : ∀ (A B C: Prop), (A ∧ C) ∨ (B ∧ C) → C:= by
  intros A B C
  intros user_precondition
  split_ands_in_pre in user_precondition
  repeat assumption