将算术表达式转换为 Isabelle 中的多项式系数列表。无法证明乘法表达式的算法

Question

简介

• 算术表达式的数据类型定义为
  

  datatype exp = Var | Const int | Add exp exp | Mult exp exp

• 我正在尝试实现一个函数

  coeffs :: exp ⟹ int list

  ，它将算术表达式转换为其多项式表示形式，其中多项式表示为其系数列表。例如，表达式 1+2x 将转换为 [1,2]，x 将转换为 [0,1]。
• 我面临的挑战是证明函数

  coeffs

  保留了原始算术表达式的值
• 我特别困惑于“coeffs”对“Mult exp exp”进行操作的情况。
• 我怀疑这个问题可能与“Mult exp exp”的“coeffs”定义方式有关。
• 目标：我正在寻求帮助来完成“coeffs”函数的证明，并在必要时改进多项式乘法的代码。

算法说明

系数

• 此函数对表达式的加法和乘法进行递归操作。

primrec coeffs :: "exp ⇒ int list" where
  "coeffs Var = [0,1]" |
  "coeffs (Const n) = [n]" |
  "coeffs (Add e1 e2) = addcoef (coeffs e1) (coeffs e2)" |
  "coeffs (Mult e1 e2) = multcoef (coeffs e1) (coeffs e2)"

添加系数

• 此函数通过对两个列表中的相应系数求和来执行两个多项式的加法。

fun addcoef :: "int list ⇒ int list ⇒ int list" where
  "addcoef xs [] = xs" |
  "addcoef [] xs = xs" |
  "addcoef (x#xs) (y#ys) = (x + y) # addcoef xs ys"

multicoef

• 此函数处理两个多项式的乘法。
• 对于第一个列表中的每个系数，它将该系数乘以第二个列表中的每个系数。然后对结果列表进行求和以产生最终的多项式
• 为了考虑每个系数的幂，在乘法之前在列表中添加 0。
  示例
  

  [1,2] * [3,4] -> [1*3,1*4] + [0,2*3,2*4] ⟹ [3,10,8]

  
  或等价地，以多项式形式：
  

  (1 + 2x)(3 + 4x) ⟹ 1(3) + 1(4x) + 2x(3) + 2x(4x) ⟹ 3 + 10x + 8x^2

fun multcoef :: "int list ⇒ int list ⇒ int list" where
  "multcoef [] _ = []" |
  "multcoef _ [] = []" |
  "multcoef (x#xs) ys = addcoef (map (λy. x * y) ys) (0 # multcoef xs ys)"

验证“系数”
背景：

• 函数

  eval :: exp ⟹ int ⟹ int

  计算给定整数的算术表达式

  x

• 函数

  evalp :: int list ⟹ int ⟹ int

  计算给定整数

  x

  处的多项式。
• 目标是证明“coeffs”函数保留原始算术表达式的值

证明：

lemma "∀ x. evalp (coeffs e) x = eval e x"
  apply(induction e)
  apply(auto)

证明状态：

proof (prove)
goal (1 subgoal):
 1. ⋀e1 e2 x.
       ⟦∀x. evalp (coeffs e1) x = eval e1 x;
        ∀x. evalp (coeffs e2) x = eval e2 x⟧
       ⟹ evalp (multcoef (coeffs e1) (coeffs e2)) x =
           eval e1 x * eval e2 x

由于引理，“addcoef”案例由

auto

证明：

lemma addcoef_evalp[simp]: "∀ x. evalp (addcoef xs ys) x = evalp xs x + evalp ys x"
  apply(induction xs rule: addcoef.induct)
    apply(simp_all add: algebra_simps)
  done

尝试对“multcoef”使用相同的策略，但证明被卡住了：

lemma multcoef_evalp[simp]: "∀ x. evalp (multcoef xs ys) x = evalp xs x * evalp ys x"
  apply(induction xs rule: multcoef.induct)
  apply(auto)
  oops

状态：

proof (prove)
goal (1 subgoal):
 1. ⋀x xs v va xa.
       ∀x. evalp (multcoef (v # va) xs) x = (v + x * evalp va x) * evalp xs x ⟹ 
    v * x + xa * (evalp (map ((*) v) xs) xa + evalp (multcoef va (x # xs)) xa) =
       (v + xa * evalp va xa) * (x + xa * evalp xs xa)

结论

• 目的是证明“coeffs”函数按预期运行。
• “coeffs”的证明目前停留在“multcoef”情况
• 我已经尝试采用与“addcoef”案例中使用的类似策略，但事实证明证明“multcoef”案例并不那么简单
• 我的假设是，问题在于“multcoef”中如何定义多项式乘法，它本质上比“addcoef”中定义的多项式加法更复杂。

完整代码供参考：

theory pol imports Main
begin

datatype exp = Var | Const int | Add exp exp | Mult exp exp

-- eval: Evaluates an arithmetic expression for a given integer x
primrec eval :: "exp ⇒ int ⇒ int" where
  "eval Var x = x" |
  "eval (Const a) x = a" |
  "eval (Add a b) x = eval a x + eval b x" |
  "eval (Mult a b) x = eval a x * eval b x"

-- evalp: Evaluates a polynomial represented as a list of coefficients for a given integer x
primrec evalp :: "int list ⇒ int ⇒ int" where
  "evalp [] x = 0" |
  "evalp (a#as) x = a + x * evalp as x"

-- addcoef: Adds two polynomials by summing their corresponding coefficients
fun addcoef :: "int list ⇒ int list ⇒ int list" where
  "addcoef xs [] = xs" |
  "addcoef [] xs = xs" |
  "addcoef (x#xs) (y#ys) = (x + y) # addcoef xs ys"

-- multcoef: Multiplies two polynomials by performing a convolution of their coefficients
fun multcoef :: "int list ⇒ int list ⇒ int list" where
  "multcoef [] _ = []" |
  "multcoef _ [] = []" |
  "multcoef (x#xs) ys = addcoef (map (λy. x * y) ys) (0 # multcoef xs ys)"

-- coeffs: Transforms an arithmetic expression into a polynomial represented as a list of coefficients
primrec coeffs :: "exp ⇒ int list" where
  "coeffs Var = [0,1]" |
  "coeffs (Const n) = [n]" |
  "coeffs (Add e1 e2) = addcoef (coeffs e1) (coeffs e2)" |
  "coeffs (Mult e1 e2) = multcoef (coeffs e1) (coeffs e2)"


(* for addcoef_evalp *)
lemma [simp]: "addcoef [] xs = xs"
  apply(induction xs)
   apply(auto)
  done

lemma addcoef_evalp[simp]: "∀ x. evalp (addcoef xs ys) x = evalp xs x + evalp ys x"
  apply(induction xs rule: addcoef.induct)
    apply(simp_all add: algebra_simps)
  done

(* for multcoef_evalp *)
lemma [simp]: "multcoef xs [] = []"
  apply(induction xs)
   apply auto
  done

lemma multcoef_evalp[simp]: "∀ x. evalp (multcoef xs ys) x = evalp xs x * evalp ys x"
  apply(induction xs rule: multcoef.induct)
  apply(auto)
  oops (* stuck here, if this resolved then theorem below fully solved *)

theorem "∀ x. evalp (coeffs e) x = eval e x"
  apply(induction e)
     apply(auto)
  oops

end

Answer 1

您的代码没有什么特别的。只是标准的事情要做。

1. 不要将 ∀ 放在引理中以实现 simpl 规则。这是行不通的，也永远不会行得通。只需删除它们，因为存在隐式元量化
2. 在您想要的各个地方（自动 simp：ac_simps Ring_distribs）确保自动展开乘法
3. 剩下的就是常见问题：我将如何手动完成此操作？是的，所以我需要添加这个引理，一切都会起作用