Proving structure equality

Stream: general

[Eric Wieser]

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]

Does by { cases a, refl } work?

[Eric Wieser]

Yes, it does - thanks

[Anne Baanen]

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

[Eric Wieser]

Is there any way to make simp handle this?

[Eric Wieser]

(for this specific struct)

[Anne Baanen]

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

[Anne Baanen]

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]

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]

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]

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]

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

[Gabriel Ebner]

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

[Eric Wieser]

Doesn't seem to work unfortunately

[Floris van Doorn]

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]

If it doesn't, please post a #mwe

[Eric Wieser]

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]

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]

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]

simps mul did the trick

[Eric Wieser]

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

[Eric Wieser]

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