Require Import Arith List Bool. Fixpoint f21 l := match l with nil => 0 | a::l' => a + f21 l' end. Fixpoint f22 l := match l with nil => nil | a::l' => S a::f22 l' end. Definition f22' := map S. Fixpoint f23 (l : list nat) := match l with nil => nil | a::l' => (a::nil)::f23 l' end. Definition f23' := map (fun x : nat => x::nil). Fixpoint f24_a m := match m with 0 => nil | S m' => 0::f24_a m' end. Fixpoint f24 m p := match m, p with 0, _ => nil | S m', 0 => 1::f24_a m' | S m', S p' => 0::f24 m' p' end. Fixpoint f25 l1 l2 := match l1, l2 with nil, l2 => map (fun x:nat => 0) l2 | a::l1', nil => map (fun x:nat => 0) l1 | a::l1', b::l2' => a * b::f25 l1' l2' end. Fixpoint f26_a k l := match l with nil => 0 | a::l' => match k with 0 => a | S k' => f26_a k' l' end end. Fixpoint f26 k ll := match ll with l::ll' => f26_a k l::f26 k ll' | nil => nil end. Definition f26' := fun k => map (fun l => nth k l 0). Compute f26 0 ((1::2::3::nil)::(4::5::6::nil)::(7::nil)::(8::9::nil)::nil::nil). Compute f26' 0 ((1::2::3::nil)::(4::5::6::nil)::(7::nil)::(8::9::nil)::nil::nil). Compute f26 1 ((1::2::3::nil)::(4::5::6::nil)::(7::nil)::(8::9::nil)::nil::nil). Compute f26' 1 ((1::2::3::nil)::(4::5::6::nil)::(7::nil)::(8::9::nil)::nil::nil). Import MinMax. Fixpoint f27 A (l : list (list A)) := match l with nil => 0 | a::tl => max (length a) (f27 A tl) end. Definition f27' A := fold_right (fun (l : list A) => max (length l)) 0. (* For question 8, we assume that all rows have the right length. Thus the number of lines of the matrix is given by the number of lists, and the number of columns is given by the length of the first list. We also assume that the number of rows of the second matrix is the same as the number of columns of the first matrix. *) (* First step, given a number n, create the list of natural numbers 0::...::n-1::nil *) Definition ns n := seq 0 n. Fixpoint mkrow row1 mat l := match l with nil => nil | k::l' => f21 (f25 row1 (f26 k mat))::mkrow row1 mat l' end. Definition mkrow' row1 mat := map (fun k => f21 (f25 row1 (f26 k mat))). Definition mat_mul mat1 mat2 := let row2 := match mat2 with nil => nil | a::_ => a end in let l := ns (length row2) in map (fun x => mkrow x mat2 l) mat1.