编辑“︁Lean活性证明”︁（章节）

== Lean中的活性证明方法 ==  

=== 1. 终止性证明 ===  
通过**良基关系**（Well-founded Relation）证明循环或递归的终止：  

<syntaxhighlight lang="lean">  
def factorial : ℕ → ℕ  
| 0 := 1  
| (n+1) := (n+1) * factorial n  

termination_by factorial n => n  -- 显式声明度量标准  
</syntaxhighlight>  

证明结构：  
1. 选择度量函数（如自然数大小）  
2. 证明每次递归调用度量值严格减小  
3. Lean自动验证良基性  

=== 2. 公平性证明 ===  
使用**调度不变式**证明并发系统的公平性：  

<syntaxhighlight lang="lean">  
inductive ScheduleEvent  
| threadA | threadB  

def fair_scheduler (events : List ScheduleEvent) : Prop :=  
  ∀ t, (∃ infinitely_many, events.count t = infinitely_many)  
</syntaxhighlight>  

=== 3. 响应性证明 ===  
通过**状态机归纳**证明系统响应：  

<mermaid>  
stateDiagram-v2  
    [*] --> Idle  
    Idle --> Processing: Request  
    Processing --> Idle: Response  
    Processing --> Processing: Timeout  
</mermaid>  

对应Lean形式化：  
<syntaxhighlight lang="lean">  
inductive SystemState  
| idle | processing  

def responsive (trace : List SystemState) : Prop :=  
  ∀ s ∈ trace, s = SystemState.processing →  
    ∃ later_state ∈ trace, later_state = SystemState.idle  
</syntaxhighlight>