Zulip Chat Archive

Stream: new members

Topic: limitations of functions on struct defined w pattern match

Nicolas Rolland (Aug 21 2023 at 19:40):

"Math in lean" 6.1 states about functions on structures defined using pattern matching :

Although it is sometimes convenient to define functions this way, the definitional properties are not as convenient. For example, the expressions addAlt a b and addAlt' a b cannot be simplified until we decompose a and b into components, which we can do with cases, rcases, etc.

But when I comment out the mentioned bits, it stills typecheck (including with simp only)
Is it still relevant or has it been invalidated with lean 4 ?

structure Point where
  x : 
  y : 
  z : 

def addAlt : Point  Point  Point
  | Point.mk x₁ y₁ z₁, Point.mk x₂ y₂ z₂ => x₁ + x₂, y₁ + y₂, z₁ + z₂

example (a b : Point) : addAlt a b = addAlt b a := by
  --rcases a with ⟨xa, ya, za⟩
  --rcases b with ⟨xb, yb, zb⟩
  simp [addAlt, add_comm]

Eric Wieser (Aug 22 2023 at 01:04):

This changed in lean 4, though I think I opened an issue asking it to be changed back!

Last updated: Dec 20 2023 at 11:08 UTC