simp on binders

Stream: mathlib4

[Eric Wieser]

This works in Lean 3:

import tactic.simp_rw

example (A B : Prop) (f : A → ℕ) (h : A ↔ B) :
  ∀ h : A, f h = 0 :=
begin
  simp only [h],
  -- goal is ∀ (h_1 : B), f _ = 0
  sorry
end

but the simp only does nothing in Lean 4:

example (A B : Prop) (f : A → ℕ) (h : A ↔ B) :
  ∀ h : A, f h = 0 := by
    simp_rw [h]
    -- goal is unchanged
    sorry

Are we missing a congr lemma?

[Eric Wieser]

Ah, docs4#forall_prop_congr' is not tagged congr, because of an error

[Eric Wieser]

Mario Carneiro said:

and would you look at that:

-- Porting note: `@[congr]` commented out for now.
-- @[congr]
theorem forall_prop_congr' {p p' : Prop} {q q' : p → Prop} (hq : ∀ h, q h ↔ q' h) (hp : p ↔ p') :
    (∀ h, q h) = ∀ h : p', q' (hp.2 h) :=
  propext (forall_prop_congr hq hp)

[Eric Wieser]

lean4#1926

[Eric Wieser]

This works in lean 3:

import tactic

example {α} (P Q : α → Prop) (h : ∀ a, P a ↔ Q a) (R : ∀ a, P a → Prop) :
  ∀ (a : α) (hp : P a), R a hp :=
begin
  simp_rw [h] -- goal is now `∀ (a : α) (hp : Q a),`
end

but fails in Lean 4

example (P Q : α → Prop) (h : ∀ a, P a ↔ Q a) (R : ∀ a, P a → Prop) :
  ∀ (a : α) (hp : P a), R a hp := by
  simp [h] -- does nothing
  sorry

(relates to !4#5349)

[Eric Wieser]

It seems docs#forall_prop_congr' doesn't get used in Lean 4

[Eric Wieser]

Ah, this is a repeat of an old thread

[Eric Wieser]

The example in !4#5349 is much worse than the previous one which was worked around with

  -- porting note: workaround for lean4#1926, was `simp_rw [pow_succ']`
  suffices h_lean4_1926 : ∀ (hx' : x ∈ M ^ n * M), C (Nat.succ n) x (by rwa [pow_succ']) from
    fun hx => h_lean4_1926 (by rwa [← pow_succ'])
  -- porting note: end workaround

[Eric Wieser]

"rewrite the whole goal in a suffices" is very unpleasant when the goal contains proof terms

[Scott Morrison]

lean4#2732. I've verified on the lean-pr-testing-2732 branch that this resolves all porting notes tagged with lean4#1926.

There were probably many more regressions during porting as people worked around lean4#1926, but without tagging them.

If anyone would like to add changes to the lean-pr-testing-2732, I've opened it as a PR at #7845.