13.7. 条件表达式🔗

条件表达式用于检查一个命题是真是假。尽管语法相似，策略语言中使用的 Lean.Parser.Tactic.tacIfThenElse : tacticif 和do 记法中使用的 Lean.Parser.Term.doIf : doElemif 是各自独立的语法形式，并在各自的小节中介绍。这要求该命题具有 Decidable 实例，因为不可能检查任意命题是真是假。从 Bool 到 Prop 还有一个强制转换，它会产生一个可判定命题（即所涉及的 Bool 等于 true）；这在关于可判定性的小节中介绍。

条件表达式有两个版本：一个只进行情况区分，另一个还会向局部上下文中加入关于该命题为真或为假的假设。这使运行时检查能够生成编译时证据，以便静态排除错误。

语法条件表达式

没有名称标注时，条件表达式只表达控制流。

term ::= ...
    | `if c then t else e` 是 `ite c t e`（即“如果—那么—否则”）的记法；它根据 `c` 是否为真返回 `t` 或 `e`。
显式参数 `c : Prop` 本身没有计算内容；另有一个由实例合成得到的 `[Decidable c]` 参数，真正决定如何把 `c` 求值为真或假。
写成 `if h : c then t else e` 时表示依赖式条件 `dite`，此时 `t` 和 `e` 可以使用 `c` 为真或假的事实。

标识符中的记法约定：建议将 `if c then t else e` 写作 `ite`，并分别用 `left`、`right` 指代 `t`、`e`。if term then
        term
      else
        term

有名称标注时，termDepIfThenElse : termif 的两个分支可以分别使用关于该命题为真或为假的局部假设。

term ::= ...
    | if binderIdent : 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.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]

在线查看 ↪

termIfLet : termif 还有一个模式匹配版本。如果模式匹配，就进入第一个分支并绑定模式变量。如果模式不匹配，就进入第二个分支。

语法模式匹配条件表达式

term ::= ...
    | if let term := term then
        term
      else
        term

如果需要只接受 Bool 的条件语句，可以使用 boolIfThenElse : termbif 变体。

语法仅布尔值条件表达式

term ::= ...
    | bif term then
        term
      else
        term