Cockerel Proposal: DRAFT

Proofs are currently done by hand for introductory logic classes. This process can lead to many missteps for the novice as a result of inconsistent notation, techniques and grading. As a student writing proofs can be tedious since there is a long delay for feedback. It is hard to know if you are on the write or wrong path towards solution and often a student will believe their proof is correct, when they have in fact made subtle errors that invalidate their efforts. What if there existed a tool that helped students stay on the right path while attempting proofs?

Current computer checked proof tools are not designed to be used by novices. They are complex and require the user to understand functional programming techniques in addition to understanding proof structures. The syntax of these tools is also very complex and intimidating. Students need a tool they can use which works with a syntactical notation similar to the current text books and reports errors that are within the context of the class. This will allow students to learn from their errors, rather than be confused by them later.


I propose creation of a web-based learning system for introductory
logic students. This system will allow students to login and type
their proofs into a web browser editor. The web editor will provide
the symbols they are used to seeing form their companion text and it
will check their proofs as they desire. This system will feel as natural
as handwritten proofs since the student will be able to check the
proof at any point, but it will also provide the feedback needed to
understand the issues during a proof process. All errors will be
reported using terms that a student will easily understand, not in the
terms of the underlying proof assistant.

Beneath the web interface, we will construct a web-server that manages
the student's progress by giving each student a unique id. The
progress will also be available to the instructors. In addition, many
students can use this tool simultaneously; it should be consistent
with all the properties of a common multiuser web-site. The web-server
will speak with one Coq process per student to perform the proof
verification.

The Coq process will require an abstraction of the underlying proof
assistant to prevent students from using the automated features of Coq,
but more importantly to keep the natural/hypothetical reasoning
abstract. It is very important that the students work without any
knowledge of the underlying proof machinery. Breaking this abstraction
will fail to achieve the ease of use we require.


The Coq abstraction problem will be broken in two components. First we
will need to reconstruct the tactics available in a typical
propositional and predicate logic course. For our purposes, we will
use "Discrete Structures, Logic, and Computability", by James L. Hein
as the sample text. Per our specifications, we must provide a similar
environment to the proofs available in the book. Adopting this system
of reasoning will require building new tactics to macro the many
sub-steps required in a similar Coq proof. We will construct these using
the LTac language. One example of a proof done without using any
macros can be seen here:
    
      Theorem ex_cons_dilemma : forall (A B C : Prop),
        (A \/ B) /\ (A \/ C) /\ ~ A -> B /\ C.
        Proof.
        intros.
        destruct H. destruct H0.
        destruct H.
        destruct (H1 H).
        destruct H0.
        destruct (H1 H0).
        split.
        assumption.
        assumption.
        Qed.

Clearly, the proof needs to have simpler tactics for a student to
apply. Rather than required the user to perform so many destructs,
this proof could be simple solved using disjunctive syllogism. This
will be one of the many tactics we will define.


The other issue with using Coq as our theorem proving engine is that
we much provide simpler error reporting to the user. Errors are
currently reported in Coq like the following:
      
         Toplevel input, characters 20-28:
         Error: Impossible to unify "B" with "C".

Since many students at this level have not dealt with a functional
language, this error will be extremely confusing. In addition, it
provides little explanation about what steps can be take to resolve
the error. When we abstract this reporting to provide precise
information about the environment and what has likely gone wrong, the
students will be able to spend less time understanding the error and
more time fixing it. An error would be required to report where it
occurred, what tactic was being used, and a likely cause of these
error. One example could read as follows:
    
       Line 10: DS could not be performed since ~A has not be proven
                or introduced.

Ideally, we would be able to focus test these reporting messages with
introductory students and develop the simplest and most precise
message possible. In all circumstances, we must maintain the Coq
abstraction.


For this summer's project, I propose the following steps
    1. Implement a wrapper library for Coq which allows us to perform
    proposition reasoning that is consistent with Hein's book. This
    includes adding the LTac macros required to complete the proofs
    and the associated errors with each tactic.

    2. Write a web-server that can connect to Coq and execute proofs
    that are submitted via a web-form.
  
    3. Add the Java-script interface to the web-site that allows us to
    execute proofs as we type them in. The editor will also need to
    provide symbols that match Hein's book.

    4. Provide a login and tracking system for assignments within the
    web-site. This will require a permissions system, a user data
    model, and other session data.

    5. Incrementally add predicate calculus, hoare clause logic and
    other reasoning systems to our underlying library. Then extend the
    web-site to support these new systems.

The design of this project will allow us to have a functioning system
very early on. This means we can have feedback from students about the
usability and correct any serious issues early in the
project. The object is to provide a working system as soon as possible
so we can spend much of our time refining it. The smoother the
experience is for a student, the more they will prefer this system
over working proofs out on paper.

I have proposed a web-based Coq proof assistant which will be
used by students through a friendly and simple Java-script
interface. I believe this is an opportunity to improve the teaching
methods for introductory logic. This project will result in a powerful and
flexible learning systm that can be expanded later on. A few ideas
include guided learning tracks based on how a student solves a proof
or how many times they have to attempt a solution. There are also many other
possibilities for collaborative learning via instant messaging and
forums. The proposed system will overcome many of difficulties
experienced by students, reduce the work load for instructors and
organize the experience into a single site.