Asking for simplifications in proofs/type-checking

Stream: lean4

[Siddhartha Gadgil]

When updating the nightly build by a month (in sync with mathlib4), some of my code no longer typechecked. A somewhat minimized version of what causes the problem is as in the example below:

def eg1IsFalse : Bool := eg1Soln.isSat
#eval eg1IsFalse                                                -- gives false
example : eg1IsFalse = false := rfl              -- gives an error

Is there some way I can ask eg1False to be simplified when making the definition, or some tactic replacing rfl where we reduce to normal form?

Thanks.

[Yakov Pechersky]

Let's say your definition was originally 1 + 0, your eval gave 1, and your example 1 + 0 = 1 := rfl worked. But then the definition of addition changed (such that zero on the left was the defintional equality), so your original rfl proof would no longer work.

[Yakov Pechersky]

My understanding is that rfl is the proof only if #reduce would have given you false.

[Siddhartha Gadgil]

I just checked: #reduce eg1IsFalse does indeed give false.
In my case eg1Soln is complicated and involves propositions in its constructions, so I am guessing that some optimization is stopping reduction, and I should force it by an annotation or tactic.

[Siddhartha Gadgil]

I have been checking further what simplifications are made. Here are some experiments:

#print eg1IsFalse
#print eg1Soln

give as info

def eg1IsFalse : Bool :=
SatSolution.isSat eg1Soln

def eg1Soln : SatSolution eg1Statement :=
solveSAT eg1Statement

So it looks as if eg1Solution is not being simplified. I also tried to force it to whnf and got the following error, perhaps because I misunderstand whnf

syntax (name:= normalform)"whnf!" term : term
@[termElab normalform] def normalformImpl : TermElab :=
  fun stx expectedType? =>
  match stx with
  | `(whnf! $s) =>
      do
        let t ← elabTerm s none
        let e ← whnf t
        return e
  | _ => Lean.Elab.throwIllFormedSyntax

def eg1SolnNorm := whnf! eg1Soln

the definition at the end gives the error:

application type mismatch
  _.codom
argument has type
  Unit
but function has type
  Containment eg1Statement → Nat

Indeed the function does have the type Containment eg1Statement → Nat and everything compiles fine since this is the type of the argument at compile time. But at the meta level apparently it is getting either optimized to Unit deliberately or distorted in some other way.

Any clarifications will be appreciated. The meta stuff here is just my exploring with limited knowledge, my real question is whether I can make the interpreter simplify eg1Soln.

[Siddhartha Gadgil]

This is getting curiouser and perhaps is a bug. There is a change in behaviour between the nightly builds "leanprover/lean4:nightly-2021-09-19" and "leanprover/lean4:nightly-2021-09-20" where whnf is failing. Here is some local output for the earlier build with whnf! as above:

We normalize with

def eg1isFalseNormal := whnf! eg1IsFalse

then the outputs for the following are:

#print eg1IsFalse   --   def eg1IsFalse : Bool := SatSolution.isSat eg1Soln
#print eg1isFalseNormal   --    def eg1isFalseNormal : Bool :=false

which is what I expect. However, in the newer versions of lean, as mentioned above the normalization gives an error.

Any clarification is appreciated.