Next: Proof Tactics Up: Computation Previous: Computational Content

# An Example

The following is a small proof in Nuprl with the extraction clauses shown explicitly. The system does not produce the comments (* *); we include them for illustrative purposes only. In the interest of condensing the presentation we also elide hypothesis lists wherever possible.

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top  (* term_of(thm) extracted *)                         |
|>> all x,y:int.(x=y in int)|some z:int.~(z=0 in int)#(x+z=y |
|   in int                                                   |
|                                                            |
|BY quantifier (* ext \x.\y.e1 (quantifier tactic does       |
|                               intro twice)     *)          |
|1* 1. x:(int)                                               |
|   2. y:(int)                                               |
|   >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))|
|                     (* ext e1 *)                           |
|2* >> (int) in U1                                           |
|                                                            |
|3* >> (int) in U1                                           |
'------------------------------------------------------------'
```

The rule quantifier is a tactic , a user--defined rule of inference, which successively applies the intro rule to each universal quantifier; in this case it performs two applications. This tactic was written by a user of the system and must be loaded as an ML object to be used; in general it would not be available. See the following chapter for more on tactics. The extracted term is a function which, given any values for x and y, will give a proof of the body; this corresponds to the intuitive meaning of all and justifies its definition as a dependent function. Note that e1 is the term extracted from the first subgoal; the next window shows the proof of this subgoal.

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top 1  (* e1 extracted *)                                 |
|1...2.                                                      |
|>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))   |
|                                                            |
|BY seq (x=y in int)|~(x=y in int) new E (* ext \E.e3(e2) *) |
|                                                            |
|1* 1...2.                                                   |
|   >> (x=y in int)|~(x=y in int)  (* ext e2 *)              |
|                                                            |
|2* 1...2.                                                   |
|   3. E:(x=y in int)|~(x=y in int)                          |
|   >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))|
|                      (* ext e3 *)                          |
'------------------------------------------------------------'
```

The seq rule extracts a function which in effect substitutes the proof of the seq term, e2, for each instance of its use in e3 (under the name E).

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top 1 1  (* e2 extracted *)                               |
|1...2.                                                      |
|>> (x=y in int)|~(x=y in int)                               |
|                                                            |
|BY arith (* ext int_eq(x;y;inl(axiom);inr(axiom)) *)        |
|                                                            |
|1* 1...2.                                                   |
|   >> x in int                                              |
|                                                            |
|2* 1...2.                                                   |
|   >> y  in int                                             |
|                                                            |
|3* 1...2.                                                   |
|   >> x in int                                              |
|                                                            |
|4* 1...2.                                                   |
|   >> y  in int                                             |
'------------------------------------------------------------'
```

The arith decision procedure produces the int_eq  term, a decision  procedure for equality on the integers.

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top 1 2 (* e3 extracted *)                                |
|1...2.                                                      |
|3. E:(x=y in int)|~(x=y in int)                             |
|>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))   |
|                                                            |
|BY elim 3 (* ext decide(E;l.e4;r.e5) *)                     |
|                                                            |
|1* 1...3.                                                   |
|   4. l:(x=y in int)                                        |
|   >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))|
|                              (* ext e4 *)                  |
|2* 1...3.                                                   |
|   4. r:~(x=y in int)                                       |
|   >> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))|
|                              (* ext e5 *)                  |
'------------------------------------------------------------'
```

The elim rule for disjoint unions produces a decide term. In the next frame the term l is extracted from the first subgoal because our goal is exactly l (the actual proof of this subgoal is not shown but is carried out using the rule hyp 4).

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top 1 2 1  (* e4 extracted *)                             |
|1...3.                                                      |
|4. l:(x=y in int)                                           |
|>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))   |
|                                                            |
|BY intro left  (* ext inl(e6) *)                            |
|                                                            |
|1* 1...4.                                                   |
|   >> (x=y in int)  (* ext e6==l (follows by hyp 4) *)      |
|                                                            |
|2* 1...4.                                                   |
|   >> some z:int.~(z=0 in int)#(x+z=y in int) in U1         |
'------------------------------------------------------------'
```

In the next frame r is extracted for the same reason as l is above.

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top 1 2 2  (* e5 extracted *)                             |
|1...3.                                                      |
|4. r:~(x=y in int)                                          |
|>> ((x=y in int)|some z:int.~(z=0 in int)#(x+z=y in int))   |
|                                                            |
|BY intro right (* ext inr(e7) *)                            |
|                                                            |
|1* 1...4.                                                   |
|   >> some z:int.~(z=0 in int)#(x+z=y in int) (ext e7 *)    |
|                                                            |
|2* 1...4.                                                   |
|   >> ((x=y in int)) in U1                                  |
'------------------------------------------------------------'
```

In the next frame, since some is defined to be a dependent product we extract a pair consisting of an element of the integers, y-x, and a proof, e8, that the proposition is true for this element. This corresponds to the desired meaning of some.

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top 1 2 2 1 (* e7 extracted *)                            |
|1...3.                                                      |
|4. r:~(x=y in int)                                          |
|>> some z:int.~(z=0 in int)#(x+z=y in int)                  |
|                                                            |
|BY intro y-x  (* ext <y-x,e8> *)                            |
|                                                            |
|1* 1...4.                                                   |
|   >> y-x in (int)                                          |
|                                                            |
|2* 1...4.                                                   |
|   >> ((y-x=0  in int)->void)#(x+y-x=y  in int) (* ext e8 *)|
|                                                            |
|3* 1...4.                                                   |
|   5. z:(int)                                               |
|   >> (~(z=0 in int)#(x+z=y in int)) in U1                  |
'------------------------------------------------------------'
```

The product intro produces a pair consisting of proofs of the two subgoals. Although the proof is not shown here, subgoal 2 can be seen to follow trivially by arith.

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top 1 2 2 1 2  (* e8 extracted *)                         |
|1...3.                                                      |
|4. r:~(x=y in int)                                          |
|>> ((y-x=0 in int)->void)#(x+y-x=y in int) (* ext <e9,e10>*)|
|                                                            |
|BY intro                                                    |
|                                                            |
|1* 1...4.                                                   |
|   >> (y-x=0  in int)->void  (* ext e9 *)                   |
|                                                            |
|2* 1...4.                                                   |
|   >> x+y-x=y  in int (* ext e10==axiom (follows by arith)*)|
'------------------------------------------------------------'
```

In the next frame we see that hypotheses 4 and 5 contradict each other. The system somewhat arbitrarily extracts ( v0.any(v0))(r(axiom)) from this (we could extract anything we desired from a contradiction).

```,------------------------------------------------------------,
|EDIT THM thm                                                |
|------------------------------------------------------------|
|* top 1 2 2 1 2 1 (* e9 extracted *)                        |
|1...3.                                                      |
|4. r:~(x=y in int)                                          |
|>> (y-x=0  in int)->void                                    |
|                                                            |
|BY intro new f (* ext \f.e11 *)                             |
|                                                            |
|1* 1...4.                                                   |
|   5. f:y-x=0  in int                                       |
|   >> void  (* ext e11==(\v0.any(v0))(r(axiom))             |
|                                                            |
|2* 1...4.                                                   |
|   >> (y-x=0  in int) in U1                                 |
'------------------------------------------------------------'
```

We could now have the following session with the evaluator . What follows has additional white space (spaces and carriage returns) to improve readability.

```,------------------------------------------------------------,
|P>eval                                                      |
|E>term_of(thm);;                                            |
|\x.\y.(\E.decide(E;l.inl(l);                                |
|        r.inr(<y-x,<\f.(\v0.any(v0))(r(axiom)),axiom>>)))   |
|       (int_eq(x;y ;inl(axiom);inr(axiom)))                 |
|E>term_of(thm)(7)(7);;                                      |
|inl(axiom)                                                  |
|E>term_of(thm)(7)(10);;                                     |
|inr(<10-7,<\f.(\v0.any(v0))(axiom(axiom)),axiom>>)          |
|E>let d = \y.decide(y;u.p1(u);u.p1(u));;                    |
|\y.decide(y;u.p1(u);u.p1(u))                                |
|E>d(term_of(thm)(7)(10));;                                  |
|3                                                           |
'------------------------------------------------------------'
```

To terminate an eval session type .

Next: Proof Tactics Up: Computation Previous: Computational Content

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995