6.7. 条件（Conditionals）🔗

条件式は命題が真か偽かをチェックするために使用されます。構文は似ていますが、 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 はタクティク言語の、 Lean.Parser.Term.doIf : doElemif は do 記法のそれぞれ別の構文形式であり、専用の節で説明されています。条件式は命題が Decidable インスタンスを持っていることを必要とします。なぜなら、 任意の 命題が真か偽であるかチェックすることはできないからです。また Bool から決定可能な命題（すなわち、問題の Bool が true と等しいという命題）の Prop への coercion があり、これは決定可能性の節で説明されています。

条件式には2つのバージョンがあります：1つは単純にケース分割を行うもので、もう1つは命題の真偽に関する仮定をローカルコンテキストに追加するものです。これによって実行時のチェックでコンパイル時の根拠を生成し、それを使って静的にエラーを除外することができます。

syntaxConditionals

名前の注釈が無い場合、条件式はフローの制御のみを表現します。

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

名前の注釈によって、 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 のそれぞれの分岐は命題がそれぞれ真または偽であるというローカルな仮定にアクセスできます。

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

配列の範囲チェック

配列のインデックス付けには、当該インデックスが配列の範囲内にあるという根拠が必要であるため、 getThird はエラボレートしません。

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

戻り値の型を Option に緩和し、範囲チェックを追加しても同じエラーになります。これはインデックスが範囲内にあるという証明がローカルコンテキストに追加されていないためです。

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

証明に h という名前をつけるだけで、たとえプログラムの本文中に明示的に出てこなくても範囲チェックを行うタクティクを成功させることができます。

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]

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 のパターンマッチバージョンも存在します。パターンがマッチした場合、パターンの変数を束縛して最初の分岐が取られます。マッチしない場合は2番目の分岐が取られます。

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

Bool のみの条件文が必要になった場合は、変種の 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 を使用することができます。

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