• 06/23 Schedule/ProofCafe_21
• 時間: 14:30 - 17:30
• 場所: 名古屋大学 理学部1号館(多元数理科学棟) 307
• 参加登録: PARTAKE: 第21回 ProofCafe
• ソフトウェアの基礎のポリモルフィズム(多相性)の「練習問題: (apply_exercises)の三つめ override_permute (小川さん担当)」から
• 参加者: 人

演習問題 fold_map

 Definition fold_map {X Y:Type} (f : X -> Y) (l : list X) : list Y :=
  fold (fun x l1 => (f x) :: l1) l [].

Theorem fold_map_correct : forall X Y (f : X-> Y)(l : list X),
  fold_map f l = map f l.
Proof. intros. induction l. 
 Case "l=[]". auto.
 Case "l =x :: l". simpl. rewrite <- IHl. auto.
 Qed.

演習問題 forall_exists_challenge

Definition forallb {X : Type} (f: X -> bool) (l: list X) : bool :=
  fold (fun x b => andb (f x) b) l true.

Definition existsb {X : Type} (f: X -> bool) (l: list X) : bool :=
  fold (fun x b => orb (f x) b) l false.

Definition existsb' {X : Type} (f: X -> bool) (l: list X) : bool :=
  negb (forallb negb (map f l)).