Prop -> Bool regression

Stream: mathlib4

[Chris Hughes]

Stating things like List.filter and Finset.filter in terms of Bool instead of a decidable Prop seems like a real regression to me in terms of proving theorems. I understand that programmers really want Bool versions, but maybe having Prop versions everywhere in mathlib seems like a good idea. It's so much hassle going between Prop and Bool.

[Johan Commelin]

What are we going to do here?

[Johan Commelin]

Because right now we aren't being consistent

[Johan Commelin]

And that certainly causes a royal boatload of trouble

[Johan Commelin]

@Mario Carneiro There are a lot of rfls that now have to be replaced with simp only [Bool.decide_coe] or simp only [decide_eq_true_eq].

[Mario Carneiro]

I think we should try to use simp lemmas to rewrite bool stuff into prop stuff, and push decide to the leaves so you can use propositional logic wherever possible

[Mario Carneiro]

the problem is that there are some current simp lemmas that are fighting this

[Johan Commelin]

It's not only that, right? It's also that we genuinely have things that used to line up well in ml3, and now no longer line up.

[Johan Commelin]

A rfl or id that stopped working is not because of a simp-lemma going in the wrong direction.

[Mario Carneiro]

like stuff that rewrites b ≠ true ↔ b = false or decide (p ∧ q) = decide p && decide q

[Mario Carneiro]

sure but that's going to happen whenever any definition changes, that's not clearly an indightment

[Johan Commelin]

So: should the definitions change?

[Johan Commelin]

That's what Chris asked at the top of the thread

[Mario Carneiro]

to answer that, we need some examples where the new world is worse than the old world, not just because change is hard

[Johan Commelin]

Or we do the port with List.filterProp and refactor later.

[Mario Carneiro]

If the prop valued version really is better for some use cases then we can make that an official thing. But it's hard to evaluate the examples in this thread alone since they are just general opinions. I totally get the sentiment, and share it to some extent, but it's not enough to make a policy decision one way or another.

[Mario Carneiro]

Also Gabriel's PR to make Decidable a wrapper for a bool may also affect this

[Johan Commelin]

Certainly, all the simp lemmas that change foo = true into bar = false are terrible

[Johan Commelin]

Because many other simp lemmas have a p x = true nested somewhere in their LHS

[Reid Barton]

Actually on the LHS, or in side conditions?

[Johan Commelin]

theorem prod_ite_of_false {p : α → Bool} (f g : α → β) (h : ∀ x ∈ s, ¬p x) :
    (∏ x in s, if p x then f x else g x) = ∏ x in s, g x

[Johan Commelin]

Should this now use bif?

[Johan Commelin]

Otherwise you have a if (p x = true) then ...

[Johan Commelin]

This is one of these places where I'm inclined to say: don't try this refactor while porting. We should either backport this stuff to mathlib3, or do the refactor after porting.

[Johan Commelin]

At that point it's also a lot easier to make a non-sentimental decision.

[Mario Carneiro]

another thing that was floated earlier was to have a IsTrue b function which would be used instead of the current b = true for Bool -> Prop coercion. That would make the expression a bit less "active" since a lot of other stuff keys on equality. For example Chris proposed a simp lemma a = b <-> (a = true <-> b = true) which doesn't really work because it would apply to itself, but it would work if it were spelled using IsTrue

[Mario Carneiro]

Note that this is also (indirectly) what happened in lean 3: since coercions are not unfolded you would get ↑b instead of b = true if you just use a bool for a prop

[Johan Commelin]

If we have p : \a -> Bool, should we write if p x then ... or bif p x then?

[Johan Commelin]

@Mario Carneiro Why do you think introducing IsTrue is better than introducing List.filterProp?

[Mario Carneiro]

For the first question, I have been recommending to use if over bif in anything used for reasoning

[Reid Barton]

IsTrue is one thing while List.filterProp is a zillion things

[Mario Carneiro]

It's not clear to me that filterProp has any fundamental advantages over filter (decide ...), as long as the lemmas are written to advantage this composition

[Johan Commelin]

Reid Barton said:

IsTrue is one thing while List.filterProp is a zillion things

I don't follow. List.filterProp is exactly what we have in Lean 3. So #align whould make things Just Work.

[Johan Commelin]

But right now we have to fix a zillion things.

[Mario Carneiro]

yeah but then we have two versions of everything and they have to interact

[Reid Barton]

But there are hundreds of definitions and lemmas about them that would need to be duplicated (it is not just filter, and not just List)

[Johan Commelin]

Mario Carneiro said:

as long as the lemmas are written to advantage this composition

But I don't know what "the lemmas" are. And clearly they currently haven't been written.

[Mario Carneiro]

the lemmas about filter should be usable without any additional overhead if the filter expression happens to be decide of something

[Mario Carneiro]

I think this is already the case for filter at least

[Yaël Dillies]

Mario Carneiro said:

Note that this is also (indirectly) what happened in lean 3: since coercions are not unfolded you would get ↑b instead of b = true if you just use a bool for a prop

So you're saying we lost the head of the expression in the port, namely coe? Then I agree IsTrue is a good idea, as it will behave like coe in Lean 3.

[Chris Hughes]

There's still a bunch of stuff that's unclear. For example, how should this theorem be stated? Should it be a boolean not, or maybe the statement should take p : α → Prop?

theorem disjoint_filter_filter_neg (s t : Finset α) (p : α → Bool) :
    Disjoint (s.filter p) (t.filter fun a => ¬p a) :=

[Mario Carneiro]

I think using a A -> Prop makes sense in that example

[Mario Carneiro]

a separate version using p and (!p .) also makes sense but I think it would not be the "normal" version

[Johan Commelin]

Should Finset.filter just use Prop?

[Johan Commelin]

Maybe all of Finset/* should just not use Bool.

[Johan Commelin]

If the motivation is whether it is computation-vs-reasoning. I guess Finset is mostly reasoning?

[Reid Barton]

Maybe... Finset should just be a Set together with a proof that it is finite...

[Mario Carneiro]

I think that insofar as Finset is not what Reid just said it should act similarly to list/multiset. But it is quite possible that "finite set" will be overall easier to use for reasoning than finset, as long as rewriting lemmas exist

[Mario Carneiro]

I'm pretty okay with getting away from finset as "computationally relevant" since it is horrible for actual computation

[Reid Barton]

How about for now we revert the multiset and finset API to talk about decidable predicates, since they are not yet in std and aren't very good for computation anyways, so that the Prop/Bool pain is confined to a relatively small number of files

[Mario Carneiro]

That's fine with me, provided that we allow for the possibility of refactoring later when it is moved to std

[Johan Commelin]

Done in mathlib4#1652