Simp not simplifying

Stream: lean4

[Michael Jam]

Hello, I have this "efficient" function that given a nat, computes true.

def f : Nat → Bool
  | 0 => true
  | n + 1  =>
    (match n with
    | 0 => true
    | _ + 1 => true
    )
    && f n

Now i'm trying to prove the important math theorem: f 1 = true

theorem p : f 1 := by
  simp [f]
  admit

My issue is that simp does not simplify (in lean4 nightly-2021-05-06) even when being specific about f

I'm learning lean so I'm not very sure, but I expected that simp would replace f 1 with its computed result: true in the goal state.

Maybe the tactic is not smart enough, but is there a way to force f 1 to unwrap itself in a single step?

[Kevin Buzzard]

refl?

[Patrick Massot]

refl is called rfl in Lean 4.

[Kevin Buzzard]

I am not too sure that I expect simp to work here. You have defined no simp lemmas and so this will just unfold to some f.rec term which the simplifier probably won't know what to do with? I'm not 100% sure of what I'm talking about though

[Scott Viteri]

Are they really the same?
Lean3: theorem hi : "".data = [] := by refl
Lean4: example : "".data = [] := by rfl <-- doesn't go through

[Kevin Buzzard]

They're not the same no

[Kevin Buzzard]

In lean 4 rfl only proves a=a. Lean 3's refl tactic proves R a a for any reflexive binary relation whose proof of reflexivity has been tagged with the @[refl] tag. Lean 4 refl does exist but only in my mathlib port :p

[Kevin Buzzard]

And instead of tagging the refl lemma you have to add it to the list of lemmas which the tactic tries ;-)

[Kevin Buzzard]

@Scott Viteri my answer no longer applies to your post because you changed == to =

[Scott Viteri]

sorry copy paste error

[Kevin Buzzard]

I'm not at lean right now so can't check the definition of .data

[Scott Viteri]

Don't want to derail this, I'll make a separate thread

[Wojciech Nawrocki]

Interestingly enough rfl doesn't work either when using and in this order (on master).

def f : Nat → Bool
  | 0 => true
  | n + 1 => (match n with
    | 0 => true
    | _ + 1 => true) && f n

def g : Nat → Bool
  | 0 => true
  | n + 1 => g n && (match n with
    | 0 => true
    | _ + 1 => true)

#reduce f 1 -- true
example : f 1 = true := rfl -- fails
#reduce g 1 -- true
example : g 1 = true := rfl -- works

[Wojciech Nawrocki]

It works with set_option smartUnfolding false.

[Daniel Selsam]

This one is subtle. Here are the smart-unfolding lemmas:

def f._sunfold : Nat → Bool :=
fun (x : Nat) =>
  match x with
  | 0 => idRhs Bool true
  | Nat.succ n =>
    (match n with
      | 0 => idRhs Bool true
      | Nat.succ x => idRhs Bool true) &&
      f n

def g._sunfold : Nat → Bool :=
fun (x : Nat) =>
  match x with
  | 0 => idRhs Bool true
  | Nat.succ n =>
    g n &&
      match n with
      | 0 => idRhs Bool true
      | Nat.succ x => idRhs Bool true

The call f 1 will smart-unfold to f 0, which recursively smart-unfolds to Bool.true, which is not wrapped with idRHS; currently WHNF does not realize that this term is acceptable, and so rejects the smart-unfold. In contrast, g 1 will smart-unfold to idRHS true, and so true is accepted.

[Mario Carneiro]

This bug looks similar to https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Smart.20unfolding.20produces.20ununfoldable.20terms . The idRhs applications in the match n seem to be spurious, it should be around the &&.

[Mario Carneiro]

reported as leanprover/lean4#445

[Daniel Selsam]

@Mario Carneiro Do you know if "smart-unfolding" has a precise semantics?

[Mario Carneiro]

The specification I would propose is that smart unfolding is a transformation on terms like so:

• If e is match x with (| pat_i => e_i)* where x is a variable,
  then smart_unfold(e) is match x with (| pat_i => smart_unfold(e_i))*

• Otherwise, smart_unfold(e) = idRhs _ e.

Another possible clause would apply to if statements:

• If e is if c then e1 else e2 then smart_unfold(e) is if c then smart_unfold(e1) else smart_unfold(e2)

but given how this interacts with the consumer of smart unfolding, namely isDefEq when it wants to unfold a function, it seems like having it depend on an arbitrary predicate being true will be difficult to control. So I would stick with just top level match (on a variable) being smart unfolded, as in the first two bullets.

[Daniel Selsam]

Are you sure that wouldn't cause simp to loop?

def foo (n : Nat) : Nat :=
  if False then 1000 else
  match n with
  | 0   => 0
  | n+1 => foo n

def foo._proposed_sunfold : Nat → Nat :=
fun (n : Nat) => idRhs $
  if False then 1000 else
    match n with
    | 0 => 0
    | Nat.succ n => foo n

Simp on foo n:

• smart-unfold foo n to expose the if
• traverse down to inner foo n
• repeat

[Mario Carneiro]

Yes, this is a common problem with definitions that don't start with a pattern match. I don't think that is an issue for smart unfolding to solve though

[Mario Carneiro]

You hit this problem in lean 3 when unfolding definitions by well founded recursion because those often don't start with a pattern match, for example gcd.

[Mario Carneiro]

One potential fix is for simp to detect simple infinite loops, in this case that a definition is going to unfold unconditionally to a term containing itself, and then handle these definitions specially, either never unfolding them or only unfolding once. In such cases I don't think it is unreasonable to ask the user to use another tactic or another configuration of simp like single_pass := true

[Mario Carneiro]

For isDefEq this isn't a major problem since it only unfolds lazily so having a recursive unfolding like this is fine as long as it is "productive" (i.e. doesn't unfold trivially to an application of itself like foo := foo)

[Mario Carneiro]

(plus these kinds of unfolding aren't definitional anyway so isDefEq generally doesn't have to worry about them)

[Michael Jam]

Hi. Here is another example:

inductive binary_tree α where
| nil
| node (value : α) (left_subtree : binary_tree α) (right_subtree : binary_tree α)

open binary_tree

def binary_tree_is_full : binary_tree α → Bool
| nil => true
| node _ nil nil => true
| node _ nil _ => false
| node _ _ nil => false
| node _ left_tree right_tree =>
  binary_tree_is_full left_tree && binary_tree_is_full right_tree

theorem th
  (value : α) (left_tree : binary_tree α) (right_tree : binary_tree α)
  (left_tree_is_full : binary_tree_is_full left_tree)
  (right_tree_is_full : binary_tree_is_full right_tree)
  : binary_tree_is_full (node value left_tree right_tree) := by
  simp [binary_tree_is_full]
  admit

simp doesn't unfold binary_tree_is_full. I expect it unfolds.
Is this still a bug? I'm using Lean (version 4.0.0-nightly-2021-05-26, commit 02e917793e07, Release)

[Sebastian Ullrich]

What do you expect it to unfold to? The case is not sufficiently determined.

[Michael Jam]

oh i see you're right

[Michael Jam]

What about this:

inductive binary_tree α where
| nil
| node (value : α) (left_subtree : binary_tree α) (right_subtree : binary_tree α)

open binary_tree

def binary_tree_is_full : binary_tree α → Bool
| nil => true
| node _ nil nil => true
| node _ nil _ => false
| node _ _ nil => false
| node _ left_tree right_tree =>
  binary_tree_is_full left_tree && binary_tree_is_full right_tree

theorem th
  (value : α) (left_tree : binary_tree α) (right_tree : binary_tree α)
  (left_tree_is_full : binary_tree_is_full left_tree)
  (right_tree_is_full : binary_tree_is_full right_tree)
  : binary_tree_is_full (node value left_tree right_tree) := by
  let tree := node value left_tree right_tree
  match tree with
  | nil => admit
  | node _ nil nil => admit
  | node _ nil _ => admit
  | node _ _ nil => admit
  | node _ l r =>
    simp [binary_tree_is_full]
    admit

Shouldn't the last simp unfold to binary_tree_is_full l && binary_tree_is_full r ?

[Michael Jam]

Maybe this unprovable theorem is cleaner:

theorem th1 (tree : binary_tree α)
  : binary_tree_is_full tree := by
  match tree with
  | nil =>
    simp [binary_tree_is_full]
  | node _ nil nil =>
    simp [binary_tree_is_full]
  | node _ nil _ =>
    simp [binary_tree_is_full]
    admit
  | node _ _ nil =>
    simp [binary_tree_is_full]
    admit
  | node _ l r =>
    simp [binary_tree_is_full]
    admit

I match with the same structure as in binary_tree definition, the first simps seem to work but not the last ones

[Sebastian Ullrich]

It's not that simple in presence of overlapping patterns. Your last case will only unfold if it's clear the prior ones did not match, i.e. on node/node. So you should match on node _ (node ..) (node ..) in the last proof case.

[Sebastian Ullrich]

Accumulating the knowledge that the prior proof cases did not match either would in theory be possible, but is very much nontrivial. It's also not clear how to actually make that knowledge accessible in general. E.g. if you match first on node _ nil _ and then node .., what should the goal state look like?

[Michael Jam]

I see... I think I will try to avoid overlapping patterns now

[Michael Jam]

Thanks

[Sebastian Ullrich]

At least in your proofs, yes :)

[Daniel Fabian]

@Sebastian Ullrich when you talk about "in proofs" are you referring to noConfusion not working in Sort 0?

[Sebastian Ullrich]

No, I don't know about any connection to that