SF

prop.v

Require Import Basics.
Require Import Induction.
Require Import Lists.

Definition even (n : nat) : Prop :=
  evenb n = true.

Inductive ev : nat -> Prop :=
  | ev_0 : ev 0
  | ev_SS : forall n : nat, ev n -> ev (S (S n)).

Definition double (n : nat) : nat :=
  n + n.

Theorem n_plus_Sm_is_S_n_plus_m : forall n m : nat,
  n + S m = S (n + m).
Proof.
  intros n m.
  generalize dependent m.
  induction n as [ |  n'].
    intros m.
    reflexivity.
  intros m.
  simpl.
  rewrite IHn'.
  reflexivity.
Qed.

Theorem double_even : forall n,
  ev (double n).
Proof.
  unfold double.
  induction n as [ | n'].
    apply ev_0.
  rewrite n_plus_Sm_is_S_n_plus_m.
  simpl.
  apply ev_SS.
  apply IHn'.
Qed.







(* 
*** Local Variables: ***
*** coq-load-path: ("../book-sources") ***
*** End: ***
*)