Old Coq proofs from my hard drive

miscellany.v

(* CanHalveEven.v *)

Inductive Even : nat -> Prop :=
| Even_base : Even 0 
| Even_step : forall n, Even n -> Even (S (S n)).

Check Even_ind.

Theorem can_halve_even :
  forall n, Even n -> (exists k, k + k = n).
Proof.
  intros n E.
  induction E;
    [ exists 0; auto
    | destruct IHE as [k H];
      exists (S k);
      rewrite <- plus_n_Sm, plus_Sn_m;
      auto ].
Qed.

(* some exercises Emily gave me *)

Theorem em1: forall n, n = O \/ exists m, n = S m.
  intro n; induction n; [auto | right; exists n; auto].
Qed.

Definition IsZero (n : nat) : Prop :=
  match n with
  | O => True
  | S _ => False
  end.

Theorem zero_isnt_n: forall n, O <> S n.
  intros n A.
  apply (eq_ind 0 IsZero I (S n)) in A.
  simpl in A; auto.
Qed.


(* Lists.v *)
(* A big old proof of: reverse (reverse list) = list. *)

Inductive list (T : Type) : Type :=
  | nil : list T
  | cons : T -> list T -> list T.

Arguments nil [T].
Arguments cons [T] _ _.

Infix "::" := cons (at level 60, right associativity).

Section Lists.
  Context {T : Type}.

  (* Append a value to the end of a list. *)
  Fixpoint snoc (l : list T) (z : T) : list T :=
    match l with
    | nil => cons z nil
    | x :: xs => x :: (snoc xs z)
    end.

  (* Reverse a list. *)
  Fixpoint rev (l : list T) : list T :=
    match l with
    | nil => nil
    | x :: xs => snoc (rev xs) x
    end.

End Lists.

Lemma snoc_rev :
  forall (A : Type) (l : list A) (a : A),
  rev (snoc l a) = a :: rev l.
Proof.
  intros.
  induction l; [auto |].
  simpl.
  rewrite IHl; simpl.
  reflexivity.
Qed.

Theorem rev_invol :
  forall (A : Type) (l : list A),
  rev (rev l) = l.
Proof.
  induction l; [auto |].
  simpl. rewrite snoc_rev.
  rewrite IHl.
  reflexivity.
Qed.