- 06/23 [Schedule/ProofCafe_21]()
- 時間: 14:30 - 17:30
- 場所: [名古屋大学 理学部1号館(多元数理科学棟)](http://www.math.nagoya-u.ac.jp/ja/direction/campus.html) 307
- 参加登録: [PARTAKE: 第21回 ProofCafe ](http://partake.in/events/a4f91b1a-15c0-419f-abe9-bd030ccfd76e)
- [ソフトウェアの基礎](http://proofcafe.org/sf/)の[ポリモルフィズム(多相性)](http://proofcafe.org/sf/Poly_J.html)の「練習問題: (apply_exercises)の三つめ override_permute (小川さん担当)」から
- 参加者: 9人

# 演習問題 fold_map 
~~~ { .v }
 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
~~~ { .v }
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 (fun x => negb (f x)) l).
~~~

----

~~~
Fixpoint forallb {X : Type} (f: X -> bool) (l: list X) : bool :=
  match l with
    | nil => true
    | x :: xs' => andb (f x) (forallb f xs')
  end.

Fixpoint existsb {X : Type} (f: X -> bool) (l: list X) : bool :=
  match l with
    | nil => false
    | x :: xs' => orb (f x) (existsb f xs')
  end.

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

Require Import Bool.

Theorem forall_exists_challenge:
  forall (A : Type) (p : A -> bool) xs, existsb p xs = existsb' p xs.
Proof.
  intros A p xs.
  induction xs.
    reflexivity.

    unfold existsb'.
    simpl.
    rewrite negb_andb.
    rewrite negb_involutive.
    rewrite IHxs.
    unfold existsb'.
    reflexivity.
Qed.
~~~

# 練習問題 (gen_dep_practice)

~~~{ .v }

Require Import Arith.
Theorem plus_n_n_injective_take2 : forall n m,
     n + n = m + m ->
     n = m.
Proof.
  intros n m. revert n. induction m.
  Case "m=0". simpl. intro. destruct n as [|n'].
    SCase "n=0". reflexivity.
    SCase "n=S n'". intro. inversion H.
  Case "m=S m'". intro. intro. destruct n as [|n'].
    SCase "n=0". inversion H.
    SCase "n=S n'". rewrite (IHm n'). reflexivity. inversion H.
      rewrite <- plus_Snm_nSm in H1.
      rewrite <- plus_Snm_nSm in H1.
      inversion H1.
      reflexivity.
  Qed.
~~~

~~~ { .v }
Theorem index_after_last: forall (n : nat) (X : Type) (l : list X),
     length l = n ->
     index (S n) l = None.
Proof.intros n X l. revert n. induction l.
Case"l=[]". auto.
Case"l=x::l". simpl. intros. 
  rewrite <- H. apply IHl. reflexivity.
Qed.
~~~