double_even.v

Inductive nat : Type :=
| z : nat
| s : nat -> nat.

Inductive even : nat -> Prop :=
| even_z : even z
| even_ss n: even n -> even (s (s n)).

Fixpoint double (n : nat) :=
  match n with
  | z => z
  | s n => s (s (double n))
  end.

Theorem ev_double:
  forall n, even (double n).
Proof.
  induction n.
  - exact even_z.
  - simpl. apply even_ss. assumption.
Qed.
(* shorter, but more inscrutable tactic sequence *)
(* Proof. induction n; constructor. assumption. Qed. *)


Fixpoint ev_double2 (n : nat) : even (double n) :=
  match n with
  | z => even_z
  | s n => even_ss _ (ev_double2 n)
  end.

Check ev_double2.