lean4 feat: error on non-rfl dsimp args

This PR implements a TODO for throwing an error on dsimp arguments which aren't proofs by reflexivity. I don't know exactly what resolveSimpIdTheorem? does, so there might be some cases which slip through - but I think this implementation should at least not produce false positives.

Dec 18 '23 02:12 marcusrossel

❗ Mathlib CI will not be attempted unless you rebase your PR onto the 'nightly' branch. (2023-12-18 02:36:08)
💥 Mathlib branch lean-pr-testing-3087 build failed against this PR. (2023-12-21 23:20:09) View Log
💥 Mathlib branch lean-pr-testing-3087 build failed against this PR. (2023-12-21 23:40:58) View Log

Dec 18 '23 02:12 leanprover-community-mathlib4-bot

I've rebased so that CI can test Mathlib against this PR.

Dec 21 '23 22:12 kim-em

@semorrison I have a fix for the Mathlib breakage lying around locally. Could I please have permission to push to the corresponding Mathlib branch?

Dec 22 '23 02:12 marcusrossel

Does it make sense to fix #2678 first before removing all such lemmas from mathlib dsimp calls?

Dec 24 '23 06:12 eric-wieser

Does it make sense to fix #2678 first before removing all such lemmas from mathlib dsimp calls?

I think that's not necessary. Fixing Mathlib's dsimp calls amounted to simply removing non-rfl arguments - no other adjustments required. And I'm guessing an implementation of #2678 would add the check for Iff.rfl in isRflProof, which is precisely the function used in this PR.

Dec 24 '23 13:12 marcusrossel

My point is that if we force mathlib to remove the non-rfl lemmas, then we end up removing all the Iff.rfl lemmas that are supposed to work in the first place. If we fix Iff.rfl first, then we don't end up removing things that in the long run we actually want to keep.

A compromise would be to have this warning only reject non-rfl non-Iff.rfl proofs, even though for now the latter don't actually work. That way we don't incentivize removing them prematurely from mathlib.

Dec 24 '23 14:12 eric-wieser

Ah ok, then it seems I don't understand the following point yet: What's the benefit of keeping dsimp arguments (the Iff.rfl arguments) which aren't actually necessary for the proof to go through? I've noticed that non-terminal dsimps are being used in Mathlib, so is the benefit somehow related to resilience?

Dec 24 '23 22:12 marcusrossel

The Iff.rfl lemmas in dsimp in mathlib are most likely left over from porting lean 3 code, where they actually worked correctly. As a result, the proofs that follow those dsimps will likely end up being longer or messier than necessary as a workaround.

Leaving the Iff.rfl lemmas in place means that when we fix dsimp to accept them, the old proof will start working again and CI will encourage us to remove any workarounds later in the proof (resulting in simpler proofs).

Dec 25 '23 05:12 eric-wieser

the proofs that follow those dsimps will likely end up being longer or messier than necessary as a workaround.

I just compared the proofs which are affected by this PR to the corresponding proofs in mathlib3. All the proofs are identical, so this shouldn't be an issue. In fact, it seems that mathlib4 doesn't currently contain any calls to dsimp which have a proof by Iff.rfl as argument except for Set.mem_setOf.

Here are the changes that would be required: https://github.com/marcusrossel/mathlib4/commit/3d3c05f78860077b090d491b1a0b202bba17bc0f

Dec 25 '23 23:12 marcusrossel

@marcusrossel, apologies for the long delay, but I just gave your write access at mathlib4!

Jan 08 '24 07:01 kim-em

@marcusrossel let me know if you need help with testing Mathlib here. Your changes need to go on the lean-pr-testing-3087 branch of Mathlib to be reflected here.

Jan 15 '24 01:01 kim-em

@semorrison thanks! I'm just waiting on #2678 to be resolved before continuing with this PR. Is there some way I can indicate that this PR is waiting for another PR/issue?

Jan 15 '24 07:01 marcusrossel

@marcusrossel, we should check in with @thorimur re: #2678, I guess; it's unclear if it will progress.

Jan 15 '24 13:01 kim-em

To be clear on my stance; I don't think we need to wait for https://github.com/leanprover/lean4/issues/2678; I just think we should be conservative with the error message and only emit it on things that would still not be accepted after #2678 goes in; if not invalidLemma.isIffRflProof then emitWarning or similar.

Jan 15 '24 14:01 eric-wieser

@eric-wieser Ok, then the question remains how to check for Iff-rfl proofs. Do you think adjusting isRflProof as follows would be a good idea? It takes approach for checking Iff-rfl proofs from #2679 and makes it optional via a flag:

mutual
  partial def isRflProofCore (type : Expr) (proof : Expr) (allowIff : Bool) : CoreM Bool := do
    match type with
    | .forallE _ _ type _ =>
      if let .lam _ _ proof _ := proof then
        isRflProofCore type proof allowIff
      else
        return false
    | _ => 
      if type.isAppOfArity ``Eq 3 then 
        checkEq type proof <||> (return allowIff) <&&> checkIff type proof   
      else if allowIff && type.isAppOfArity ``Iff 2 then
        checkIff type proof
      else
        return false
  where 
    checkEq (type : Expr) (proof : Expr) : CoreM Bool :=
      if proof.isAppOfArity ``Eq.refl 2 || proof.isAppOfArity ``rfl 2 then
        return true
      else if proof.isAppOfArity ``Eq.symm 4 then
        -- `Eq.symm` of rfl theorem is a rfl theorem
        isRflProofCore type proof.appArg! allowIff -- small hack: we don't need to set the exact type
      else if proof.getAppFn.isConst then
        -- The application of a `rfl` theorem is a `rfl` theorem
        -- A constant which is a `rfl` theorem is a `rfl` theorem
        isRflTheorem proof.getAppFn.constName! allowIff
      else
        return false
    checkIff (type : Expr) (proof : Expr) : CoreM Bool :=
      if proof.isAppOfArity ``Iff.refl 1 || proof.isAppOfArity ``Iff.rfl 1 then
        return true
      else if proof.isAppOfArity ``Iff.symm 3 then
        -- `Iff.symm` of rfl theorem is a rfl theorem
        isRflProofCore type proof.appArg! allowIff -- small hack: we don't need to set the exact type
      else if proof.isAppOfArity ``propext 3 then
        -- `propext` is applied to `Iff` proofs during preprocessing
        if let some n := proof.appArg!.constName? then
          -- Check if the proof of `a ↔ b` is a `rfl` theorem.
          isRflTheorem n allowIff
        else
          -- small hack: we don't need the exact type: `type` is `a = b`, and `proof.appArg!` has
          -- type `a ↔ b`. Both `a = b` and `a ↔ b` behave the same way in this function.
          isRflProofCore type proof.appArg! allowIff
      else if proof.getAppFn.isConst then
        -- The application of a `rfl` theorem is a `rfl` theorem
        -- A constant which is a `rfl` theorem is a `rfl` theorem
        isRflTheorem proof.getAppFn.constName! allowIff
      else
        return false

  partial def isRflTheorem (declName : Name) (allowIff := false) : CoreM Bool := do
    let .thmInfo info ← getConstInfo declName | return false
    isRflProofCore info.type info.value allowIff
end

def isRflProof (proof : Expr) (allowIff := false) : MetaM Bool := do
  if let .const declName .. := proof then
    isRflTheorem declName allowIff
  else
    isRflProofCore (← inferType proof) proof allowIff

Then all current isRflProof and isRflTheorem calls remain unaffected, while I could use isRflProof (allowsIff := true) for this PR.

Jan 18 '24 16:01 marcusrossel