编辑“︁Lean引理与推论”︁（章节）

== 实际应用案例 ==

考虑实现一个安全的加密协议验证系统，我们需要证明某些属性：

<syntaxhighlight lang="lean">
-- 定义消息和加密函数
inductive Message
| plain : String → Message
| enc : Key → Message → Message

-- 辅助引理：加密不会改变消息长度
lemma enc_preserves_length (k : Key) (m : Message) :
  (enc k m).length = m.length :=
by cases m; simp [enc, length]

-- 主要安全属性定理
theorem no_length_leakage (k : Key) (m₁ m₂ : Message) :
  m₁.length = m₂.length → (enc k m₁).length = (enc k m₂).length :=
by intro h; simp [enc_preserves_length, h]

-- 实用推论：空消息加密后的长度
corollary enc_empty_length (k : Key) :
  (enc k (Message.plain "")).length = 0 :=
by simp [enc_preserves_length]
</syntaxhighlight>