## Working with ProofWeb

1. Go to the web page
http://prover.cs.ru.nl/
OR
http://lolita.dimap.ufrn.br/proofweb
(ProofWeb does not work in all browsers. Firefox should be okay.)

2. Click on the name of your course near the bottom of the page.

4. Click on the button of the problem that you want to work on.

5. Select from the Display menu the item
Box proofs

6. (Possibly select from the Debug menu the item
Toggle Electric Terminator
This will make the commands execute automatically every time you type a period character (.'). Else you will need to click on the down arrow or type control-down to execute commands.)

7. Click on the down arrow or type control-down until you have executed the
Proof.
line after the Theorem line. Now you will be able to work on a proof. When you are doing this, the incomplete version of the proof will be shown on the lower right.

8. Replace the
(*! prop_proof *)
comment with a sequence of tactics as described on the next pages. If you did not toggle the electric terminator, execute these tactics by clicking the down arrow repeatedly (or by typing control-down repeatedly.)

9. You can also enter tactics by selecting items from the Template, Backward and Forward menus. Replace the question marks (?') by labels, formulas and terms and add a period after the command. After you did so click the down arrow or type control-down.

10. You can edit the part of the text that has not yet been executed (the part that has been executed will be green). To undo steps in the proof click the up arrow or type control-up.

11. If you have problems with ProofWeb, or want to exchange experiences, use the ProofWeb forum on the discussion board (on Blackboard') of your course.

# Example

## Exercise

(* Exercise 1 *)

Require Import ProofWeb.

Variables A B : Prop.

Theorem prop_001 : (A /\ B) -> A.
Proof.
(*! prop_proof *)

Qed.


## Solution

(* Exercise 1 *)

Require Import ProofWeb.

Variables A B : Prop.

Theorem prop_001 : (A /\ B) -> A.
Proof.
imp_i H.
f_con_e1 H.
Qed.


## Proof

 1 assumption 2 e 1 3 i 1--2

## Rendering in ProofWeb

 1 H: A B assumption 2 A e 1 3 A B A i 1-2

# Formula syntax

 False True ~ /\ \/ -> <-> all , exi ,

When formulas that are not single identifiers are used as arguments of tactics, they need to be put in brackets.

The all' and exi' quantifiers bind more strongly than the built-in Coq quantifiers forall' and exists'.

The all' and exi' internally use a function _K'. If through a bug in one of the tactics this function ever appears in a goal, one should use the tactic remove_K' to get rid of it (and report the bug).

# Tactics

The green H' labels that occur in these descriptions are not part of the way proofs are written in Huth & Ryan, but are necessary for working in ProofWeb. They are the symbolic equivalents (which stay the same throughout the proof process) of the line numbers (which change all the time).

## Structural tactics

 exact H H H ... copy insert H ... H ... ...

## Backward tactics

The tactic names may be prefixed with b_... to contrast them to the corresponding forward tactics.

Rules that are not intuitionistically valid are marked with a star. Rules that according to Huth & Ryan are derived rules are marked with a dagger.

 conjunction introduction con_i ... ... ... i conjunction elimination left con_e1 ... ... e
 conjunction elimination right con_e2 ... ... e disjunction introduction left dis_i1 ... ... i disjunction introduction right dis_i2 ... ... i disjunction elimination dis_e ( \/ ) H1 H2 ... H1 assumption ... H2 assumption ... ... e ,--,-- implication introduction imp_i H H assumption ... ... i --
 implication elimination imp_e ... ... ... e negation introduction neg_i H H assumption ... ... i -- negation elimination neg_e ... ... ... e falsum elimination fls_e ... ... e truth introduction tru_i ... i double negation introduction negneg_i ... ... i
 double negation elimination* negneg_e ... ... e law of excluded middle* LEM ... LEM proof by contradiction* PBC H H assumption ... ... PBC -- modus tollens MT ... ... ... MT universal introduction all_i ... ... i -- universal elimination all_e (all x, ) ... ... e
 existential introduction exi_i ... ... i existential elimination exi_e (exi x, ) H ... H ... ... e ,-- equality introduction equ_i ... i equality elimination, simple version equ_e ( = ) ... ... ... e equality elimination, general version ( may occur in ) equ_e' ( = ) (fun x => ) ... ... ... ... e

## Forward tactics

 conjunction introduction f_con_i H1 H2 H1 H1 H2 H2 ... i conjunction elimination left f_con_e1 H H H ... e conjunction elimination right f_con_e2 H H H ... e disjunction introduction left f_dis_i1 H H H ... i disjunction introduction right f_dis_i2 H H H ... i
 disjunction elimination f_dis_e H H1 H2 H H H1 assumption ... H2 assumption ... ... e ,--,-- implication elimination f_imp_e H1 H2 H1 H1 H2 H2 ... e negation elimination f_neg_e H1 H2 H1 H1 H2 H2 ... e falsum elimination f_fls_e H H H ... e
 truth introduction f_tru_i ... i double negation introduction f_negneg_i H H H ... i double negation elimination* f_negneg_e H H H ... e law of excluded middle* f_LEM ... LEM modus tollens f_MT H1 H2 H1 H1 H2 H2 ... MT universal elimination f_all_e H H H ... e
 existential introduction f_exi_i H H H ... i existential elimination f_exi_e H H1 H H H1 ... ... e ,-- equality introduction f_equ_i ... i equality elimination f_equ_e H1 H2 H1 H1 H2 H2 ... e