coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] map_eq_nil lemma

From: Pierre Casteran <pierre.casteran AT labri.fr>
To: Taral <taralx AT gmail.com>
Cc: Michael Day <mikeday AT yeslogic.com>, coq-club AT inria.fr
Subject: Re: [Coq-Club] map_eq_nil lemma
Date: Thu, 08 Apr 2010 07:32:37 +0200

Le 08/04/2010 07:07, Taral a �crit :

On Wed, Apr 7, 2010 at 9:08 PM, Michael
Day<mikeday AT yeslogic.com>
wrote:

map_eq_nil : forall l, map f l = nil -> l = nil.

dependent destruction l; auto. ?

A simple case analysis is enough.

Lemma L : forall (A B:Type)(f : A -> B) l, map f l = nil -> l = nil.
destruct l;simpl;auto.
intro; discriminate.
Qed.
Pierre

[Coq-Club] map_eq_nil lemma, Michael Day
- Re: [Coq-Club] map_eq_nil lemma, Taral
  - Re: [Coq-Club] map_eq_nil lemma, Pierre Casteran
    - Re: [Coq-Club] map_eq_nil lemma, Michael Day