sf chap1

gistfile1.txt

Section Basics_J.

Definition nandb (b1 b2 : bool) : bool :=
 match (b1, b2) with
 | (false, _) => true
 | (_, false) => true
 | _ => false
 end.

Example test_nandb1: (nandb true false) = true.
Proof.
unfold nandb.
reflexivity.
Qed.

Example test_nandb2: (nandb false false) = true.
Proof.
unfold nandb.
reflexivity.
Qed.

Example test_nandb3: (nandb false true) = true.
Proof.
unfold nandb.
reflexivity.
Qed.

Example test_nandb4: (nandb true true) = false.
Proof.
unfold nandb.
reflexivity.
Qed.


Definition andb3 (b1:bool) (b2:bool) (b3:bool) : bool :=
 match (b1, b2, b3) with
 | (true, true, true) => true
 | _ => false
 end.

Example test_andb31: (andb3 true true true) = true.
Proof.
unfold andb3.
reflexivity.
Qed.

Example test_andb32: (andb3 false true true) = false.
Proof.
unfold andb3.
reflexivity.
Qed.

Example test_andb33: (andb3 true false true) = false.
Proof.
unfold andb3.
reflexivity.
Qed.

Example test_andb34: (andb3 true true false) = false.
Proof.
unfold andb3.
reflexivity.
Qed.

Fixpoint factorial (n:nat) : nat :=
 match n with
 | O => 1
 | S n' => n * factorial n'
 end.


Example test_factorial1: (factorial 3) = 6.
Proof.
simpl.
reflexivity.
Qed.

Example test_factorial2: (factorial 5) = (mult 10 12).
Proof.
simpl.
reflexivity.
Qed.

Fixpoint beq_nat (n m : nat) : bool :=
  match n with
  | O => match m with
         | O => true
         | S m' => false
         end
  | S n' => match m with
            | O => false
            | S m' => beq_nat n' m'
            end
  end.

Fixpoint ble_nat (n m : nat) : bool :=
  match n with
  | O => true
  | S n' =>
      match m with
      | O => false
      | S m' => ble_nat n' m'
      end
  end.

Definition blt_nat (n m : nat) : bool :=
 negb (beq_nat n m) && ble_nat n m.

Example test_blt_nat1: (blt_nat 2 2) = false.
Proof.
reflexivity.
Qed.

Example test_blt_nat2: (blt_nat 2 4) = true.
Proof.
reflexivity.
Qed.

Example test_blt_nat3: (blt_nat 4 2) = false.
Proof.
reflexivity.
Qed.


Goal forall n : nat, n + 0 = n.
Proof.
Abort.

Goal forall n : nat, n = n
Proof.
reflexivity.
Qed.


Theorem plus_id_exercise : forall n m o : nat,
  n = m -> m = o -> n + m = m + o.
Proof.
intros.
subst.
reflexivity.
Qed.


Theorem mult_1_plus : forall n m : nat,
  (1 + n) * m = m + (n * m).
Proof.
intros.
rewrite mult_plus_distr_r.
rewrite mult_1_l.
reflexivity.
Qed.


Theorem zero_nbeq_plus_1 : forall n : nat,
  beq_nat 0 (n + 1) = false.
Proof.
intros.
destruct n; reflexivity.
Qed.


Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
intros.
destruct b; destruct c; unfold andb in * |-;
 [ reflexivity | discriminate | reflexivity | discriminate ].
Qed.


Theorem mult_0_r : forall n:nat,
  n * 0 = 0.
Proof.
intros.
induction n.
 reflexivity.

 simpl.
 assumption.
Qed.

Theorem plus_n_Sm : forall n m : nat,
  S (n + m) = n + (S m).
Proof.
intros.
induction n; induction m.
 reflexivity.

 reflexivity.

 simpl.
 f_equal.
 assumption.

 simpl.
 f_equal.
 assumption.
Qed.

Theorem plus_comm : forall n m : nat,
  n + m = m + n.
Proof.
intros.
induction n.
 simpl.
 induction m.
  reflexivity.

  simpl.
  f_equal.
  assumption.

 simpl.
 rewrite IHn.
 rewrite plus_n_Sm.
 reflexivity.
Qed.


Fixpoint double (n:nat) :=
  match n with
  | O => O
  | S n' => S (S (double n'))
  end.

Lemma double_plus : forall n, double n = n + n .
Proof.
intros.
induction n.
 reflexivity.

 simpl.
 f_equal.
 rewrite IHn.
 rewrite plus_n_Sm.
 reflexivity.
Qed.

(* 
destructとinductionの違いを短く説明しなさい。 
*)
(* ... ? *)

(* 非形式的証明が2問 *)

Theorem beq_nat_refl : forall n : nat,
  true = beq_nat n n.
Proof.
intros.
induction n.
 reflexivity.

 simpl.
 assumption.
Qed.


Theorem plus_swap : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
intros.
assert (forall n m p : nat, n + (m + p) = m + (n + p)) as H.
 apply plus_permute.

 rewrite H.
 reflexivity.
Qed.

(* plus_swapを使えていないので何かおかしい… *)
Theorem mult_comm : forall m n : nat,
 m * n = n * m.
Proof.
intros.
induction m.
 simpl.
 rewrite mult_0_r.
 reflexivity.

 simpl.
 rewrite <- mult_n_Sm.
 rewrite plus_comm.
 rewrite IHm.
 reflexivity.
Qed.

Fixpoint evenb (n:nat) : bool :=
  match n with
  | O => true
  | S O => false
  | S (S n') => evenb n'
  end.

Theorem evenb_n__oddb_Sn : forall n : nat,
  evenb n = negb (evenb (S n)).
Proof.
intros.
induction n.
 reflexivity.

 simpl.
 rewrite IHn.
 simpl.
 assert (forall b, b = negb (negb b)).
  intros.
  induction b; reflexivity.

  rewrite <- H.
  reflexivity.
Qed.


(* c *)
Theorem ble_nat_refl : forall n:nat,
  true = ble_nat n n.
Proof.
induction n.
 reflexivity.

 simpl.
 assumption.
Qed.

(* a *)
Theorem zero_nbeq_S : forall n:nat,
  beq_nat 0 (S n) = false.
Proof.
reflexivity.
Qed.

(* b *)
Theorem andb_false_r : forall b : bool,
  andb b false = false.
Proof.
destruct b; reflexivity.
Qed.

(* c *)
Theorem plus_ble_compat_l : forall n m p : nat,
  ble_nat n m = true -> ble_nat (p + n) (p + m) = true.
Proof.
intros.
induction p; [ idtac | simpl ]; assumption.
Qed.

(* a *)
Theorem S_nbeq_0 : forall n:nat,
  beq_nat (S n) 0 = false.
Proof.
intros.
simpl.
reflexivity.
Qed.

(* c *)
Theorem mult_1_l : forall n:nat, 1 * n = n.
Proof.
intros.
simpl.
induction n.
 reflexivity.

 simpl.
 f_equal.
 assumption.
Qed.

(* b *)
Theorem all3_spec : forall b c : bool,
    orb
      (andb b c)
      (orb (negb b)
               (negb c))
  = true.
Proof.
intros.
destruct b; destruct c; reflexivity.
Qed.

(* c *)
Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
intros.
induction n.
 reflexivity.

 simpl.
 rewrite IHn.
 rewrite plus_assoc_reverse.
 reflexivity.
Qed.

(* c *)
Theorem mult_assoc : forall n m p : nat,
  n * (m * p) = (n * m) * p.
Proof.
intros.
induction n.
 reflexivity.

 simpl.
 rewrite IHn.
 rewrite Mult.mult_plus_distr_r.
 reflexivity.
Qed.

Theorem plus_swap' : forall n m p : nat,
  n + (m + p) = m + (n + p).
Proof.
intros.
induction n.
 simpl.
 reflexivity.

 simpl.
 replace (n + (m + p)) with (m + (n + p)) .
 rewrite plus_n_Sm.
 reflexivity.
Qed.


Inductive bin : Type :=
  | BinO : bin
  | Mult2 : bin -> bin
  | Mult2S : bin -> bin.

Fixpoint bin_incr b :=
 match b with
 | BinO => Mult2S BinO
 | Mult2 b' => Mult2S b'
 | Mult2S b' => Mult2 (bin_incr b')
 end.

Fixpoint bin_to_nat b :=
 match b with
 | BinO => O
 | Mult2 b' => 2 * bin_to_nat b'
 | Mult2S b' => 2 * bin_to_nat b' + 1
 end.

Goal forall (b:bin),
 bin_to_nat (bin_incr b) = S (bin_to_nat b).
Proof.
intros.
induction b.
 reflexivity.

 simpl.
 rewrite plus_comm.
 reflexivity.

 simpl.
 rewrite plus_0_r.
 rewrite plus_0_r.
 rewrite IHb.
 simpl.
 f_equal.
 rewrite plus_assoc_reverse.
 f_equal.
 rewrite plus_comm.
 reflexivity.
Qed.

Fixpoint mod n :=
 match n with
 | O => 0
 | S (S n') => mod n'
 | S _ => 1
 end.

Fixpoint div2' acc n :=
 match n with
 | O => acc
 | S (S n') => div2' (1+acc) n'
 | S _ => acc
 end.

Definition div2 n := div2' 0 n.

End Basics_J.