The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Andrew Pennebaker wrote:
> Mathematical formalization using Coq
>
> 1.1 Declarations and Types

I assume Daniel is grateful for your feedback on his tutorial, but it 
would probably be best to send your comments only to him.  They'll get 
back to the rest of us indirectly through any changes he decides to make!

> Axiom left_id : forall x:G, mult e x = x.
> Axiom left_inv : forall x:G, mult (inv x) x = e.
> Axiom assoc : forall x y z:G,
>   mult x (mult y z) = mult (mult x y) z.
>
> These declarations are fairly straightforward to read.
>
> Comment:
>
> I don't know how to read them. In words, what does the left_id axiom 
> mean? I read it as "For all x and e, ex = x," which isn't right, or 
> "There exists e such that ex = x, for any x," which would have a 
> different form.

...but this bit is worrying, suggesting that you should review one or 
both of first-order logic or typed functional programming (Haskell, ML, 
etc.) before proceeding.