ProofWeb

Working with ProofWeb

  1. Go to the web page
    http://prover.cs.ru.nl/
    OR
    http://carol.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.

  3. Log in using your username and password. (Ask your teacher for this information if you do not know it yet.)

  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


 

Formula


\begin{displaymath}(A \land B) \to A\end{displaymath}

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 $A \land B$ assumption
2 $A$ $\land$e$_1$ 1
3   $A \land B \to A$ $\to$i 1--2

Rendering in ProofWeb

1 H: A $\land$ B assumption
2 A $\land$e$_1$ 1
3 A $\land$ B $\to$ A $\to$i 1-2

Formula syntax

$\bot$   False
$\top$   True
$\neg A$   ~$\;A$
$A \land B$   $A$ /\ $B$
$A \lor B$   $A$ \/ $B$
$A \to B$   $A$ -> $B$
$A \leftrightarrow B$   $A$ <-> $B$
$\forall x\, A$   all $x$, $A$
$\exists x\, A$   exi $x$, $A$

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                


$m$

 $\;$H $A$   $m$ $\;$H $A$    


  ...            
$n$   $A$ $\quad$$\to$$\quad$ $n$   $A$ copy $m$  

insert H $B$		                


          ...    
      $n$ $\;$H $B$    
  ...       ...    
$n$   $A$ $\quad$$\to$$\quad$ $n + 1$   $A$    

               

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                
          ...    
      $n$   $A$    
          ...    
  ...   $n + 1$   $B$    
$n$   $A \land B$ $\quad$$\to$$\quad$ $n + 2$   $A \land B$ $\land$i $n,(n + 1)$  

conjunction elimination left		                
con_e1 $B$                
          ...    
  ...   $n$   $A \land B$    
$n$   $A$ $\quad$$\to$$\quad$ $n + 1$   $A$ $\land$e$_1$ $n$  

               
conjunction elimination right                
con_e2 $A$                
          ...    
  ...   $n$   $A \land B$    
$n$   $B$ $\quad$$\to$$\quad$ $n + 1$   $B$ $\land$e$_2$ $n$  

disjunction introduction left		                
dis_i1                
          ...    
  ...   $n$   $A$    
$n$   $A \lor B$ $\quad$$\to$$\quad$ $n + 1$   $A \lor B$ $\lor$i$_1$ $n$  

disjunction introduction right		                
dis_i2                
          ...    
  ...   $n$   $B$    
$n$   $A \lor B$ $\quad$$\to$$\quad$ $n + 1$   $A \lor B$ $\lor$i$_1$ $n$  

disjunction elimination		                
dis_e ($A$ \/ $B$) H1 H2                
          ...    
      $n$   $A \lor B$    
      $n + 1$ H1 $A$ assumption
        ...  
      $n + 2$ $C$  
      $n + 3$ H2 $B$ assumption
        ...  
  ...   $n + 4$ $C$  
$n$   $C$ $\quad$$\to$$\quad$ $n + 5$   $C$ $\lor$e $n$,$(n + 1)$--$(n + 2)$,$(n + 3)$--$(n + 4)$  

implication introduction		                
imp_i H                
      $n$ H $A$ assumption
        ...  
  ...   $n + 1$ $B$  
$n$   $A \to B$ $\quad$$\to$$\quad$ $n + 2$   $A \to B$ $\to$i $n$--$(n + 1)$  

               
implication elimination                
imp_e $A$                
          ...    
      $n$   $A \to B$    
          ...    
  ...   $n + 1$   $A$    
$n$   $B$ $\quad$$\to$$\quad$ $n + 2$   $B$ $\to$e $n,(n + 1)$  

negation introduction		                
neg_i H                
      $n$ H $A$ assumption
        ...  
  ...   $n + 1$ $\bot$  
$n$   $\neg A$ $\quad$$\to$$\quad$ $n + 2$   $\neg A$ $\neg$i $n$--$(n + 1)$  

negation elimination		                
neg_e $A$                
          ...    
      $n$   $\neg A$    
          ...    
  ...   $n + 1$   $A$    
$n$   $\bot$ $\quad$$\to$$\quad$ $n + 2$   $\bot$ $\neg$e $n,(n + 1)$  

falsum elimination		                
fls_e                
          ...    
  ...   $n$   $\bot$    
$n$   $A$ $\quad$$\to$$\quad$ $n + 1$   $A$ $\bot$e $n$  

truth introduction		                
tru_i                
  ...            
$n$   $\top$ $\quad$$\to$$\quad$ $n$   $\top$ $\top$i $n$  

double negation introduction$^\dagger$		                
negneg_i                
          ...    
  ...   $n$   $A$    
$n$   $\neg\neg A$ $\quad$$\to$$\quad$ $n + 1$   $\neg\neg A$ $\neg\neg$i $n$  

               
double negation elimination*                
negneg_e                
          ...    
  ...   $n$   $\neg\neg A$    
$n$   $A$ $\quad$$\to$$\quad$ $n + 1$   $A$ $\neg\neg$e $n$  

law of excluded middle*$^\dagger$		                
LEM                
  ...            
$n$   $A \lor \neg A$ $\quad$$\to$$\quad$ $n$   $A \lor \neg A$ LEM  

proof by contradiction*$^\dagger$		                
PBC H                
      $n$ H $\neg A$ assumption
        ...  
  ...   $n + 1$ $\bot$  
$n$   $A$ $\quad$$\to$$\quad$ $n + 2$   $A$ PBC $n$--$(n + 1)$  

modus tollens$^\dagger$		                
MT $B$                
          ...    
      $n$   $A \to B$    
          ...    
  ...   $n + 1$   $\neg B$    
$n$   $\neg A$ $\quad$$\to$$\quad$ $n + 2$   $\neg A$ MT $n,(n + 1)$  

universal introduction		                
all_i $y$                
        $y$    
        ...  
  ...   $n$ $A[y/x]$  
$n$   $\forall x\, A$ $\quad$$\to$$\quad$ $n + 1$   $\forall x\, A$ $\forall$i $n$--$n$  

universal elimination		                
all_e (all x, $A$)                
          ...    
  ...   $n$   $\forall x\, A$    
$n$   $A[t/x]$ $\quad$$\to$$\quad$ $n + 1$   $A[t/x]$ $\forall$e $n$  

               
existential introduction                
exi_i $t$                
          ...    
  ...   $n$   $A[t/x]$    
$n$   $\exists x\, A$ $\quad$$\to$$\quad$ $n + 1$   $\exists x\, A$ $\exists$i $n$  

existential elimination		                
exi_e (exi x, $A$) $y$ H                
          ...    
      $n$   $\exists x\, A$    
        $y$    
      $n + 1$ H $A[y/x]$  
        ...  
  ...   $n + 2$ $B$  
$n$   $B$ $\quad$$\to$$\quad$ $n + 3$   $B$ $\exists$e $n$,$(n + 1)$--$(n + 2)$  

equality introduction		                
equ_i                
  ...            
$n$   $t = t$ $\quad$$\to$$\quad$ $n$   $t = t$ $=$i  

equality elimination, simple version		                
equ_e ($t_1$ = $t_2$)                
          ...    
      $n$   $t_1 = t_2$    
          ...    
  ...   $n + 1$   $A[t_1/x]$    
$n$   $A[t_2/x]$ $\quad$$\to$$\quad$ $n + 2$   $A[t_2/x]$ $=$e $n,(n + 1)$  

equality elimination, general version ($t_2$ may occur in $A$)		                
equ_e' ($t_1$ = $t_2$) (fun x => $A$)                
          ...    
  ...   $n$   $t_1 = t_2$    
          ...    
  ...   $n + 1$   $A[t_1/x]$    
$n$   $A[t_2/x]$ $\quad$$\to$$\quad$ $n + 2$   $A[t_2/x]$ $=$e $n,(n + 1)$  

               

Forward tactics

conjunction introduction                
f_con_i H1 H2                


$m_1$

 $\;$H1 $A$   $m_1$ $\;$H1 $A$    


$m_2$

 $\;$H2 $B$   $m_2$ $\;$H2 $B$    


  ...            
$n$   $A \land B$ $\quad$$\to$$\quad$ $n$   $A \land B$ $\land$i $m_1,m_2$  

conjunction elimination left		                
f_con_e1 H                


$m$

 $\;$H $A \land B$   $m$ $\;$H $A \land B$    


  ...            
$n$   $A$ $\quad$$\to$$\quad$ $n$   $A$ $\land$e$_1$ $m$  

conjunction elimination right		                
f_con_e2 H                


$m$

 $\;$H $A \land B$   $m$ $\;$H $A \land B$    


  ...            
$n$   $B$ $\quad$$\to$$\quad$ $n$   $B$ $\land$e$_2$ $m$  

disjunction introduction left		                
f_dis_i1 H                


$m$

 $\;$H $A$   $m$ $\;$H $A$    


  ...            
$n$   $A \lor B$ $\quad$$\to$$\quad$ $n$   $A \lor B$ $\lor$i$_1$ $m$  

disjunction introduction right		                
f_dis_i2 H                


$m$

 $\;$H $B$   $m$ $\;$H $B$    


  ...            
$n$   $A \lor B$ $\quad$$\to$$\quad$ $n$   $A \lor B$ $\lor$i$_2$ $m$  

               
disjunction elimination                
f_dis_e H H1 H2                


$m$

 H $A \lor B$   $m$ H $A \lor B$    


      $n$ H1 $A$ assumption
        ...  
      $n + 1$ $C$  
      $n + 2$ H2 $B$ assumption
        ...  
  ...   $n + 3$ $C$  
$n$   $C$ $\quad$$\to$$\quad$ $n + 4$   $C$ $\lor$e $m$,$n$--$(n + 1)$,$(n + 2)$--$(n + 3)$  

implication elimination		                
f_imp_e H1 H2                


$m_1$

 $\;$H1 $A \to B$   $m_1$ $\;$H1 $A \to B$    


$m_2$

 $\;$H2 $A$   $m_2$ $\;$H2 $A$    


  ...            
$n$   $B$ $\quad$$\to$$\quad$ $n$   $B$ $\to$e $m_1,m_2$  

negation elimination		                
f_neg_e H1 H2                


$m_1$

 $\;$H1 $\neg A$   $m_1$ $\;$H1 $\neg A$    


$m_2$

 $\;$H2 $A$   $m_2$ $\;$H2 $A$    


  ...            
$n$   $\bot$ $\quad$$\to$$\quad$ $n$   $\bot$ $\neg$e $m_1,m_2$  

falsum elimination		                
f_fls_e H                


$m$

 $\;$H $\bot$   $m$ $\;$H $\bot$    


  ...            
$n$   $A$ $\quad$$\to$$\quad$ $n$   $A$ $\bot$e $m$  

               
truth introduction                
f_tru_i                
  ...            
$n$   $\top$ $\quad$$\to$$\quad$ $n$   $\top$ $\top$i $n$  

double negation introduction$^\dagger$		                
f_negneg_i H                


$m$

 $\;$H $A$   $m$ $\;$H $A$    


  ...            
$n$   $\neg\neg A$ $\quad$$\to$$\quad$ $n$   $\neg\neg A$ $\neg\neg$i $m$  

double negation elimination*		                
f_negneg_e H                


$m$

 $\;$H $\neg\neg A$   $m$ $\;$H $\neg\neg A$    


  ...            
$n$   $A$ $\quad$$\to$$\quad$ $n$   $A$ $\neg\neg$e $m$  

law of excluded middle*$^\dagger$		                
f_LEM                
  ...            
$n$   $A \lor \neg A$ $\quad$$\to$$\quad$ $n$   $A \lor \neg A$ LEM  

modus tollens$^\dagger$		                
f_MT H1 H2                


$m_1$

 $\;$H1 $A \to B$   $m_1$ $\;$H1 $A \to B$    


$m_2$

 $\;$H2 $\neg B$   $m_2$ $\;$H2 $\neg B$    


  ...            
$n$   $\neg A$ $\quad$$\to$$\quad$ $n$   $\neg A$ MT $m_1,m_2$  

universal elimination		                
f_all_e H                


$m$

 $\;$H $\forall x\, A$   $m$ $\;$H $\forall x\, A$    


  ...            
$n$   $A[t/x]$ $\quad$$\to$$\quad$ $n$   $A[t/x]$ $\forall$e $m$  

               
existential introduction                
f_exi_i H                


$m$

 $\;$H $A[t/x]$   $m$ $\;$H $A[t/x]$    


  ...            
$n$   $\exists x\, A$ $\quad$$\to$$\quad$ $n$   $\exists x\, A$ $\exists$i $m$  

existential elimination		                
f_exi_e H $y$ H1                


$m$

 H $\exists x\, A$   $m$ H $\exists x\, A$    


        $y$    
      $n$ H1 $A[y/x]$  
        ...  
  ...   $n + 1$ $B$  
$n$   $B$ $\quad$$\to$$\quad$ $n + 2$   $B$ $\exists$e $m$,$n$--$(n + 1)$  

equality introduction		                
f_equ_i                
  ...            
$n$   $t = t$ $\quad$$\to$$\quad$ $n$   $t = t$ $=$i  

equality elimination		                
f_equ_e H1 H2                


$m_1$

 $\;$H1 $t_1 = t_2$   $m_1$ $\;$H1 $t_1 = t_2$    


$m_2$

 $\;$H2 $A[t_1/x]$   $m_2$ $\;$H2 $A[t_1/x]$    


  ...            
$n$   $A[t_2/x]$ $\quad$$\to$$\quad$ $n$   $A[t_2/x]$ $=$e $m_1,m_2$  

               

About this document ...

This document was generated using the LaTeX2HTML translator Version 2002-2-1 (1.71)

Copyright © 1993, 1994, 1995, 1996, Nikos Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999, Ross Moore, Mathematics Department, Macquarie University, Sydney.

The command line arguments were:
latex2html -split 0 man.tex

The translation was initiated by Cezary Kaliszyk on 2008-01-24