Zulip Chat Archive

Stream: general

Topic: simp of structures equality


kana (Jun 24 2021 at 21:37):

I have such goal

{hom := λ (y : Cᵒᵖ), category.comp 𝟭, nat := _} = {hom := λ (_x : Cᵒᵖ), id, nat := _}

where nat : Prop.

Both homs have the same type.

λ (y : Cᵒᵖ), category.comp 𝟭 : Π (y : Cᵒᵖ), (y.unop  x)  (y.unop  x)

λ (_x : Cᵒᵖ), id             : Π (_x : Cᵒᵖ), (_x.unop  x)  (_x.unop  x)

But simp does not simplify goal to just

λ (y : Cᵒᵖ), category.comp 𝟭 = λ (_x : Cᵒᵖ), id

Is it a bug, or I missed something?

Not minimal example line 191

Adam Topaz (Jun 24 2021 at 21:41):

Looks like you should prove an ext lemma.

Yakov Pechersky (Jun 24 2021 at 21:41):

You're dealing with equality of structures. You have to use ext, the extensionality tactic, which splats out the structure, and asks you to prove that all the fields of the two structures match.

Adam Topaz (Jun 24 2021 at 21:42):

I assume these are natural transformations. If you put a @[ext] over your structure natural_transformation ... then lean will make the extensionality lemma for you automatically. Then use the ext tactic in the proof

kana (Jun 24 2021 at 22:57):

Thanks. It works.

But with that structure just simp works, what is the difference?

structure qwe :=
(a : nat) (b : a = a)

example : ({ a := 1, b := rfl } : qwe) = { a := 2, b := rfl } :=
begin
  simp,
end

Last updated: Dec 20 2023 at 11:08 UTC