Can a theorem ever have itself as a value?

Stream: lean4

[Thomas Murrills]

In diving into dsimp, I noticed that it doesn't handle wrapped constants properly:

theorem const_thm_internal : (or true false) = true := rfl
@[simp] theorem const_thm : (or true false) = true := const_thm_internal

example : (or true false) = true := by dsimp -- dsimp made no progress

-- same thing, but with an (unused) argument:
theorem const_thm_internal' (_ : Nat) : (or true false) = true := rfl
@[simp] theorem const_thm' : (or true false) = true := const_thm_internal' 0

example : (or true false) = true := by dsimp -- success

Whether a theorem is marked as dsimp-worthy is determined by the mutually recursive functions isRflProofCore (type proof : Expr) and isRflTheorem (declName : Name). isRflTheorem just gets the ConstantInfo of the declName theorem if it can, makes sure it's a .thmInfo, then feeds the .type and .value of the enclosed TheoremVal to isRflPRoofCore.

An easy fix would be to allow isRflProofCore to then check if that info.value is itself a constant, and, if so, pass it back to isRflTheorem. Currently, it demands that it's an application. This amounts to simply removing the condition proof.isApp && ... before proof.getAppFn.isConst.

My concern is that that could somehow loop. I'd expect (and hope) that looping in this way is impossible, but I'd also want to not introduce the possibility for nontermination even in edge cases or due to hacks/implementation details. Would such a change be safe?

Moreover, is there a reason that we shouldn't change this in the first place? Some case in which the wrapping theorem should not be used for dsimp even if the wrapped theorem should? I can't think of one, but maybe I'm just not coming up with it.

I imagine wrapped constants like this are relatively rare in practice, but I haven't checked.

[Timo Carlin-Burns]

If your code sees the same declaration values as #print, then it seems like self-referencing recursive declarations will already be translated to applications of WellFounded.fix. Example:

inductive MyFalse : Prop
| mk : MyFalse → MyFalse

-- theorem whose proof is an application of itself
theorem false_of_myFalse (h : MyFalse) : False :=
  false_of_myFalse <| let .mk h' := h; h'
termination_by false_of_myFalse h => h
decreasing_by sorry -- proof omitted

#print false_of_myFalse
-- theorem false_of_myFalse : MyFalse → False :=
--   WellFounded.fix (...)

[Thomas Murrills]

That's encouraging! My biggest fear is some kind of hack or implementation detail that keeps (or makes) it recursive for some reason.

[Mario Carneiro]

No, theorems cannot be recursive. (I know this since I recently implemented the kernel!) Definitions are typechecked in a context that does not contain them, unless they are marked as .partial or .unsafe (note, these are related but different from the partial and unsafe keywords you can actually write on a definition), and unsafe/partial theorems do not exist (they only support the .safe safety marking)

[Eric Wieser]

Making dsimp work for Iff.rfl went through just fine in Lean3 when I added that feature there, so I'd be surprised if there's any particularly troublesome obstacle here

[Eric Wieser]

(though indeed we never attempted to unwrap)

[Mario Carneiro]

I don't think unwrapping is necessary or desirable

[Mario Carneiro]

I think it is fine just to look for Iff.rfl or rfl as the proof. Don't make this more complicated than it has to be to address the existing issues

[Thomas Murrills]

I mean, this is a separate issue that doesn’t have to do with Iff at all, I just was explaining the context; original message now edited to remove unnecessary info.

The current infrastructure already unwraps, it just artificially prevents itself from doing so when the constant isn’t applied to anything by checking proof.isApp. I’m not adding anything there

[Thomas Murrills]

(As long as we’re on the same page as to what unwrapping means. I’m using it just to mean “recursively exposes constants in heads of Exprs”)

[Thomas Murrills]

To wrap this up: I think there might have been a misunderstanding here. This doesn't have anything to do with Iff; I'm not proposing a new unwrapping feature; and I think the edge case shown at the top should not happen. My inclination is to open a small issue and a draft PR, which consists of a 15-character deletion (plus a test)—but I don't want to proceed under apparent advice not to. :)

[Mario Carneiro]

I think it's fine (and important) to add iff to the existing handling without changing the other stuff. I don't think unwrapping is necessary but if the code is pre-existing then this is a separate matter

[Thomas Murrills]

Yes, this thread is 100% unrelated to handling Iff, and simp already unwraps. It just explicitly stops itself from doing so in the edge case at the top for some reason—maybe there's a good reason, but it could also be an oversight.

[Mario Carneiro]

maybe I don't understand what the thread (or proposed PR) is about then

[Thomas Murrills]

Current status quo: if a @[simp] theorem has a proof that's a constant applied to some arguments, and that constant is a rfl theorem, it gets used by dsimp. Example: (note that we are just manipulating bools for the sake of something to manipulate)

theorem const_thm_internal_with_arg (_ : Nat) : (or true false) = true := rfl
@[simp] theorem const_thm' : (or true false) = true := const_thm_internal_with_arg 0

example : (or true false) = true := by dsimp -- success

[Thomas Murrills]

However, if the proof of the simp theorem is a constant that doesn't have any arguments, it doesn't get used by dsimp.

[Thomas Murrills]

-- exactly the same but without the `Nat` argument
theorem const_thm_internal : (or true false) = true := rfl
@[simp] theorem const_thm : (or true false) = true := const_thm_internal

example : (or true false) = true := by dsimp -- dsimp made no progress

[Thomas Murrills]

This is because the check for whether something is a rfl theorem explicitly excludes this case:

if proof.isApp && proof.getAppFn.isConst then
  <unwrap proof.getAppFn and eventually recurse>

but it doesn't mention why it demands proof.isApp.

[Thomas Murrills]

The title of this thread is one part of the question: is there a good reason for the code being the way it is? For instance, maybe if we didn't check proof.isApp, some theorem would unwrap to itself when we recursed, and then the check would never terminate? Or can we just delete this part of the check?

[Thomas Murrills]

The proposed PR is just “delete proof.isApp && and see if that’s still fine”. It should make dsimp work in the case where it doesn’t (and not change its behavior otherwise).

[Mario Carneiro]

sgtm