; $Id: higman-finite.scm,v 1.9 2008/03/26 09:50:37 logik Exp $
; higman-finite.scm: Higman's Lemma for a finite alphabet.

(set! COMMENT-FLAG #f)
(exload "bar/bar.scm")
(set! COMMENT-FLAG #t)

(animate "Prop1")
(animate "BarThm")

; 1. Inductive definition bar on letters (use small capitals)

(add-program-constant "ll" (py "list nat=>nat=>boole"))

; Note have introduced ll (corresponds to Good(.,.)in the main text)
; as aprogram constant instead of an inductive predicate since ll
; should be decidable.

(add-computation-rule (pt "ll(Nil nat)b") (pt "False"))
(add-computation-rule (pt "ll(as::a)b")
                      (pt "[if (a=b) True (ll as b)]"))

; "llTotal"
(set-goal (pf "Total ll"))
(use "Total")
(use "All-AllPartial")

(ind)
; Base
(ng)
(use "Total")
(assume "a^" "u1")
(ng)
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "boole"))))
(use "Truth-Axiom")
; Step
(assume "w" "a" "IH")
(ng)
(use "Total")
(use "All-AllPartial")
(assume "a1")
(ng)
(cases (pt "a=a1"))
(assume "a=a1")
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "boole"))))
(use "Truth-Axiom")
(assume "a=a1 -> F")
(ng)
(use "Total")
(use "IH")
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "nat"))))
(use "Truth-Axiom")
; Proof finished.
(save "llTotal")

(add-ids (list (list "good" (make-arity word)))
	 '("all as,a(ll as a -> good(as::a))")
	 '("all as,a(good as -> good(as::a))"))

(add-ids (list (list "barw" (make-arity word) "algbarw"))
	 '("allnc as(good as -> barw as)" "leaf")
	 '("allnc as((all a barw(as::a)) -> barw as)" "branch"))

; 2. Inductive definition of Bars

(define seqlist (py "list list list nat"))
(add-var-name "vss" "wss" seqlist)

(add-program-constant "Insertfolder" (mk-arrow seqlist word nat seqlist))
(add-computation-rule (pt "Insertfolder(Nil list list nat)w i")
		      (pt "(Nil list list nat)"))
(add-computation-rule (pt "Insertfolder(vss::ws)w i")
                      (pt "[if (i=Lh vss)
                               (vss::(ws::w))
                               ((Insertfolder vss w i)::ws)]"))

; "InsertfolderTotal"
(set-goal (pf "Total Insertfolder"))
(use "Total")
(use "All-AllPartial")

(ind)
; Base
(ng)
(use "Total")
(assume "w^" "u1")
(ng)
(use "Total")
(assume "a^" "u2")
(ng)
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst
				 (py "list list list nat"))))
(use "Truth-Axiom")

; Step
(assume "vss" "ws" "IH")
(ng)
(use "Total")
(use "All-AllPartial")
(assume "w")
(ng)
(use "Total")
(use "All-AllPartial")
(assume "a")
(ng)
(cases (pt "a=Lh vss"))
(assume "a=Lh vss")
(ng)
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst
				 (py "list list list nat"))))
(ng)
(use "Truth-Axiom")

(assume "a=Lh vss -> F")
(ng)
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst
				 (py "list list list nat"))))
(ng)
(use (make-proof-in-aconst-form (finalg-to-total-to-e-aconst
				 (py "list list list nat"))))
(use "Total")
(use "Total")
(use "IH")
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst
				 (py "list nat"))))
(use "Truth-Axiom")
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "nat"))))
(use "Truth-Axiom")
; Proof finished.
(save "InsertfolderTotal")


(add-ids
 (list (list "Bars" (make-arity seqlist) "algBars"))
 '("allnc vss,i(i<Lh vss -> Good ((vss)__i) -> Bars vss)" "Leafs")
 '("allnc vss(all w,i,n(n=Lh vss -> i<n -> Bars(Insertfolder vss w i))
                       -> Bars vss)" "Branchs"))

; 3. Definitions of lasts, bseq and Folder

(add-program-constant "lasts" (mk-arrow seq word) t-deg-one)
(add-computation-rule (pt "lasts(Nil list nat)") (pt "(Nil  nat)"))  
(add-computation-rule (pt "lasts(ws::(w::a))") (pt "(lasts ws)::a"))

; We need an extra element x of type nat not in the finite alphabet
; and an additional computation rule (pt "lasts(ws::(Nil nat))") ->
; (pt "(lasts w}::x") to ensure that "lasts" is total.

(add-program-constant "bseq" (mk-arrow word word))
(add-computation-rule (pt "bseq(Nil nat)") (pt "(Nil  nat)")) 
(add-computation-rule (pt "bseq(as::a)")
                      (pt "[if (ll(bseq as)a)
                               (bseq as)
                               ((bseq as)::a)]"))

; "bseqTotal"
(set-goal (pf "Total bseq"))
(use "Total")
(use "All-AllPartial")
(ind)

; Base
(ng)
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "list nat"))))
(use "Truth-Axiom")

; Step
(assume "w" "a" "IH")
(ng)
(cases (pt "ll(bseq w)a"))
(use (make-proof-in-aconst-form (finalg-to-total-to-e-aconst (py "boole"))))
(use "Total")
(use "Total")
(use "llTotal")
(use "IH")
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "nat"))))
(use "Truth-Axiom")
(assume "ll(bseq w)a")
(ng)
(use "IH")
(assume "ll(bseq w)a -> F")
(ng)
(use (make-proof-in-aconst-form (finalg-to-e-to-total-aconst (py "list nat"))))
(ng)
(use (make-proof-in-aconst-form (finalg-to-total-to-e-aconst (py "list nat"))))
(use "IH")
; Proof finished.
(save "bseqTotal")


(add-program-constant "memb" (mk-arrow nat word nat) t-deg-one)
(add-computation-rule (pt "memb a(w::b)") (pt "[if (a=b) (Lh w) (memb a w)]"))

; We need an extra computation rule (pt "memb a(Nil nat)") -> (pt "0")
; to ensure that "memb" is total.  Then memb a w<Lh w means that memb
; is properly applied.

(add-program-constant "folder" (mk-arrow seq seqlist) t-deg-one)
(add-computation-rule (pt "folder(Nil list nat)")
                      (pt "(Nil list list nat)"))
(add-computation-rule (pt "folder(ws::(w::a))")
                      (pt "[if (ll(bseq(lasts ws))a)
                               (Insertfolder(folder ws)w  
                                  (memb a(bseq(lasts ws))))
                               ((folder ws)::(ws::w))]"))   

; We need an additional computation rule (pt "folder(ws::(Nil nat)")
; -> (pt "(folder ws)::ws") to ensure that "folder" is total.


; 4. Interactive proofs and program extraction

; Lemma 1 (Lemma 5.7)

(add-global-assumption
 "Lemma1" (pf "allnc vss,ws,i(i<Lh vss -> Good(vss__i) -> 
                                   folder ws= vss -> Good ws)"))
; Lemma 2i (Lemma 5.8 i)

(set-goal (pf "Bars(Nil list list nat)"))
(intro 1)
(ng)
(assume "w" "i" "n" "H1")
(simp "H1")
(strip)
(use "Efq")
(use 2)
; Proof finished.
(save "Lemma2i")

; Lemma 2ii (Lemma 5.8ii)

(set-goal
 (pf "allnc ws(Bar ws -> allnc wss(Bars wss -> Bars(wss::ws)))"))
(assume "ws0")

; 1. Ind(Bar).
(elim)

; 1.1
(strip)
(intro 0 (pt "Lh wss"))
(ng)
(use "Truth-Axiom")
(ng)
(use 2)

; 1.2
(assume "ws" "IH1a" "IH1b" "wss0")
(drop "IH1a")

; 2. Ind(Bars).
(elim)

; 2.1.
(strip)
(intro 0 (pt "i"))
(add-global-assumption "Aux1" (pf "allnc i,j(i<j -> i<j+1)"))
(use-with "Aux1" (pt "i") (pt "Lh vss") 5)
(ng)
(add-global-assumption "Aux2" (pf "allnc i,j(i<j -> i=j -> F)"))
(inst-with  "Aux2" (pt "i") (pt "Lh vss") 5)
(simp 7)
(ng)
(simp 5)
(ng)
(use 6)

; 2.2 
(assume "wss" "IH2a" "IH2b")
(intro 1)
(assume "w" "i" "n" 7)
(simp 7)
(strip)
(ng)

; 6:i<Succ Lh wss, hence either i=Lh vss  or  i<Lh vss
; instead of cases on i=Lh wss, which is not allowed since wss is a cv-var,
; we do cases on i+1=n (Note: 5:n=Succ Lh wss). 

(cases (pt "i+1=n"))

; case1: i=Lh vss 
(simp 7)
(ng)
(strip)
(simp 9)
(ng)
(use "IH1b")
(intro 1)
(use "IH2a")

;case 2: i<Lh vss (= n-1)
(simp 7)
(ng)
(strip)
(simp 9)
(ng)
(use "IH2b" (pt "n--1"))
(simp 7)
(ng)
(use "Truth-Axiom")
(simp 7)
(ng)
(add-global-assumption "Aux3" (pf "allnc i,k(i<k+1 -> (i=k -> F) -> i<k)"))
(use "Aux3")
(use 8)
(use 9)
; Proof finished.
(save "Lemma2ii")

; Program extraction
(add-var-name "gc" (py "list nat=>algBars=>algBars"))
(add-var-name "gd" (py "list nat=>nat=>nat=>algBars"))
(pp (nt (proof-to-extracted-term (theorem-name-to-proof "Lemma2ii"))))

; [algBar0]
;  (Rec algBar=>algBars=>algBars)algBar0([algBars2]cLeafs)
;  ([ga2,gc3,algBars4]
;    (Rec algBars=>algBars)algBars4 cLeafs
;    ([gd5,gd6]
;      cBranchs
;      ([w7,a8,a9]
;        [if (Succ a8=a9) (gc3 w7(cBranchs gd5)) (gd6 w7 a8(Pred a9))])))

; Higman's Lemma (Proposition 5.9)

(set-goal (pf "allnc as(barw as ->
               allnc vss(Bars vss ->
               all ws(bseq(lasts ws)=as ->
                       folder ws = vss ->
                       Bar ws)))"))
(assume "as0")

; Ind(barw)
(elim)

; 1.1
(strip)
(use "Efq")
(add-global-assumption
 "Aux4" (pf "allnc as,ws(good as -> bseq(lasts ws)=as -> F)"))
(use-with "Aux4" (pt "as") (pt "ws") 2 4)

; 1.2
(assume "as" "IH1a" "IH1b" "vss0")
(drop "IH1a")

;Ind(Bars)
(elim)

; 2.1.
(strip)
(intro 0)
(use-with "Lemma1" (pt "vss") (pt "ws") (pt "i") 5 6 8)

; 2.2.
(assume "vss" "IH2a" "IH2b" "ws" 7 8)

(intro 1)

; Ind(w)
(ind)

; 3.1
(use "Prop1")

; 3.2
(assume "w" "a" "IH3")

; To show: Bar(ws::w::a)

(cases (pt "ll (bseq(lasts ws)) a"))
; Problem: lasts is not total

; case1: ll (bseq(lasts ws)) a
(strip)

(use "IH2b" (pt "w") (pt "memb a (bseq (lasts (ws::(w::a))))") 
            (pt "Lh (folder ws)"))
(simp 8)
(use "Truth-Axiom")

(add-global-assumption
 "Aux5" (pf "allnc ws,a(ll(bseq(lasts ws))a -> 
                  memb a(bseq(lasts ws::a))<Lh(folder ws))"))
(use "Aux5")
(use 10)

; bseq(lasts(ws::(w::a)))=as from
(ng)
(simp 10)
(ng)
(use 7)

; folder(ws::(w::a))=Insertfolder vss w(memb a(bseq(lasts(ws::(w::a))))) from
(ng)
(simp 10)
(ng)
(simp 8)
(ng)
(use "Truth-Axiom")

; case2: (ll(bseq(lasts ws))a -> F)
(strip)
(use "IH1b" (pt "a") (pt "(folder ws)::(ws::w)"))

; Bars(folder ws)::(ws::w)
(use "Lemma2ii")

; Bar(ws::w)
(use "IH3")

; Bars vss
(simp 8)
(intro 1)
(use "IH2a")

; bseq(lasts(ws::(w::a)))=(as::a)
(ng)
(simp 10)
(ng)
(use 7)

;folder(ws::(w::a))=(folder ws)::(ws::w)
(ng)
(simp 10)
(ng)
(use "Truth-Axiom")
; Proof finished.
(save "Theorem")

(add-var-name "ge" (py "nat=>algbarw"))
(add-var-name "gf" (py "nat=>algBars=>list(list nat)=>algbarw"))
(add-var-name "gg" (py "list nat=>nat=>nat=>list(list nat)=>algbarw"))
(define program (proof-to-extracted-term (theorem-name-to-proof "Theorem")))
(pp (nt program))

; [algbarw0]
;  (Rec algbarw=>algBars=>list list nat=>algBar)algbarw0([algBars3,ws4]cLeaf)
;  ([ge3,(nat=>algBars=>list list nat=>algBar)_4,algBars5]
;    (Rec algBars=>list list nat=>algBar)algBars5([ws7]cLeaf)
;    ([gd7,(list nat=>nat=>nat=>list list nat=>algBar)_8,ws9]
;      cBranch
;      ([w10]
;        (Rec list nat=>algBar)w10 cPropOne
;        ([w11,a12,algBar13]
;          [if (ll(bseq(lasts ws9))a12)
;            ((list nat=>nat=>nat=>list list nat=>algBar)_8 w11
;            (memb a12
;             [if (ll(bseq(lasts ws9))a12)
;               (bseq(lasts ws9))
;               (bseq(lasts ws9)::a12)])
;            Lh(folder ws9)
;            (ws9::(w11::a12)))
;            ((nat=>algBars=>list list nat=>algBar)_4 a12
;            (cLemmaTwoii algBar13(cBranchs gd7))
;            (ws9::(w11::a12)))]))))
 
(animate "Theorem")
(animate "Lemma2i")
(animate "Lemma2ii")

; Since the given alphabet is finite, here for simplicity we assume
; a fixed number of letters, e.g., 5.

(add-global-assumption "FiniteAlphabet" (pf "all as(5<Lh as -> good as)"))

(set-goal (pf "barw(Nil nat)"))
(intro 1) (assume "a0")
(intro 1) (assume "a1")
(intro 1) (assume "a2")
(intro 1) (assume "a3")
(intro 1) (assume "a4")
(intro 1) (assume "a5")
(intro 0) (use "FiniteAlphabet")
(ng)
(use "Truth-Axiom")
; Proof finished.
(save "barwNil")
(animate "barwNil")

; Higman's Lemma: Bar[]

(set-goal (pf "Bar(Nil list nat)"))
(use "Theorem" (pt "(Nil nat)") (pt "(Nil list list nat)"))
(use "barwNil")
(use "Lemma2i")
(ng)
(use "Truth-Axiom")
(ng)
(use "Truth-Axiom")
; Proof finished.
(save "HigmanFinite")
(animate "HigmanFinite")

; Every infinite sequence has a good initial segment

(set-goal (pf "all f ex m Good(f fbar m)"))
(assume "f")
(use "BarThm" (pt "(Nil list nat)") (pt "0"))
(use "HigmanFinite")
(ng)
(use "Truth-Axiom")
; Proof finished.

(define program (proof-to-extracted-term (current-proof)))
(define nprogram (nt program))

; 5. Test of the program

; We define sequences: nat->word via adding term rewriting rules.  The
; extracted program yields a number n such that the initial segment of
; length n is good.

(define (run-higman infinite-sequence)
  (pp (nt (mk-term-in-app-form nprogram infinite-sequence))))

; a. The sequence [4 1], [3 3 0], [0 4 0 1], [2], ...

(add-program-constant "Seq" (mk-arrow (py "nat") (py "list nat")))
(add-rewrite-rule (pt "Seq 0") (pt ":4::1"))
(add-rewrite-rule (pt "Seq 1") (pt ":3::3::0"))
(add-rewrite-rule (pt "Seq 2") (pt ":0::4::0::1"))
(add-rewrite-rule (pt "Seq(n+3)") (pt ":2"))
(run-higman (pt "Seq"))
; ==> 3

; b. [0 0], [1], [1 0], [], [], ...

(add-program-constant "Interesting" (mk-arrow nat word))
(add-rewrite-rule (pt "Interesting 0") (pt ":0::0"))
(add-rewrite-rule (pt "Interesting 1") (pt ":1"))
(add-rewrite-rule (pt "Interesting 2") (pt ":1::0"))
(add-rewrite-rule (pt "Interesting 3") (pt "(Nil nat)"))
(add-rewrite-rule (pt "Interesting(n+4)") (pt "(Nil nat)"))
(run-higman (pt "Interesting"))
; ==> 5  
; Example that not the shortest good initial seqment is found!

; c. [1], [3], [5], [7], [9], [0], ...

(add-program-constant "Sixelts" (mk-arrow nat word))
(add-rewrite-rule (pt "Sixelts 0") (pt ":1"))
(add-rewrite-rule (pt "Sixelts 1") (pt ":3"))
(add-rewrite-rule (pt "Sixelts 2") (pt ":5"))
(add-rewrite-rule (pt "Sixelts 3") (pt ":7"))
(add-rewrite-rule (pt "Sixelts 4") (pt ":9"))
(add-rewrite-rule (pt "Sixelts 5") (pt ":0"))
(run-higman (pt "Sixelts"))

;==> 6
; Note by assumption there are only five different letters;
; So the proof yields that the sequence [[1] [3] [5] [7] [9] [0]] is good;
; i.e., two of the used numbers must be equal.


; 6. Proof of unproven assumptions.

; In order to prove 
; Aux4: all as,ws(good as -> bseq(lasts ws)=as -> F),
; Aux5: all ws,a(ll(bseq(lasts ws))a -> 
;                  memb a(bseq(lasts ws::a))<Lh(folder ws)),
; we need computation rules (which should have been introduced before)

(add-computation-rule (pt "lasts(ws::(Nil nat))")
        	      (pt "(Nil nat)"))
(add-computation-rule (pt "folder(ws::(Nil nat))")
                      (pt "(Nil list list nat)"))

(set-goal (pf "all as,a(ll as a -> (memb a as)<Lh as)"))
(ind)
(ng)
(search)

(assume "w" "b" "IH" "a")
(ng)
(cases (pt "b=a"))
(assume 2)
(ng)
(simp 2)
(ng)
(search)

(assume 2)
(ng)
(cut (pf "a=b ->F"))
(assume 3)
(simp 3)
(ng)
(assume 4)
(use "Aux1")
(use-with "IH" (pt "a") 4)

(assume 3)
(use 2)
(simp 3)
(use "Truth-Axiom")
; Proof finished.
(save "Aux5a")

(set-goal (pf "all vss,w,a Lh(Insertfolder vss w a)=Lh vss"))
(ind)
(strip)
(ng)
(use "Truth-Axiom")

(assume "vss" "ws" "IH" "w" "a")
(ng)

(cases (pt "a=Lh vss"))
(assume 2)
(ng)
(use "Truth-Axiom")

(assume 2)
(ng)
(use "IH")
; Proof finished.
(save "LhInsertfolder")

; Next, we prove the following invariant:
(set-goal (pf "all ws Lh(folder ws)=Lh (bseq(lasts ws))"))
(ind)
(ng)
(use "Truth-Axiom")
(assume "ws")
(ind)
(ng)
(search)

(assume "w" "a" 1 2)
(ng)
(cases (pt "(ll(bseq(lasts ws))a)"))
(assume 3)
(ng)

; Lh(Insertfolder(folder ws)w(memb a(bseq(lasts ws))))=Lh(bseq(lasts ws)) 

; (add-rewrite-rule (pt "Lh(Insertfolder vss w a)") (pt "Lh vss"))
; gives an error
; arguments in lhs need to fit the *unsubstituted* type of op
; But we can simplify with "LhInsertfolder"

(simp "LhInsertfolder")
(use 2)

(ng)
(assume 3)
(use 2)
(save "Aux5b")


; Proof of Aux5:
(set-goal (pf "all ws,a(ll(bseq(lasts ws))a -> 
               memb a(bseq(lasts ws::a))<Lh(folder ws))"))
(strip)
(inst-with "Aux5b" (pt "ws"))
(ng)
(simp 1)
(ng)
(simp 2)
(ng)
(use "Aux5a")
(use 1)
; Proof finished.


; Proof of Aux4:
(set-goal (pf "all as(good as -> (Nil nat)=as -> F)"))
(assume "as")
(elim)
(ng)
(search)
(assume "bs" "b" 1 2 3)
(use 4)
; Proof finished.
(save "Aux4a")


(set-goal (pf "all w,a(w::a=w-> F)"))
(ind)
(search)
(assume "w" "b" "IH" "a" "H1")
(use "IH" (pt "b"))
(use "H1")
; Proof finished.

; (set-goal (pf "all w,a. (w::a)=w-> F"))
; (ind)
; (ng)
; (search)
; (assume "w" "b" "IH" "a" 2)
; (use "IH" (pt "b"))
; (add-global-assumption "lemma1" (pf "all v,w,a,b. (v::a)=(w::b) -> v=w"))
; (use "lemma1" (pt "a") (pt "b"))
; (use 2)
; (save "wa-ne-w")


(set-goal (pf "all as,a(good(as::a) -> all bs((as::a)=bseq bs -> F))"))
(assume "as1" "a1" "IdHyp")
(elim "IdHyp")

; 1. allnc as,a(ll as a -> all bs(as::a=bseq bs -> F)) from
(assume "as" "a" "H1")
(ind)
; bs=[]
(ng)
(search)

; bs::b
(assume "bs" "b" "H2")
(ng)

(cases (pt "(ll(bseq bs)b)"))
(assume "H3")
(ng)
(use "H2")

; not ll(bseq bs)b.

(assume "H3")
(ng)
(strip)
(use "H3")
(inst-with 5 'left)
(simp "<-" 6)
(inst-with 5 'right)
(simp "<-" 7)
(use "H1")

;allnc as,a(good as -> (all bs.as=bseq bs -> F) -> all bs.(as::a)=bseq bs -> F)
(assume "as" "a" "H1" "H2")
(ind)
; bs=[]
(ng)
(search)

; bs::b
(assume "bs" "b" "H3")
(ng)

(cases (pt "(ll(bseq bs)b)"))

(assume "H4")
(ng)
(use "H3")

; not ll(bseq bs)b.

(assume "H4")
(ng)
(assume "H5")
(inst-with-to "H5" 'left "H6")
(use-with "H2" (pt "bs") "H6")
; Proof finished.
(save "Aux4b")


(set-goal (pf "all as(good as -> all bs(as=bseq bs -> F))"))
(cases)
(strip)
(use "Aux4a" (pt "(Nil nat)"))
(use 1)
(use "Truth-Axiom")
(use "Aux4b")
; Proof finished.
(save "Aux4c")


(set-goal (pf "all as,ws(good as -> bseq(lasts ws)=as -> F)"))
(strip)
(use "Aux4c" (pt "as") (pt "lasts ws"))
(use 1)
(simp 2)
(use "Truth-Axiom")
; Proof finished.