Eta-expansion of `Prop`-structures

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

During iota-reduction, terms of structures that live in Prop do not get eta-expanded. This was introduced in #1033 in order to avoid constructing primitive projections for terms that shouldn't have them (i.e existentials). However, the criteria applied is too strong, and blocks the reduction of subsingletons that could get eta-expanded otherwise. This, among other things, break both the transitivity and congruence of definitional equality.

Context

This issue has been reported by a few different users on Zulip: here, here and here

Steps to Reproduce

variable (P Q : Prop) (A : Type) (f : P → Q → A) (x : P ∧ Q)

example : And.rec f ⟨x.1,x.2⟩ = f (And.left x) (And.right x) := rfl --works
example : (And.rec f ⟨x.1,x.2⟩ : A) = And.rec f x  := rfl --fails

Expected behavior: both examples work

Actual behavior: The first one works, the second fails.

Versions

4.5.0-rc1
Web Browser

Additional Information

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start with the criteria around line 145 of src/Lean/Meta/WHNF.lean and run the minimal reproduction from the issue. Compare the two definitional-equality examples and verify that both are accepted with rfl, including the eta-expansion case for the Prop structure.