change in `simp` behaviour #2

Stream: lean4

[Scott Morrison]

Compare Lean 3:

import logic.basic

open list

example {P : Prop} : ∀ (x : ℕ) (h : x ∈ ([] : list ℕ)), P :=
begin
  simp only [forall_prop_of_false (not_mem_nil _)],
  guard_target ℕ → true,
  simp,
end

and Lean 4:

open List

-- Some definitions inlined to avoid having imports:
def Not.elim {α : Sort _} (H1 : ¬a) (H2 : a) : α := absurd H2 H1
theorem iff_of_true (ha : a) (hb : b) : a ↔ b := ⟨fun _ => hb, fun _ => ha⟩
theorem iff_true_intro (h : a) : a ↔ True := iff_of_true h ⟨⟩
theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True :=
  iff_true_intro fun h => hn.elim h
@[simp] theorem not_mem_nil (a : α) : ¬ a ∈ [] := fun x => nomatch x

example {P : Prop} : ∀ (x : Nat) (_ : x ∈ []), P :=
by
  simp only [forall_prop_of_false (not_mem_nil _)] -- Succeeds but does nothing.
  simp

I'm not sure why this difference in behaviour is occurring. Mario suggested it may be a change in the simplifier's handling of multiple binders, and in Lean 4 there is no way for the simplifier to "stop" after passing through just the first x : Nat binder and notice that the lemma applies.

This arose in porting List.pairwise_append, where in Lean 3 we relied on this behaviour of the simplifier.

[Chris Lovett]

And since the simp only is doing nothing, the proof becomes just simp and this trace shows why it works:

set_option trace.Meta.Tactic.simp.rewrite true
example {P : Prop} : ∀ (x : Nat) (_ : x ∈ []), P :=
by
   simp

--[Meta.Tactic.simp.rewrite] not_mem_nil:1000, x ∈ [] ==> False
--[Meta.Tactic.simp.rewrite] false_implies:1000, False → P ==> True
--[Meta.Tactic.simp.rewrite] implies_true:1000, Nat → True ==> True

[David Renshaw]

@Scott Morrison try

simp only [(forall_prop_of_false (not_mem_nil _): ((_ → _) ↔ _ ))]

[David Renshaw]

and see https://github.com/leanprover/lean4/issues/1549

[Scott Morrison]

Ahha, I'm reporting an exact duplicate! I'm not so interested in a workaround, more wondering about the relative likelihoods of a general fix, or having to flag this as a gotcha for mathport.

[David Renshaw]

My impression is that this is a bug in some AST traversal somewhere.

[Leonardo de Moura]

Pushed a fir for this issue: https://github.com/leanprover/lean4/commit/6bc414440990760b6224e592e2c8e82f595aa742