Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Transforming arithmetic expressions into polyn...

Email Gateway (Oct 11 2023 at 12:23):

From: Eero Pomell <eero.the.engineer@gmail.com>
Hi, I'm trying to implement code that transforms an arithmetic expression
into a polynomial which is represented as a list of its coefficients. For
example 1 + 2x + 3x^2 would be [1,2,3], a single variable 'x' would be
[0,1] and a constant 'n' would be [n].

The algorithm works as follows:

• 'coeffs' takes as input an expression and outputs the list, it works
  recursively on complex expressions like 1 + 2x + 3x^2

• 'addcoef' does list addition by adding the corresponding coefficients in
  the two lists, for example the polynomials 1 + 2x and 3 + 4x are [1,2] and
  [3,4], and their addition [1,2] + [3,4] = [4,6], since (1 + 2x) + (3 + 4x)
  = 4 + 6x

• 'multcoef' does list multiplication. For each coefficient in the first
  list, it multiplies by every term in the second list; these lists are then
  added together. For example [1,2] * [3,4] = [13,14] + 0 # [23,24]; It
  works recursively and the '0' is appended to take into account the power of
  the coefficients.

The code that implements the algorithm

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

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"

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

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

The problem
I have these functions for evaluating expressions and polynomials:

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"

primrec evalp :: "int list ⇒ int ⇒ int" where
  "evalp [] x = 0" |
  "evalp (a#as) x = a + x * evalp as x"

I'm trying to prove that coeffs preserves the value of the expression by
proving: lemma "∀ x. evalp (coeffs e) x = eval e x"
I haven't been able to prove the 'multcoef' case.
Here is the code and at the end are details about remaining proof state:

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

(* needed for the main 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

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

(* for main lemma *)
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

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

At the multcoef_evalp, the proof state is:

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)

At the main lemma, the proof state is:

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

Therefore the only thing I have left to prove is the multcoef_evalp lemma.
How could I prove it?

Email Gateway (Oct 11 2023 at 12:34):

From: Wenda Li <wl302@cam.ac.uk>
Hi Eero,

As you are working with univariate polynomials, proofs from HOL-Computational_Algebra.Polynomial (https://isabelle.in.tum.de/dist/library/HOL/HOL-Computational_Algebra/Polynomial.html) might give you some hints about how to progress.

Best,
Wenda

Email Gateway (Oct 16 2023 at 10:08):

From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Hi,

did you study
HOL/Algebra/Polynomials.thy
from the distribution?
A polynomial multiplication is defined there. It could also help you to
understand problems with your own code.
In general, before implementing anything, in particular something as
basic as polynomials, it is a good idea to look at what is already
available.
Both to use it, and to learn.

Stepan

Last updated: Apr 28 2024 at 20:16 UTC