dite

Stream: new members

[Martin Dvořák]

From TPIL, I know about dite (dependent if-then-else).

def dite (c : Prop) [d : decidable c] {α : Type*}
  (t : c → α) (e : ¬ c → α) : α :=
decidable.rec_on d (λ hnc : ¬ c, e hnc) (λ hc : c, t hc)

However, I don't understand what is the purpose of dite. Can t extract any information from c apart from that it is True?

[Henrik Böving]

The idea behind dite is that you can communicate the fact that what you are branching on is true/false to the branches themselves, if you take a look at the regular ite this is not the case there. This is useful if you for example do a case split on some property h and say the if branch has a function that requires a proof of that property h as a parameter.

[Martin Dvořák]

I don't know whether I understand your reply. Can we use the same function in place of t and e then?

[Kevin Buzzard]

t and e have different types so your last question doesn't seem to make sense

[Yaël Dillies]

Martin Dvořák said:

Can t extract any information from c apart from that it is True?

What else would you want it to extract?

[Martin Dvořák]

Sorry. Then I missed the point.

[Henrik Böving]

Maybe a concrete example would be better here, the following is some Lean 4 code but it conceptually works the same in lean 3:

if h : args = [] then
  IO.println "Missing argument: mode"
  return 1
else
  IO.println s!"Mode is: {args.head h}"
  return 0

If we take a look at the definition of List.head:

def head : (as : List α) → as ≠ [] → α

it requires a proof that the list we want to get the head of is not empty (which makes sense of course). And in this case we obtain this proof by doing a dite on the fact that h : args = [] so by the definition of dite in the else case h is of type args ≠ [] which is precisely what we need in order to obtain the head. And this concept of "passing the fact that the property we are branching on is true/false to the individual branches" is what distinguishes dite from ite.

[Yakov Pechersky]

(deleted)