Instance binders in exists

Stream: mathlib4

[Mario Carneiro]

These aren't supported in lean 4, since the meaning is dubious, but they do occur in mathlib, e.g. src#metric.second_countable_of_countable_discretization . There are 19 occurrences in mathlib + liquid. Support? Backport?

[Johan Commelin]

@Mario Carneiro Can you post the full list?

[Johan Commelin]

I'm happy to remove them from liquid, if that can be my little contribution to the porting process (-;

[Mario Carneiro]

The line numbers are approximate, since these are wrt the ported files

Lib4/Liquid/Condensed/ProetaleSiteSyn.lean:64:-- error in Condensed.ProetaleSite: Mathport/Syntax/Translate/Basic.lean:411:58: unsupported: instance binder
Lib4/Liquid/ForMathlib/RationalConesSyn.lean:267:-- error in ForMathlib.RationalCones: Mathport/Syntax/Translate/Basic.lean:411:58: unsupported: instance binder
Lib4/Liquid/LiquidSyn.lean:39:-- error in Liquid: Mathport/Syntax/Translate/Basic.lean:411:58: unsupported: instance binder
Lib4/Liquid/PolyhedralLattice/BasicSyn.lean:64:-- error in PolyhedralLattice.Basic: Mathport/Syntax/Translate/Basic.lean:411:58: unsupported: instance binder
Lib4/Liquid/StatementSyn.lean:18:-- error in Statement: Mathport/Syntax/Translate/Basic.lean:411:58: unsupported: instance binder
Lib4/Liquid/Thm95/DefaultSyn.lean:129:-- error in Thm95.Default: Mathport/Syntax/Translate/Basic.lean:411:58: unsupported: instance binder
Lib4/Mathlib/Analysis/Convex/CaratheodorySyn.lean:164:-- error in Analysis.Convex.Caratheodory: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/CategoryTheory/Abelian/PseudoelementsSyn.lean:94:-- error in CategoryTheory.Abelian.Pseudoelements: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/CategoryTheory/EssentiallySmallSyn.lean:25:-- error in CategoryTheory.EssentiallySmall: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/Combinatorics/HalesJewettSyn.lean:176:-- error in Combinatorics.HalesJewett: Mathport/Syntax/Translate/Basic.lean:340:40: in suffices: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/Combinatorics/HalesJewettSyn.lean:255:-- error in Combinatorics.HalesJewett: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/GroupTheory/SubgroupSyn.lean:1390:-- error in GroupTheory.Subgroup: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/GroupTheory/SubgroupSyn.lean:1442:-- error in GroupTheory.Subgroup: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/Order/ExtensionSyn.lean:18:-- error in Order.Extension: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/RingTheory/FinitenessSyn.lean:177:-- error in RingTheory.Finiteness: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/RingTheory/FinitenessSyn.lean:314:-- error in RingTheory.Finiteness: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/RingTheory/Polynomial/DicksonSyn.lean:188:-- error in RingTheory.Polynomial.Dickson: Mathport/Syntax/Translate/Basic.lean:340:40: in obtain: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/Topology/MetricSpace/BasicSyn.lean:648:-- error in Topology.MetricSpace.Basic: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder
Lib4/Mathlib/Topology/MetricSpace/BasicSyn.lean:2316:-- error in Topology.MetricSpace.Basic: Mathport/Syntax/Translate/Basic.lean:477:58: unsupported: instance binder

[Johan Commelin]

Since there's so few of them, I'm inclined to just remove them.

[Johan Commelin]

What is the dubious meaning currently? I can imagine that TC fills in the term, so you don't have to write \<bla, bla, infer_instance, foo, bar\>, but can just write \<bla, bla, foo, bar\>. But at the same time, that feels fragile.

[Mario Carneiro]

That's not what happens currently, I think?

[Mario Carneiro]

I'm pretty sure the binder mode is just ignored

[Johan Commelin]

Ok. So let's just replace [foobar X] with (hX : foobar X) everywhere. That should fix the issue right?

[Scott Morrison]

I'll have a go at the mathlib ones now.

[Scott Morrison]

How about we just replace with (_ : foobar X)?

[Scott Morrison]

Seems to work in the few I've tried.

[Johan Commelin]

Ok, I'll try that in LTE.

[Scott Morrison]

I've got them all except the GroupTheory/SubgroupSyn.lean ones. Do you have the synported file handy? I can go find the latest otherwise.

[Johan Commelin]

Nope, I don't

[Scott Morrison]

I'm downloading the 750mb tarball now!

[Scott Morrison]

#9083, we'll see what CI says, but locally it looks okay so far.

[Johan Commelin]

00980af145fe97427c31ce919b11633dd2c4800c removes instance binders from LTE.

[Mario Carneiro]

We don't actually need to backport it BTW, mathport can normalize this away if we decide we don't care to preserve the distinction

[Mario Carneiro]

but I'm also fine with backporting it in addition

[Mario Carneiro]

But I wonder whether people want to be able to write ∃ [group G], bla even if it doesn't mean anything different from ∃ _ : group G, bla

[Mario Carneiro]

for example, in order to ease refactoring foralls to exists, or just making them more syntactically similar

[Johan Commelin]

I think it's a nice shorthand. But we can add it later. The backport was really easy.

[Sebastian Ullrich]

I have to admit that it looks nice, but since it implies some semantic significance that doesn't actually exist, personally I would advise against allowing it

[Mario Carneiro]

Regarding actually making it mean something, I think this would be hard, since it would entail making Exists.intro change its binder mode when the P argument is a lambda with an instance binder

[Sebastian Ullrich]

Just needs first-class binder kinds :grimacing: