Instances and proof

Stream: general

[Gihan Marasingha]

If I understand correctly, to prove something in Lean is to find a term of type p, where p is a a term of type Prop. But the type of add_comm_group, for example, is Type u → Type u. So add_comm_group int is not a term of type Prop. Thus, it is meaningless to talk about 'proving' add_comm_group int.

And yet, constructing a term of type add_comm_group int corresponds to what I think of mathematically as proving that the integers form an additive abelian group. Of course, unlike a term of type Prop, we don't have proof irrelevance. It matters what term of type add_comm_group int I construct as there are many different ways to impose an additive abelian group structure on int.

However, if h : add_comm_group int, then the type of h.add_left_neg does have type Prop. So here is a sense in which something is proved by constructing an instance of a type class.

Is there a standard way to express the proof content of finding an instance of a type class? Can one do this in Lean?

[Johan Commelin]

I don't think there is a standard way to do this. But like you said, some fields of add_comm_group have type Type* and others have type Prop. And that's certainly something that Lean can recognize.

[Johan Commelin]

So in principal, one could write a meta program, and if you feed it add_comm_group, then it could tell you: these fields are data, and those fields are properties.

[Adam Topaz]

We probably have something like such a meta program, at least as part of another meta program? For example, how does the @[ext] tag generate ext lemmas?

[Damiano Testa]

I do not know if this is related, but sometimes, the linter complains that something was mislabeled lemma/def and this might have to do with the Type*/Prop distinction?

[Johan Commelin]

That linter complains if you write lemma foobar : X := _ where X is a type, or vice versa def foobar : P := _ where P is a prop.

[Johan Commelin]

But in fact, occasionally lemma foobar : some_type := _ is a useful hack, because it switches on a different elaboration mode. In complicated definitions, I've seen the def-mode get hung up on incomplete definitions that still had _ or sorry in them. Apparently it's trying to figure out whether or not the whole defn should be noncomputable or not, and it doesn't realize that "oh, I don't care, the user isn't even finished with writing the complete def yet; I'll come back to this question tomorrow"

[Kevin Buzzard]

You can't prove add_comm_group int because you don't know the addition, but if you know the data part of the definition then you can make the rest into a prop, e.g.

structure is_add_group (A : Type) [has_add A] [has_zero A] [has_neg A] : Prop :=
(add_assoc : ∀ (a b c : A), a + b + c = a + (b + c))
(zero_add : ∀ (a : A), 0 + a = a)
(add_left_neg : ∀ (a : A), -a + a = 0)

My experience from UG group theory texts is that they often don't think about the identity and inverses as part of the structure, so if you just wanted something which was a Prop and needed only the addition (which of course is essential and not a Prop, the theorem is that $(\mathbb{Z},+)$ is a group, even if we informally say $\Z$ is a group) then you can do something horrible like

structure is_group_structure' (A : Type) [has_add A] : Prop :=
(add_assoc : ∀ (a b c : A), a + b + c = a + (b + c))
(zero_add : ∃! z : A, ∀ b, z + b = b)
(add_left_neg : ∃ neg : A → A, ∀ (a b : A), (neg a + a) + b = b)

but this is a bit more horrible in DTT because you can't get to z computably (which is fair enough, saying it exists is probably not enough information to find it in general)

[Gihan Marasingha]

@Kevin Buzzard your second definition was similar to what I did when I first tried formalising parts of my introductory pure mathematics course, except that I had the conjunction of zero_add and add_zero as a field. I soon abandoned that approach after realising how nasty it was to work with in Lean.

It's interesting how some statements that seem natural in informal mathematics are cumbersome in Lean (and, presumably, vice versa). In this respect, understanding (say) the group concept in informal mathematics is different to understanding the group concept in Lean.

@Jeremy Avigad what do you think?

[Jeremy Avigad]

From an expository point of view, I think it is important to be clear on the distinction between data and proofs, and correspondingly datatypes and propositions). But it is also useful to point out how Lean handles them uniformly by having expressions for both, and even lets you combine them. Finding a group by class inference is a good example -- you are relying on Lean to figure out what the operations are (the data) and also their properties (the proofs). Similarly, the subtype {n // n > 0} is, overall, treated like a data type, but it combines both data and a proof.

You can similarly compare the statements "5 is odd," "there is an odd number," and "there is a unique odd number between 4 and 6." Mathematically, we can produce data from the latter two facts by talking about "some odd number" or "the unique odd number between 4 and 6." Lean can do that too, and I wouldn't too much of a big deal about the distinction here. Both ways of talking about groups are common in the informal literature. It's just that sooner or later we have to talk about "the inverse" and introduce names for it, and if you were coding up a symbolic algebra package you want to provide code to compute inverses.

Overall, I think it is important not to make things more confusing than they are. Talk about the different representations of groups in ordinary mathematical terms, make sure students are clear about that the differences are (and why they are mathematically irrelevant), and then talk about how you could represent them in Lean and why one way might be better than another.

[Kyle Miller]

I wonder if this example of zero_add with its existential quantifier is just a Lean problem -- even in math, algebraic theories seem to be best as equations with free variables, i.e. universally quantified equalities. (I might be biased toward preferring when things can be defined using commutative diagrams.)

[Patrick Massot]

I think it's not Lean-related at all. Especially, trying to define groups without putting the neutral element in the definition is simply cumbersome. Just look at https://en.wikipedia.org/wiki/Group_(mathematics)#Definition. This is a mess featuring a uniqueness claim stuck in the middle of the definition after the second axiom and used in the third axiom. It is much cleaner to put e (and the inversion function) in the package from the beginning and then state that any e' which is also neutral equals e.

[Mario Carneiro]

It just means you have to put the quantifiers in the right order, which means presenting it as a flat list of axioms doesn't work. Incidentally, metamath uses this approach: df-mnd

[Mario Carneiro]

Once the predicate of being a monoid is defined, you can define a function returning "the identity element" and restate the axioms to talk about it, so the definition of a group can use that definition, so it doesn't need to also be nested in the same quantifier

[Mario Carneiro]

One advantage of that approach is that you get that two monoids with the same carrier and multiplication are equal for free

[Patrick Massot]

Sure, there are ways to do it right, but they are not what we teach. Saying "we teach it naturally but surprisingly it becomes painful in Lean" is simply expressing how we lie to ourselves while teaching.

[Mario Carneiro]

but that's not really a disambiguator because both approaches have that theorem in the end. In lean, the real disambiguator is that defeq will hate you if you use choice to extract the identity element, and there is nothing you can do to work around this. This is why even things like gsmul are migrating to fields in lean

[Mario Carneiro]

Saying "we teach it naturally but surprisingly it becomes painful in Lean" is simply expressing how we lie to ourselves while teaching.

I don't follow. Lean is not the source of truth here, mathematics is leading the charge. Lean just made some early design decisions that make certain mathematically equivalent ways of saying this easier than others

[Mario Carneiro]

I believe that teaching how quantifiers work is important in pure mathematics, and presentations using an existential quantifier in axiom 2 that implicitly also scopes over axiom 3 is confusing matters

[Mario Carneiro]

There is a technique in discourse theory called "dynamic quantifiers" that validates this particular pattern, and there is evidence to suggest that you need it all the time to understand natural language mathematics

[Mario Carneiro]

(For example, a mathematical proof might say "Suppose there exists a foo $x$ which is bar. Then x is also quux, ..." where we are referring to $x$ even though the existential quantifier itself only lasts until the end of the first sentence, which in FOL would be a scope error, but with dynamic quantification the existential quantifier expression has another scope that lasts until the end of the paragraph or so and denotes the part of the proof where we have used obtain and are now able to talk about $x$ again.)

[Eric Wieser]

Mario Carneiro said:

One advantage of that approach is that you get that two monoids with the same carrier and multiplication are equal for free

Does mathlib have the non-free version of this result? docs#monoid.ext seems not to exist, which is where I'd expect to find it.

[Mario Carneiro]

That's what it should be called if it existed

[Mario Carneiro]

although I thought someone looked at this a while ago for the algebraic classes

[Mario Carneiro]

I know the order classes have ext lemmas

[Heather Macbeth]

Mario Carneiro said:

There is a technique in discourse theory called "dynamic quantifiers" that validates this particular pattern, and there is evidence to suggest that you need it all the time to understand natural language mathematics

Mario, this sounds very interesting, do you have some recommended reading for it?

[Mario Carneiro]

I learned about it from Ganesalingam's thesis