Newman.ml

%*****************************************************************************

                       Newman's Lemma

                        Jan 18 1985                                      

*****************************************************************************%

use `relations`;;

% We show here Newman's lemma: A Noetherian relation is confluent iff it is
locally confluent. %

% We first need to show that xR+y implies for some z xRz & zR*y %
% We thus give a dual definition Plus' of transitive closure %

% In order to avoid unduly currification, we give a preliminary construction
  for "Exists x : P(x) & Q(x)". %
let SIGMA2 = "!A.{P|A->*}{Q|A->*}!B.([x:A](P x)->(Q x)->B)->B";;
CLASS `Sig2` SIGMA2;; % Some better notation should be used %

let PLUS' = "!A.{R|A->A->*}[x:A][y:A]
    		(Sig2 A [z:A](R x z) [z:A](Star A R z y))";;
CLASS `Plus'` PLUS';;

% Two intermediate lemmas needed for PLUS_TO_PLUS' %
let ONE_TO_PLUS' = "!A.{R|A->A->*}[x:A][y:A] (R x y)->(Plus' A R x y)";;

let ONE_TO_PLUS'_PROOF = "!A.{R|A->A->*}[x:A][y:A]
                    [h1:(R x y)]
                    !B.
                    [h2:[z:A](R x z)->(Star A R z y)->B]
                    (h2 y h1 (Refl_Star A R y))";;
LET `R_to_R'` ONE_TO_PLUS'_PROOF ONE_TO_PLUS';;

let HER_PLUS' = "!A.{R|A->A->*}[x:A] (Her A R (Plus' A R x))";;

let HER_PLUS'_PROOF = "!A.{R|A->A->*}[x:A][y:A][z:A]
                    [h1:(Plus' A R x y)]
                    [h2:(R y z)]
                    !B.
                    [h3:[u:A](R x u)->(Star A R u z)->B]
(h1 B
 ([v:A][h4:(R x v)][h5:(Star A R v y)]
  (h3 v h4 (Plus_to_Star A R v z (Star_to_Plus A R v y z h5 h2)))))";;

LET `Her_Plus'` HER_PLUS'_PROOF HER_PLUS';;

let PLUS_TO_PLUS' = "!A.{R|A->A->*}[x:A][y:A] 
    			(Plus A R x y)->(Plus' A R x y)";;

let PLUS_TO_PLUS'_PROOF = "!A.{R|A->A->*}[x:A][y:A]
                    [h1:(Plus A R x y)]
                    (h1 
                     (Plus' A R x)
                     (Her_Plus' A R x) 
                     (R_to_R' A R x))";;

LET `Plus_to_Plus'` PLUS_TO_PLUS'_PROOF PLUS_TO_PLUS';;

let STAR_CASES = "!A.{R|A->A->*}[x:A][y:A]
    	(Star A R x y)->((<A>x=y)+(Plus A R x y))";;

let STAR_CASES_PROOF = "!A.{R|A->A->*}[x:A][y:A][h:(Star A R x y)]
		    !B.
                    [h1:(<A>x=y)->B]
                    [h2:(Plus A R x y)->B]
		    (h B ([eq:(<A>y=x)](h1 (sym_equal A y x eq))) h2)";;
% Remark that we pay here the orientation of = in the definition of Star %

LET `Star_cases` STAR_CASES_PROOF STAR_CASES;;

let TRANS_STAR = "!A.{R|A->A->*}(Trans A (Star A R))";;

let TRANS_STAR_PROOF = "!A.{R|A->A->*}[x:A][y:A][z:A]
	[h1:(Star A R x y)]
	[h2:(Star A R y z)]
	(h1 (Star A R x z)
   ([h3:(<A>y=x)](h3 [u:A](Star A R u z) h2))
   ([h3:(Plus A R x y)](Star_cases A R y z h2
    (Star A R x z)
    [h4:(<A>y=z)](Plus_to_Star A R x z (h4 ([u:A](Plus A R x u)) h3))
    [h4:(Plus A R y z)](Plus_to_Star A R x z (Trans_Plus A R x y z h3 h4)))))"
;;

LET `Trans_Star` TRANS_STAR_PROOF TRANS_STAR;;

let COHERENT = "!A.{R|A->A->*}[x:A][y:A]
	     (Sig2 A (Star A R x) (Star A R y))";;
CLASS `Coherent` COHERENT;;

let CONFLUENT = "!A.{R|A->A->*}[x:A][y:A][z:A]
             (Star A R x y)->(Star A R x z)->(Coherent A R y z)";;
CLASS `Confluent` CONFLUENT;;

let LOCALLY_CONFLUENT = "!A.{R|A->A->*}[x:A][y:A][z:A]
             (R x y)->(R x z)->(Coherent A R y z)";;
CLASS `Locally_Confluent` LOCALLY_CONFLUENT;;

let DIAGRAM = "!A.{R|A->A->*}[x:A]
  ([u:A](R x u)->(Confluent A R u))->(Locally_Confluent A R x)->
  [y:A][z:A](Plus' A R x y)->(Plus' A R x z)->(Coherent A R y z)";;

let DIAGRAM_PROOF = "!A.{R|A->A->*}[x:A]
[induction_hyp:[u:A](R x u)->(Confluent A R u)]
[hyp:(Locally_Confluent A R x)]
[y:A][z:A]
[arc1:(Plus' A R x y)]
[arc2:(Plus' A R x z)]
!B.
[coher:[u:A](Star A R y u)->(Star A R z u)->B]
(arc1 B
([b:A][arc3:(R x b)][arc4:(Star A R b y)]
(arc2 B 
([c:A][arc5:(R x c)][arc6:(Star A R c z)]
(hyp b c arc3 arc5 B
   ([u:A][arc7:(Star A R b u)][arc8:(Star A R c u)]
    (induction_hyp b arc3 y u arc4 arc7 B
       ([v:A][arc9:(Star A R y v)][arc10:(Star A R u v)]
        (induction_hyp c arc5 v z (Trans_Star A R c u v arc8 arc10) arc6 B
           ([w:A][arc11:(Star A R v w)][arc12:(Star A R z w)]
            (coher w (Trans_Star A R y v w arc9 arc11) arc12)))))))))))";;

LET `diagram` DIAGRAM_PROOF DIAGRAM;;

let COROLLARY = "!A.{R|A->A->*}[x:A]
         ([a:A](R x a)->(Confluent A R a))->(Locally_Confluent A R x)->
         [y:A][z:A](Plus A R x y)->(Plus A R x z)->(Coherent A R y z)";;

let COROLLARY_PROOF  = "!A.{R|A->A->*}[x:A]
                    [induction_hyp:[a:A](R x a)->(Confluent A R a)]
                    [hyp:(Locally_Confluent A R x)]
                    [y:A][z:A]
                    [arc:(Plus A R x y)]
                    [arc':(Plus A R x z)]
                    (diagram A R x induction_hyp hyp y z 
			(Plus_to_Plus' A R x y arc)
			(Plus_to_Plus' A R x z arc'))";;

LET `corollary` COROLLARY_PROOF COROLLARY;;

let NEWMAN_IND = "!A.{R|A->A->*}[x:A]
       ([a:A](R x a)->(Confluent A R a))->(Locally_Confluent A R x)->
       [y:A][z:A](Star A R x y)->(Star A R x z)->(Coherent A R y z)";;

let NEWMAN_IND_PROOF = "!A.{R|A->A->*}[x:A]
                     [induction_hyp:[a:A](R x a)->(Confluent A R a)]
                     [hyp:(Locally_Confluent A R x)]
                     [y:A][z:A]
                     [arc:(Star A R x y)]
                     [arc':(Star A R x z)]
(Star_cases A R x y arc (Coherent A R y z)
    ([case1:(<A>x=y)]!B.[coher:[v:A](Star A R y v)->(Star A R z v)->B]
                       (coher z
                           (case1 ([u:A](Star A R u z)) arc')
                           (Refl_Star A R z)))
    ([case2:(Plus A R x y)](Star_cases A R x z arc' (Coherent A R y z)
    	   ([case21:(<A>x=z)]!B.[coher:[v:A](Star A R y v)->(Star A R z v)->B]
                       (coher y
                           (Refl_Star A R y)
                           (case21 ([u:A](Star A R u y)) arc)))
           ([case22:(Plus A R x z)]
		(corollary A R x induction_hyp hyp y z case2 case22)))))";;
LET `Newman_ind` NEWMAN_IND_PROOF NEWMAN_IND;;


let NOETHERIAN = "!A.{R|A->A->*}{P|A->*}
                  ([x:A]([y:A](R x y)->(P y))->(P x))->[x:A](P x)";;
CLASS `Noetherian` NOETHERIAN;;
% Noetherian induction %

let NEWMAN = "!A.{R|A->A->*}
	(Noetherian A R)->(Locally_Confluent A R)->(Confluent A R)";;

let NEWMAN_PROOF= "!A.{R|A->A->*}
                    [h1:(Noetherian A R)]
                    [h2:(Locally_Confluent A R)]
                    (h1 
                       ([u:A](Confluent A R u))  
                       ([x:A][ind:[y:A](R x y)->(Confluent A R y)]
                              (Newman_ind A R x ind (h2 x))))";;
LET `Newman` NEWMAN_PROOF NEWMAN;;