Zulip Chat Archive

Stream: general

Topic: missing ext lemmas?


view this post on Zulip Johan Commelin (Oct 03 2018 at 08:22):

How many of the following should be marked with @[extensionality]?

data/buffer/basic.lean:lemma ext :  {b₁ b₂ : buffer α}, to_list b₁ = to_list b₂  b₁ = b₂
data/equiv/basic.lean:lemma ext (f g : equiv α β) (H :  x, f x = g x) : f = g :=
data/finsupp.lean:lemma ext : {f g : α  β}, (a, f a = g a)  f = g
data/list/basic.lean:lemma foldl_ext (f g : α  β  α) (a : α)
data/list/basic.lean:lemma foldr_ext (f g : α  β  β) (b : β)
data/prod.lean:lemma ext {α β} {p q : α × β} : p.1 = q.1  p.2 = q.2  p = q :=
data/subtype.lean:lemma subtype.ext {a1 a2 : {x // β x}} : a1 = a2  a1.val = a2.val :=
data/subtype.lean:lemma subtype.coe_ext {a1 a2 : {x // β x}} : a1 = a2  (a1 : α) = a2 :=
logic/function.lean:lemma hfunext {α α': Sort u} {β : α  Sort v} {β' : α'  Sort v} {f : Πa, β a} {f' : Πa, β' a}
order/filter.lean:protected lemma ext : ( s, s  f.sets  s  g.sets)  f = g :=
category/applicative.lean:theorem applicative.ext {F} :  {A1 : applicative F} {A2 : applicative F}
category/functor.lean:theorem functor.ext {F} :  {F1 : functor F} {F2 : functor F}
data/analysis/topology.lean:theorem ext [T : topological_space α] {σ : Type*} {F : ctop α σ}
data/complex/basic.lean:theorem ext :  {z w : }, z.re = w.re  z.im = w.im  z = w
data/finset.lean:theorem ext {s₁ s₂ : finset α} : s₁ = s₂   a, a  s₁  a  s₂ :=
data/list/basic.lean:theorem ext :  {l₁ l₂ : list α}, (n, nth l₁ n = nth l₂ n)  l₁ = l₂
data/list/perm.lean:theorem perm_ext {l₁ l₂ : list α} (d₁ : nodup l₁) (d₂ : nodup l₂) : l₁ ~ l₂  a, a  l₁  a  l₂ :=
data/multiset.lean:theorem ext {s t : multiset α} : s = t   a, count a s = count a t :=
data/multiset.lean:theorem nodup_ext {s t : multiset α} : nodup s  nodup t  (s = t   a, a  s  a  t) :=
data/multiset.lean:theorem erase_dup_ext {s t : multiset α} : erase_dup s = erase_dup t   a, a  s  a  t :=
data/option.lean:theorem ext :  {o₁ o₂ : option α}, ( a, a  o₁  a  o₂)  o₁ = o₂
data/real/cau_seq.lean:theorem ext {f g : cau_seq β abv} (h :  i, f i = g i) : f = g :=
data/semiquot.lean:theorem ext {q₁ q₂ : semiquot α} : q₁ = q₂   a, a  q₁  a  q₂ :=
data/seq/wseq.lean:theorem equiv.ext {s t : wseq α} (h :  n, nth s n ~ nth t n) : s ~ t :=
data/set/basic.lean:theorem set_coe.ext {s : set α} {a b : s} : (a : α) = b  a = b :=
data/set/basic.lean:theorem ext {a b : set α} (h :  x, x  a  x  b) : a = b :=
group_theory/free_abelian_group.lean:protected theorem ext (g h : free_abelian_group α  β)
linear_algebra/linear_map_module.lean:theorem ext (h :  x, A x = B x) : A = B := subtype.eq $ funext h
linear_algebra/tensor_product.lean:theorem to_module.ext {g h : M  N  P}
number_theory/dioph.lean:  theorem ext {S S' : set (α  )} (d : dioph S) (H : v, S v  S' v) : dioph S' :=
number_theory/pell.lean:  theorem ext :  {z w : d}, z = w  z.re = w.re  z.im = w.im
order/basic.lean:theorem preorder.ext {α} {A B : preorder α}
order/basic.lean:theorem partial_order.ext {α} {A B : partial_order α}
order/basic.lean:theorem linear_order.ext {α} {A B : linear_order α}
order/bounded_lattice.lean:theorem order_top.ext {α} {A B : order_top α}
order/bounded_lattice.lean:theorem order_bot.ext {α} {A B : order_bot α}
order/bounded_lattice.lean:theorem bounded_lattice.ext {α} {A B : bounded_lattice α}
order/lattice.lean:theorem semilattice_sup.ext {α} {A B : semilattice_sup α}
order/lattice.lean:theorem semilattice_inf.ext {α} {A B : semilattice_inf α}
order/lattice.lean:theorem lattice.ext {α} {A B : lattice α}
set_theory/zfc.lean:theorem equiv.ext : Π (x y : pSet), equiv x y  (x  y  y  x)
set_theory/zfc.lean:theorem mem.ext : Π {x y : pSet.{u}}, (w:pSet.{u}, w  x  w  y)  equiv x y
set_theory/zfc.lean:theorem ext {x y : Set.{u}} : (z:Set.{u}, z  x  z  y)  x = y :=

view this post on Zulip Johan Commelin (Oct 03 2018 at 08:22):

Is it worth going through this list. Or have people done that before, and decided that this should not get the extensionality attribute?

view this post on Zulip Kenny Lau (Oct 03 2018 at 08:37):

thanks for bringing this up

view this post on Zulip Patrick Massot (Oct 03 2018 at 08:38):

I think it's worth going through the list

view this post on Zulip Simon Hudon (Oct 03 2018 at 08:39):

I, for one, have not done it and I was working on the basis of "let's add them when we need them" after I added the most obvious ones.

view this post on Zulip Johan Commelin (Oct 03 2018 at 08:46):

Can someone give an entry on the list that should not be tagged with the extensionality attribute? If I understand the reason, then I might be able to go through the list myself.

view this post on Zulip Simon Hudon (Oct 03 2018 at 08:50):

set_theory/zfc.lean:theorem equiv.ext

view this post on Zulip Scott Morrison (Oct 03 2018 at 08:58):

You missed yoneda.ext :-). (Perhaps because it's a def?) Anyway, it probably shouldn't have @[extensionality].

view this post on Zulip Simon Hudon (Oct 03 2018 at 08:59):

Also, I wouldn't tag semilattice_sup.ext_sup

view this post on Zulip Johan Commelin (Oct 03 2018 at 09:00):

Can you explain why?

view this post on Zulip Johan Commelin (Oct 03 2018 at 09:00):

@Scott Morrison Indeed, I only looked for lemmas and theorems

view this post on Zulip Simon Hudon (Oct 03 2018 at 09:11):

It's a comparison of class instances rather than the objects themselves. It seems like it could produce surprising results

view this post on Zulip Johan Commelin (Oct 03 2018 at 09:15):

Ok, I see. @Johannes Hölzl Does it make sense to create an extensionality PR that adds about 40 extensionality attributes?

view this post on Zulip Johannes Hölzl (Oct 03 2018 at 09:16):

Do we have 40 types? Are sensible? Also be careful that they don't overlap.

view this post on Zulip Johan Commelin (Oct 03 2018 at 09:17):

See the list I posted above.

view this post on Zulip Johan Commelin (Oct 03 2018 at 09:17):

Simon mentioned a couple that shouldn't be tagged, but I think a lot of them could reasonably be tagged.

view this post on Zulip Simon Hudon (Oct 03 2018 at 09:21):

Some of them are equivalences while ext uses implications. When I encounter such lemma, I rename them ext_iff so that I can add a ext lemma as an implication

view this post on Zulip Johannes Hölzl (Oct 03 2018 at 11:51):

also before you add the extensionality lemmas we should change the semantics of ext. Instead of applying all possible extensionality lemmas it should only work along the names given by the user, or accept * to apply all.

view this post on Zulip Johan Commelin (Oct 03 2018 at 11:53):

Hmm, ok. Do you mean you want people to write ext set or ext subtype etc...?

view this post on Zulip Simon Hudon (Oct 03 2018 at 11:54):

Right now, ext detects the type of the arguments (e.g. set) and only tries relevant extensionality lemmas

view this post on Zulip Simon Hudon (Oct 03 2018 at 11:54):

It used to be that functional extensionality might be selected for the equality of two sets. It's no longer the case.

view this post on Zulip Patrick Massot (Oct 03 2018 at 11:54):

Johannes, that would be very sad

view this post on Zulip Patrick Massot (Oct 03 2018 at 11:54):

I like to type ext and Lean figures out what I mean

view this post on Zulip Johannes Hölzl (Oct 03 2018 at 11:55):

and I hate it to add an attribute and half of mathlib breaks

view this post on Zulip Mario Carneiro (Oct 03 2018 at 11:55):

Johannes this was implemented recently, like simon says

view this post on Zulip Johannes Hölzl (Oct 03 2018 at 11:55):

okay, thats good!

view this post on Zulip Mario Carneiro (Oct 03 2018 at 11:55):

You don't need to say ext set, it looks at the type of the objects in the equality in the goal

view this post on Zulip Simon Hudon (Oct 03 2018 at 11:56):

It's also tolerant on the kind of relation you can prove but I think sticking close to = is a good idea.

view this post on Zulip Mario Carneiro (Oct 03 2018 at 11:57):

But this also means that you essentially want one extensionality lemma for each type, so no multiples, and no equalities over generic types

view this post on Zulip Johan Commelin (Oct 03 2018 at 11:57):

Right, but functor.ext seems like a good exception

view this post on Zulip Mario Carneiro (Oct 03 2018 at 11:58):

If there are multiple candidates for extensionality, e.g. roption.ext vs roption.ext' then you have to think about which one is better general-purpose and pick one

view this post on Zulip Simon Hudon (Oct 03 2018 at 11:59):

@Johan Commelin I'm tempted to agree with you but technically, there's no reason why functor.ext wouldn't work as an extensionality lemma

view this post on Zulip Johan Commelin (Oct 03 2018 at 11:59):

@Simon Hudon I meant that it is an exception to sticking to =

view this post on Zulip Mario Carneiro (Oct 03 2018 at 11:59):

Also keep in mind that ext will apply all extensionality lemmas it can all the way down so you don't want loopable hypotheses

view this post on Zulip Simon Hudon (Oct 03 2018 at 12:00):

@Mario Carneiro You can also give the most general one a lower priority

view this post on Zulip Johan Commelin (Oct 03 2018 at 12:00):

Or we want ext to take an optional small_nat argument like congr

view this post on Zulip Johan Commelin (Oct 03 2018 at 12:00):

Or congr', whatever

view this post on Zulip Simon Hudon (Oct 03 2018 at 12:00):

It already does: ext : 3

view this post on Zulip Mario Carneiro (Oct 03 2018 at 12:01):

AFAIK competing extensionality lemmas always apply in the same generality, they just have different hypotheses, so giving priority wouldn't help

view this post on Zulip Simon Hudon (Oct 03 2018 at 12:01):

But I think Mario is right. There has to be a sense that something decreases as we keep applying ext, for instance the complexity of the objects being compared

view this post on Zulip Simon Hudon (Oct 03 2018 at 12:02):

@Mario Carneiro I don't understand what you mean by "in the same generality"

view this post on Zulip Mario Carneiro (Oct 03 2018 at 12:04):

Most theorems that could qualify as @[extensionality] have a conclusion (a : T) = b, so if this is the goal then all extensionalities for T will apply

view this post on Zulip Mario Carneiro (Oct 03 2018 at 12:05):

With other kinds of theorems there might be a difference in generality like if one theorem only has say F a = G b in the conclusion, but with extensionality lemmas it's always a = b where a and b match anything in the type

view this post on Zulip Simon Hudon (Oct 03 2018 at 12:05):

You could see one lemma being (a : set α) = b and another be (a : set (list α)) = b. The first one is the most general one although both would be attempted

view this post on Zulip Mario Carneiro (Oct 03 2018 at 12:06):

I suppose that is a possibility, but so far I don't think we have any such "composite extensionality lemmas"

view this post on Zulip Mario Carneiro (Oct 03 2018 at 12:06):

it's always a constant or type constructor applied to variables

view this post on Zulip Mario Carneiro (Oct 03 2018 at 12:08):

Looking at the list, I see free_abelian_group.ext and to_module.ext have composite types, and dioph has something that isn't an extensionality at all

view this post on Zulip Mario Carneiro (Oct 03 2018 at 12:09):

I don't think free_abelian_group.ext qualifies as an extensionality, this is some kind of yoneda thing

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:53):

what about topological_space_eq?

view this post on Zulip Patrick Massot (Oct 03 2018 at 20:54):

yes


Last updated: May 11 2021 at 00:31 UTC