Make this command more concise.

Stream: lean4

[Asei Inoue]

I have written a command to assert theorem does not depend on Classical.choice.

Can this command be made more concise? elab or elab_rules command is useful for this?

import Lean

open Lean Elab Command

private def detectClassicalOf (constName : Name) : CommandElabM Unit := do
  let axioms ← collectAxioms constName
  if axioms.isEmpty then
    logInfo m!"'{constName}' does not depend on any axioms"
  else
    let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm
    if caxes.isEmpty then
      logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}"
    else
      throwError m!"'{constName}' depends on classical axioms: {caxes.toList}"

syntax (name:=detectClassical) "#detect_classical " ident : command

@[command_elab «detectClassical»] def elabDetectClassical : CommandElab
  | `(#detect_classical%$tk $id) => withRef tk do
    let cs ← liftCoreM <| realizeGlobalConstWithInfos id
    cs.forM detectClassicalOf
  | _ => throwUnsupportedSyntax

/-- info: 'Nat.add_zero' does not depend on any axioms -/
#guard_msgs in
  #detect_classical Nat.add_zero

/-- info: 'Nat.div_add_mod' is non-classical and depends on axioms: [propext] -/
#guard_msgs in
  #detect_classical Nat.div_add_mod

/-- info: 'Nat.log2' is non-classical and depends on axioms: [propext] -/
#guard_msgs in
  #detect_classical Nat.log2

[Eric Wieser]

In Lean3 we had an attribute-based implementation, !3#10954

[Asei Inoue]

@Eric Wieser it sounds nice. why mathlib4 doesn't have such an attribute?

[Asei Inoue]

This is more concise veresion.

import Lean

open Lean Elab Command

elab "#detect_classical " id:ident : command => do
  let constName ← liftCoreM <| realizeGlobalConstNoOverload id
  let axioms ← collectAxioms constName
  if axioms.isEmpty then
    logInfo m!"'{constName}' does not depend on any axioms"
    return ()

  let caxes := axioms.filter fun nm => Name.isPrefixOf `Classical nm
  if caxes.isEmpty then
    logInfo m!"'{constName}' is non-classical and depends on axioms: {axioms.toList}"
  else
    throwError m!"'{constName}' depends on classical axioms: {caxes.toList}"

/-- info: 'Nat.add_zero' does not depend on any axioms -/
#guard_msgs in
  #detect_classical Nat.add_zero

/-- info: 'Nat.div_add_mod' is non-classical and depends on axioms: [propext] -/
#guard_msgs in
  #detect_classical Nat.div_add_mod

/-- info: 'Nat.log2' is non-classical and depends on axioms: [propext] -/
#guard_msgs in
  #detect_classical Nat.log2

[Mario Carneiro]

Asei Inoue said:

Eric Wieser it sounds nice. why mathlib4 doesn't have such an attribute?

I wrote a version of this command, but it wasn't useful at the time because lots and lots of things were unnecessarily classical. I'm pretty sure this is even more true now than then

[Asei Inoue]

Can we gradually erase unnecessarily used classical logic?

[Mario Carneiro]

I have no idea, last time I tried it I got a lot of irrationally strong pushback and I don't know if the mood has changed