Lean4中如何用自定义定理重写带索引的Finset.sort表达式

需求概述 #

在Lean4策略模式下，需要将目标中的表达式：

(Finset.sort (fun x x_1 => x ≤ x_1)
      (Finset.map { toFun := fun x => p ^ x, inj' := (_ : Function.Injective fun x => p ^ x) }
        (Finset.range (k + 1))))[i]

重写为：

(List.map { toFun := fun x => p ^ x, inj' := (_ : Function.Injective fun x => p ^ x)} 
    (Finset.sort (fun x x_1 => x ≤ x_1)
        (Finset.range (k + 1))))[i]

已证明相关辅助定理，但无法通过rw完成重写，需解决匹配问题。

已证明的辅助定理 #

通用排序-映射交换定理 #

theorem sort_monotone_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] 
 (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] 
  (s : β → β → Prop) [DecidableRel s] [IsTrans β s] [IsAntisymm β s] [IsTotal β s] 
    (f : α ↪ β) (preserve_lt : {x : α} → {y : α} → (h : r x y) → (s (f x) (f y))) 
    (fst : Finset α): Finset.sort s (Finset.map f fst) = List.map f (Finset.sort r fst) := by sorry

质数幂递增性质 #

theorem pow_p_increasing (p : ℕ) (h1 : Nat.Prime p): {x y: ℕ} → x ≤ y → ((⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) x) ≤ ((⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) y) := by sorry

针对质数幂的具体重写定理 #

theorem sort_divisor_thm (p k : ℕ) (h1 : Nat.Prime p) : 
  Finset.sort (. ≤ .) (Finset.map (pow_p p h1) (Finset.range (k + 1))) =
  List.map (⇑(pow_p p h1)) (Finset.sort (. ≤ .) (Finset.range (k + 1))) := 
    sort_monotone_map (. ≤ .) (. ≤ .) (⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) (pow_p_increasing p h1) (Finset.range (k + 1))

完整代码 #

import Mathlib

def sorted_divisors (n : ℕ) : List ℕ := Finset.sort (. ≤ .) (Nat.divisors n) 

def pow_p (p : ℕ) (h1 : Nat.Prime p): ℕ ↪ ℕ := ⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩

theorem pow_p_increasing (p : ℕ) (h1 : Nat.Prime p): {x y: ℕ} → x ≤ y → ((⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) x) ≤ ((⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) y) := by sorry

theorem sort_monotone_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] 
 (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [IsAntisymm α r] [IsTotal α r] 
  (s : β → β → Prop) [DecidableRel s] [IsTrans β s] [IsAntisymm β s] [IsTotal β s] 
    (f : α ↪ β) (preserve_lt : {x : α} → {y : α} → (h : r x y) → (s (f x) (f y))) 
    (fst : Finset α): Finset.sort s (Finset.map f fst) = List.map f (Finset.sort r fst) := by sorry

theorem sort_divisor_thm (p k : ℕ) (h1 : Nat.Prime p) : 
  Finset.sort (. ≤ .) (Finset.map (pow_p p h1) (Finset.range (k + 1))) =
  List.map (⇑(pow_p p h1)) (Finset.sort (. ≤ .) (Finset.range (k + 1))) := 
    sort_monotone_map (. ≤ .) (. ≤ .) (⟨Nat.pow p, Nat.pow_right_injective h1.two_le⟩: ℕ ↪ ℕ) (pow_p_increasing p h1) (Finset.range (k + 1))

theorem desired_goal (p k : ℕ) (h1 : Nat.Prime p) (i : Fin (sorted_divisors (p^k)).length): 
  (sorted_divisors (p^k))[i] = p^(i.val) := by 
  have h := Nat.divisors_prime_pow h1 k
  unfold sorted_divisors
  simp_rw [h]
  --unable to proceed here
  sorry

解决方案 #

无法使用rw的核心原因是目标中的匿名嵌入表达式与定理中使用的pow_p p h1定义不匹配，需先统一表达式结构：

修改后的证明代码 #

theorem desired_goal (p k : ℕ) (h1 : Nat.Prime p) (i : Fin (sorted_divisors (p^k)).length): 
  (sorted_divisors (p^k))[i] = p^(i.val) := by 
  have h := Nat.divisors_prime_pow h1 k
  unfold sorted_divisors
  simp_rw [h]
  -- 1. 将目标中的匿名嵌入转换为pow_p定义，统一表达式结构
  change (Finset.sort (. ≤ .) (Finset.map (pow_p p h1) (Finset.range (k + 1))))[i] = _
  -- 2. 应用自定义定理完成重写
  rw [sort_divisor_thm p k h1]
  -- 3. 利用Mathlib定理简化排序后的range列表
  simp [Finset.sort_range_le]
  -- 4. 应用List.map的下标性质，结合pow_p定义完成证明
  simp [List.map_nth, pow_p]
  rfl

步骤解释 #

1. change调整表达式：目标中的{ toFun := fun x => p ^ x, inj' := (_ : ...) }是pow_p p h1的匿名写法，用change将其显式转换为定义好的pow_p p h1，让表达式结构与sort_divisor_thm的左式完全匹配。
2. rw应用自定义定理：此时结构匹配成功，rw可以正常替换表达式。
3. simp [Finset.sort_range_le]：调用Mathlib定理，将Finset.sort (. ≤ .) (Finset.range (k+1))简化为List.range (k+1)（即[0,1,...,k]）。
4. simp [List.map_nth, pow_p]：List.map_nth保证(List.map f l)[i] = f (l[i])，结合pow_p的定义，最终得到p^(i.val)。

内容的提问来源于stack exchange，提问作者davik