5.7. Conditionals🔗

The conditional expression is used to check whether a proposition is true or false.Despite their syntactic similarity, the Lean.Parser.Tactic.tacIfThenElse : tacticIn tactic mode, `if t then tac1 else tac2` is alternative syntax for: ``` by_cases t · tac1 · tac2 ``` It performs case distinction on `h† : t` or `h† : ¬t`, where `h†` is an anonymous hypothesis, and `tac1` and `tac2` are the subproofs. (It doesn't actually use nondependent `if`, since this wouldn't add anything to the context and hence would be useless for proving theorems. To actually insert an `ite` application use `refine if t then ?_ else ?_`.) if used in the tactic language and the Lean.Parser.Term.doIf : doElemif used in do-notation are separate syntactic forms, documented in their own sections. This requires that the proposition has a Decidable instance, because it's not possible to check whether arbitrary propositions are true or false. There is also a coercion from Bool to Prop that results in a decidable proposition (namely, that the Bool in question is equal to true), described in the section on decidability.

There are two versions of the conditional expression: one simply performs a case distinction, while the other additionally adds an assumption about the proposition's truth or falsity to the local context. This allows run-time checks to generate compile-time evidence that can be used to statically rule out errors.

syntaxConditionals

Without a name annotation, the conditional expression expresses only control flow.

term ::= ...
    | `if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
if term then
        term
      else
        term

With the name annotation, the branches of the termDepIfThenElse : term"Dependent" if-then-else, normally written via the notation `if h : c then t(h) else e(h)`, is sugar for `dite c (fun h => t(h)) (fun h => e(h))`, and it is the same as `if c then t else e` except that `t` is allowed to depend on a proof `h : c`, and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypothesis, even though it has different types in the two cases.) We use this to be able to communicate the if-then-else condition to the branches. For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...` to avoid the bounds check inside the if branch. (Of course in this case we have only lifted the check into an explicit `if`, but we could also use this proof multiple times or derive `i < arr.size` from some other proposition that we are checking in the `if`.) if have access to a local assumption that the proposition is respectively true or false.

term ::= ...
    | "Dependent" if-then-else, normally written via the notation `if h : c then t(h) else e(h)`,
is sugar for `dite c (fun h => t(h)) (fun h => e(h))`, and it is the same as
`if c then t else e` except that `t` is allowed to depend on a proof `h : c`,
and `e` can depend on `h : ¬c`. (Both branches use the same name for the hypothesis,
even though it has different types in the two cases.)

We use this to be able to communicate the if-then-else condition to the branches.
For example, `Array.get arr i h` expects a proof `h : i < arr.size` in order to
avoid a bounds check, so you can write `if h : i < arr.size then arr.get i h else ...`
to avoid the bounds check inside the if branch. (Of course in this case we have only
lifted the check into an explicit `if`, but we could also use this proof multiple times
or derive `i < arr.size` from some other proposition that we are checking in the `if`.)
if `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
h : term then
        term
      else
        term
Checking Array Bounds

Array indexing requires evidence that the index in question is within the bounds of the array, so getThird does not elaborate.

def getThird (xs : Array α) : α := failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid α : Type ?u.7 xs : Array α ⊢ 2 < xs.sizexs[2] 
failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.7
xs : Array α
⊢ 2 < xs.size

Relaxing the return type to Option and adding a bounds check results the same error. This is because the proof that the index is in bounds was not added to the local context.

def getThird (xs : Array α) : Option α := if xs.size ≥ 3 then none else failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid α : Type ?u.7 xs : Array α ⊢ 2 < xs.sizexs[2] 
failed to prove index is valid, possible solutions:
  - Use `have`-expressions to prove the index is valid
  - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid
  - Use `a[i]?` notation instead, result is an `Option` type
  - Use `a[i]'h` notation instead, where `h` is a proof that index is valid
α : Type ?u.7
xs : Array α
⊢ 2 < xs.size

Naming the proof h is sufficient to enable the tactics that perform bounds checking to succeed, even though it does not occur explicitly in the text of the program.

def getThird (xs : Array α) : Option α := if h : xs.size ≥ 3 then none else failed to prove index is valid, possible solutions: - Use `have`-expressions to prove the index is valid - Use `a[i]!` notation instead, runtime check is performed, and 'Panic' error message is produced if index is not valid - Use `a[i]?` notation instead, result is an `Option` type - Use `a[i]'h` notation instead, where `h` is a proof that index is valid α : Type ?u.7 xs : Array α h : ¬xs.size ≥ 3 ⊢ 2 < xs.sizexs[2]

There is also a pattern-matching version of termIfLet : term`if let pat := d then t else e` is a shorthand syntax for: ``` match d with | pat => t | _ => e ``` It matches `d` against the pattern `pat` and the bindings are available in `t`. If the pattern does not match, it returns `e` instead. if. If the pattern matches, then it takes the first branch, binding the pattern variables. If the pattern does not match, then it takes the second branch.

syntaxPattern-Matching Conditionals
term ::= ...
    | `if let pat := d then t else e` is a shorthand syntax for:
```
match d with
| pat => t
| _ => e
```
It matches `d` against the pattern `pat` and the bindings are available in `t`.
If the pattern does not match, it returns `e` instead.
if let term := term then
        term
      else
        term

If a Bool-only conditional statement is ever needed, the boolIfThenElse : term`cond b x y` is the same as `if b then x else y`, but optimized for a boolean condition. It can also be written as `bif b then x else y`. This is `@[macro_inline]` because `x` and `y` should not be eagerly evaluated (see `ite`). bif variant can be used.

syntaxBoolean-Only Conditional
term ::= ...
    | `cond b x y` is the same as `if b then x else y`, but optimized for a
boolean condition. It can also be written as `bif b then x else y`.
This is `@[macro_inline]` because `x` and `y` should not
be eagerly evaluated (see `ite`).
bif term then
        term
      else
        term