Is a `definition_wanted` keyword possible?

Stream: mathlib4

[Terence Tao]

We have a proof_wanted keyword for theorem statements that we wish to assert without affecting the proof environment; a proof_wanted claim cannot be used to prove other claims. This turned out to be important in an unanticipated use case of the PFR repository, in which a placeholder statement of the form theorem <theorem_name> : 0 = 1 := by sorry was used by an automated theorem prover to "prove" several other statements. Replacing this with proof_wanted <theorem_name> : 0 = 1 or proof_wanted <theorem_name> : (sorry:Prop) removes this exploit.

Is it possible to also have a definition_wanted keyword that is a placeholder for a definition, and allows the definition to be used in notation and in subsequent proof_wanted statements, but cannot be used in actual theorems? The existing technique def <definition name> : <definition type> := sorry has the unintended consequence that downstream theorems using that definition can be artificially solved using tactics such as rfl. Here is a concrete example from (an outdated version of) PFR, discovered by an automated theorem prover:

noncomputable def multiDist {m:ℕ} {Ω: Fin m → Type*} (hΩ: (i:Fin m) → MeasureSpace (Ω i))
  (X : (i : Fin m) → (Ω i) → G) : ℝ := sorry

@[inherit_doc multiDist] notation3:max "D[" X " ; " hΩ "]" => multiDist hΩ X

lemma multiDist_copy {m:ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i))
    (hΩ': (i : Fin m) → MeasureSpace (Ω' i)) (X : (i : Fin m) → (Ω i) → G) (X' : (i : Fin m) → (Ω' i) → G)
    (hident: ∀ i, IdentDistrib (X i) (X' i) (hΩ i).volume (hΩ' i).volume) :
    D[X ; hΩ] = D[X' ; hΩ'] := by
  rfl

Ideally, I would like instead to write

noncomputable definition_wanted multiDist {m:ℕ} {Ω: Fin m → Type*} (hΩ: (i:Fin m) → MeasureSpace (Ω i))
  (X : (i : Fin m) → (Ω i) → G) : ℝ

@[inherit_doc multiDist] notation3:max "D[" X " ; " hΩ "]" => multiDist hΩ X

proof_wanted multiDist_copy {m:ℕ} {Ω : Fin m → Type*} {Ω' : Fin m → Type*} (hΩ : (i : Fin m) → MeasureSpace (Ω i))
    (hΩ': (i : Fin m) → MeasureSpace (Ω' i)) (X : (i : Fin m) → (Ω i) → G) (X' : (i : Fin m) → (Ω' i) → G)
    (hident: ∀ i, IdentDistrib (X i) (X' i) (hΩ i).volume (hΩ' i).volume) :
    D[X ; hΩ] = D[X' ; hΩ']

but to not permit multiDist (or D[X; hΩ]) to be used in any actual theorem statements or proofs. Is such a syntax even possible in Lean?

[Kyle Miller]

One solution might be opaque def, which seals up the definition completely, but, unlike axiom, it still ensures you can't prove falsehoods since it requires that there exist some definition with the type, using the Nonempty typeclass.

In this case, making multiDist be opaque would prevent D[X ; hΩ] = D[X' ; hΩ'] from being solved by rfl.

[Eric Wieser]

So opaque def multiDist {m:ℕ} {Ω: Fin m → Type*} /- etc -/ : ℝ := sorry

[Eric Wieser]

Though this leaves a trap for an unsuspecting mathematician who fills in the sorry and doesn't understand why they can't prove anything about multiDist (answer: they must delete opaque)

[Terence Tao]

So this is why I propose a custom definition_wanted keyword, which could be as simple as an alias for opaque def ... := sorry, but which forces the mathematician filling in the sorry to replace that keyword with an actual def with non-sorry content (and presumably this mathematician would not also supply an opaque modifier).

[Gabriel Ebner]

A long time ago I wanted to change sorry so that every sorry is unique, which prevents this class of gotchas entirely. Maybe it's too much of a breaking change to do that in core, but you could always add new syntax for it, analogously to Type* vs. Type.

import Lean
open Lean Meta

elab "sorry*" : term <= expectedType => do
  let id := toExpr (← mkFreshUserName `sorry)
  let fvs := (← (← getLCtx).getFVars.mapM (getFVarLocalDecl ·))
    |>.toList.dropWhile (·.isImplementationDetail)
    |>.toArray.map (·.toExpr)
  let ty := mkForall `h .default (← mkEq id id)
    (← mkForallFVars fvs expectedType)
  return mkAppN (← mkSorry ty (synthetic := false))
    (#[← mkEqRefl id] ++ fvs)

def norm1 (x : Nat) : Nat := sorry*
def norm2 (x : Nat) : Nat := sorry*

example {x y} : norm1 x = norm1 y := rfl -- fails
example {x} : norm1 x = norm2 x := rfl -- fails

[Terence Tao]

One could perhaps implement both ideas: an (optional) more "secure" version sorry* of sorry, and make definition_wanted syntactic sugar for opaque def ... := sorry*. (One could also update other tactics such as stop to incorporate this version of sorry, as a precaution, even if I can't directly think of an exploit here.)

[Yaël Dillies]

Isn't opaque a bit too stringent? Assume Kevin wants to state that two groups are isomorphic and also state that such an isomorphism commutes with some other operations. I would expect he does something like

definition_wanted iso : G =~* G'

proof_wanted iso_comp_f : iso \comp f = g

But now he has to prove that G =~* G' is nonempty! That goes against the point.

[Adam Topaz]

The way proof_wanted works is that it creates an axiom, but inside a block that (by force) does not change the environment. To use a similar approach across multiple declarations like this, one would need to have a whole section that doesn't modify the environment. I don't know if we have anything that can be used to accomplish this. The function that's used for proof_wanted is Lean.withoutModifyingEnv.

[Adam Topaz]

one could imagine syntax roughly as follows:

throwaway section

definition_wanted foobar : Nat

axiom Baz : GroupCat

proof_wanted : False

end

[Adam Topaz]

But I also don't see how to ensure that definition_wanted and proof_wanted are only used in a throwaway section.

[Vincent Beffara]

Wait, wouldn't the point of throwaway section be to use plain old def and theorem inside?

[Ruben Van de Velde]

With what as body?

[Adam Topaz]

Ruben Van de Velde said:

With what as body?

sorry*

[Vincent Beffara]

With sorry if necessary, since there is no danger of spilling out?

[Adam Topaz]

yes, if we implement throwaway section, then you can do whatever you want in there.

[Adam Topaz]

Maybe it's much easier than I had envisioned:

import Lean
open Lean

elab "throwaway" cmds:command* "catch" : command => withoutModifyingEnv do
  for cmd in cmds do
    Elab.Command.elabCommand cmd

throwaway

axiom A : Nat

catch

[Damiano Testa]

I think that this may have some issues: for instance, you cannot define notation among the cmds:

throwaway

notation "ℕ" => Nat
/-- error: unknown identifier '«ℕ»' -/
#guard_msgs in
#check ℕ

catch

[Damiano Testa]

Maybe that is not a huge limitation, but "sequential parsing of commands" is not the same as "parsing a file".

[Damiano Testa]

(I knew about this, because of that).

[Adam Topaz]

I see. And looking at the other thread, there is no easy solution that would make this approach work.

[Kyle Miller]

It'd take a core change, but it seems like it would be possible to make a throwaway section ... end command, that has the same effect as Adam's command, but which would allow new syntaxes in the interim.

[Terence Tao]

On a slightly different note: it appears that linter.unusedVariables complains when a proof_wanted statement involves variables that are not used in the (non-existent) proof. Is there a way to disable this linter for proof_wanted statements by default?

[Kyle Miller]

@Terence Tao Turned out to be doable: batteries#997

[Yaël Dillies]

Taking note for the future: Don't open an issue, bother Kyle directly :laughing:

[Kyle Miller]

I tried out @Gabriel Ebner's proposal, but it turns out there's a gotcha when it comes to section variables. Likely you want to use sorry for definitions, and in that case sorry will include all section variables into the type of the definition automatically.

I'm experimenting in lean4#5757 with making sorries unique at least in the sense that each sorry that appears in the source is not defeq to any other, so for example (rfl : (sorry : Nat) = sorry) fails to typecheck. The norm1 x = norm1 y example is still a defeq, but at least the norm1 x = norm2 x one fails.

If we had a revert_all tactic, then one could implement Gabriel's sorry* as a macro for by revert_all; sorry

[Eric Wieser]

revert_all didn't make sense as a tactic with the pre-4.11.0 inclusion mechanism, right?

[Eric Wieser]

Am I now right in saying it is always safe in by blocks, or is it only after theorem statements that the context is frozen?

[Kyle Miller]

Just theorems

[Kyle Miller]

Update: we added unique sorrys to core Lean @Terence Tao. They will show up in a few weeks in the release candidate for the next version. #rss > Recent Commits to lean4:master @ 💬

It still takes a little bit of care to use it — this is not the context-capturing sorry that Gabriel proposed. Instead, it's a sorry that is different from any other sorry. For example, given

def x : ℝ := sorry
def y : ℝ := sorry

then x and y are not definitionally equal. No need for the opaque trick. (These also have a feature that if the sorry ever shows up in the Infoview, you can "go to definition" on them to see where they came from.)

To use it correctly, rather than

noncomputable def multiDist {m:ℕ} {Ω: Fin m → Type*} (hΩ: (i:Fin m) → MeasureSpace (Ω i))
  (X : (i : Fin m) → (Ω i) → G) : ℝ := sorry

you would write

noncomputable def multiDist : {m:ℕ} → {Ω: Fin m → Type*} → (hΩ: (i:Fin m) → MeasureSpace (Ω i)) →
  (X : (i : Fin m) → (Ω i) → G) → ℝ := sorry

The first form gives a sorry : ℝ that's unique to multiDist, so the gotcha is multiDist is a constant function. The second form makes multiDist a parameterized family of sorrys, so if the arguments are different the sorry is different, so to speak.

It should be possible to make a definition_wanted macro that does the transformation into the correct form.

Something that might also be helpful is this macro

macro "sorry " args:term:arg+ : term => do
  let ty ← args.foldrM (init := (← `(_))) (fun _ ty => `(_ → $ty))
  `((sorry : $ty) $args*)

to let you specify what the sorry is supposed to depend on.

For example,

noncomputable def multiDist {m:ℕ} {Ω: Fin m → Type*} (hΩ: (i:Fin m) → MeasureSpace (Ω i))
  (X : (i : Fin m) → (Ω i) → G) : ℝ := sorry m Ω hΩ X

This is a manual version of Gabriel's sorry*.

[Adam Topaz]

Will the last macro also be in core? If not, then we should probably add it to mathlib.

[Kim Morrison]

That last macro is not part of lean#5757, no.