List.v

Require Export Basics.

Module NatList.
  Inductive natprod: Type :=
    pair : nat -> nat -> natprod.

  Definition fst (p: natprod): nat :=
    match p with pair x y => x end.

  Definition snd (p: natprod): nat :=
    match p with pair x y => y end.

  Notation "( x , y )" := (pair x y).

  Eval simpl in (fst (3,4)).

  Definition fst' (p: natprod): nat :=
    match p with (x,y) => x end.

  Definition snd' (p: natprod): nat :=
    match p with (x,y) => y end.

  Definition swap_pair (p: natprod): natprod :=
    match p with (x, y) => (y,x) end.


  Theorem surjective_parsing': forall (n m: nat),
    (n,m) = (fst (n,m), snd (n,m)).
  Proof.
    intros.
    simpl.
    reflexivity.
  Qed.

  Theorem surjective_parsing: forall p: natprod,
    p = (fst p, snd p).
  Proof.
    intros p.
    destruct p as (n,m).
    simpl.
    reflexivity.
  Qed.

  (* Ex. snd_fst_is_swap *)
  Theorem snd_fst_is_swap: forall p: natprod,
    (snd p, fst p) = swap_pair p.
  Proof.
    intros p.
    destruct p as (n,m).
    simpl.
    reflexivity.
  Qed.


  (* 数のリスト *)
  Inductive natlist: Type :=
    | nil: natlist
    | cons: nat -> natlist -> natlist.

  Definition l_123 := cons 1 (cons 2 (cons 3 nil)).

  Notation "x :: l" := (cons x l) (at level 60, right associativity).
  Notation "[ ]" := nil.
  Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

  (* リスト操作関数 *)
  Fixpoint repeat (n count: nat): natlist :=
    match count with
      | O => nil
      | S count' => n :: (repeat n count')
    end.

  Fixpoint length (list: natlist): nat :=
    match list with
      | nil => O
      | head :: tail => S (length tail)
    end.

  Fixpoint app (lhs rhs: natlist): natlist :=
    match lhs with
      | nil => rhs
      | head :: tail => head :: (app tail rhs)
    end.

  Notation "x ++ y" := (app x y) (at level 60, right associativity).

  Example test_app1: [1,2,3] ++ [4,5] = [1,2,3,4,5].
  Proof. simpl. reflexivity. Qed.
  Example test_app2: nil ++ [4,5] = [4,5].
  Proof. reflexivity. Qed.
  Example test_app3: [1,2,3] ++ nil = [1,2,3].
  Proof. reflexivity. Qed.


  Definition hd (default: nat) (list: natlist): nat :=
    match list with
      | nil => default
      | head :: tail => head
    end.

  Definition tail (list: natlist): natlist :=
    match list with
      | nil => nil
      | head :: tail => tail
    end.

  Example test_hd1: hd 0 [1,2,3] = 1.
  Proof. reflexivity. Qed.
  Example test_hd2: hd 0 [] = 0.
  Proof. reflexivity. Qed.
  Example test_tail: tail [1,2,3] = [2,3].
  Proof. reflexivity. Qed.

  (* Ex. list_funs *)
  Fixpoint nonzeros (l: natlist): natlist :=
    match l with
      | nil => nil
      | 0 :: t => nonzeros t
      | h :: t => h :: nonzeros t
    end.
  Example test_nonzeros: nonzeros [0,1,0,2,3,0,0] = [1,2,3].
  Proof. reflexivity. Qed.

  Fixpoint oddmembers (l:natlist) : natlist :=
    match l with
      | nil => nil
      | h :: t =>
        match oddb h with
          | true => h :: oddmembers t
          | false => oddmembers t
        end
    end.
  Example test_oddmembers: oddmembers [0,1,0,2,3,0,0] = [1,3].
  Proof. reflexivity. Qed.

  Fixpoint countoddmembers (l:natlist) : nat :=
    length (oddmembers l).
  Example test_countoddmembers1: countoddmembers [1,0,3,1,4,5] = 4.
  Proof. reflexivity. Qed.
  Example test_countoddmembers2: countoddmembers [0,2,4] = 0.
  Proof. reflexivity. Qed.
  Example test_countoddmembers3: countoddmembers nil = 0.
  Proof. reflexivity. Qed.


  (* リストを使ったバッグ *)
  Definition bag := natlist.

  (* Ex. bag_functions *)
  Fixpoint count (v: nat) (s: bag): nat :=
    match s with
      | nil => 0
      | h :: t =>
        match beq_nat v h with
          | true => 1 + count v t
          | false => count v t
        end
    end.
  Example test_count1: count 1 [1,2,3,1,4,1] = 3.
  Proof. reflexivity. Qed.
  Example test_count2: count 6 [1,2,3,1,4,1] = 0.
  Proof. reflexivity. Qed.

  Definition sum : bag -> bag -> bag := app.
  Example test_sum1: count 1 (sum [1,2,3] [1,4,1]) = 3.
  Proof. reflexivity. Qed.

  Definition add: nat -> bag -> bag := cons.

  Example test_add1: count 1 (add 1 [1,4,1]) = 3.
  Proof. reflexivity. Qed.
  Example test_add2: count 5 (add 1 [1,4,1]) = 0.
  Proof. reflexivity. Qed.

  Definition member (v:nat) (s:bag) : bool :=
    blt_nat 0 (count v s).

  Example test_member1: member 1 [1,4,1] = true.
  Proof. reflexivity. Qed.
  Example test_member2: member 2 [1,4,1] = false.
  Proof. reflexivity. Qed.


  (* Ex. bag_more_functions *)
  Fixpoint remove_one (v:nat) (s:bag) : bag :=
    match s with
      | nil => nil
      | h :: t =>
        match beq_nat v h with
          | true => t
          | false => h :: remove_one v t
        end
    end.
  Example test_remove_one1: count 5 (remove_one 5 [2,1,5,4,1]) = 0.
  Proof. reflexivity. Qed.
  Example test_remove_one2: count 5 (remove_one 5 [2,1,4,1]) = 0.
  Proof. reflexivity. Qed.
  Example test_remove_one3: count 4 (remove_one 5 [2,1,4,5,1,4]) = 2.
  Proof. reflexivity. Qed.
  Example test_remove_one4:
    count 5 (remove_one 5 [2,1,5,4,5,1,4]) = 1.
  Proof. reflexivity. Qed.

  Fixpoint remove_all (v:nat) (s:bag) : bag :=
    match s with
      | nil => nil
      | h :: t =>
        match beq_nat v h with
          | true => remove_all v t
          | false => h :: remove_all v t
        end
    end.


  Example test_remove_all1: count 5 (remove_all 5 [2,1,5,4,1]) = 0.
  Proof. reflexivity. Qed.
  Example test_remove_all2: count 5 (remove_all 5 [2,1,4,1]) = 0.
  Proof. reflexivity. Qed.
  Example test_remove_all3: count 4 (remove_all 5 [2,1,4,5,1,4]) = 2.
  Proof. reflexivity. Qed.
  Example test_remove_all4: count 5 (remove_all 5 [2,1,5,4,5,1,4,5,1,4]) = 0.
  Proof. reflexivity. Qed.

  Fixpoint subset (s1:bag) (s2:bag) : bool :=
    match s1 with
      | nil => true
      | h :: t => andb (member h s2) (subset t (remove_one h s2))
    end.

  Example test_subset1: subset [1,2] [2,1,4,1] = true.
  Proof. reflexivity. Qed.
  Example test_subset2: subset [1,2,2] [2,1,4,1] = false.
  Proof. reflexivity. Qed.


  (* Ex. bag_theorem: バッグに関する面白い定理をつくれ *)
  Lemma add_hd: forall (n: nat) (b: bag), add n b = n :: b.
  Proof. reflexivity. Qed.

  Lemma count_single: forall n: nat, count n [n] = 1.
  Proof.
    intros.
    induction n.
    reflexivity.
    simpl.
    rewrite <- beq_nat_refl.
    reflexivity.
  Qed.

  Theorem add_count: forall (n: nat) (b: bag), count n (add n b) = 1 + count n b.
  Proof.
    intros.
    induction n.
    reflexivity.
    simpl.
    rewrite <- beq_nat_refl.
    reflexivity.
  Qed.

  Theorem add_remove: forall (n: nat) (b: bag), b = remove_one n (add n b).
  Proof.
    intros.
    induction n.
    reflexivity.
    simpl.
    rewrite <- beq_nat_refl.
    reflexivity.
  Qed.

  (* リストに関する推論 *)
  Theorem nil_app: forall l: natlist, l = [] ++ l.
  Proof. reflexivity. Qed.

  Theorem tl_length_pred: forall l: natlist,
    pred (length l) = length (tail l).
  Proof.
    intros l.
    destruct l as [|n l'].
    Case "l = nil".
      reflexivity.
    Case  "l = n :: l '".
      reflexivity.
  Qed.


  (* リスト上の帰納法 *)
  Theorem app_ass : forall l1 l2 l3 : natlist,
    (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
  Proof.
    intros l1 l2 l3. induction l1 as [| n l1'].
    Case "l1 = nil".
      reflexivity.
    Case "l1 = cons n l1'".
      simpl.
      rewrite -> IHl1'.
      reflexivity.
  Qed.


  Theorem app_length : forall l1 l2 : natlist,
     length (l1 ++ l2) = (length l1) + (length l2).
  Proof.
    intros l1 l2.
    induction l1 as [| n l1'].
    Case "l1 = nil".
      reflexivity.
    Case "l1 = cons".
      simpl.
      rewrite -> IHl1'.
      reflexivity.
  Qed.


  Fixpoint snoc (l:natlist) (v:nat) : natlist :=
    (* 末尾に要素を追加 *)
    match l with
      | nil => [v]
      | h :: t => h :: (snoc t v)
    end.

  Fixpoint rev(l: natlist): natlist :=
    match l with
      | nil => nil
      | h :: t => snoc (rev t) h
    end.

  Lemma length_snoc: forall n: nat, forall l: natlist,
     length (snoc l n) = S (length l).
  Proof.
    intros n l.
    induction l.
    Case "nil".
      reflexivity.
    Case "n0 :: l".
      simpl.
      rewrite -> IHl.
      reflexivity.
  Qed.

  Theorem rev_length: forall l: natlist,
     length (rev l) = length l.
  Proof.
    intros l.
    induction l.
    Case "nil".
      reflexivity.
    Case "n :: l".
      simpl.
      rewrite -> length_snoc.
      rewrite -> IHl.
      reflexivity.
  Qed.


  (* 関数や型について定義や証明を一覧する *)
  SearchAbout add.
  SearchAbout bit.


  (* リストについての練習問題(1) *)
  Theorem app_nil_end: forall l: natlist,
    l ++ [] = l.
  Proof.
    intros l.
    induction l.
    Case "nil".
      reflexivity.
    Case "n :: l".
      simpl.
      rewrite -> IHl.
      reflexivity.
  Qed.

  Lemma snoc_append: forall n: nat, forall l: natlist,
    snoc l n = l ++ [n].
  Proof.
    intros.
    induction l.
    reflexivity.
    simpl.
    rewrite -> IHl.
    reflexivity.
  Qed.

  Lemma snoc_rev: forall n: nat, forall l: natlist,
    snoc (rev l) n = rev l ++ [n].
  Proof.
    intros.
    destruct l.
    Case "nil".
      reflexivity.
    Case "n0 :: l".
      simpl.
      rewrite -> snoc_append.
      reflexivity.
  Qed.

  Theorem distr_rev: forall a b: natlist,
    rev (a ++ b) = rev b ++ rev a.
  Proof.
    intros.
    induction a.
    Case "nil".
      simpl.
      rewrite -> app_nil_end.
      reflexivity.
    Case "n :: a".
      simpl.
      rewrite -> snoc_rev.
      rewrite -> IHa.
      rewrite -> app_ass.
      rewrite -> snoc_rev.
      reflexivity.
  Qed.

  Theorem rev_involutive : forall l : natlist,
    rev (rev l) = l.
  Proof.
    intros l.
    induction l.
    Case "nil".
      reflexivity.
    Case "n :: l".
      simpl.
      rewrite -> snoc_rev.
      rewrite -> distr_rev.
      rewrite -> IHl.
      simpl.
      reflexivity.
  Qed.

  Theorem app_ass4 : forall l1 l2 l3 l4 : natlist,
    l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4.
  Proof.
    intros.
    rewrite -> app_ass.
    rewrite -> app_ass.
    reflexivity.
  Qed.

  Lemma nonzeros_length : forall l1 l2 : natlist,
    nonzeros (l1 ++ l2) = (nonzeros l1) ++ (nonzeros l2).
  Proof.
    intros.
    induction l1.
    Case "nil".
      simpl.
      reflexivity.
    Case "n :: l1".
      simpl.
      rewrite -> IHl1.
      destruct n.
      SCase "0".
        reflexivity.
      SCase "S n".
        simpl.
        reflexivity.
  Qed.

  (* リストについての練習問題2 *)

  (* Ex. list_design *)
  Theorem cons_snoc_app: forall (n: nat) (l: natlist),
    snoc l n ++ l = l ++ n :: l.
  Proof.
    intros.
    rewrite -> snoc_append.
    rewrite -> app_ass.
    reflexivity.
  Qed.

  Theorem rev_app_comm: forall (n: nat) (l: natlist),
    rev (l ++ [n]) = n :: rev l.
  Proof.
    intros.
    apply distr_rev.
  Qed.

  Theorem rev_cons_comm: forall (n: nat) (l: natlist),
    rev (n :: l) = rev l ++ [n].
  Proof.
    intros.
    simpl.
    apply snoc_rev.
  Qed.


  (* Ex. bag_proofs *)
  Theorem count_member_nonzero: forall s: bag,
    ble_nat 1 (count 1 (1 :: s)) = true.
  Proof.
    reflexivity.
  Qed.


  Theorem ble_n_Sn : forall n,
    ble_nat n (S n) = true.
  Proof.
    intros n.
    induction n as [| n'].
    Case "0".
      simpl. reflexivity.
    Case "S n'".
      simpl.
      rewrite -> IHn'.
      reflexivity.
  Qed.

  Theorem remove_decreases_count : forall (s : bag),
    ble_nat (count 0 (remove_one 0 s)) (count 0 s) = true.
  Proof.
    intro s;
    induction s as [| n s'].
    Case "s = []".
      reflexivity.
    Case "s = n::s'".
      simpl.
      destruct n as [| n'].
      SCase "n = 0".
        apply ble_n_Sn.
      SCase "n = S n'".
        simpl.
        exact IHs'.
  Qed.

  (* Ex. rev_injective *)
  Theorem eq_arrow: forall a b c: natlist,
    a = b -> a = c -> b = c.
  Proof.
    intros.
    rewrite <- H.
    rewrite <- H0.
    reflexivity.
  Qed.

  Theorem rev_injective:
    forall (l1 l2: natlist), rev l1 = rev l2 -> l1 = l2.
  Proof.
    intros.
    rewrite <- rev_involutive.
    rewrite <- H.
    rewrite -> rev_involutive.
    reflexivity.
  Qed.


  (* Option *)
  Inductive natoption : Type :=
    | Some : nat -> natoption
    | None : natoption.

  Fixpoint index (n: nat) (l: natlist): natoption :=
    match l with
      | nil => None
      | a :: l' =>
        match beq_nat n O with
          | true => Some a
          | false => index (pred n) l'
        end
    end.
  Example test_index1 : index 0 [4,5,6,7] = Some 4.
  Proof. reflexivity. Qed.
  Example test_index2 : index 3 [4,5,6,7] = Some 7.
  Proof. reflexivity. Qed.
  Example test_index3 : index 10 [4,5,6,7] = None.
  Proof. reflexivity. Qed.

  (* 条件式 if の使い方 *)
  Fixpoint index' (n:nat) (l:natlist) : natoption :=
    match l with
      | nil => None
      | a :: l' =>
        if beq_nat n O
        then Some a
        else index (pred n) l'
    end.


  Definition option_elim (o : natoption) (d : nat) : nat :=
    match o with
      | Some n' => n'
      | None => d
    end.


  (* Ex. hd_opt *)
  Definition hd_opt (l : natlist) : natoption :=
    match l with
      | nil => None
      | h :: t => Some h
    end.
  Example test_hd_opt1 : hd_opt [] = None.
  Proof. reflexivity. Qed.
  Example test_hd_opt2 : hd_opt [1] = Some 1.
  Proof. reflexivity. Qed.
  Example test_hd_opt3 : hd_opt [5,6] = Some 5.
  Proof. reflexivity. Qed.


  (* Ex. option_elim_hd *)
  Theorem option_elim_hd:
    forall (l: natlist) (default: nat),
      hd default l = option_elim (hd_opt l) default.
  Proof.
    intros.
    destruct l.
    reflexivity.
    reflexivity.
  Qed.

  (* Ex. beq_natlist *)
  Fixpoint beq_natlist (l1 l2: natlist): bool :=
    match l1, l2 with
      | nil, nil => true
      | nil, _ => false
      | _, nil => false
      | h1::t1, h2::t2 => andb (beq_nat h1 h2) (beq_natlist t1 t2)
    end.
  Example test_beq_natlist1 : (beq_natlist nil nil = true).
  Proof. reflexivity. Qed.
  Example test_beq_natlist2 : beq_natlist [1,2,3] [1,2,3] = true.
  Proof. reflexivity. Qed.
  Example test_beq_natlist3 : beq_natlist [1,2,3] [1,2,4] = false.
  Proof. reflexivity. Qed.

  Theorem beq_natlist_refl : forall l:natlist,
    true = beq_natlist l l.
  Proof.
    intros.
    induction l.
    Case "nil".
      reflexivity.
    Case "n :: l".
      induction n.
      SCase "0".
        rewrite -> IHl.
        reflexivity.
      SCase "S n".
        simpl.
        rewrite <- beq_nat_refl.
        rewrite <- IHl.
        reflexivity.
  Qed.


  (* apply タクティック *)
  Theorem silly1 : forall (n m o p : nat),
     n = m ->
     [n,o] = [n,p] ->
     [n,o] = [m,p].
  Proof.
    intros n m o p eq1 eq2.
    rewrite <- eq1.
    apply eq2.
  Qed.

  Theorem silly2 : forall (n m o p : nat),
     n = m ->
     (forall (q r : nat), q = r -> [q,o] = [r,p]) ->
     [n,o] = [m,p].
  Proof.
    intros n m o p eq1 eq2.
    apply eq2.
    apply eq1.
  Qed.


  (* Ex. silly_ex *)
  Theorem silly_ex :
    (forall n, evenb n = true -> oddb (S n) = true) ->
     evenb 3 = true ->
     oddb 4 = true.
  Proof.
    intros.
    apply H0.
  Qed.

  Theorem silly3: forall n: nat,
    true = beq_nat n 5 ->
    beq_nat (S (S n)) 7 = true.
  Proof.
    intros.
    simpl.                      (* Goal beq_nat n 5 = true *)
    symmetry.                   (* Goal true = beq_nat n 5 *)
    apply H.
  Qed.

  (* Ex. apply_exercise1 *)
  Theorem rev_exercise1: forall l l': natlist,
    l = rev l' -> l' = rev l.
  Proof.
    intros.
    rewrite -> H.
    symmetry.
    apply rev_involutive.
  Qed.


  (* 帰納法の仮定を変更する *)
  Check app_ass. (* forall l1 l2 l3 : natlist, (l1 ++ l2) ++ l3 = l1 ++ l2 ++ l3 *)


  (* より強い例 *)
  Theorem app_ass': forall l1 l2 l3: natlist,
    (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).
  Proof.
    intros l1.
    induction l1 as [| n l1'].
    Case "nil".
      reflexivity.
    Case "n :: l1'".
      intros l2 l3.
      simpl.
      rewrite -> IHl1'.
      reflexivity.
  Qed.

  (* Ex. apply_excersice2 *)
  Theorem beq_nat_sym : forall (n m : nat),
    beq_nat n m = beq_nat m n.
  Proof.
    intros n.
    induction n as [| n'].
    Case "O".
      destruct m.
      reflexivity.
      reflexivity.
    Case "S n'".
      destruct m.
      reflexivity.
      simpl.
      apply IHn'.
  Qed.
End NatList.


Module Dictionary.
  Inductive dictionary: Type :=
    | empty : dictionary
    | record : nat -> nat -> dictionary -> dictionary.

  Definition insert (key value: nat) (d: dictionary): dictionary :=
    (record key value d).

  Fixpoint find (key: nat) (d: dictionary): option nat :=
    match d with
      | empty => None
      | record k v d' =>
        if (beq_nat key k)
        then Some v else find key d'
    end.

  (* Ex. dictionary_invariant1 *)
  Theorem dictionary_invariant1: forall (d: dictionary) (k v:nat),
    find k (insert k v d) = Some v.
  Proof.
    intros d k.
    simpl.
    rewrite <- beq_nat_refl.
    reflexivity.
  Qed.

  (* Ex. dictionary_invariant2 *)
  Theorem dictionary_invariant2:
    forall (d: dictionary) (m n o: nat),
       beq_nat m n = false -> find m d = find m (insert n o d).
  Proof.
    intros.
    simpl.
    rewrite -> H.
    reflexivity.
  Qed.

End Dictionary.

Definition beq_nat_sym := NatList.beq_nat_sym.