restricting axioms

Stream: lean4

[awalterschulze]

Is there a way to limit the axioms used. For example to prevent the use of law of excluded middle?

I want to prove decidability of a language: String -> Prop for denotations of my inductive type.
So basically I want to show that this is a DecidablePred and make sure via github's CI that I didn't use LEM by accident and make sure that I won't make the mistake in future as I update the code.

Currently I know how to use #print axioms decidableDenote and this prints the axioms [propext, Quot.sound]. I want to make sure that this list is not expanded upon by accident, by me or my collaborators, which sounds like a job for CI.

For reference here is my current proof: https://github.com/katydid/proofs/blob/main/Katydid/Regex/SimpleRegex.lean#L262

[Ruben Van de Velde]

I think someone (@Mario Carneiro ?) made this for lean 3, but I don't know if it exists for lean 4

[Edward van de Meent]

you could use #guard_msgs to ensure the message doesn't change?

[Edward van de Meent]

i believe that raises an error when the provided message doesn't match the one it catches?

[Henrik Böving]

Why do you want to exclude em for this? If you show DecidablePred for something you have to provide an executable algorithm as a decision procedure, unless that one is marked noncomputable its always executable. Whether the proof of correctness for the procedure uses em doesnt matter for being able to execute the procedure.

[Kyle Miller]

It should look something like

def decidableDenote (r: Regex α): DecidablePred (denote r) :=
  fun xs => decidable_of_iff _ (by rw [validate_commutes])

(Untested of course, but you shouldn't be using tactics to create DecidablePred instances. They tend to have issues with reduction.)

[Kyle Miller]

Like Henrik is asking, what's your specific use case for avoiding LEM?

[Asei Inoue]

here is a implementation of command which detect classical axiom

https://lean-ja.github.io/lean-by-example/Diagnostic/Print.html#%E8%88%9E%E5%8F%B0%E8%A3%8F

[Damiano Testa]

Since this shows up every once in a while and I wanted to have something similar to grade my module, here is a linter that flags uses of Classical.choice.

import Lean.Util.CollectAxioms
import Mathlib.Tactic.DeclarationNames

/-!
#  The "detectClassical" linter

The "detectClassical" linter emits a warning on declarations that depend on the `Classical.choice`
axiom.
-/

open Lean Elab Command

namespace Mathlib.Linter

/--
The "detectClassical" linter emits a warning on declarations that depend on the `Classical.choice`
axiom.
-/
register_option linter.detectClassical : Bool := {
  defValue := true
  descr := "enable the detectClassical linter"
}

/--
The `linter.verbose.detectClassical` option is a flag to make the `detectClassical` linter emit
a confirmation on declarations that depend *not* on the `Classical.choice` axiom.
-/
register_option linter.verbose.detectClassical : Bool := {
  defValue := false
  descr := "enable the verbose setting for the detectClassical linter"
}

namespace DetectClassical

@[inherit_doc Mathlib.Linter.linter.detectClassical]
def detectClassicalLinter : Linter where run := withSetOptionIn fun stx ↦ do
  unless Linter.getLinterValue linter.detectClassical (← getOptions) do
    return
  if (← get).messages.hasErrors then
    return
  let nms := (← getNamesFrom (stx.getPos?.getD default)).filter (! ·.getId.isInternal)
  let verbose? := Linter.getLinterValue linter.verbose.detectClassical (← getOptions)
  for constStx in nms do
    let constName := constStx.getId
    let axioms ← collectAxioms constName
    if axioms.isEmpty then
      if verbose? then
        logInfoAt constStx m!"'{constName}' does not depend on any axioms"
      return
    if !axioms.contains `Classical.choice then
      if verbose? then
        logInfoAt constStx
          m!"'{constName}' is non-classical and depends on axioms:\n{axioms.toList}"
    else
      Linter.logLint linter.detectClassical constStx
        m!"'{constName}' depends on 'Classical.choice'.\n\nAll axioms: {axioms.toList}\n"

initialize addLinter detectClassicalLinter

end DetectClassical

end Mathlib.Linter

[Damiano Testa]

You can configure it to emit information on all declarations, confirming that they do not depend on any axiom/do not depend on Classical.choice, using set_option linter.verbose.detectClassical true.

[Damiano Testa]

By default, it will only emit a warning on declarations that depend on Classical.choice.

[Kevin Buzzard]

Since this shows up every once in a while and I wanted to have something similar to grade my module, here is a linter that flags uses of Classical.choice.

You don't allow AC in your module??

[Damiano Testa]

I want to know what depends on sorry, but the logic of the linter is very similar!

[Damiano Testa]

Instead of checking Classical.choice, I use sorryAx.

[Kevin Buzzard]

I allow sorrys in my students' projects, but I usually try and either prove or disprove them when I'm marking them; it would be great if you had a linter for figuring out whether they're true or false but this might be quite a tough challenge.

[Damiano Testa]

I do the same, but, when I cannot prove the sorries, then I want to check the extent of the dependence on them.

[Damiano Testa]

So, the sorryLinter is not required to be silent on successful projects: it is just a diagnostic that I use to see where some issues might be.

[Damiano Testa]

With respect to autofiguring out true or false: if the lemmas are in scope for plausible, you could use that. Of course, in general it is hopeless.

[awalterschulze]

Damiano Testa said:

Since this shows up every once in a while and I wanted to have something similar to grade my module, here is a linter that flags uses of Classical.choice.

import Lean.Util.CollectAxioms
import Mathlib.Tactic.DeclarationNames

/-!
#  The "detectClassical" linter

The "detectClassical" linter emits a warning on declarations that depend on the `Classical.choice`
axiom.
-/

open Lean Elab Command

namespace Mathlib.Linter

/--
The "detectClassical" linter emits a warning on declarations that depend on the `Classical.choice`
axiom.
-/
register_option linter.detectClassical : Bool := {
  defValue := true
  descr := "enable the detectClassical linter"
}

/--
The `linter.verbose.detectClassical` option is a flag to make the `detectClassical` linter emit
a confirmation on declarations that depend *not* on the `Classical.choice` axiom.
-/
register_option linter.verbose.detectClassical : Bool := {
  defValue := false
  descr := "enable the verbose setting for the detectClassical linter"
}

namespace DetectClassical

@[inherit_doc Mathlib.Linter.linter.detectClassical]
def detectClassicalLinter : Linter where run := withSetOptionIn fun stx ↦ do
  unless Linter.getLinterValue linter.detectClassical (← getOptions) do
    return
  if (← get).messages.hasErrors then
    return
  let nms := (← getNamesFrom (stx.getPos?.getD default)).filter (! ·.getId.isInternal)
  let verbose? := Linter.getLinterValue linter.verbose.detectClassical (← getOptions)
  for constStx in nms do
    let constName := constStx.getId
    let axioms ← collectAxioms constName
    if axioms.isEmpty then
      if verbose? then
        logInfoAt constStx m!"'{constName}' does not depend on any axioms"
      return
    if !axioms.contains `Classical.choice then
      if verbose? then
        logInfoAt constStx
          m!"'{constName}' is non-classical and depends on axioms:\n{axioms.toList}"
    else
      Linter.logLint linter.detectClassical constStx
        m!"'{constName}' depends on 'Classical.choice'.\n\nAll axioms: {axioms.toList}\n"

initialize addLinter detectClassicalLinter

end DetectClassical

end Mathlib.Linter

Thank you, this works quite well:
https://github.com/katydid/regex-deriv-lean/pull/134

It finds uses of Classical.choice
and there are many more than I thought there would be

[awalterschulze]

Asei Inoue said:

here is a implementation of command which detect classical axiom

https://lean-ja.github.io/lean-by-example/Diagnostic/Print.html#%E8%88%9E%E5%8F%B0%E8%A3%8F

I tried this, but Command was an unknown import for some reason

[Aaron Liu]

Try import Lean

[awalterschulze]

Edward van de Meent said:

you could use #guard_msgs to ensure the message doesn't change?

I do not know how to use gaurd_msgs with print axioms, an example would be very helpful

[awalterschulze]

Henrik Böving said:

Why do you want to exclude em for this? If you show DecidablePred for something you have to provide an executable algorithm as a decision procedure, unless that one is marked noncomputable its always executable. Whether the proof of correctness for the procedure uses em doesnt matter for being able to execute the procedure.

I was to state in a paper that the property is decidable. Maybe I am a little over perfectionist in this case and it being executable is enough, but I am not sure.

[awalterschulze]

Kyle Miller said:

It should look something like

def decidableDenote (r: Regex α): DecidablePred (denote r) :=
  fun xs => decidable_of_iff _ (by rw [validate_commutes])

(Untested of course, but you shouldn't be using tactics to create DecidablePred instances. They tend to have issues with reduction.)

I tried it, but unfortunately it doesn't work.
Also was wondering about not being allowed to use tactics to create DecidablePred instances.

1. Shouldn't I be warned in some way about this?
2. Is it okay that validate_commutes uses tactics?
3. How is it possible to do this correctly and know that it is correct?

[awalterschulze]

Kyle Miller said:

Like Henrik is asking, what's your specific use case for avoiding LEM?

I want to say in a paper that the language has been proven to be decidable. I assume this is the way to do it, but maybe I am wrong?

[Henrik Böving]

If your proof of a decision procedure is using em you have still shown that the thing you are proving is decidable, there are different combinations possible here:

• derive a decision procedure using em and verify it (with or without em) would not be decidability in the usual sense
• derive a decision procedure without em and verify it without em is decidability and the proof for its correctness is constructive
• derive a decision procedure without em and verify it with em is decidability and the proof for its correctness is non constructive

Regardless the last case still shows decidability of a predicate.

[Asei Inoue]

@Damiano Testa

what this line does in your detectClassical linter?

  if (← get).messages.hasErrors then
    return

[Damiano Testa]

It makes sure that the linter says nothing if the declaration contains errors.

[Damiano Testa]

It is fairly standard for linters to ignore commands that have errors.

[Damiano Testa]

In particular, in this case, if the declaration contains errors, it likely will not have added anything to the environment, so there would be nothing to check for axioms anyway.

[Asei Inoue]

thanks!

[awalterschulze]

Henrik Böving said:

If your prove of a decision procedure is using em you have still shown that the thing you are proving is decidable, there are different combinations possible here:

• derive a decision procedure using em and verify it (with or without em) would not be decidability in the usual sense
• derive a decision procedure without em and verify it without em is decidability and the proof for its correctness is constructive
• derive a decision procedure without em and verify it with em is decidability and the proof for its correctness is non constructive

Regardless the last case still shows decidability of a predicate.

Thank you this is very helpful
Let me just do a triple check that I understand correctly.
Here is a minimal example that I wonder if it is true in general:

-- Step 1: define some language

inductive Regex: Type where ...

def Lang: Type := String -> Prop

def denote (r: Regex): Lang := ...

-- Step 2: define a matching function

def match (r: Regex) (s: String): bool := ...
  -- matching r is decidable, since it returns a bool and is computable (does not have noncomputable tag)

-- Step 3: prove that the matching function is correct

theorem commutes (r: Regex) (s: String): (execute r s = true) = (denote r s) := by
  -- feel free to use EM and tactics
  -- using EM just means the proof is not constructive, but doesn't affect decidability

-- decidability of r is proven via match, the next step is really just a formality and not sure if it is really needed.

-- Step 4: prove decidability

def decidable (r: Regex): DecidablePred (denote r) := by
  -- proven via commutes
  -- feel free to use more EM and tactics

-- decidability of r is proven, but the proof is not constructive, which is fine

[Kyle Miller]

For step 4, a clarification: you don't prove decidability, you provide a decision procedure. If you do make a mistake and accidentally use EM in a computationally relevant way, you'll notice because Lean will say the definition must be noncomputable. If it's not noncomputable, it's fine.

Just like any definition, you don't generally want to define it with tactics. Here's how it could be defined, modulo bugs from typing it directly into Zulip:

def decidable (r: Regex): DecidablePred (denote r) :=
  fun _ => decidable_of_decidable_of_eq _ _

This causes execute to be used to evaluate denote.

[awalterschulze]

Thank you that worked perfectly https://github.com/katydid/regex-deriv-lean/commit/b8acdfd4ecce5a1c7148b3a53f23a12b7b0c0069

So just to conclude and check if I understood correctly: it sounds like it is generally frowned upon to use tactics in definitions, but technically it would not have made the proof that the predicate is decidable invalid, if tactics were used.