The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

  Two suggestions if you expect help from people on this list:

• don't send your messages multiple times!
  
• use a sensible user name (you were already asked before to do that)
  

Example Code:
Require Import String.
Require Import List.
Record Product:Set := {productName:string}.
Record Store:Set := {products:list Product}.

Theorem T: forall p:Product,forall s:Store, In (productName p) (productName (products s)).
(*A product's name must be in the list of Product Names that a Store has.
How is this written?  I don't want to check that the Product is in the list of
Products, only that the name is in the Store's list of product names.*)

  Obviously you get an error because productName is a function from Product to string:

Check productName

> productName : Product -> string

  and products gives a list of products:

Check productName
> productName : Product -> string

  so Coq's error message makes perfect sense. What you probably want to do is this:

Theorem T: forall p s, In (productName p) (List.map productName (products s)).

  though I hope you are aware that you will not be able to prove this theorem.


  Cheers,
  Adam

-- 
=====================================================
Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski


The difference between impossible and possible
lies in determination (Tommy Lasorda)
=====================================================