proving equality of structures

Stream: general

[Reid Barton]

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]

congr, which doesn't always work

[Reid Barton]

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]

From the changelog:

[Kevin Buzzard]

"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]

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

[Nicholas Scheel]

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]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

(and I have lots of these, unfortunately)

[Mario Carneiro]

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]

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]

Yes, that proof works too.

[Kevin Buzzard]

@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]

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

[Mario Carneiro]

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]

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