match in defs

Stream: general

[Chris Hughes]

Out of the following two definitions, I find the first much easier to use.

private  def  mul_aux : α × S → α × S → loc α S :=
λ x y, ⟦⟨x.1  * y.1, x.2.1  * y.2.1, is_submonoid.mul_mem x.2.2 y.2.2⟩⟧

private def mul_aux : α × S → α × S → loc α S :=
λ ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩, ⟦⟨r₁ * r₂, s₁ * s₂, is_submonoid.mul_mem hs₁ hs₂⟩⟧

The first one unfolds much more easily if I give it arguments either of the form x y but also works okay with ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ as arguments. What are the advantages/disadvantages of each approach?

[Kevin Buzzard]

Let me make the comment that in the past, when I have used pointy brackets and lambdas when writing a definition, I've found it much more difficult to prove things by rfl because high powered stuff is going on behind the scenes.

[Chris Hughes]

Essentially, I think it's because λ ⟨r₁, s₁, hs₁⟩ uses prod.rec and subtype.rec, or the various derived lemmas like subtype.cases_on and these don't reduce to anything unless you give them something of the form subtype.mk _ _ The first def will unfold when the arguments are not of the form subtype.mk _ _

[Kenny Lau]

don't use any pointy brackets or tactics in a definition

[Simon Hudon]

Any reason not to want this?

private def mul_aux : α × S → α × S → loc α S
| ⟨r₁, s₁, hs₁⟩ ⟨r₂, s₂, hs₂⟩ := ⟦⟨r₁ * r₂, s₁ * s₂, is_submonoid.mul_mem hs₁ hs₂⟩⟧

It only unfolds with explicit tuples, unlike the first alternative. In the second alternative, it will unfold to a useless auxiliary definition.

[Kenny Lau]

it's private

[Simon Hudon]

Why is that relevant?

[Kenny Lau]

it isn't

[Simon Hudon]

Why was that your response to my question then?

[Kenny Lau]

it wasn't

[Kenny Lau]

it's relevant because I'm not going to unfold that definition except in the definition of multiplication

[Kenny Lau]

and I only need to use its properties, not its definition

[Simon Hudon]

Are you saying that the whole conversation is pointless?

[Kenny Lau]

he's asking about one of my definitions

[Kenny Lau]

I don't know why he's doing that

[Simon Hudon]

ok

[Kenny Lau]

Are you saying that the whole conversation is pointless?

• <-- there you go, a point

[Simon Hudon]

Sorry that, was the wrong place to write that.

[Kenny Lau]

sorry