Formal and semi-formal proof development

Henk Barendregt henk@cs.kun.nl

September 15, 2002

1. Newman’s Lemma

As an appendix to “Towards an interactive mathematical proof language” the present file contains a simulation of an interactive mathematical proof development for Newman’s lemma. The file should not be printed but viewed for the interactive effect. This is best done using active dvi, URL

<pauillac.inria.fr/activedvi>
Variable A:Set.
Definition Bin:=[B:Set](B->B->Prop).
Inductive TC [R:(Bin A)]: (Bin A) :=
TCb:  (x,y:A)(R x y)->(TC R x y)|
TCf:  (x,y,z:A)((R x z)->(TC R z y)->(TC R x y)).
Inductive TRC [R:(Bin A)]: (Bin A) :=
TRCb:  (x:A)(TRC R x x)|
TRCf:  (x,y,z:A)((R x z) -> (TRC R z y)->(TRC R x y)).
Definition Trans [R:(Bin A)]: Prop:=
(x,y,z:A)((R x y)->(R y z)->(R x z)).
Definition IND [R: (Bin A);P:(A->Prop)]:  Prop :=
((a:A)((y:A)(a R y)-> (P y))->(P a)).
Definition cr [R:(Bin A);a:A]:=
(b1,b2:A)(TRC R a b1)/\(TRC R a b2)->(EX c:A|(TRC R b1 c)/\(TRC R b2
c)).

Definition CR [R:(Bin A)]:=(a:A)(cr R a).
Definition WCR [R:(Bin A)]:=
(a,b1,b2:A)(a R b1)->(a R b2)->(EX c:A|(TRC R b1 c)/\(TRC R b2 c)).
Definition WF [R:(Bin A)]:Prop:= (P:A->Prop)(IND R P)->(a:A)(P a).
Variable R:(Bin A).
Lemma p0:  (x,y:A)((R x y) -> (TC R x y)).
Lemma p1:  (x,y:A)((R x y) -> (TRC R x y)).
Lemma p2:  (x,y:A)((TC R x y) -> (TRC R x y)).
Lemma p3:  (Trans (TC R)).
Lemma p4:  (Trans (TRC R)).
Lemma p5:  (x,y,z:A)(R x y)->(TRC R y z)->(TRC R x z).
Lemma p6:  (x,y:A)((TC R x y)->(EX z:A | (R x z)/\(TRC R z y))).
Lemma p7:  (x,y:A)((TRC R x y)-> (eq A x y)\/(TC R x y)).

The proof-script for these lemmas are not shown. The main lemma is as follows.

Lemma main :  (WCR R)->(IND R (cr R)).

Now we will give an interactive mathematical proof script, for which we claim that it should essentially be acceptable by a mathematician-friendly proof-assistant. On the left we find the mathematical script, on the right the proof-state. Notice that it does contain some Coq-like statements, like “Intros”, but these disappear and are replaced by mathematical statements. Statements typed by the user are first displayed in red, by the system in green.

First we introduce some userfriendly notation.

Notation. For a,b:A we write
   (i) a R  b := (R a b).
  (ii) a R+ b := (TC R a b).
  (iii) a R* b := (TRC R a b).

1.1. Mathmode

Lemma main :  (WCR R)->(IND R (cr R)).
Proof                                          \underline{(WCR R)->(IND R (cr R))}
Intros.

Lemma main :  (WCR R)->(IND R (cr R)).
Proof.                                         \underline{(IND R (cr R))}
Assume WCR(R).                                 (WCR R)
⟨Clicking on IND above⟩.

Lemma main :  (WCR R)->(IND R (cr R)).
Proof.                                         \underline{(a:A)(y:A)((aRy)->(cr R y))->(cr R a)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Intros.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{cr R a}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
⟨Clicking on cr above⟩.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{(b1,b2:A)(a R* b1/\ a R* b2)->(EX c|b1 R* c/\ b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Intros.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],
[a=b2 \/ a R+ b2],
by lemma 6.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b2).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,
by lemma 7.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b1).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,                 p5:(EX x1:A|a R x1 R* b1)
by lemma 7.                                    p6:(EX x2:A|a R x2 R* b2)
Pick x1.  Pick x2.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b1).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,                 p5:(EX x1:A|a R x1 R* b1)
by lemma 7.                                    p6:(EX x2:A|a R x2 R* b2)
Pick x1.  Pick x2.                             x1,x2:A
                                               p7:a R x1
                                               p8:x1 R* b1
                                               p9:a R x2
                                               p10:x2 R* b2
We have
(EX x.xi R* x), i=1,2,
by (WCR R).

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b1).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,                 p5:(EX x1:A|a R x1 R* b1)
by lemma 7.                                    p6:(EX x2:A|a R x2 R* b2)
Pick x1.  Pick x2.                             x1,x2:A
                                               p7:a R x1
                                               p8:x1 R* b1
                                               p9:a R x2
                                               p10:x2 R* b2
We have
(EX x.xi R* x), i=1,2,                         p11:(EX x.x1 R* x)
by (WCR R).                                    p12:(EX x.x2 R* x)
Pick x.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b1).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,                 p5:(EX x1:A|a R x1 R* b1)
by lemma 7.                                    p6:(EX x2:A|a R x2 R* b2)
Pick x1.  Pick x2.                             x1,x2:A
                                               p7:a R x1
                                               p8:x1 R* b1
                                               p9:a R x2
                                               p10:x2 R* b2
We have
(EX x.xi R* x), i=1,2,                         p11:(EX x.x1 R* x)
by (WCR R).                                    p12:(EX x.x2 R* x)
Pick x.                                        x:A
                                               p13:x1 R* x
                                               p14:x2 R* x
We have
(cr R x1),
by IH.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b1).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,                 p5:(EX x1:A|a R x1 R* b1)
by lemma 7.                                    p6:(EX x2:A|a R x2 R* b2)
Pick x1.  Pick x2.                             x1,x2:A
                                               p7:a R x1
                                               p8:x1 R* b1
                                               p9:a R x2
                                               p10:x2 R* b2
We have
(EX x.xi R* x), i=1,2,                         p11:(EX x.x1 R* x)
by (WCR R).                                    p12:(EX x.x2 R* x)
Pick x.                                        x:A
                                               p13:x1 R* x
                                               p14:x2 R* x
We have
(cr R x1),                                     p15:(cr R x1)
by IH.
Hence
(EX b.b1 R* b /\ x R* b).
Pick b.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b1).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,                 p5:(EX x1:A|a R x1 R* b1)
by lemma 7.                                    p6:(EX x2:A|a R x2 R* b2)
Pick x1.  Pick x2.                             x1,x2:A
                                               p7:a R x1
                                               p8:x1 R* b1
                                               p9:a R x2
                                               p10:x2 R* b2
We have
(EX x.xi R* x), i=1,2,                         p11:(EX x.x1 R* x)
by (WCR R).                                    p12:(EX x.x2 R* x)
Pick x.                                        x:A
                                               p13:x1 R* x
                                               p14:x2 R* x
We have
(cr R x1),                                     p15:(cr R x1)
by IH.
Hence
(EX b.b1 R* b /\ x R* b).                      b:A
Pick b.                                        p17:x R* b
                                               p18:b1 R* x
Moreover
(cr R x2),
by IH.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b1).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,                 p5:(EX x1:A|a R x1 R* b1)
by lemma 7.                                    p6:(EX x2:A|a R x2 R* b2)
Pick x1.  Pick x2.                             x1,x2:A
                                               p7:a R x1
                                               p8:x1 R* b1
                                               p9:a R x2
                                               p10:x2 R* b2
We have
(EX x.xi R* x), i=1,2,                         p11:(EX x.x1 R* x)
by (WCR R).                                    p12:(EX x.x2 R* x)
Pick x.                                        x:A
                                               p13:x1 R* x
                                               p14:x2 R* x
We have
(cr R x1),                                     p15:(cr R x1)
by IH.
Hence
(EX b.b1 R* b /\ x R* b).                      b:A
Pick b.                                        p17:x R* b
                                               p18:b1 R* x
Moreover
(cr R x2),                                     p19:(cr R x2)
by IH.
Hence
(EX c.b R* c /\ b2 R* c),
by x2 R* b.  Pick c.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.                                         \underline{EX c:A.(b1 R* c)/\(b2 R* c)}
Assume WCR(R).                                 (WCR R)
Remember IND.
Let a:A.                                       a:A
Assume
(y:A)((aRy)->(cr R y)).   (IH)                 IH:(y:A)(a R y)->(cr R y)
Remember cr.
Let a,b1,b2:A.                                 b1, b2:A
Assume a R* bi, i=1,2.                         a R* b1
                                               a R* b2
We have
[a=b1 \/ a R+ b1],                             p1:[a=b1 \/ a R+ b1]
[a=b2 \/ a R+ b2],                             p2:[a=b2 \/ a R+ b2]
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).                                     p3:(a R+ b1)
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).                                     p4:(a R+ b1).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,                 p5:(EX x1:A|a R x1 R* b1)
by lemma 7.                                    p6:(EX x2:A|a R x2 R* b2)
Pick x1.  Pick x2.                             x1,x2:A
                                               p7:a R x1
                                               p8:x1 R* b1
                                               p9:a R x2
                                               p10:x2 R* b2
We have
(EX x.xi R* x), i=1,2,                         p11:(EX x.x1 R* x)
by (WCR R).                                    p12:(EX x.x2 R* x)
Pick x.                                        x:A
                                               p13:x1 R* x
                                               p14:x2 R* x
We have
(cr R x1),                                     p15:(cr R x1)
by IH.
Hence
(EX b.b1 R* b /\ x R* b).                      b:A
Pick b.                                        p17:x R* b
                                               p18:b1 R* x
Moreover
(cr R x2),                                     p19:(cr R x2)
by IH.
Hence
(EX c.b R* c /\ b2 R* c),                      p20:b R* c
by x2 R* b.  Pick c.                           p21:b2 R* c
                                               c:A
Since
b1 R* c,
by (Trans R*),
we have bi R* c, i=1,2.                        p22:b1 R* c
                                               p23:b2 R* c
Thus c works.

Lemma main :  (WCR R)->(IND R (cr R))
Proof.
Assume WCR(R).
Remember IND.
Let a:A.
Assume
(y:A)((aRy)->(cr R y)).   (IH)
Remember cr.
Let a,b1,b2:A.
Assume a R* bi, i=1,2.

We have
[a=b1 \/ a R+ b1],
[a=b2 \/ a R+ b2],
by lemma 6.
Case a=b1, take c=b2.  Trivial.
Hence wlog
(a R+ b1).
Case a=b2, take c=b1.  Trivial.
Hence wlog
(a R+ b2).
Therefore
(EX xi:A|a R xi R* bi), i=1,2,
by lemma 7.
Pick x1.  Pick x2.

We have
(EX x.xi R* x), i=1,2,
by (WCR R).
Pick x.

We have
(cr R x1),
by IH.
Hence
(EX b.b1 R* b /\ x R* b).
Pick b.
Moreover
(cr R x2),
by IH.
Hence
(EX c.b R* c /\ b2 R* c),
by x2 R* b.  Pick c.
Since
b1 R* c,
by (Trans R*),
we have bi R* c, i=1,2.
Thus c works.  QED                             Goal proved!

This establishes the correctness of main lemma by a certified proof. We display it again in the usual more compact form.

Lemma main :  (WCR R)->(IND R (cr R)).
Proof.  Assume WCR(R). Remember IND. Let a:A. Assume
        (y:A)((aRy)->(cr R y)).                            (IH)
Remember cr.  Let a,b1,b2:A. Assume a R* bi, i=1,2.
We have
[a=b1 \/ a R+ b1],
[a=b2 \/ a R+ b2],
by lemma 6.
Case a=b1, take c=b2.  Trivial.  Hence wlog (a R+ b1).
Case a=b2, take c=b1.  Trivial.  Hence wlog (a R+ b2).
Therefore (EX xi:A|a R xi R* bi), i=1,2, by lemma 7.
Pick x1.  Pick x2.
We have (EX x.xi R* x), i=1,2, by (WCR R). Pick x.
We have (cr R x1), by IH. Hence
(EX b.b1 R* b /\ x R* b).
Pick b.  Moreover (cr R x2), by IH. Hence
(EX c.b R* c /\ b2 R* c),
by x2 R* b.  Pick c.  Since b1 R* c, by (Trans R*), we have
(bi R* c), i=1,2.  Thus c works.  QED
Newman's Lemma.  WCR(R)/\WF(R) -> CR(R).
Proof.  Assume WCR(R) and WF(R). Then (IND R( cr R)),
by WCR(R) and main.  Remember IND. We have
(P:(A->Prop))((a:A)((y:A)(a R y)-> (P y))->(P a)).          (+)
Apply (+) to P(a)=(cr R a).  Then CR(R). QED