INRIA Sophia Antipolis - BP 93 06902 Sophia Antipolis - France Olivier.Pons@inria.fr

Undoing and Managing a proof

Olivier Pons[*]

April 8, 1998

Abstract:

In this paper we work in the area of proof script management. We study the dependencies between commands in a script and how they can be exploited in the undoing process. We present some problems that we have met in our implementation of proof managing tools in the Ctcoq interface for the Coq System.

Introduction

.

Developing a theory or proving a non-trivial theorem is not a linear and monotonic process. It is sometimes necessary to change and refine the context and the specification of the problem, and the proof investigation is done by trial and error and by multiple attempts. Often this task is not convenient and not easy with proof assistants based on tactics.

Most systems maintain a historical dependency between steps. This type of dependency is not sufficient and logical dependency is more useful. We have experimented and implemented some tools to help the user to understand the structure of proofs and to manage proofs using this type of dependency.

The whole implementation has been done in Ctcoq, a graphical user-interface [#!Ctcoq!#] for the Coq proof assistant [#!Coq95!#] based on the Centaur system [#!Centaur2.0!#].

Proof Structure

Like many other proof systems (Lego[#!Luo92!#,#!Pollack94!#], Alf[#!Magnusson95!#]

) the Coq proof assistant is based on a higher order type theory (for Coq this is the Inductive Calculus of Construction). Following the Curry-Howard isomorphism, a formula (or a specification) is represented by a type, and a proof of this formula (or the program that realizes it) by a 1#1-term of this type. Proving a formula consists in giving a term whose type is the formula.

For example, in Coq, we can express the associativity of addition with the following lemma. The notation (n,m,p:nat) must be read 2#2 and [ ] is a notation for lambda abstraction. 



Lemma plus_assoc_l : (n,m,p:nat)((plus n (plus m p))=(plus (plus n m) p)).

proof:
[n,m,p:nat]
 (nat_ind [n0:nat](plus n0 (plus m p))=(plus (plus n0 m) p)
   (refl_equal nat (plus m p))
   [n0:nat]
    [H:(plus n0 (plus m p))=(plus (plus n0 m) p)]
     (eq_ind_r nat (plus (plus n0 m) p)
       [n1:nat](S n1)=(S (plus (plus n0 m) p))
       (refl_equal nat (S (plus (plus n0 m) p))) (plus n0 (plus m p)) H)
   n)


The proof script

Constructing a proof term is a difficult task. In fact, the proof term is usually not handled directly. To build a proof term, we use a goal directed transition engine. This means that we state the goal to prove and we transform this formula, step by step, by applying commands that break it down in a number of subgoals until we reach a final state with no more goals. The commands used in this process are called tactics. The list of tactics, called the proof script can be edited directly by the user or generated by mechanism like proof-by-pointing or drag-and-drop[#!pbp!#].

This script has a linear structure. But behind this, there is an arborescent structure where each node is a tactic and the children nodes are the tactics applied on the subgoals generated by the parent tactic. For example, the proof term given above corresponds to the script and the tree below:





Navigating in a proof script

The first step towards understanding the proof is understanding its tree structure. We have implemented tools to navigate in this tree structure. With our tools, by selecting a tactic anywhere in the script, we can move up, down, and transversally according to the tree structure just by a key-strokes. For example in the script above selecting the tactic intros and striking C-c C-U we move up the selection on the tactic Elim n. The implementation of these facilities is described in section [*].

Undoing: Coherence of the remaining script

Generally, during goal-directed proofs, there are several goals that can be attacked indifferently. Processing a given goal is performed by combining the tactic with a numeric prefix referring to the goal's rank (when no number is provided the default value is 1). Pruning a proof branch may affect the position of goals and the numeric prefixes have to be updated.

This problem can be divided in two subtasks. First we want to be sure that the part of the script that is not undone is still valid (that is, if we replay it we will get the same result), secondly we want to be able to replay the undone part possibly after modification. Figure [*] show the undoing mechanisms.

Coherence of the preserved script

The problem is to determine the lines where a numeric prefix change is needed. All the tactics in the script that are above the head of the branch to prune can stay unchanged. For the others, tactics that are ``before'' the branch head (with a lexicographic order on the path set) in the tactics tree can also stay unchanged. Tactics that are behind must have their numeric prefix decremented by (n-1) where n is the number of open subgoals in the pruned branch at that point.

Here is the algorithm, where T is the undone branch head, (number t) is the numeric prefix number of tactic t, (rank t) is the position of t in the script and (path t) is the path of t in the proof tree. The order ``<'' on paths is simply a lexicographic order. 

Update-preserved-part T
-----------------------
  shift := number-of-sub-goals T
  t        := t-initial
 WHILE t IN played-script  DO
     IF  rank (t) > rank (T)
       THEN  IF path (t) > path (T)
                THEN IF  (path T) is-prefix-of? (path t)
                        THEN (shift := shift + (number-of-sub-goals t) -1)
                        ELSE (number t) <- (number t) - shift
                     END IF
       END IF
 (next t)
 END OF WHILE

Olivier Pons
4/8/1998