Zulip Chat Archive

Stream: general

Topic: Proving structure equality


view this post on Zulip 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?

view this post on Zulip Anne Baanen (Sep 30 2020 at 09:34):

Does by { cases a, refl } work?

view this post on Zulip Eric Wieser (Sep 30 2020 at 09:35):

Yes, it does - thanks

view this post on Zulip Anne Baanen (Sep 30 2020 at 09:35):

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

view this post on Zulip Eric Wieser (Sep 30 2020 at 09:36):

Is there any way to make simp handle this?

view this post on Zulip Eric Wieser (Sep 30 2020 at 09:36):

(for this specific struct)

view this post on Zulip Anne Baanen (Sep 30 2020 at 09:36):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Eric Wieser (Sep 30 2020 at 09:50):

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

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Sep 30 2020 at 09:53):

Doesn't seem to work unfortunately

view this post on Zulip 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.

view this post on Zulip Floris van Doorn (Sep 30 2020 at 09:54):

If it doesn't, please post a #mwe

view this post on Zulip 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

view this post on Zulip 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]?

view this post on Zulip 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).

view this post on Zulip Eric Wieser (Sep 30 2020 at 09:58):

simps mul did the trick

view this post on Zulip Eric Wieser (Sep 30 2020 at 10:00):

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

view this post on Zulip 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