#|


You have to work in pairs for this homework, but you can work
with anyone you want to. Send the name of your partner to
Zhifeng (austin@ccs.neu.edu) by the end of the day, on Wednesday,
April 9th. If you do not do this, you will get a 0 on your
homework. If you need a partner, send email to Zhifeng by the end
of the day on Wednesday, April 9th, and he will randomly assign
partners. 

Each pair should submit their homework via blackboard. Each
pair should submit just once. That is, one person per team should
submit the homework via their blackboard account. Your submission
should be this lisp file with your solutions inserted in the
appropriate place. Make sure that you start by putting the names
of the team at the beginning of this comment.

For this assignment, you will implement the game "Lights Out", released by
Tiger Toys in 1995, now owned by Hasbro, and prove some theorems about it.

We will not describe how the game works.  This is easily found on the web,
as in http://en.wikipedia.org/wiki/Lights_Out_%28game%29
You can play the game at http://www.whitman.edu/mathematics/lights_out/

You will eventually use the ACL2s graphics package to implement an
interactive version of the game.  See the ACL2s web page for a guide:
http://acl2s.peterd.org/acl2s/doc/#guide_graphics

We will outline a recommended design, but you are free to alter this if you
feel so motivated and so capable.  Rules for deviating significantly:

* You should document your design even more thoroughly with comments
   (semicolon to end-of-line) and test cases (using assert-event).

* You are expected to prove essentially the same properties from part II.
   This means you are allowed to skip part I, but if you do this, part II
   expectations will count for both.


=========================================================================
======================== I. SIMPLIFIED GAME LOGIC =======================
=========================================================================

First you will implement the logic of the game, and we will start with
a much simplified version of the game:  a one-dimensional version.
Consider there to be only one row of lights, but of arbitrary length.


###############################
### A. Data Representation  ###
###############################

First we should come up with a data definition for the state of a
one-dimensional Lights Out board.  Conceptually, this is a row of booleans
indicating whether each light is ON or OFF.  We recommend using a "list of
booleans" because this encoding includes the extent of the board, as in one
can look at such a structure and determine how long the row is.  Let us use
left-to-right ordering.


##### CONFIG-ROW-EQUAL function & proofs ######

From what you have been taught so far, a logical next step would be to write
a predicate function for our data type, but we recommend a different approach
for this problem.  Write a function CONFIG-ROW-EQUAL that will test whether
two ACL2 objects are the same when interpreted as a Lights Out row.  We will
analyze this recursively.  Two rows correspond iff the booleans along their
"spines" correspond.  Two booleans correspond iff they satisfy the ACL2
function IFF.  Here are some test cases you can use (in addition to your own):
|#

(assert-event (config-row-equal nil 37))
(assert-event (config-row-equal '(nil nil t)
                                '(nil nil 5 . "hi")))
(assert-event (not (config-row-equal '(nil t)
                                     '(nil t nil))))

#|
Now we want to prove that CONFIG-ROW-EQUAL is an equivalence relation.
(Refer to Homework 4, Problem 1(a).)  Write a DEFTHM for each of reflexivity,
symmetry, and transitivity of CONFIG-ROW-EQUAL, and then write
|#

(defequiv config-equal)

#|
which also requires that CONFIG-ROW-EQUAL return only T or NIL.
 
This tells ACL2 that it can treat CONFIG-ROW-EQUAL as an equivalence relation
in ways other than as three rewrite rules.

If any of your proofs use more than one induction, you should prove a
separate, reusable lemma that enables proof with at most one induction, but
this shouldn't happen for any of the preceding proofs.


##### CONFIG-ROW-GET function & proofs #####

Now write a function CONFIG-ROW-GET which takes a 0-based column index and a
row, and returns non-nil iff the light should be on at that position.  It
should be easiest to return NIL if the indices are "out of bounds," simply
because the CAR or CDR of a non-cons is NIL.  And you are welcome to treat
values that are not natural numbers as 0.

Ok, so ACL2 already has a function that does the same thing.  If you know
what it is, don't bother writing the function CONFIG-ROW-GET if it just
calls this other function.  Instead, just use that function whenever we
refer to CONFIG-ROW-GET.  This violates guidelines you have learned in
the past (regarding abstraction and reusability), but the motivation here
has to do with reasoning.  When new to ACL2, avoid writing non-recursive
functions!  It takes expertise to work with them in a way so that ACL2
does not get lost.

Here are two basic tests for CONFIG-ROW-GET.  You should write more,
including "out-of-bounds" tests.
|#

(assert-event (config-row-get 1 '(nil 5 nil)))

(assert-event (not (config-row-get 0 '(nil t "hi" t))))

#|
Now we want to prove something special about CONFIG-ROW-GET and its
relationship to CONFIG-ROW-EQUAL.  Specifically, we want to prove that the
"nilness" of CONFIG-ROW-GET isn't changed by replacing the row it is given
with another that is CONFIG-ROW-EQUAL to it.  The ACL2 function for comparing
"nilness" is IFF.  It turns out that the theorem we want is a case of
what ACL2 calls "congruence-based reasoning," which makes use of equivalence
relations such as EQUAL, IFF, and (since your proof) CONFIG-ROW-EQUAL.  Write
|#

(defcong config-row-equal iff (config-row-get cidx row) 2)

#|
You can read about DEFCONG in the ACL2 (theorem prover) documentation.  You
should have a local copy of that documentation, whose URL should be shown at
the start of ACL2s session output.  Follow the URL, click on "The User's
Manual", "Index of all documented topics", "D", and "DEFCONG". 

ACL2 attempts to prove 

  (IMPLIES (CONFIG-ROW-EQUAL ROW ROW-EQUIV)
           (IFF (CONFIG-ROW-GET RIDX CIDX ROW)
                (CONFIG-ROW-GET RIDX CIDX ROW-EQUIV)))

which corresponds to what we described as the theorem we want, and ACL2
can use it in very helpful ways.

Once again, this proof should use only one induction, which should be
the case considering the corresponding single-recursive behaviors of
CONFIG-ROW-EQUAL and CONFIG-ROW-GET.


##############################
### B. Board Manipulation  ###
##############################

##### FLIP-COL function & proofs #####

Now write a function FLIP-COL that takes a column index and a row and
returns a configuration in which the corresponding position has had its
ON/OFF status flipped.  If the position is invalid for the row, the row
should be returned unchanged.  No helper function should be needed, since
ACL2 has a function for flipping the "nilness" of a value: NOT.

You should come up with lots of tests for the function to convince yourself
it is correct.  If you have trouble with any of the proofs, you should
reconsider whether your notion of correctness is consistent with the theorem
and whether the function really does satisfy that notion and the theorem.

Prove these theorems, keeping in mind that you *might* need to prove lemmas
to aid ACL2 in the proofs and to avoid double-induction.

**IMPORTANT**:  In a comment above each of the following, explain what the
theorem means in your own words.
|#

(defcong config-row-equal config-row-equal (flip-col cidx row) 2)

(defthm flip-cols-commute
  (config-row-equal (flip-col c1 (flip-col c2 row))
                    (flip-col c2 (flip-col c1 row))))

(defthm double-flip-col
  (config-row-equal (flip-col cidx (flip-col cidx row))
                    row))

#|
##### MOVE-1D function & proofs #####

Write a non-recursive function MOVE-1D which takes a column index and a row
uses multiple calls of FLIP-COL to flip the specified column and the two
on either side.

If you have written FLIP-COL in a robust way, MOVE-1D should not even need
any conditionals (IF or COND), and definitely shouldn't need recursion.

An example test is
|#

(assert-event
 (equal
  (move-1d 1 '(nil nil t t))
  '(t t nil t)))

#|
When convinced your function is correct, prove analogues for MOVE-1D of the
three things we proved about FLIP-COL.  The theorems we proved about FLIP-COL
should be sufficient lemmas, but for these proofs, ACL2 can get lost if it
uses the exact definition of FLIP-COL.  We can prevent this by putting
|#

(in-theory (disable flip-col))

#|
before these proofs regarding MOVE-1D.  This tells ACL2 to "turn off" the
rule in its database for the definition of FLIP-COL.  Then in proofs,
FLIP-COL will be like a "black box" function, except for other rules
we have about FLIP-COL.

After our proofs above MOVE-1D, reenable FLIP-COL:
|#

(in-theory (enable flip-col))

#|

**IMPORTANT**:  In a comment above each of your proofs about MOVE, explain
in your own words what the theorem means.



=========================================================================
========================== II. FULL GAME LOGIC ==========================
=========================================================================

If you completed Part I, extending this to a two-dimensional grid will be
easy.


###############################
### A. Data Representation  ###
###############################

First we should come up with a data definition for the state of a Lights Out
board.  Conceptually, this is an N x M grid of booleans indicating whether
each light is ON or OFF.  Using our encoding of rows, it makes sense to use
"list of lists of booleans" to encode a 2-dimensional board.  Let us use
row-major, top-to-bottom, left-to-right, ordering, which means the outer
list is of rows from top to bottom, and each row (sublist) is a list of
booleans (nil or non-nil) from left to right.


##### CONFIG-EQUAL function & proofs ######

Analogous to what we did for rows, write a function CONFIG-EQUAL that will
test whether two ACL2 objects are the same when interpreted as a Lights Out
board configuration.  We will analyze this recursively.  Two objects are
CONFIG-EQUAL iff the rows along their "spines" correspond.  Two rows
correspond iff they satisfy CONFIG-ROW-EQUAL.  Here are some test cases you
can use (in addition to your own):
|#

(assert-event (config-equal nil 37))
(assert-event (config-equal '((t nil t)     (nil nil t))
                            '((5 nil (nil)) (nil nil 5 . 4) . "hi")))
(assert-event (not (config-equal '((nil) (t))
                                 '((nil) (t) nil))))

#|
An interesting observation is that this notion of CONFIG-EQUAL not only allows
rectangular (N x M) boards, but also boards with rows of differing lengths.
This is okay.  It turns out to be simple to allow this and doesn't cause a
problem.  Thus, your CONFIG-EQUAL function does not need to do any arithmetic
or numerical comparisons of any kind.

Now we want to prove that CONFIG-EQUAL is an equivalence relation.  Write a
DEFTHM for each of reflexivity, symmetry, and transitivity of CONFIG-EQUAL,
and then write
|#

(defequiv config-equal)

#|
which also requires that CONFIG-EQUAL return only T or NIL.

Should any of your proofs use more than one induction, you should prove a
separate, reusable lemma that enables proof with at most one induction.



##### CONFIG-GET function & proofs #####

Now write a function CONFIG-GET which takes a 0-based row index and a 0-based
column index and a configuration, and returns non-nil iff the light should be
on at that position.  It should be easiest to return NIL if the indices are
"out of bounds," simply because the CAR or CDR of a non-cons is NIL.  And
you are welcome to treat values that are not natural numbers as 0.

You are free to use CONFIG-ROW-GET (or the built-in function you substituted),
but please make CONFIG-GET a recursive function.
  ________________________________________________________________________
 |                                                                        |
 | To make it easiest for ACL2 to prove & use theorems about CONFIG-GET   |
 | and other functions you write, here are some guidelines.  In places,   |
 | these will contradict other perfectly valid guidelines you have        |
 | received that have with different goals:                               |
 |                                                                        |
 |  * Make each function as simple as possible.  Thus, consider using     |
 |    helper functions, except...                                         |
 |                                                                        |
 |  * Avoid writing non-recursive functions (functions that just call     |
 |    other functions).  The only non-recursive function in the design    |
 |    we describe are MOVE-1D and MOVE.                                   |
 |                                                                        |
 |  * If there is an existing function that does EXACTLY what you want,   |
 |    feel free to use it, unless it would cause you to write a           |
 |    non-recursive function to use it properly.                          |
 |                                                                        |
 |  * Make your recursive calls as simple as possible.  Thus, avoid       |
 |    functions that use accumulators.                                    |
 |________________________________________________________________________|

Here are two basic tests for CONFIG-GET.  You should write more.
|#

(assert-event (config-get 1 1 '((nil nil nil)
                                (nil t nil)
                                (nil nil nil))))

(assert-event (not (config-get 0 2 '((t t nil t)
                                     (t t t   t)
                                     (t t t   t)))))

#|
Anologous to CONFIG-ROW-GET and CONFIG-ROW-EQUAL, we now prove something
special about CONFIG-GET and its relationship to CONFIG-EQUAL.  Specifically,
we want to prove that the "nilness" of CONFIG-GET isn't changed by replacing
the configuration it is given with another that is CONFIG-EQUAL to it.  The
ACL2 function for comparing "nilness" is IFF.  This theorem is a case of
ACL2's "congruence-based reasoning," makes special use of CONFIG-EQUAL as
an equivalence relation.  Write
|#

(defcong config-equal iff (config-get ridx cidx config) 3)

#|
which is 

  (IMPLIES (CONFIG-EQUAL CONFIG CONFIG-EQUIV)
           (IFF (CONFIG-GET R C CONFIG)
                (CONFIG-GET R C CONFIG-EQUIV)))

Once again, your previous results should enable ACL2 to prove this with just
one induction, but if it uses more than one, prove separate, reusable lemmas
that enable proof with at most one induction.



##############################
### B. Board Manipulation  ###
##############################

##### FLIP function & proofs #####

Now write a function FLIP that takes a row index, a column index and a
configuration and returns a configuration in which the corresponding position
has had its ON/OFF flipped.  If the position is invalid for the
configuration, the configuration should be returned unchanged.  You should
use FLIP-COL in defining this function.

You should come up with lots of tests for the function to convince yourself
it is correct.  If you have trouble with any of the proofs, you should
reconsider whether your notion of correctness is consistent with the theorem
and whether the function really does satisfy that notion and the theorem.

Prove these theorems, keeping in mind that you might need to prove lemmas to
aid ACL2 in the proofs and to avoid double-induction.

**IMPORTANT**:  In a comment above each of the following, explain what the
theorem means in your own words.
|#

(defcong config-equal config-equal (flip row col config) 3)

(defthm flips-commute
  (config-equal (flip r1 c1 (flip r2 c2 config))
                (flip r2 c2 (flip r1 c1 config))))

(defthm double-flip
  (config-equal (flip row col (flip row col config))
                config))

#|
##### MOVE function & proofs #####

Write a non-recursive function MOVE which takes a row index, a column index,
and a configuration and uses multiple calls of FLIP to perform the change
that should happen when a light is clicked in a (2-dimensional) Lights Out
game.

If you have written FLIP in a robust way, MOVE should not even need any
conditionals (IF or COND).

An example test is
|#

(assert-event
 (equal
  (move 0 1 '((nil nil nil nil)
              (nil nil nil nil)
              (nil nil nil t)
              (nil nil t   t)))
  '((t   t   t   nil)
    (nil t   nil nil)
    (nil nil nil t)
    (nil nil t   t))))

#|
When convinced your function is correct, prove analogues for MOVE of the
three things we proved about FLIP.  The theorems we proved about FLIP should
be sufficient lemmas, but for these proofs, ACL2 can get lost if it uses the
exact definition of FLIP.  We can prevent this by putting
|#

(in-theory (disable flip))

#|
before these proofs regarding MOVE.  

**IMPORTANT**:  In a comment above each of your proofs about MOVE, explain
in your own words what the theorem means.



=========================================================================
============================== III. GRAPHICS =============================
=========================================================================

Now that we have the logic of the game written, you should make it
graphical and interactive.  We will start by defining how to present the
board, then make it respond to clicks, then make it recognize winning.

As discussed on the ACL2s web page,
http://acl2s.peterd.org/acl2s/doc/#guide_graphics
load graphics support into your file by writing
|#

(include-book "graphics" :dir :acl2s :ttags :all)

#|
The code you write under this part of the assignment can be written under
different guidelines, since you will not be required to prove any theorems
about this code.  One difference here is that there will be places in which
you have to tie your code to a particular board size.  Implement a 5x5 board,
but when refering to that size please use constants such as these:
|#

(defconst *rows* 5)
(defconst *cols* 5)

#|
Now I can use these as constants, as in (* *rows* *cols*), which is 25.

You can add the following to set an initial logical configuration of your
graphical application:
|#

(defconst *initial-config*
  '((nil nil nil nil nil)
    (nil nil nil t   nil)
    (nil nil nil nil nil)
    (nil t   nil t   nil)
    (nil nil nil nil nil)))
    
(set-initial-configuration *initial-config*)

#|
That is one of many solvable configurations (there are also unsolvable ones).



#############################
### A. Board Presentation ###
#############################


Write a "configuration presenter" function as called for by the graphics
library.  Thus, it should take in a configuration (first parameter) and an
empty presentation (second parameter) and return the modified presentation.
This is where you actually compose drawing of dots and lines to make a
sensible presentation of the game.

See the graphics example on the ACL2s web page for an example presenter
function:

http://acl2s.peterd.org/acl2s/doc/reversi.lisp

Once you have your "configuration presenter" function, call it PRESENTER,
write this to register it with ACL2:
|#

(set-configuration-presenter 'presenter)

#|
You should now be able to test your presenter by typing (big-bang) at the
command prompt.  You should see your presentation of *initial-config* above.



####################
### B. Clickable ###
####################

This part is actually quite easy since we are going to give you the code you
need for it--besides the MOVE function you wrote.  Write this:
|#

(defun on-click (button x y config)
  (declare (ignore button))
  (let* ((row (floor (* *rows* y) 1))
         (col (floor (* *cols* x) 1)))
    (move row col config)))

(add-click-handler 'on-click)

#|
Except replace or define *rows* to be the number of rows (5) and likewise
with *cols* and the number of columns (5).



###########################
### C. Solved Detection ###
###########################

Modify your presenter to check for the solved configuration, one that is
CONFIG-EQUAL to '((nil nil nil nil nil)
                  (nil nil nil nil nil)
                  (nil nil nil nil nil)
                  (nil nil nil nil nil)
                  (nil nil nil nil nil)).

In that case, you can do something special, like put the string "SOLVED!"
into the status bar, using the SET-STATUS-BAR function in the ACL2s graphics
package.

Also, modify the ON-CLICK function to check for the solved case as well,
and respond to any click by returning the initial configuration, which will
restart the game.




=========================================================================
=========================== IV. MORE VALIDATION =========================
=========================================================================

#############################
### A. Shape Preservation ###
#############################

Define a function CONFIG-SHAPE-EQUAL which recognizes whether two
configurations have the same dimensions.  Considering we allowed for
irregular "shapes" of the board, it's most effective and easiest not to
involve numbers in this computation.  It can work much like CONFIG-EQUAL
except ignoring the status of the individual lights.


Prove that CONFIG-SHAPE-EQUAL is an equivalence relation.


Then prove that CONFIG-EQUALity implies CONFIG-SHAPE-EQUALity.  You will
need to formalize this and come up with lemmas that are needed.  Note that
this is not good as a rewrite rule, so specify a different :rule-classes
like so:

 (defthm config-equal--implies--config-shape-equal
    ...
    :rule-classes :forward-chaining)


Prove that FLIP preserves CONFIG-SHAPE-EQUALity.  That is, the configuration
returned is CONFIG-SHAPE-EQUAL to the one passed in.  You will need to
formalize this and come up with any lemmas that might be needed to get a
proof with only one induction.  You probably want to
(in-theory (enable flip)) before this proof.


Prove that MOVE preserves CONFIG-SHAPE-EQUALity.  You will need to
formalize this and come up with any lemmas that might be needed to get a
proof with only one induction.  You probably want to
(in-theory (disable flip)) before this proof.




=========================================================================
============================= V. EXTRA CREDIT ===========================
=========================================================================

These are probably in order of increasing difficulty, but you probably
don't need any earlier ones to pursue later ones.


###################################
### A. Special case solvability ###
###################################

Prove that the *initial-config* we give above is solvable.  That is, that
there is a sequence of moves that leads to the solved configuration.
(Think carefully about what theorem to prove, and it should be easy to prove.)



###################################
### B. Number of lights changed ###
###################################

Define a function that computes the number of lights that are in a different
state between two configurations.

Prove that it returns a natural number.

Prove that FLIP changes at most one light.

Prove that MOVE changes at most 5.

Prove that MOVE changes 3 lights iff it's on a corner.

Prove that for a board of sufficient size, MOVE never changes only 2 lights.



#################
### C. Solver ###
#################

First write a function that applies lists of moves, where a move is a cons
of a row index and a column index.

Write a function that determines whether a 5x5 Lights Out game is solvable.

Write a function that returns a sequence of moves that solve a configuration
of 5x5 Lights Out, if the given configuration is solvable.

Prove these functions correct.

|#