Lean 语言参考手册

22.5. 迭代器推理🔗

22.5.1. 消费者推理🔗

迭代器库提供了大量有用的引理。 大多数关于有限迭代器的定理都可以通过将命题改写为关于列表的命题来证明，因为迭代器组合子与相应列表操作之间的对应关系已经得到证明。 实践中，许多此类定理已经注册为 simp 引理。

这些引理的命名规则非常容易预测，其中许多位于默认化简集中。 其中最重要的包括：

  • Iter.all_toList、Iter.any_toList 和 Iter.foldl_toList 等消费者引理，它们引入列表作为模型。

  • Iter.toList_map 和 Iter.toList_filter 等化简引理，它们把列表模型向目标内部推进。

  • List.toList_iter 和 Array.toList_iter 等生产者引理，它们用列表模型替换生产者，从目标中彻底消除迭代器。

后两类通常可由 simp 自动处理。

通过列表推理

一个迭代器若将从另一迭代器消费的数乘以二，则其返回的每个元素都是偶数。 为证明该命题，可以使用 Iter.all_toList、Iter.toList_map 和 Array.toList_iter 将关于迭代器的命题替换为关于列表的命题，随后由 simp 完成目标：

example (l : Array Nat) : (l.iter.map (· * 2)).all (· % 2 = 0) := l:Array Nat⊢ Iter.all (fun x => decide (x % 2 = 0)) (Iter.map (fun x => x * 2) l.iter) = true l:Array Nat⊢ ((Iter.map (fun x => x * 2) l.iter).toList.all fun x => decide (x % 2 = 0)) = true l:Array Nat⊢ ((List.map (fun x => x * 2) l.iter.toList).all fun x => decide (x % 2 = 0)) = true l:Array Nat⊢ ((List.map (fun x => x * 2) l.toList).all fun x => decide (x % 2 = 0)) = true All goals completed! 🐙

事实上，由于所需的大多数引理都位于默认化简集中，证明可以相当简短：

example (l : Array Nat) : (l.iter.map (· * 2)).all (· % 2 = 0) := l:Array Nat⊢ Iter.all (fun x => decide (x % 2 = 0)) (Iter.map (fun x => x * 2) l.iter) = true All goals completed! 🐙
在线查看 ↪

22.5.2. 逐步推理🔗

当没有足够引理通过改写为列表模型来证明某个性质时，可能需要直接推理迭代器的步骤函数。 本节的归纳原理适用于逐步推理。

🔗定义
Std.Iter.inductSkips.{x, u_1} {α β : Type u_1} [Iterator α Id β]
  [Productive α Id] (motive : Iter β → Sort x)
  (step :
    (it : Iter β) →
      ({it' : Iter β} →
          it.IsPlausibleStep (IterStep.skip it') → motive it') →
        motive it)
  (it : Iter β) : motive it
Std.Iter.inductSkips.{x, u_1}
  {α β : Type u_1} [Iterator α Id β]
  [Productive α Id]
  (motive : Iter β → Sort x)
  (step :
    (it : Iter β) →
      ({it' : Iter β} →
          it.IsPlausibleStep
              (IterStep.skip it') →
            motive it') →
        motive it)
  (it : Iter β) : motive it

能产迭代器的归纳原理：要定义一个把每个迭代器 映射到 motive it 中元素的函数 f，可以依据 f 在 it 的合理跳过后继上的值来定义 f it。

🔗定义
Std.IterM.inductSkips.{x, u_1, u_2} {α : Type u_1}
  {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β]
  [Productive α m] (motive : IterM m β → Sort x)
  (step :
    (it : IterM m β) →
      ({it' : IterM m β} →
          it.IsPlausibleStep (IterStep.skip it') → motive it') →
        motive it)
  (it : IterM m β) : motive it
Std.IterM.inductSkips.{x, u_1, u_2}
  {α : Type u_1} {m : Type u_1 → Type u_2}
  {β : Type u_1} [Iterator α m β]
  [Productive α m]
  (motive : IterM m β → Sort x)
  (step :
    (it : IterM m β) →
      ({it' : IterM m β} →
          it.IsPlausibleStep
              (IterStep.skip it') →
            motive it') →
        motive it)
  (it : IterM m β) : motive it

能产单子式迭代器的归纳原理：要定义一个把每个迭代器 映射到 motive it 中元素的函数 f，可以依据 f 在 it 的合理跳过后继上的值来定义 f it。

🔗定义
Std.Iter.inductSteps.{x, u_1} {α β : Type u_1} [Iterator α Id β]
  [Finite α Id] (motive : Iter β → Sort x)
  (step :
    (it : Iter β) →
      ({it' : Iter β} →
          {out : β} →
            it.IsPlausibleStep (IterStep.yield it' out) → motive it') →
        ({it' : Iter β} →
            it.IsPlausibleStep (IterStep.skip it') → motive it') →
          motive it)
  (it : Iter β) : motive it
Std.Iter.inductSteps.{x, u_1}
  {α β : Type u_1} [Iterator α Id β]
  [Finite α Id] (motive : Iter β → Sort x)
  (step :
    (it : Iter β) →
      ({it' : Iter β} →
          {out : β} →
            it.IsPlausibleStep
                (IterStep.yield it' out) →
              motive it') →
        ({it' : Iter β} →
            it.IsPlausibleStep
                (IterStep.skip it') →
              motive it') →
          motive it)
  (it : Iter β) : motive it

有限迭代器的归纳原理：要定义一个把每个迭代器 映射到 motive it 中元素的函数 f，可以依据 f 在 it 的合理后继上的值来定义 f it。

🔗定义
Std.IterM.inductSteps.{x, u_1, u_2} {α : Type u_1}
  {m : Type u_1 → Type u_2} {β : Type u_1} [Iterator α m β] [Finite α m]
  (motive : IterM m β → Sort x)
  (step :
    (it : IterM m β) →
      ({it' : IterM m β} →
          {out : β} →
            it.IsPlausibleStep (IterStep.yield it' out) → motive it') →
        ({it' : IterM m β} →
            it.IsPlausibleStep (IterStep.skip it') → motive it') →
          motive it)
  (it : IterM m β) : motive it
Std.IterM.inductSteps.{x, u_1, u_2}
  {α : Type u_1} {m : Type u_1 → Type u_2}
  {β : Type u_1} [Iterator α m β]
  [Finite α m]
  (motive : IterM m β → Sort x)
  (step :
    (it : IterM m β) →
      ({it' : IterM m β} →
          {out : β} →
            it.IsPlausibleStep
                (IterStep.yield it' out) →
              motive it') →
        ({it' : IterM m β} →
            it.IsPlausibleStep
                (IterStep.skip it') →
              motive it') →
          motive it)
  (it : IterM m β) : motive it

有限单子式迭代器的归纳原理：要定义一个把每个迭代器 映射到 motive it 中元素的函数 f，可以依据 f 在 it 的合理后继上的值来定义 f it。

标准库还包含描述所有生产者和组合子逐步行为的引理。 例如 List.step_iter_nil、List.step_iter_cons 和 IterM.step_map。

22.5.3. 用于推理的单子🔗

🔗结构体
Std.Iterators.PostconditionT.{w, w'} (m : Type w → Type w')
  (α : Type w) : Type (max w w')
Std.Iterators.PostconditionT.{w, w'}
  (m : Type w → Type w') (α : Type w) :
  Type (max w w')

PostconditionT m α 表示单子 m 中的一项操作，并内蕴地证明某个后置条件对该单子式 α 值结果成立。它由关于 α 的谓词 P 和一个 m ({ a // P a }) 元素组成；在迭代器语境下，它是进行内蕴验证（尤其是终止性证明）的有用工具。

若 m 是单子，则 PostconditionT m 也是单子。但请注意，PostconditionT m α 是结构体，因此编译器会为返回 PostconditionT m α 的递归函数生成低效代码；针对 ReaderT、StateT 等的优化不适用于结构体。

此外，PostconditionT m α 不是行为良好的单子变换器，因为 PostconditionT.lift 既不与 pure 交换，也不与 bind 交换。

构造子

Std.Iterators.PostconditionT.mk.{w, w'}

字段

Property : α → Prop

对 m 单子式操作的返回值成立的谓词。

operation : m (Subtype self.Property)

实际的单子式操作。其返回值与它满足 Property 的证明打包在一起。

🔗定义
Std.Iterators.PostconditionT.run.{w, w'} {m : Type w → Type w'}
  [Monad m] {α : Type w} (x : PostconditionT m α) : m α
Std.Iterators.PostconditionT.run.{w, w'}
  {m : Type w → Type w'} [Monad m]
  {α : Type w} (x : PostconditionT m α) :
  m α

把操作从 PostConditionT m 转换到 m，并丢弃后置条件。

🔗定义
Std.Iterators.PostconditionT.lift.{w, w'} {α : Type w}
  {m : Type w → Type w'} [Functor m] (x : m α) : PostconditionT m α
Std.Iterators.PostconditionT.lift.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  [Functor m] (x : m α) :
  PostconditionT m α

把操作从 m 提升到 PostconditionT m，但不断言任何非平凡的后置条件。

注意：lift 不是合法的提升函数。 例如，pure a : PostconditionT m α 与 PostconditionT.lift (pure a : m α) 并不相同。

🔗定义
Std.Iterators.PostconditionT.liftWithProperty.{w, w'} {α : Type w}
  {m : Type w → Type w'} {P : α → Prop} (x : m { α // P α }) :
  PostconditionT m α
Std.Iterators.PostconditionT.liftWithProperty.{w,
    w'}
  {α : Type w} {m : Type w → Type w'}
  {P : α → Prop} (x : m { α // P α }) :
  PostconditionT m α

把单子式值从 m { a : α // P a } 提升为 PostconditionT m α 值。

🔗归纳谓词
Std.Iter.IsPlausibleIndirectOutput.{w} {α β : Type w}
  [Iterator α Id β] : Iter β → β → Prop
Std.Iter.IsPlausibleIndirectOutput.{w}
  {α β : Type w} [Iterator α Id β] :
  Iter β → β → Prop

断言某个迭代器 it 有可能在任意多步之后合理地发出值 out。

构造子

Std.Iter.IsPlausibleIndirectOutput.direct.{w} {α β : Type w}
  [Iterator α Id β] {it : Iter β} {out : β} :
  it.IsPlausibleOutput out →
    it.IsPlausibleIndirectOutput out

该输出值有可能在下一步被合理地发出。

Std.Iter.IsPlausibleIndirectOutput.indirect.{w}
  {α β : Type w} [Iterator α Id β] {it it' : Iter β}
  {out : β} :
  it'.IsPlausibleSuccessorOf it →
    it'.IsPlausibleIndirectOutput out →
      it.IsPlausibleIndirectOutput out

该输出值有可能在下一步之后的某一步被合理地发出。

🔗结构体
Std.Iterators.HetT.{w, w', v} (m : Type w → Type w') (α : Type v) :
  Type (max v w')
Std.Iterators.HetT.{w, w', v}
  (m : Type w → Type w') (α : Type v) :
  Type (max v w')

若 m 是单子，则 HetT m 是具有以下两个特性的单子：

  • 它把 m 推广到任意宇宙。

  • 它像 PostconditionT 一样，跟踪一个对单子式返回值成立的后置条件性质。

此单子不可计算，仅用于让证明更方便，尤其是迭代器等价性的证明：它避免了宇宙问题，也省去用户手动处理后置条件的工作。

注意：与 PostconditionT 一样，它也不是合法的单子变换器。要从 m 提升到 HetT m，请使用 HetT.lift。

由于此单子从根本上是宇宙多态的，为保持一致，建议始终使用方法 HetT.pure、HetT.map 和 HetT.bind，而不要使用齐次版本 Pure.pure、Functor.map 和 Bind.bind。

构造子

Std.Iterators.HetT.mk.{w, w', v}

字段

Property : α → Prop

对 m 单子式操作的返回值成立的谓词。

small : Std.Internal.Small (Subtype self.Property)

可能的返回值等价于某个 w-小类型的证明。

operation : m (Std.Internal.USquash (Subtype self.Property))

实际的单子式操作。其返回值与它满足 Property 的证明打包，并被压缩到足以放入单子 m 的大小。

🔗定义
Std.IterM.stepAsHetT.{u_1, u_2} {α : Type u_1} {m : Type u_1 → Type u_2}
  {β : Type u_1} [Iterator α m β] [Monad m] (it : IterM m β) :
  HetT m (IterStep (IterM m β) β)
Std.IterM.stepAsHetT.{u_1, u_2}
  {α : Type u_1} {m : Type u_1 → Type u_2}
  {β : Type u_1} [Iterator α m β]
  [Monad m] (it : IterM m β) :
  HetT m (IterStep (IterM m β) β)

使用 HetT 单子的 IterM.step 不可计算变体。它用于定义迭代器上的等价关系，即 IterM.Equiv 和 Iter.Equiv。

🔗定义
Std.Iterators.HetT.lift.{w, w'} {α : Type w} {m : Type w → Type w'}
  [Monad m] (x : m α) : HetT m α
Std.Iterators.HetT.lift.{w, w'}
  {α : Type w} {m : Type w → Type w'}
  [Monad m] (x : m α) : HetT m α

以平凡后置条件把 x : m α 提升到 HetT m α。

注意：这不是合法的单子提升函数。

🔗定义
Std.Iterators.HetT.prun.{u_1, u_2, u_3} {m : Type u_1 → Type u_2}
  {α : Type u_3} {β : Type u_1} [Monad m] (x : HetT m α)
  (f : (a : α) → x.Property a → m β) : m β
Std.Iterators.HetT.prun.{u_1, u_2, u_3}
  {m : Type u_1 → Type u_2} {α : Type u_3}
  {β : Type u_1} [Monad m] (x : HetT m α)
  (f : (a : α) → x.Property a → m β) : m β

将给定函数应用于所含 m 单子式操作的结果，同时提供后置条件性质成立的证明，并返回 m 中的另一个操作。

🔗定义
Std.Iterators.HetT.pure.{w, w', v} {m : Type w → Type w'} [Pure m]
  {α : Type v} (a : α) : HetT m α
Std.Iterators.HetT.pure.{w, w', v}
  {m : Type w → Type w'} [Pure m]
  {α : Type v} (a : α) : HetT m α

Pure.pure 的宇宙异质版本。给定 a : α，它返回一个后置条件为 (a = ·) 的 HetT m α 元素。

🔗定义
Std.Iterators.HetT.map.{w, w', u, v} {m : Type w → Type w'} [Functor m]
  {α : Type u} {β : Type v} (f : α → β) (x : HetT m α) : HetT m β
Std.Iterators.HetT.map.{w, w', u, v}
  {m : Type w → Type w'} [Functor m]
  {α : Type u} {β : Type v} (f : α → β)
  (x : HetT m α) : HetT m β

Functor.map 的宇宙异质版本。

🔗定义
Std.Iterators.HetT.pmap.{w, w', u, v} {m : Type w → Type w'} [Functor m]
  {α : Type u} {β : Type v} (x : HetT m α)
  (f : (a : α) → x.Property a → β) : HetT m β
Std.Iterators.HetT.pmap.{w, w', u, v}
  {m : Type w → Type w'} [Functor m]
  {α : Type u} {β : Type v} (x : HetT m α)
  (f : (a : α) → x.Property a → β) :
  HetT m β

HetT.map 的推广：它把后置条件性质提供给映射函数。

🔗定义
Std.Iterators.HetT.bind.{w, w', u, v} {m : Type w → Type w'} [Monad m]
  {α : Type u} {β : Type v} (x : HetT m α) (f : α → HetT m β) : HetT m β
Std.Iterators.HetT.bind.{w, w', u, v}
  {m : Type w → Type w'} [Monad m]
  {α : Type u} {β : Type v} (x : HetT m α)
  (f : α → HetT m β) : HetT m β

Bind.bind 的宇宙异质版本。

🔗定义
Std.Iterators.HetT.pbind.{w, w', u, v} {m : Type w → Type w'} [Monad m]
  {α : Type u} {β : Type v} (x : HetT m α)
  (f : (a : α) → x.Property a → HetT m β) : HetT m β
Std.Iterators.HetT.pbind.{w, w', u, v}
  {m : Type w → Type w'} [Monad m]
  {α : Type u} {β : Type v} (x : HetT m α)
  (f :
    (a : α) → x.Property a → HetT m β) :
  HetT m β

HetT.bind 的推广：它把后置条件性质提供给映射函数。

22.5.4. 等价性🔗

迭代器等价性依据迭代器的可观察行为定义，而非依据其实现。 尤其是，内部状态会被忽略。

🔗定义
Std.Iter.Equiv.{u_1} {α₁ α₂ β : Type u_1} [Iterator α₁ Id β]
  [Iterator α₂ Id β] (ita : Iter β) (itb : Iter β) : Prop
Std.Iter.Equiv.{u_1} {α₁ α₂ β : Type u_1}
  [Iterator α₁ Id β] [Iterator α₂ Id β]
  (ita : Iter β) (itb : Iter β) : Prop

迭代器上的等价关系。只要不直接检查内部状态，等价迭代器的行为就相同。

两个迭代器（类型可以不同）等价，当且仅当它们具有相同的 Iterator.IsPlausibleStep 关系，并且其步进函数相同——这里后继迭代器只要求在等价意义下相同。这个余归纳定义刻画了如下思想：迭代器唯一相关的特征是其步进函数。能从迭代器取得的其他信息——例如它是列表迭代器还是数组迭代器——对等价性判断完全无关。

🔗定义
Std.IterM.Equiv.{w, w'} {m : Type w → Type w'} [Monad m] [LawfulMonad m]
  {β α₁ α₂ : Type w} [Iterator α₁ m β] [Iterator α₂ m β]
  (ita : IterM m β) (itb : IterM m β) : Prop
Std.IterM.Equiv.{w, w'}
  {m : Type w → Type w'} [Monad m]
  [LawfulMonad m] {β α₁ α₂ : Type w}
  [Iterator α₁ m β] [Iterator α₂ m β]
  (ita : IterM m β) (itb : IterM m β) :
  Prop

单子式迭代器上的等价关系。只要不直接检查内部状态，等价迭代器的行为就相同。

两个迭代器（类型可以不同）等价，当且仅当它们具有相同的 Iterator.IsPlausibleStep 关系，并且其步进函数相同——这里后继迭代器只要求在等价意义下相同。这个余归纳定义刻画了如下思想：迭代器唯一相关的特征是其步进函数。能从迭代器取得的其他信息——例如它是列表迭代器还是数组迭代器——对等价性判断完全无关。