The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

Since this has made its way onto coq-club, I decided to post the current 
state 
of the work at http://people.debian.org/~schepler/coqtut.pdf ;.

On Wednesday, November 02, 2011 11:45:24 PM Andrew Pennebaker wrote:
> Text:
> 
> 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.
> 
> Similarly, I don't know how to read the axiom left_inv. It looks to me like
> "for all x and e, x(x^-1) = e," which isn't right.
> 
> The last axiom is perhaps the most readable: the principle of association,
> that x(yz) = xy(z).

The general answer to these questions: maybe you forgot about the declaration

Parameter e : G.

In other words, e is a *predefined* element of G.
> 
> 1.2 Proof mode
> 
> I see what the proof is doing, but it feels backwards. Can the proof be
> rewritten so that it transforms x * y = x * z into inv x * (x * y) = inv x
> * (x * z), then uses left_inv to reduce that to y = z. Maybe that's what
> the proof is already doing, but the order is tricky.

Hmm, that brings up a good point.  Maybe I should explain that in Coq, the 
easiest way to construct a proof is "working backward" from the goal using 
apply, rewrite, etc.  On the other hand, tactics like assert, pose/set, pose 
proof, * in H*, etc. let you "work forward" from the hypotheses, which is 
probably the more familiar style of argumentation for mathematicians.  It's 
similar to the difference in functional programming between building a 
function 
"top down" as a big complex expression, or building a function "bottom up" 
using let statements.  (And in fact, in Coq's proof terms, the backward 
reasoning/forward reasoning difference is exactly the same as the top 
down/bottom up definition difference.)

Also, I answer your specific question later, where I introduce the use of
  apply f_equal with (f:=fun g:G => inv x * g) in Htocancel.
I just wanted to keep things simple for the first proof.
-- 
Daniel Schepler