The Coq mailing list

[Coq User <coquser AT googlemail.com>]

With the revised listing, can the theorem prover be given the store:Store and c:Product to complete the proof?

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

Definition a:Product := Build_Product "apple".
Definition b:Product := Build_Product "pear".
Definition c:Product := Build_Product "apple".
Definition store:Store := Build_Store (a::p::nil).

(*Should be able to verify that c:Product is in the Store's list of Products.*)
Theorem T:
forall s:Store,forall p:Product, In (productName p) (map productName (products s)).
Proof.
intro.
intro.
(*Next??*)

On Wed, Jul 29, 2009 at 7:10 PM, Cedric Auger <Cedric.Auger AT lri.fr> wrote:

Coq User a écrit :

In the (very simplified) example below I want to check that all product's names appear in the list of product names in a Store.  However, I always get this error:
Error: In environment
p : Product
s : Store
The term "products s" has type "list Product"
while it is expected to have type "Product".

Any Ideas??

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.*)

What you wrote is meaningless:
productName has type Product -> string
products has type Store -> list Product
In fact you may want to use a morphism like List.map:

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

But you won't be able to prove such a thing:

Theorem T:
~forall p:Product,forall s:Store, In (productName p) (map productName (products s)).
Proof.
 intro.
 exact (H (Build_Product ""%string) (Build_Store nil)).
Qed.

--
Cédric AUGER

Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay