## Stream: general

### Topic: Proving structure equality

#### Eric Wieser (Sep 30 2020 at 09:33):

This looks like it should be obvious, but I'm stuck with a goal state of ⊢ {value := a.value, proof := _} = a, where the type is

structure aux {C : free_algebra R X → Prop} (p : grade_proof C) :=
(value : free_algebra R X)
(proof : C value)


How do I invoke proof-irrelevance to close this?

#### Anne Baanen (Sep 30 2020 at 09:34):

Does by { cases a, refl } work?

#### Eric Wieser (Sep 30 2020 at 09:35):

Yes, it does - thanks

#### Anne Baanen (Sep 30 2020 at 09:35):

These kinds of properties are sometimes called eta, see e.g. prod.mk.eta.

#### Eric Wieser (Sep 30 2020 at 09:36):

Is there any way to make simp handle this?

#### Eric Wieser (Sep 30 2020 at 09:36):

(for this specific struct)

#### Anne Baanen (Sep 30 2020 at 09:36):

@[simp] lemma aux.eta := by { cases a, refl }? :wink:

#### Anne Baanen (Sep 30 2020 at 09:38):

My rule of thumb is that project_a (mk a b) is easily reduced and mk (project_a x) (project_b x) needs some help from cases.

#### Kevin Buzzard (Sep 30 2020 at 09:38):

Many definitions of basic objects in the library are followed almost immediately by an eta lemma with proof by cases e.g. https://github.com/leanprover-community/mathlib/blob/743f82ca17c1690fead4ce0f882c590b37cb2842/src/data/complex/basic.lean#L37-L38

#### Kevin Buzzard (Sep 30 2020 at 09:39):

In Lean, project (mk) is often rfl but mk (project) is not, because this was some design decision. It's called eta reduction and we have to do it by hand and add it as a simp lemma.

#### Eric Wieser (Sep 30 2020 at 09:49):

On a similar note, is there any way to automate

instance : has_mul(grade_proof.aux p) := ⟨λ a b, ⟨a.value * b.value, p.mul a.proof b.proof⟩⟩
@[simp] lemma mul_def (a b : aux p) : a * b = ⟨a.value * b.value, p.mul a.proof b.proof⟩ := rfl


#### Eric Wieser (Sep 30 2020 at 09:50):

Specifically to avoid writing the same expression twice in both the lemma and the instance

#### Gabriel Ebner (Sep 30 2020 at 09:51):

For structures @[simps] does exactly that. I'm not sure how well it works for type class instances.

#### Eric Wieser (Sep 30 2020 at 09:53):

Doesn't seem to work unfortunately

#### Floris van Doorn (Sep 30 2020 at 09:53):

It does!

import tactic.simps
@[simps] instance : has_mul bool := ⟨band⟩
example (b₁ b₂ : bool) : b₁ * b₂ = band b₁ b₂ := by simp


It hasn't been tested a lot though.

#### Floris van Doorn (Sep 30 2020 at 09:54):

If it doesn't, please post a #mwe

#### Eric Wieser (Sep 30 2020 at 09:55):

I'm unfortunately quite a way off an mwe, so for now I'll stick with the anecdotal claim that one of my simp proof works with add_def and not simps

#### Floris van Doorn (Sep 30 2020 at 09:56):

If grade_proof.aux is a structure, it is possible that @[simps] tries to apply projections recursively. Can you try @[simps mul]?

#### Floris van Doorn (Sep 30 2020 at 09:57):

If that doesn't work, the output of set_option trace.simps.verbose true just before using the @[simps] attribute would also be helpful (you don't have to minimize the example).

#### Eric Wieser (Sep 30 2020 at 09:58):

simps mul did the trick

#### Eric Wieser (Sep 30 2020 at 10:00):

I now have a semiring instance where almost every field is by simp :)

#### Eric Wieser (Sep 30 2020 at 10:52):

#4335 is the result, any tips for golfing would be appreciated :)

Last updated: May 11 2021 at 13:22 UTC