Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
(* Exercise 1. Define the function that computes the polynomial 1 + 3 x + 4 x ^ 3 Evaluate this polynomial on the values 1 3 5 20. *) Require Import List. (* Define a list that contains the value 1 3 5 20, and use the map function to compute of the polynomial on all elements of this list. *) (* Redo the same computations using integers of type Z. *) Require Import ZArith. Open Scope Z_scope. (* Define a function that takes four natural numbers as arguments and returns true exactly when these four numbers are given in increasing order (allowing equalities) *) (* Define the same function, but taking integers of type Z as inputs. *) (* Advanced exercises: to be done only if you have reached the end of the other exercises and are still in the exercise period for the first course. *) (* We define vector to be the type list Z, and matrix to be the type list (list Z) *) Definition vector := list Z. Definition matrix := list (list Z). (* We re-use the matrix definitions from the lesson. *) Definition mx_row (M : matrix) (n:nat) : vector := nth n M nil. Definition mx_col (M : matrix) (n:nat) : vector := map (fun row => nth n row 0) M. Definition vec_sum (v : vector) : Z := fold_right Zplus 0 v. Definition pairwise_mult (V1 V2 : vector) : vector := map (fun (p : Z * Z) => let (x,y) := p in x*y) (combine V1 V2). Definition vec_prod (V1 V2 : vector) : Z := vec_sum (pairwise_mult V1 V2). Definition coord_mx (n m:nat) : list (list (nat * nat)) := map (fun i => map (fun j => (i, j)) (seq 0 m)) (seq 0 n). Definition mx_prod (n m p : nat) (M N:matrix) : matrix := map (map (fun t : nat*nat => let (i, j) := t in vec_prod (mx_row M i) (mx_col N j))) (coord_mx n p). (* Define the function that returns the element at coordinates i j of a matrix - ith row, jth column. Call this function val, take the matrix as first argument, and then the coordinates, return 0 if the matrix is ill-formed. *) (* Define the function that returns the diagonal of a matrix, and the trace, in other words, the sum of all elements on the diagonal. Call this function diagonal (use the val function from the previous exercise). *) (* Verify on a few matrices that trace n (mx_prod n n n A B) = trace n (mx_prod n n n B A). *)