Zulip Chat Archive

Stream: lean4

Topic: Simp and structure projection problem


Tomas Skrivan (Feb 21 2022 at 22:00):

I have a simp lemma that behaves differently on projection Prod.fst : α × β → α and on a custom function my_fst : α × β → α.

The lemma is that an adjoint of composition is composition of adjoints: adjoint (λ x => f (g x)) = adjoint g ∘ adjoint f . Interestingly, the simplifier applies this lemma on adjoint Prod.fst with g = id but it does not apply this lemma on adjoint my_fst.

What is going on? Why is Prod.fst and my_fst treated by the simplifier differently? Is this an intended behavior? Is it an unfortunate consequence of another reasonable choice?

mwe:

variable {α β γ} [Inhabited α] [Inhabited β] [Inhabited γ]

constant adjoint : (α  β)  (β  α)

@[simp]
theorem adjoint_of_comp (f : β  γ) (g : α  β) :
  adjoint (λ x => f (g x)) = adjoint g  adjoint f
  :=
  by sorry

@[simp]
theorem adjoint_of_fst :
  adjoint (Prod.fst : α × β  α) = fun x : α => (x, default)
  := by sorry

example : adjoint (Prod.fst : α × β  α) = fun x : α => (x, default)
  :=
by
  -- This applies `adjoint_of_comp` for some reason
  simp (config := { singlePass := true })

  simp -- infinite recursion
  done


constant my_fst : α × β  α

@[simp]
theorem adjoint_of_my_fst :
  adjoint (my_fst : α × β  α) = fun x : α => (x, default)
  := by sorry

example : adjoint (my_fst : α × β  α) = fun x : α => (x, default)
  :=
by
  simp
  done

Last updated: Dec 20 2023 at 11:08 UTC