Email Gateway (Aug 23 2022 at 08:22): Email Gateway (Aug 23 2022 at 08:22):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Hi,
there is Exercise 2.11 in Concrete Semantics:
Define arithmetic expressions in one variable over integers
(type int) as a data type:
datatype exp = Var | Const int | Add exp exp | Mult exp exp
Define a function eval :: exp ⇒ int ⇒ int such that eval e x evaluates e at
the value x. A polynomial can be represented as a list of coefficients, starting with the
constant. For example, [4, 2, − 1, 3] represents the polynomial 4+2x−x^2 +3x^3 .
Define a function evalp :: int list ⇒ int ⇒ int that evaluates a polynomial at
the given value. Define a function coeffs :: exp ⇒ int list that transforms an
expression into a polynomial. This may require auxiliary functions. Prove that
coeffs preserves the value of the expression: evalp (coeffs e) x = eval e x.
Hint: consider the hint in Exercise 2.10. ›
For now I tried to do without multiplication:
datatype exp = Var | Const int | Add exp exp (* | Mult exp exp *)
fun eval :: "exp ⇒ int ⇒ int" where
"eval Var x = x"
| "eval (Const n) _ = n"
| "eval (Add e1 e2) x = (eval e1 x) + (eval e2 x)"
(* | "eval (Mult e1 e2) x = (eval e1 x) * (eval e2 x)" *)
fun evalp :: "int list ⇒ int ⇒ int" where
"evalp [] v = 0"|
"evalp (p#ps) v = p + v * (evalp ps v) "
fun add_coeffs :: "int list ⇒ int list ⇒ int list" where
"add_coeffs [] [] = []"
| "add_coeffs (a # as) (b# bs) = (a+b) # (add_coeffs as bs)"
| "add_coeffs as [] = as"
| "add_coeffs [] bs = bs"
fun add_coeffs2 :: "int list ⇒ int list ⇒ int list" where
"add_coeffs2 p1 p2 =
(if length p1 ≥ length p2
then (map2 (+) p1 (p2 @ (replicate (length p1 - length p2) 0)))
else add_coeffs2 p2 p1)"
fun coeffs :: "exp ⇒ int list" where
"coeffs (Var) = [0,1]"
| "coeffs (Const n) = [n]"
| "coeffs (Add e1 e2) = add_coeffs (coeffs e1) (coeffs e2)"
Somebody emphasized me the importance of writing good definitions.
I did not get far with neither add_coeffs nor add_coeffs2. The latter I transcribed from Algebra/Polynomials.thy.
For this verification, which one is better and why? Or, some third version should I write?
Email Gateway (Aug 23 2022 at 08:23):From: Tobias Nipkow <nipkow@in.tum.de>
Your add_coeffs is fine, I used it myself and the proofs are all induction-auto.
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:23):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
I could not go through it with auto:
lemma evalp_add: "evalp (add_coeffs (coeffs e1) (coeffs e2)) x = eval e1
x + eval e2 x"
apply (induction e1 arbitrary:e2)
apply (auto simp add:algebra_simps)
lemma evalp_coeffs_eval: "evalp (coeffs e) x = eval e x"
apply (induction e rule:exp.induct)
apply (auto simp add: algebra_simps)
I got some subgoals at evalp_add which auto does not solve.
2020-02-06 09:46 időpontban Tobias Nipkow ezt írta:
Email Gateway (Aug 23 2022 at 08:23):From: Tobias Nipkow <nipkow@in.tum.de>
See Section 2.3.4.
Tobias
smime.p7s
Email Gateway (Aug 23 2022 at 08:23):From: Gergely Buday <buday.gergely@uni-eszterhazy.hu>
Indeed. Thanks. I had to use the rule for add_coeffs. What is the
general method for choosing the induction rule?
Also, when I tried to name the induction variable e1 using rule:
add_coeffs.induct below, Isabelle/JEdit complained about ill-typed
instantiation. Why is that? And, when should I name the variables
besides the induction rule?
2020-02-06 11:30 időpontban Tobias Nipkow ezt írta:
Last updated: Apr 26 2024 at 08:19 UTC