Lemmata for if_then_else_

[pmbittner]

We used if_then_else_ a lot in one of our projects and it turned out that sometimes these basic lemmata on if_then_else_ are quite useful. While it is typically straightforward to resolve if_then_else_ expressions by pattern matching on the boolean condition instead, sometimes it is convenient to use these lemmata when an if_then_else_ occurs somewhere deep in an equational-reasoning chain.

[Taneb]

Normally we abbreviate idempotent to idem

[gallais]

Is it more of an if-eta?

[pmbittner]

I think if-eta is a good name because it removes the unnecessary if-abstraction. Idempotence might rather be something like the following, which I am going to add:

if-idem : ∀ b {x y : A} → (if b then (if b then x else y) else y) ≡ (if b then x else y)
if-idem false = refl
if-idem true  = refl

[pmbittner]

Ah and this is again rather an if-idem-then and there is also an if-idem-else.

[gallais]

Is it more of an if-eta?

[gallais]

Is this if-swapʳ? Which suggests there's an opportunity for a left version too.

[Taneb]

I'd prefer it was called if-swap-else, there's three sides to every if (and similar for the if-congs below)

[pmbittner]

Ok, I will rename the theorem to if-swap-else, and I will also add the if-swap-then case.

Speaking of the cong-theorems, I noticed that a cong-theorem for the boolean condition is missing, so I am going to add that as well.

[Taneb]

Thinking about it, isn't this just cong (if_then x else y)? And similar for the other cong lemmas. Is it worth including?

[pmbittner]

Yes, it is indeed exactly that.

The benefit of the if-cong lemmas is that we can infer some of the branches automatically with implicit arguments, so we can omit them. That was the reason why I created these cong-lemmas in our project because sometimes we had large expressions in these branches and it was tedious to spell them out. Example:

open import Data.Bool using (if_then_else_)
open import Data.Bool.Properties using (if-cong-else)
open import Data.Nat using (ℕ; _+_)
open import Data.Nat.Properties using (+-comm)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)

looooooong-expression = 1

with-if-cong : ∀ b (x y : ℕ)
  → (if b then looooooong-expression else x + y)
  ≡ (if b then looooooong-expression else y + x)
with-if-cong b x y = if-cong-else b (+-comm x y)

with-cong : ∀ b (x y : ℕ)
  → (if b then looooooong-expression else x + y)
  ≡ (if b then looooooong-expression else y + x)
with-cong b x y = cong (if b then looooooong-expression else_) (+-comm x y)

[pmbittner]

This does not help with all elements within an if_then_else_ though because we still have to spell out the condition (b in the example above).

[JacquesCarette]

Nice.

A lot of these generalize to partitions and piecewise functions. Which I should implement.