;; 2022-06-19. ueb11.scm (load "~/git/minlog/init.scm") (set! COMMENT-FLAG #f) (libload "nat.scm") (set! COMMENT-FLAG #t) ;; Exercise 42 ;; Adding the graph of fib (add-ids (list (list "G" (make-arity (py "nat") (py "nat")))) '("G 0 0" "InitGZero") '("G 1 1" "InitGOne") '("allnc n^,m^,l^(G n^ m^ -> G(Succ n^)l^ -> G(Succ(Succ n^))(m^ +l^))" "GenG")) (display-idpc "G") ;; We will need "NatPlusTotal at some point. (pp "NatPlusTotal") ;; allnc n^(TotalNat n^ -> allnc n^0(TotalNat n^0 -> TotalNat(n^ +n^0))) ;; Fib (set-goal "allnc n^(Total n^ -> exr m^(Total m^ andl G n^ m^))") (assume "n^" "Tn") (cut "allnc n^ (Total n^ -> exr m^,l^ (Total m^ andi Total l^ andi G n^ m^ andi G (Succ n^) l^))") (assume "CutHyp") ;; ... (define proof (np (current-proof))) ;; (proof-to-expr-with-formulas proof) (define eterm (proof-to-extracted-term proof)) (add-var-name "nm" (py "nat yprod nat")) (define neterm (rename-variables (nt eterm))) (pp neterm) ;; Exercise 44 (load "~/git/minlog/init.scm") (set! COMMENT-FLAG #f) (libload "nat.scm") (libload "list.scm") (libload "pos.scm") (libload "int.scm") (libload "rat.scm") (set! COMMENT-FLAG #t) (add-var-name "M" (py "nat=>nat=>rat")) (remove-var-name "i" "j" "k") (add-var-name "i" "j" "k" (py "nat")) ;; We prove the general proposition MaxSegRel, relative to an assumption ;; u expressing the step for end segments. (set-goal "all M( all n( exl j(j<=n andnc all j1(j1<=n -> M j1 n<=M j n)) -> exl j(j<=n+1 andnc all j1(j1<=n+1 -> M j1(n+1)<=M j(n+1)))) -> all n exd i,j exl k( i<=k andnc j<=n andnc k<=n andnc all i1,k1(i1<=k1 -> k1<=n -> M i1 k1<=M i k) andnc all j1(j1<=n -> M j1 n<=M j n)))") (assume "M" "u") (ind) ;; 3,4 ;; Base (intro 0 (pt "Zero")) (intro 0 (pt "Zero")) (intro 0 (pt "Zero")) (ng #t) (msplit) ;; all j(j=Zero -> M j Zero<=M Zero Zero) (assume "j" "j=0") (simp "j=0") (use "Truth") (use "LeqRefl") ;; 15 all i,k(i<=k -> k=Zero -> M i k<=M Zero Zero) (assume "i" "k" "i<=k" "k=0") (simp "k=0") (simphyp-with-to "i<=k" "k=0" "i<=0") (ng "i<=0") (simp "i<=0") (use "Truth") (use "Truth") (use "Truth") (use "Truth") ;; 4 ;; Step (assume "n" "IHn") (by-assume-with "IHn" "i" "iProp") (by-assume-with "iProp" "j" "jProp") (by-assume-with "jProp" "k" "IH") (cut "exl j(j<=n+1 andnc all j1(j1<=n+1 -> M j1(n+1)<=M j(n+1)))") (use "Id") ;for let (assume "ExEndSegStep") (by-assume-with "ExEndSegStep" "j1" "j1Prop") ;; Now we can define i1 and k1 (cases (pt "M j1(n+1)<=M i k")) ;; 42,43 ;; Case M j1(n+1)<=M i k (assume "CaseHyp") (intro 0 (pt "i")) (intro 0 (pt "j1")) (intro 0 (pt "k")) (msplit) ;; all j(j<=Succ n -> M j(Succ n)<=M j1(Succ n)) (use "j1Prop") ;; all i0,k0(i0<=k0 -> k0<=Succ n -> M i0 k0<=M i k) (assume "i1" "k1" "i1<=k1" "k1<=n+1") (use "NatLeCases" (pt "k1") (pt "Succ n")) (use "k1<=n+1") (assume "k1 F). Then the maximal end segment is ;; the maximal segment. Take i1=j1 and k1=n+1. (assume "CaseHyp") (intro 0 (pt "j1")) (intro 0 (pt "j1")) (intro 0 (pt "n+1")) (msplit) ;; all j(j<=Succ n -> M j(Succ n)<=M j1(Succ n)) (use "j1Prop") ;; all i,k(i<=k -> k<=Succ n -> M i k<=M j1(n+1)) (assume "i1" "k1" "i1<=k1" "k1<=n+1") (use "NatLeCases" (pt "k1") (pt "Succ n")) (use "k1<=n+1") (assume "k1 M j0(n+1)<=M j(n+1))) (use "u") (intro 0 (pt "j")) (split) (use "IH") (use "IH") ;; Proof finished. ;; (cp) (save "MaxSegRel") (define eterm (proof-to-extracted-term)) (add-var-name "ijk" (py "nat yprod nat yprod nat")) (add-var-name "jk" (py "nat yprod nat")) (add-var-name "step" (py "nat=>nat=>nat")) (define neterm (rename-variables (nt eterm))) (ppc neterm) ;; EndSeg (set-goal "all M,n,m(m<=n -> exl j2(j2<=m andnc all j1(j1<=m -> M j1 n<=M j2 n)))") (assume "M" "n") (ind) ;; 3,4 ;; Base (assume "Useless") (intro 0 (pt "Zero")) (split) (use "Truth") (assume "j1") (ng #t) (assume "j1=0") (simp "j1=0") (use "Truth") ;; 4 ;; Step (assume "m" "IHm" "m+1<=n") (assert "exl j(j<=m andnc all j0(j0<=m -> M j0 n<=M j n))") (use "IHm") (use "NatLeTrans" (pt "Succ m")) (use "Truth") (use "m+1<=n") (assume "ExHyp") (by-assume-with "ExHyp" "j" "jProp") (cases (pt "M j n<=M(m+1)n")) ;; 23,24 ;; Case M j n<=M(m+1)n (assume "CaseHyp") (intro 0 (pt "Succ m")) (split) (use "Truth") (assume "j1" "j1<=m+1") (use "NatLeCases" (pt "j1") (pt "Succ m")) (use "j1<=m+1") (assume "j1 F (assume "CaseHyp") (intro 0 (pt "j")) (split) (use "NatLeTrans" (pt "m")) (use "jProp") (use "Truth") (assume "j1" "j1<=m+1") (use "NatLeCases" (pt "j1") (pt "Succ m")) (use "j1<=m+1") (assume "j1 k1<=n -> M i1 k1<=M i k) andnc all j1(j1<=n -> M j1 n<=M j n))") (assume "M") (use "MaxSegRel") (assume "n" "Useless") (use "EndSeg") (use "Truth") ;; Proof finished. ;; (cp) (save "MaxSeg") (define eterm (proof-to-extracted-term)) (define neterm (rename-variables (nt eterm))) (pp neterm) (animate "MaxSegRel") (animate "EndSeg") (define neterm (rename-variables (nt eterm))) (ppc neterm) (deanimate "MaxSegRel") (deanimate "EndSeg") ;; We prove EndSegStepMon, assuming the monotonicity of seg. ;; EndSegStepMon (set-goal "all M( all i,j,k(M i k<=M j k -> M i(k+1)<=M j(k+1)) -> all n( exl j(j<=n andnc all j1(j1<=n -> M j1 n<=M j n)) -> exl j(j<=n+1 andnc all j1(j1<=n+1 -> M j1(n+1)<=M j(n+1)))))") (assume "M" "MMon" "n" "EndSeg-n") (by-assume-with "EndSeg-n" "j" "EndSeg-j") (inst-with-to "EndSeg-j" 'left "j<=n") (inst-with-to "EndSeg-j" 'right "IHj") (drop "EndSeg-j") (cases (pt "M j(n+1)<=M(n+1)(n+1)")) ;; 11,12 ;; Case M j(n+1)<=M(n+1)(n+1) ;; ... (define eterm (proof-to-extracted-term)) (define neterm (rename-variables (nt eterm))) (pp neterm) ;; MaxSegMon (set-goal "all M( all i,j,k(M i k<=M j k -> M i(k+1)<=M j(k+1)) -> all n exd i,j exl k( i<=k andnc j<=n andnc k<=n andnc all i1,k1(i1<=k1 -> k1<=n -> M i1 k1<=M i k) andnc all j1(j1<=n -> M j1 n<=M j n)))") ;; ... (define eterm (proof-to-extracted-term)) (define neterm (rename-variables (nt eterm))) (pp neterm) (animate "MaxSegRel") (animate "EndSegStepMon") (define neterm (rename-variables (nt eterm))) (ppc neterm)