dite vs ite

Stream: lean4

[Tomas Skrivan]

What is the purpose of ite if we have dite? Why doesn't normal if statement introduce the hypothesis into the context? I.e. why is normal if statement implemented with ite and not dite?

I am asking because I want to do some rewriting in one of the if branches and if I do not use dite explicitly then tactics do not have access to the if condition.

[Yaël Dillies]

if p then a else b is notation for ite p a b. if h : p then a h else b h is notation for dite p a b. Does that answer your question?

[Patrick Massot]

I don't think it answers his question. He asks why ite exists at all when it's strictly less powerful than dite.

[Patrick Massot]

I'm sure the answer is pretty technical and in an ideal world ite wouldn't exist.

[Ruben Van de Velde]

Yeah, I think it comes down to "dite is somewhat more difficult to work with in practice"

[Yaël Dillies]

The answer is pretty technical but surely you already know it: non-dependent arguments are much easier to rewrite than dependent ones. At any rate, it sounds like Tomas is looking for a congruency lemma. docs#if_congr isn't quite strong enough as I would have expected it to take p -> x = u and not p -> y = v as arguments instead of x = u and y = v.

[Tomas Skrivan]

Yes I'm interested in the technical details. Is there a simple example that demonstrates that working with dite is more difficult than working with ite? Does dite prevent compilers from doing some smart stuff? Something along those lines.

[Tomas Skrivan]

One possible argument: ite c x y would be dite c (fun _ => x) (fun _ => y) and applying rewrite x = x' is a bit more difficult as x is under a binder with dite.

[Mario Carneiro]

yes, the usual situation is that x has some spurious dependency on the fun _ => variable

[Tomas Skrivan]

What do you mean by "spurious dependency"?

[Mario Carneiro]

like fun h => Function.const _ x h only less obvious

[Mario Carneiro]

I mean, if there is a real dependency on the variable then it's not an ite and it will definitely be harder to rewrite, but you are talking about cases which are "in principle" ite applications, so there shouldn't actually be a dependency

[Tomas Skrivan]

But if you write an if statement with ite then there is no dependency, no? Why not convert it immediately to dite without any spurious dependency?

[Mario Carneiro]

From the compiler perspective dite is definitely preferred, and it has to bend over backwards to make sure that ite is unfolded to something with a lambda in it

[Mario Carneiro]

Tomas Skrivan said:

But if you write an if statement with ite then there is no dependency, no? Why not convert it immediately to dite without any spurious dependency?

After some simplifications and rewrites it may not stay that way

[Mario Carneiro]

also, at what stage are you talking about "convert it immediately to dite"? Is ite in the user source?

[Mario Carneiro]

is it there at elaboration time?

[Mario Carneiro]

Another way to find out the answer to this question BTW would be to change the definition of the if then else syntax in core and try to compile lean

[Tomas Skrivan]

Yes probably during elaboration, effectively I'm advocating for getting rid of ite all together

[Mario Carneiro]

actually maybe a more controlled place to try it out would be mathlib, just put

macro_rules | `(if $c then $t else $e) => `(if _ : $c then $t else $e)

in Mathlib.Tactic.Basic

[Tomas Skrivan]

Mario Carneiro said:

Tomas Skrivan said:

But if you write an if statement with ite then there is no dependency, no? Why not convert it immediately to dite without any spurious dependency?

After some simplifications and rewrites it may not stay that way

Well but I can't do those rewrites and simplifications when using ite in the first place. I would have to convert ite to dite, do the rewrites and then the branches will depend on h. That is ok

[Mario Carneiro]

no I mean doing simplifications on a non-dependent lambda might not retain the property of being non-dependent

[Mario Carneiro]

and there are things like assumption that might randomly decide to use the variable just because it's there

[Tomas Skrivan]

I would be curious if this spurious use is really a problem. My expectation is that giving access to that variable to assumption would allow me to do more desirable rewrites.

[Tomas Skrivan]

I'm on the phone right now and I can't test but I'm expecting that if (x != 0) then x/x else 1 does not simplify to 1 but dite version does(or easily can)

[Mario Carneiro]

you assume incorrectly

[Mario Carneiro]

or at least, it is provably equal to 1 and I don't know whether there is a simp lemma for it

[Mario Carneiro]

but you can definitely do conditional rewrites in an ite, this is the docs#if_ctx_congr theorem Yael mentioned before

[Tomas Skrivan]

Wouldn't that work if I run simp with assumptiondischarger and add simple simp lemma if _ : c then x else x = x?

[Tomas Skrivan]

And mark x != 0 -> x/x = 1 as simp lemma which I do not know if it is done or not

[Eric Wieser]

In Lean3 you needed contextual := true to make simp use hypotheses in binders

[Mario Carneiro]

lean 4 as well

[Tomas Skrivan]

Ok I turn on contextual, then it works right? And there is not much hope doing the same with ite

[Mario Carneiro]

there is, you can use contextual congr rules for ite

[Mario Carneiro]

like the one I linked

[Tomas Skrivan]

Right, but I would have to write my own automation or can I use such congruence lemma with simp?

[Mario Carneiro]

there is a @[congr] attribute for these kind of rules

[Mario Carneiro]

at least, as long as we are talking about the system we want to see it is not too hard to posit that this is marked up to work as expected

[Eric Wieser]

In the same way that finset.sum doesn't include the information that the element is in the set, but docs#finset.sum_congr does

[Tomas Skrivan]

Ok, I will look into these congr lemmas, see how they are commonly used and see if I can do what I want.