ite.intro

Stream: Is there code for X?

[Yaël Dillies]

Do we not have any introduction rule for ite and dite?

[Yury G. Kudryashov]

What exactly are you looking for?

[Kyle Miller]

Usually ite and dite are just terms, not types, unless the cases are types themselves. Do you mean something like this?

lemma ite.if_true {p q r : Prop} [decidable p] (hp : p) (hq : q) : if p then q else r :=
decidable.rec_on_true hp hq

lemma ite.if_false {p q r : Prop} [decidable p] (hp : ¬p) (hq : r) : if p then q else r :=
decidable.rec_on_false hp hq

These are like constructors if ite had been Prop-valued and an inductive type:

inductive ite' (p q r : Prop) : Prop
| if_true : p → q → ite'
| if_false : ¬p → r → ite'

[Yaël Dillies]

Exactly what I meant was q → r → ite p q r.

[Johan Commelin]

Wouldn't (p → q) → (¬p → r) → ite p q r be more useful/general?

[Yaël Dillies]

Yup it would.

[Yaël Dillies]

The best would be to have both.

[Yury G. Kudryashov]

I can't find it. Feel free to PR both functions (and a dite version of Johan's function).