forbid_axioms

Stream: lean4

[Johan Commelin]

Is it possible to have a Lean 4 command

#forbid_axioms My.Fancy.Constant My.Other.Axiom

at the top of some file, which makes sure that all the decls in that file can not depend on those axioms? (If they try to depend on the axioms, this should result in an error.)

It might be easier to have some linter at the bottom of the file, with errors reported at the line that invokes the linter. That would be a good start. But it would be really nice if errors are reported while writing the decl, at the line where a "forbidden" lemma is used.

[Ruben Van de Velde]

If it goes at the start, it might be good to make it section-scoped rather than file-scoped

[Mario Carneiro]

You might be able to hack that together with a "linter" that makes errors instead of warnings

[Mario Carneiro]

since linters get to spy on every command as they go by

[Mario Carneiro]

it won't catch decls created directly via addDecl though

[Mario Carneiro]

plus you have to reconstruct the declaration to check from the syntax, since you are just given the raw command syntax

[Eric Wieser]

#10954 seems relevant here

[Gabriel Ebner]

Mario Carneiro said:

it won't catch decls created directly via addDecl though

You can always do what whatsnew does and just compare the two environments. (Beware of the quadratic runtime though.)

[Johan Commelin]

How do I programmatically ask for the axioms of a certain decl?

[Johan Commelin]

Oooh cool! You can go-to-defn on #print axioms :bulb:

[Johan Commelin]

Here is my current broken attempt:

import Lean.Elab.Print
import Std.Tactic.Lint
import Mathlib.Tactic.RunCmd

namespace Lean

namespace Parser.Command
@[builtin_command_parser] def forbiddenAxioms    := leading_parser
  "#forbiddenAxioms " >> ident
end Parser.Command

namespace Elab.Command

private def forbiddenAxioms (bad : List Name) : CommandElabM Unit := do
  let env ← getEnv
  let decls ← liftCoreM Std.Tactic.Lint.getDeclsInCurrModule
  decls.forM fun n ↦
    let axs := ((((CollectAxioms.collect n).run env).run {}).2).axioms.toList
    let l := bad.filter fun a ↦ a ∈ axs
    if l.isEmpty then pure ()
    else logInfo m!"'{n}' depends on: {l}"

@[builtin_command_elab Parser.Command.forbiddenAxioms]
def elabForbiddenAxioms : CommandElab
  | `(#forbiddenAxioms%$tk $id) => withRef tk do -- <== ERROR: expected token
    let cs ← resolveGlobalConstWithInfos id
    cs.forM printAxiomsOf
  | _ => throwUnsupportedSyntax

end Elab.Command

end Lean

axiom LEM (P : Prop) : P ∨ ¬P

theorem test1 (P : Prop) : ¬P ∨ P :=
  (LEM P).elim .inr .inl

def test2 (P : Prop) : True := trivial

open Lean Elab Command in
run_cmd
  forbiddenAxioms [`LEM] -- prints: 'LEM' depends on [LEM], 'test1' depends on [LEM]

[Johan Commelin]

There is red squiggles under #forbiddenAxioms at the indicated line

[Mario Carneiro]

@[builtin_*] attributes should not be used outside lean core

[Mario Carneiro]

you should just use syntax

[Johan Commelin]

could you please tell me how to do just that?

[Mario Carneiro]

namespace Lean

open Elab Command
private def forbiddenAxioms (bad : List Name) : CommandElabM Unit := do
  let env ← getEnv
  let decls ← liftCoreM Std.Tactic.Lint.getDeclsInCurrModule
  decls.forM fun n ↦
    let axs := ((((CollectAxioms.collect n).run env).run {}).2).axioms.toList
    let l := bad.filter fun a ↦ a ∈ axs
    if l.isEmpty then pure ()
    else logInfo m!"'{n}' depends on: {l}"

open private printAxiomsOf from Lean.Elab.Print
elab tk:"#forbiddenAxioms " id:ident : command => do
  let cs ← resolveGlobalConstWithInfos id
  withRef tk <| cs.forM printAxiomsOf

end Lean

[Johan Commelin]

Ok, thanks, I'll try to take it from there

[Johan Commelin]

Result so far

import Lean.Elab.Print
import Std.Tactic.Lint

namespace Lean

def Parser.Command.forbiddenAxioms := leading_parser
  "#forbiddenAxioms " >> termParser

open Elab Command
private def forbiddenAxioms (bad : List Name) : CommandElabM Unit := do
  let env ← getEnv
  let decls ← liftCoreM Std.Tactic.Lint.getDeclsInCurrModule
  decls.forM fun n ↦
    let axs := ((((CollectAxioms.collect n).run env).run {}).2).axioms.toList
    let l := bad.filter fun a ↦ a ∈ axs
    if l.isEmpty then pure ()
    else logInfo m!"'{n}' depends on: {l}"

open private printAxiomsOf from Lean.Elab.Print
elab tk:"#forbiddenAxioms " ids:ident* : command => withRef tk do
  let ns ← ids.mapM resolveGlobalConstNoOverloadWithInfo
  withRef tk <| forbiddenAxioms ns.toList

end Lean

[Mario Carneiro]

you don't want the first def there, the elab already does everything

[Johan Commelin]

good point, thanks!