Lean 语言参考

13.7. 条件句🔗

条件表达式用于检查命题是真还是假。尽管语法相似，但 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 ?_`.) The assumptions in each subgoal can be named. `if h : t then tac1 else tac2` can be used as alternative syntax for: ``` by_cases h : t · tac1 · tac2 ``` It performs case distinction on `h : t` or `h : ¬t`. You can use `?_` or `_` for either subproof to delay the goal to after the tactic, but if a tactic sequence is provided for `tac1` or `tac2` then it will require the goal to be closed by the end of the block. if 使用 在策略语言中，而 Lean.Parser.Term.doIf : doElemif 使用 在do-notation 是单独的语法形式，记录在它们自己的部分中。 这要求该命题具有 Decidable 实例，因为无法检查任意命题是真还是假。 还有一个从 Bool 到 Prop 的 强制，它会产生可判定的命题（即，所讨论的 Bool 等于 true），如 关于可判定性的部分中所述。

条件表达式有两种版本：一种仅执行大小写区分，而另一种则另外在本地上下文中添加有关命题真假的假设。 这允许运行时检查生成可用于静态排除错误的编译时证据。

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.
binderIdent : term then
        term
      else
        term
Checking Array Bounds

数组索引需要证据证明相关索引在数组范围内，因此 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.3xs: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.3xs:Array α⊢ 2 < xs.size

将返回类型放宽为 Option 并添加边界检查会导致相同的错误。 这是因为索引在边界内的证明没有添加到本地上下文中。

def getThird (xs : Array α) : Option α := if xs.size ≤ 2 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.3xs: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.3xs:Array α⊢ 2 < xs.size

将证明命名为 h 足以使执行边界检查的策略成功，即使它没有在程序文本中明确出现。

def getThird (xs : Array α) : Option α := if h : xs.size ≤ 2 then none else xs[2]
Live ↪

还有 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 的模式匹配版本。 如果模式匹配，则它采用第一个分支，绑定模式变量。 如果模式不匹配，则采用第二个分支。

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 : termThe conditional function. `cond c x y` is the same as `if c then x else y`, but optimized for a Boolean condition rather than a decidable proposition. It can also be written using the notation `bif c then x else y`. Just like `ite`, `cond` is declared `@[macro_inline]`, which causes applications of `cond` to be unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and only the selected branch is evaluated. bif 变体。

syntaxBoolean-Only Conditional
term ::= ...
    | The conditional function.

`cond c x y` is the same as `if c then x else y`, but optimized for a Boolean condition rather than
a decidable proposition. It can also be written using the notation `bif c then x else y`.

Just like `ite`, `cond` is declared `@[macro_inline]`, which causes applications of `cond` to be
unfolded. As a result, `x` and `y` are not evaluated at runtime until one of them is selected, and
only the selected branch is evaluated.
bif term then
        term
      else
        term