set theory and order stuff in lean

Stream: general

[Leonard Wiechmann]

Hey all!
Lean newbie here. I worked through the awesome natural number game, and I'm now trying to prove some theorems from a uni course.
The first one is: For all sets A, (powerset A, subset) is a poset.
In mathlib, I found: set_theory.zfc.Set.powerset and init.algebra.order.partial_order.
But this code won't compile because powerset returns a Set, while partial_order expects a Type.

instance {α : Set} : partial_order (Set.powerset α) :=
  sorry

Like I said, I'm new to lean, so I have no idea, whether any of these things are the right tools to prove the "theorem".
I'd really appreciate some help/links!

[Bjørn Kjos-Hanssen]

I think you could get a powerset that is a type using {A : Set // A \subseteq \alpha} (the // is the set-builder symbol for subtype)

[Eric Rodriguez]

So the issue is that set_theory.zfc.Set is the wrong type for what you're looking for; remember from NNG, sets from normal mathematics are replaced by types here. set_theory.zfc.Set is an advanced concept, which is trying to recreate ZFC within Lean, and so is quite complicated. So if you remember that α : Type in Lean basically means let α be a set, you are actually looking for docs#set (the type of all sets made up of the type α) instead, and your instance would instead be phrased as:

instance {α : Type*} : partial_order (set α) := sorry

I hope my comment makes sense to you, I found it confusing whilst writing it ngl

[Leonard Wiechmann]

Thanks @Bjørn Kjos-Hanssen and @Eric Rodriguez!

I tried {A : Set // A \subseteq \alpha}, but that collided with subset.partial_order, which seems to be related to subsets, not powersets.

set does appear to be what I was looking for. https://leanprover.github.io/logic_and_proof/sets_in_lean.html also proved useful.
It is defined as def set (α : Type u) := α → Prop, which I guess means that subsets are defined as predicate functions. I'll have to do some more research on Prop.

Thanks again!

[Eric Rodriguez]

An easy way to think about why set is α → Prop is if you had the "set of all things". (We know that can't exist, but bear with me for a moment). Then, you can describe any set by saying, for each item in the set of all things, whether that item is in your set or not (true if it is, false if it isn't). But in Lean we do have the set of all sets! It's the parent type. But mostly, this is an implementation detail - it's pretty well encouraged here to ignore it :)

[Scott Morrison]

Eric Rodriguez said:

But in Lean we do have the set of all sets! It's the parent type.

This isn't correct. I think perhaps you meant to say "set of all things", like in your first sentence.

[Eric Rodriguez]

Yes, that is what I meant - thanks

[Kevin Buzzard]

To give a subset of X is to give, for every term of type X , the information of whether it's in the subset or not. Thus subsets of X are the same as maps from X to {true,false}

[Leonard Wiechmann]

Some background: One of my motivations for studying lean is that I want to create a dependently typed programming language. Understanding lean is supposed to give me some intuition for type theory before I tackle the HOTT book, or something like that.

Prop is a real puzzler to me. Let me try to explain:
Maps from X to {true, false} make sense, but subsets are defines as maps from X to Prop.
My understanding of Prop is that it is the type of all propositions. And those propositions are again types, and they are "true" if they are inhabited. So unit/true has a single element, but false has none. Similarly, a <= b : Prop is a (dependent) type, and if it is inhabited, that means that a is indeed leq b.
Now, I could define a set of naturals less than some bound: bounded_set := lambda (max : NN) (lambda (n : NN) n <= max)) (this is supposed to mean: given a bound, construct the predicate function from NN to Prop).
The problem is however: For some natural number, the predicate returns me a Prop. But how do I figure out whether that prop is inhabited ("true")?
For example, I might want to do a case distinction between "is in the set" vs "is not". But that now means that I have to "decide the Prop", which, to my understanding, isn't possible because constructive math doesn't have the law of the excluded middle?

Ok, that was a lot. I understand that this isn't a great question. I'm mostly confused, so I don't really know what to ask.. Maybe someone magically understands why I'm confused, of maybe you just have some nice "resources" that I could study to better understand Prop and especially how to "use" Prop.

[Yaël Dillies]

That's what all the decidable/decidable_pred/decidable_rel/decidable_eq stuff is about: A decidability instance gives you a way (understand, an algorithm) to decide whether p : Prop is true or false.

[Eric Wieser]

src#ite (which implements if / then/else on props) and src#decidable might help

[Yaël Dillies]

By "is true or false", I don't mean "is docs#true or docs#false" because those are specific types. What I mean precisely is "is inhabited or p → false is inhabited)

[Leonard Wiechmann]

that actually makes a lot of sense (having a proof/algorithm for deciding a prop)
thanks!

[Kevin Buzzard]

Prop is the type of all propositions, but before you can have a mental model of Prop you need to know what equality of propositions means. For example 2 + 2 = 4 and 3 + 3 = 6 are both strings of characters, so they're definitely not equal at that point. After processing they become Props but if you are trying to get a handle on Prop you need to know whether they're equal or not. And Lean's propositional extensionality axiom says that P = Q <-> (P <-> Q) so because the sums are both (equivalent to) true, they're both equal. The thing which is so rich about Prop is that even though it only has two terms, true and false (assuming we're working in a fixed model of classical mathematics eg ZFC), there are so many ways we have of representing both of them as strings.

[Kevin Buzzard]

Does this help? https://xenaproject.wordpress.com/2020/06/20/mathematics-in-type-theory/

If there was a method to evaluate Props then you just disproved theorems of Goedel and Hilbert I should think. Maths is hard!

[Kevin Buzzard]

In normal maths you are allowed functions for which you don't know the formula -- "the smallest n such that this happens", e.g. if G represents Waring's G function then we're happy to know that 4<=G(3)<=7 because G(3) is just the first time something happens, and we proved it doesn't happen for 3 and that it does happen for 7. In Lean you can make these functions but you can't evaluate them. In constructive maths you can't make them at all until you've proved that their value can be computed in finite time with some algorithm.

[Leonard Wiechmann]

"In normal maths you are allowed functions for which you don't know the formula." Yeah, exactly, and I assumed something like that is also possible in lean.
In particular, I was wondering: If you used lean to do "normal" programming, how would you do a conditional based on a runtime "boolean"? Say,a <= b gives you a Prop, then you have to somehow compute whether it is true or not. For general Props there's no general way to do it (that'd be great, huh?) So <= for (eg) naturals cannot give you "just a Prop"; it needs to give you some extra info to evaluate it.
If I understand correctly, this is what decidable is about: It is an interface, which requires a function, which you can evaluate, to "decide" the corresponding Prop, effectively turning it into a boolean.
(Now, that raises some new questions: What does an actual if expression look like: Do you have to explicitly call the "decider function" - or is there a syntactic convenience if the types are known (eg: naturals)? How is Prop actually represented - is it a symbolic formula until you evaluate it? But I guess I can figure those out myself. If not, I'll start a new "Understanding Prop" thread :P )

There were definitely some terms, like "proof irrelevance" and "lean's propositional extensionality axiom", that I'll look up, thanks!

[Kevin Buzzard]

It's true that there's no algorithm for deciding whether an arbitrary Prop is true or false, but if a and b are computable naturals then there's an algorithm for working out if a<=b

[Reid Barton]

From a computational perspective, a Prop is not represented by anything at all.
if takes an implicit decidable argument which contains the data of whether the proposition is true or false.

[Leonard Wiechmann]

Oh interesting!
Does "computational perspective" mean "implementation" in this case? As in: Is prop simply a type-level construct, that is not processed by the kernel at all?
Though I don't see how that would work for decidable. My current mental model is this: Some expression like a <= b has type Prop and needs to be "decided" to be used as a boolean (done automatically when used in an if). That sounds an awful lot like lazy evaluation. So in this case, one piece of code could "produce" the (decidable) prop a <= b, and some other code, later, could evaluate the prop. In the meantime (implementation wise), the expression a <= b needs to be represented symbolically in some way. Right?
(Links to the c++ source code would be interesting. If they're remotely readable :P )

[Reid Barton]

This is a bit tricky to discuss since there are several meanings that "computation" could have. In your case I assume we're talking about the traditional ideas of compilation and execution. In this case the kernel behaves as a type checker, which is part of the compiler--in the compiler everything is an expression. At run time nothing is an expression, e.g., a value of type nat could be succ (succ zero) but not 1 + 1.

[Reid Barton]

In this model (at least in Lean) propositions are effectively types and, like types, they have no representation at runtime

[Reid Barton]

What happens if you write something like if a <= b then x else y is this:

• if a <= b then x else y really means ite (a <= b) x y and docs#ite needs an argument [decidable (a <= b)]
• Type class inference will synthesize this instance using docs#nat.decidable_le -- this is where the algorithm for deciding the proposition gets chosen
• Now we end up with code that is equivalent to something like match (nat.decidable_le a b) with { is_true _ -> x ; is_false _ -> y }.

So at runtime, all that happens is we use the implementation of nat.decidable_le. But effectively what we have accomplished is to decide the proposition a <= b.

[Leonard Wiechmann]

Ok, that helps a ton, many thanks!
So if I wanted to extract the condition a <= b into a helper function, I'd return a boolean instead of a Prop and "force" the evaluation of nat.decidable_le in the helper?

[Reid Barton]

I think there is a coercion for decidable propositions so you can write (a <= b : bool) if that's what you want--internally it will use the same kind of mechanism