Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] case & inversion, Set & Prop

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] case & inversion, Set & Prop


chronological Thread 
  • From: Taral <taralx AT gmail.com>
  • To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
  • Cc: coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] case & inversion, Set & Prop
  • Date: Thu, 6 Aug 2009 13:27:31 -0700
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; b=uW1B3gdWmD1+gwcf9QkkPlWAMPUzRYuWMOFnBEpfPJjUX0rfXDy1j1vo0EKQHaUjMu 1iQnGRpsouCQMhHUIBxP94c3okY/KN5EY6EIGYN7fsBoQ9h0xSs8SuZz0roPAlpwXLtE jqYYPJUQjMO4T7v5yDHSuJqHqivHmuGA0/mv8=
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On Thu, Aug 6, 2009 at 5:28 AM, Keiko 
Nakata<keiko AT kurims.kyoto-u.ac.jp>
 wrote:
> I have been confused by different behaviour of case and inversion tactics,
> when I moved from Set to Prop.
> Will someone please explain?

You have:

intro l0. case l0. intro n0. intro l1.
case l1. intro n1. intro h1.

Then do:

case h1. constructor.

inversion doesn't work because you're trying to extract a nat (which
is in Set) from a list_eq (which is in Prop). You're not allowed to
get information (Set) out of non-informative things (Prop).

-- 
Taral 
<taralx AT gmail.com>
"Please let me know if there's any further trouble I can give you."
    -- Unknown



Archive powered by MhonArc 2.6.16.

Top of Page