;; 2025-12-05.  ueb09.scm

#|
(load "~/git/minlog/init.scm")
(set! COMMENT-FLAG #f)
(libload "nat.scm")
(set! COMMENT-FLAG #t)
|#

;; Gauss sum based coding

;; 36
;; 28  37
;; 21  29  38
;; 15  22  30  39
;; 10  16  23  31  40
;;  6  11  17  24  32
;;  3   7  12  18  25  33
;;  1   4   8  13  19  26  34
;;  0   2   5   9  14  20  27  35

;; The Gauss sum (Gs n) is the sum of the first n natural numbers.

(add-program-constant "Gs" (py "nat=>nat"))
(add-computation-rules
 "Gs Zero" "Zero"
 "Gs(Succ n)" "Succ(Gs n)+n")

(set-totality-goal "Gs")
(fold-alltotal)
(ind)
(ng #t)
(intro 0)
;; 3
(assume "n" "IH")
(ng #t)
(use "NatPlusTotal")
(intro 1)
(use "IH")
(use "TotalVar")
;; Proof finished.
;; (cp)

;; Before going into Gauss sum based coding we prove the main property
;; of Gauss sums called here GsChar: Gs n=NatHalf(n*Succ n).  This
;; requires some preparations.

;; GsEq
(set-goal "all n Gs(Succ n)=Gs n+Succ n")
(assume "n")
(use "Truth")
;; Proof finished.
;; (cp)
(save "GsEq")

;; GsChar
(set-goal "all n Gs n=NatHalf(n*Succ n)")
(ind)
;; ...
;; Proof finished.
;; (cp)
(save "GsChar")

;; The following theorems may be helpful
(pp "GsEq")
(pp "NatDoubleEq")
(pp "NatDoublePlus")
(pp "NatDoublePlusEq")
(pp "NatDoubleHalfEven")
(pp "NatEvenTimesSucc")

;; GsProp
(set-goal "all n Gs(Succ n)+Gs n=(Succ n)*(Succ n)")
(ng)
(ind)
;; ...
;; Proof finished.
;; (cp)
(save "GsProp")

;; The following theorems may be helpful
(pp "NatPlusCancelEqR")
(pp "NatPlusAssoc")
(pp "NatPlusCancelEqL")
(pp "NatPlusComm")