The Coq mailing list

[Andrew Pennebaker <andrew.pennebaker AT gmail.com>]

Mathematical formalization using Coq

1.1 Declarations and Types

Text:

Then submit this directive to Coq by pressing Alt+Ctrl+down arrow. Note that the terminating . is important: it tells Coq where a directive ends. If you forget it, Alt+Ctrl+down arrow won’t do anything.

Suggested:

Then submit this directive to Coq by pressing the shortcut Alt+Ctrl+Down (Alt+Ctrl+Cmd+Down for Macs). In the code, note the terminating period. It is important: it tells Coq where a directive ends. If you forget it, the shortcut won’t do anything.

Text:

You can do this either by pressing Ctrl+Alt+up arrow repeatedly until the green highlight does not include any of them, or by positioning the cursor just before the first Check directive and then clicking on the “Go to cursor” button (it looks like a green arrow pointing to a yellow sphere).

Suggested:

You can do this either by pressing Ctrl+Alt+Up (Ctrl+Alt+Cmd+Up for Macs) repeatedly until the green highlight does not include any of them, or by positioning the cursor just before the first Check directive and then clicking on the “Go to cursor” button (it looks like a green arrow pointing to a yellow sphere).

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

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.

The rest of the proofs seem to have good explanations and practical tips ("We can reduce this tedium by using repeat: if T is a proof tactic, then repeat T will execute T repeatedly until it fails.").


There were several spurious warnings during the exercises, someone should contact Coq Dev about them.

Parameter G : Type.

Warning: Input method gtk-im-context-simple should not use GTK's translation domain gtk20

G is assumed

assert (inv x * (x * y) = inv x * (x * z))
  as Hinvx_times_tocancel.

Warning: Invalid text buffer iterator: either the iterator is uninitialized, or the characters/pixbufs/widgets in the buffer have been modified since the iterator was created.

You must use marks, character numbers, or line numbers to preserve a position across buffer modifications.
You can apply tags and insert marks without invalidating your iterators,
but any mutation that affects 'indexable' buffer contents (contents that can be referred to by character offset)

will invalidate all outstanding iterators

(repeated 21x)

1.4 Exercises

Perhaps the most important section, a springboard for budding Coq provers to apply what they just learned. Based on the exercises, I have an idea of what the sample proofs are doing: proving basic mathematical relations. I just got lost in the semantics of axioms 1 and 2 in section 1.1.

Overall I like the tone and especially the helpful tips, like "However, personally, I find this pane more cumbersome to work with than just entering the Check directives directly and then cleaning them up." You give the user options (but not too many options), and let them decide which ones to use.

Cheers,

Andrew Pennebaker

www.yellosoft.us

On Wed, Nov 2, 2011 at 9:03 PM, Andrew Pennebaker <andrew.pennebaker AT gmail.com> wrote:

Daniel, I'll check it out.

Adam, I started reading CPDT Chapter 3 and came up with this:

https://github.com/mcandre/mcandre/blob/master/coq/bertrand.v

Cheers,

Andrew Pennebaker

www.yellosoft.us

On Wed, Nov 2, 2011 at 7:49 PM, Daniel Schepler <dschepler AT gmail.com> wrote:

I've started working on a Coq tutorial focused more on mathematics formalization than on program verification.  Right now, I only have the first chapter done, without even an introduction written (although I have a rough outline in mind for what I want to cover -- it hopefully shouldn't be too hard to find in the recent coq-club archives).

This first chapter starts off by declaring the "language/syntax" of the theory of groups, then declaring the "axioms", then proving several basic results using the axioms.

I'd be interested in any comments you might have about it.
--
Daniel Schepler