Transforming arithmetic expressions into lists of polynomial coefficients in Isabelle. Can't prove algorithm for expressions with multiplication

Question

Introduction

• The datatype for an arithmetic expression is defined as
  datatype exp = Var | Const int | Add exp exp | Mult exp exp
• I am attempting to implement a function, coeffs :: exp ⟹ int list, that transforms an arithmetic expression into its polynomial representation, where the polynomial is represented as a list of its coefficients. For instance, the expression 1+2x would be transformed into [1,2], and x would be transformed into [0,1].
• The challenge I am facing is in proving that the function coeffs preserves the value of the original arithmetic expression
• I am particularly stuck on the case where 'coeffs' operates on 'Mult exp exp'.
• I suspect that the issue may be related to how 'coeffs' is defined for 'Mult exp exp'.
• Objective: I am seeking assistance in completing the proof for the 'coeffs' function and, if necessary, improving the code for polynomial multiplication.

Explanation of Algorithm

coeffs

• This function operates recursively on both addition and multiplication of expressions.

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)"

addcoef

• This function performs the addition of two polynomials by summing the corresponding coefficients from the two lists.

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

• This function handles the multiplication of two polynomials.
• For each coefficient in the first list, it multiplies that coefficient by every coefficient in the second list. The resulting lists are then summed to produce the final polynomial
• To account for the power of each coefficient, a 0 is prepended to the list before multiplication.
  Example
  [1,2] * [3,4] -> [1*3,1*4] + [0,2*3,2*4] ⟹ [3,10,8]
  or equivalently, in polynomial form:
  (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)"

Verifying 'coeffs'
Context:

• The function eval :: exp ⟹ int ⟹ int evaluates an arithmetic expression for a given integer x
• The function evalp :: int list ⟹ int ⟹ int evaluates a polynomial at a given integer x.
• The goal is to prove that the 'coeffs' function preserves the value of the original arithmetic expression

Proof:

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

Proof state:

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

The 'addcoef' case is proved by auto because of the lemma:

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

Trying to use same strategy for 'multcoef', but proof is stuck:

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

state:

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)

Conclusion

• The objective is to prove that the 'coeffs' function operates as intended.
• The proof for 'coeffs' is currently stuck at the 'multcoef' case
• I have already attempted to adapt a similar strategy as used in the 'addcoef' case, but it turns out that proving the 'multcoef' case is not as straightforward
• My hypothesis is that the problem lies in how polynomial multiplication is defined in 'multcoef', which is inherently more complex than polynomial addition as defined in 'addcoef'.

Entire code for reference:

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

There is nothing special in your code. Just standard stuff to do.

1. Do not put ∀ in lemmas for simp rule. This does not work and never will. Just remove them as there are implicitly meta-quantified
2. At various places you want (auto simp: ac_simps ring_distribs) to make sure that auto unfolds the multiplications
3. The rest is the usual question: how would I do this by hand? Right so I need to add this lemma and everything will work