Zulip Chat Archive

Stream: general

Topic: simps and function application

view this post on Zulip Simon Hudon (Sep 04 2020 at 16:26):

I'm creating instances for a bundled hom type:

import order.preorder_hom
import order.lattice

variables {α β : Type*} [preorder α]

@[simps {rhs_md := semireducible}]
instance [partial_order β] : partial_order (α  β) :=
partial_order.lift preorder_hom.to_fun $ by rintro ⟨⟩ ⟨⟩ h; congr; exact h

instance [semilattice_sup β] : semilattice_sup (α  β) :=
{ sup := λ f g, f.to_fun  g.to_fun, λ x y h, sup_le_sup (f.monotone h) (g.monotone h),
  le_sup_left := λ a b x, le_sup_left,
  le_sup_right := λ a b x, le_sup_right,
  sup_le := λ a b c h₀ h₁ x, sup_le (h₀ x) (h₁ x),
  .. (_ : partial_order (α  β)) }

-- generates
-- preorder_hom.semilattice_sup_sup_to_fun : ∀ {α : Type u_1} [_inst_1 : preorder α] {β : Type u_2}
-- [_inst_4 : semilattice_sup β] (f g : α →ₘ β) (a : α),
-- ⇑(semilattice_sup.sup f g) a = (f.to_fun ⊔ g.to_fun) a

simps generates the wrong equality for sup. I'd like it to generate ⇑(semilattice_sup.sup f g) a = f a ⊔ g a. Is this possible and if so how?

view this post on Zulip Simon Hudon (Sep 04 2020 at 16:28):

Update: Defining sup as:

sup := λ f g, ⟨λ a, f a  g a, λ x y h, sup_le_sup (f.monotone h) (g.monotone h),

does it but why does simps not know that we can distribute function application and sup on pi types?

view this post on Zulip Johan Commelin (Sep 14 2020 at 08:02):

@Floris van Doorn Do you think simps could be made to take here of https://github.com/leanprover-community/mathlib/pull/4125#discussion_r487682684?

Last updated: May 10 2021 at 00:31 UTC