Using rename_i with try

Stream: lean4

[LambdaDuck (Andreas Källberg)]

When I try using try rename_i x when no inaccessible variables are present, I still get a "too many variable names provided" error despite using try. Is there a workaround?

I'm probably trying to solve the wrong problem though. My actual goal is to get access to all the variables generated from the cases tactic without having to manually mention each case. Is there a version of the macro that's equivalent to intro h ; cases h ; all_goals revert <all the variables introduced by cases?

[Kyle Miller]

This is a bug in rename_i. It's merely logging an error, but not aborting execution, so try doesn't catch it and backtrack. Would you mind reporting it in the Lean 4 github?

[Kyle Miller]

For your second question, I suppose this is where a Coq-style ssreflect-style sublanguage could come in handy. In ssreflect, there is a focus on manipulating the target rather than introducing local variables.

If you know what the type is (say it's T) you could do apply T.recOn rather than doing intro first. (Never mind, I thought this would work, but in a test it didn't.)

[LambdaDuck (Andreas Källberg)]

I found that using the variable within the try block so that the other tactic can report an error did work, which seems consistent with your description. For example, I could do this to revert all inaccessible variables into arguments for the goal: all_goals repeat rename_i h; revert h

[Kyle Miller]

Here's a sketch of a tactic (cases_on) that does cases on the first parameter. It doesn't fully implement what cases does though (like it doesn't pick up on custom eliminators). It's possible to do this by calling out to the cases tactic, or cases tactic internals, but I was just experimenting and figured I'd paste it here.

import Lean

open Lean Elab Tactic Meta in
elab "cases_on" : tactic => do
  let g0 ← popMainGoal
  g0.withContext do
    let (x, g) ← g0.intro1
    g.withContext do
      let dom ← x.getType
      matchConstInduct dom.getAppFn
        (fun _ => throwError "Expecting type to be an inductive type, not{indentExpr dom}")
        (fun ival _ => do
          let c ← mkConstWithFreshMVarLevels (mkCasesOnName ival.name)
          -- use the g0 context so that `x` doesn't appear in any premises
          let (args, _) ← g0.withContext do forallMetaTelescope (← inferType c)
          let params := dom.getAppArgs
          for i in [0:params.size] do
            unless ← isDefEq args[i]! params[i]! do
              throwError "(internal error) failed to assign inductive type parameter"
          let mut args := args
          -- Set major premise (replace the metavariable)
          args := args.set! (ival.numParams + 1) (.fvar x)
          -- Set remaining arguments as synthetic opaque so they can be tactic goals
          let minors := args[ival.numParams + 2 : args.size].toArray.toList.map (·.mvarId!)
          for m in minors do
            m.setKind .syntheticOpaque
          -- Construct recursor application, motive still needs solving-for
          let casesOn := mkAppN c args
          let gs ← g.apply casesOn
          pushGoals gs)

example : (xs : List Nat) → 0 ≤ xs.length := by
  cases_on
  /-
  case nil
  ⊢ 0 ≤ [].length

  case cons
  ⊢ ∀ (head : Nat) (tail : List Nat), 0 ≤ (head :: tail).length
  -/