Skip to content

Instantly share code, notes, and snippets.

@t0yv0

t0yv0/List.v

Created October 24, 2010 15:00
Show Gist options
  • Save t0yv0/643581 to your computer and use it in GitHub Desktop.
Save t0yv0/643581 to your computer and use it in GitHub Desktop.
Download ZIP
The only list of length zero is the empty list.
Raw
List.v
Require Import Coq.Lists.List.
(** The only list of length zero is the empty list. *)
Lemma length_zero : forall (a : Type) (x : list a),
length x = 0 <-> x = nil.
Proof.
intros; split; intro.
induction x; auto; discriminate.
rewrite H; compute; auto.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment