From 05d6901af70c3501eaf7f97a9789a047670877ba Mon Sep 17 00:00:00 2001 From: simon Date: Tue, 5 Jan 2010 23:40:42 +0000 Subject: [PATCH] Proof that check_errors() is sufficient. git-svn-id: svn://svn.tartarus.org/sgt/puzzles@8813 cda61777-01e9-0310-a592-d414129be87e --- unfinished/group.c | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/unfinished/group.c b/unfinished/group.c index d2ff194..4987a9e 100644 --- a/unfinished/group.c +++ b/unfinished/group.c @@ -1047,6 +1047,34 @@ static int check_errors(game_state *state, long *errors) digit *grid = state->grid; int i, j, k, x, y, errs = FALSE; + /* + * To verify that we have a valid group table, it suffices to + * test latin-square-hood and associativity only. All the other + * group axioms follow from those two. + * + * Proof: + * + * Associativity is given; closure is obvious from latin- + * square-hood. We need to show that an identity exists and that + * every element has an inverse. + * + * Identity: take any element a. There will be some element e + * such that ea=a (in a latin square, every element occurs in + * every row and column, so a must occur somewhere in the a + * column, say on row e). For any other element b, there must + * exist x such that ax=b (same argument from latin-square-hood + * again), and then associativity gives us eb = e(ax) = (ea)x = + * ax = b. Hence eb=b for all b, i.e. e is a left-identity. A + * similar argument tells us that there must be some f which is + * a right-identity, and then we show they are the same element + * by observing that ef must simultaneously equal e and equal f. + * + * Inverses: given any a, by the latin-square argument again, + * there must exist p and q such that pa=e and aq=e (i.e. left- + * and right-inverses). We can show these are equal by + * associativity: p = pe = p(aq) = (pa)q = eq = q. [] + */ + if (errors) for (i = 0; i < a; i++) errors[i] = 0; -- 2.11.0