Zulip Chat Archive

Stream: general

Topic: proving equality of structures


Reid Barton (May 16 2018 at 13:18):

Is there a tactic or something that's like apply subtype.eq, but works for a general structure? Or do I have to write down the equality lemma manually?

Kenny Lau (May 16 2018 at 13:19):

congr, which doesn't always work

Reid Barton (May 16 2018 at 13:22):

I thought about congr, but my goal is literally e1 = e2 and congr made no progress. Somehow I need to eta expand each side first, and then apply congr.

Kevin Buzzard (May 16 2018 at 13:53):

From the changelog:

Kevin Buzzard (May 16 2018 at 13:53):

"simp now reduces equalities c a_1 ... a_n = c b_1 ... b_n to a_1 = b_1 /\ ... /\ a_n = b_n if c is a constructor. This feature can be disabled using simp {constructor_eq := ff}"

Kevin Buzzard (May 16 2018 at 13:54):

of course, simp might do other things as well...

Nicholas Scheel (May 16 2018 at 16:59):

hm I asked a similar question a while ago, but it was about a lemma not a tactic: https://leanprover.zulipchat.com/#narrow/stream/113488-general/subject/structure.20equality.20from.20parts/near/124033713

Reid Barton (May 16 2018 at 17:05):

Yes, same goal. I managed to write my lemma by copying subtype.eq very carefully.

Scott Morrison (May 17 2018 at 01:08):

Someone (yikes, I've forgotten who, and my copy doesn't record the name) wrote for me a tactic called congr_struct that sometimes is useful for proving equalities of structures. In the presence of fields with dependencies on earlier fields it create new heq goals, which isn't always what you want.

Scott Morrison (May 17 2018 at 01:08):

There's a copy at <https://github.com/semorrison/lean-tidy/blob/master/src/tidy/congr_struct.lean> (you can just remove the import if you want to steal a copy).

Scott Morrison (May 17 2018 at 01:09):

If anyone wants it I can PR it into mathlib. I'm not actually using it anywhere myself at the moment.

Scott Morrison (May 17 2018 at 01:10):

I end up writing my own lemmas, e.g. of the form

structure NaturalTransformation (F G : C ↝ D) : Type (max (u+1) v) :=
  (components: Π X : C, (F +> X) ⟶ (G +> X))
  (naturality: ∀ {X Y : C} (f : X ⟶ Y), (F &> f) ≫ (components Y) = (components X) ≫ (G &> f))

infixr ` ⟹ `:50  := NaturalTransformation

lemma NaturalTransformations_componentwise_equal
  (α β : F ⟹ G)
  (w : ∀ X : C, α.components X = β.components X) : α = β :=
  begin
    induction α with α_components α_naturality,
    induction β with β_components β_naturality,
    have hc : α_components = β_components := funext w,
    subst hc
  end

Scott Morrison (May 17 2018 at 01:10):

(and I have lots of these, unfortunately)

Mario Carneiro (May 17 2018 at 02:02):

Mathlib is calling these lemmas "extensionality" theorems, for use with Simon's ext tactic. The fastest way to prove them is to case on both structures, then apply congr and other extensionality theorems to the resulting goals

Mario Carneiro (May 17 2018 at 02:07):

I don't have the necessary stuff to test your example, but I think it is possible to have a proof that looks something like by cases α; cases β; congr; exact funext w

Scott Morrison (May 17 2018 at 03:51):

Yes, that proof works too.

Kevin Buzzard (Apr 06 2019 at 18:11):

@Mario Carneiro thanks for refactoring my unbundled presheaves of types code; whilst you no longer reduce the length of what I write by a factor of 10, you still input some new ideas which I can learn from. Here's something I picked up. I am interested in proving equalities of structures, i.e. writing extensionality lemmas (I'm adding to an old thread, I thought it might be a way of making things more coherent). I had thought that Lean generated lemmas which did these things for me. But I learnt from your refactor that Lean does not always generate the best ones. Here's a concrete example:

import data.fintype

structure foo (α : Type*) :=
(s : set α)
(fs : fintype s) -- this is a subsingleton but not a prop

variable {α : Type*}

lemma foo.ext (x y : foo α) (hs : x.s = y.s) (hf : x.fs == y.fs) : x = y :=
begin
  cases x,
  cases y,
  rw foo.mk.inj_eq, -- auto-generated lemmas FTW
  exact hs, hf
end

-- but hf is not needed!
lemma foo.ext_better1 (s : set α) (t : set α) (hs : s = t) (fs : fintype s) (ft : fintype t):
foo.mk s fs = foo.mk t ft :=
begin
  congr,
  exact hs
end

lemma foo.ext_better2 (x y : foo α) (hs : x.s = y.s) : x = y :=
begin
  cases x,
  cases y,
  cases hs, -- what does this even do?
  congr,
end

Lean basically generated the first proof automatically. But the heq can be avoided. There are two ways of avoiding it, both of which I demonstrate here. The first is a direct application of congr. The second does cases on an equality! What is going on there? I don't understand what happens. Hypothesis hs changes from

hs : {s := x_s, fs := x_fs}.s = {s := y_s, fs := y_fs}.s

to

hs : {s := x_s, fs := x_fs}.s = {s := x_s, fs := y_fs}.s

One of those structures doesn't even look type correct to to me. Oh -- wait -- the type of y_fs changes! So it is type correct! The cases is doing something magic. What is going on?

Side question: which ext lemma is the best one to prove? The one with the structures or the one with the components? Or should one prove both?

Johan Commelin (Apr 06 2019 at 18:15):

I think better2 is the one that you want to have.

Mario Carneiro (Apr 06 2019 at 19:52):

Cases on an equality is one of the most useful things you can do in the presence of dependencies. The effect is the same as subst: The variable (in this case y_s) is removed from the context and all occurrences are replaced with x_s. This usually means you can make progress, because now x_fs and y_fs have the same type, so you can reasonably state and prove an equality about them

Mario Carneiro (Apr 06 2019 at 19:54):

What actually happened is that cases first reverts all dependencies, like y_fs, and then rewrites the goal (which is a dependent pi making reference to y_s) to change y_s to x_s. Then the type of y_fs changes at the same time as the goal changes, so it stays type correct


Last updated: Dec 20 2023 at 11:08 UTC