;; 2019-10-21.  intro.scm

(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)

;; 1.  Coercions
;; =============

;; We overload operators like +,*,/,<=,<, and automatically raise the
;; type of arguments when reading.  For instance, + should take its
;; arguments, compute the lub rho of their types, raise the type of
;; both arguments to type rho, apply RhoPlus to the results.  A number
;; should be displayed at the lowest possible level.

(display-alg "nat" "pos" "int" "rat")

;; nat
;; 	Zero:	nat
;; 	Succ:	nat=>nat
;; pos
;; 	One:	pos
;; 	SZero:	pos=>pos
;; 	SOne:	pos=>pos
;; int
;; 	IntPos:	pos=>int
;; 	IntZero:	int
;; 	IntNeg:	pos=>int
;; rat
;; 	RatConstr:	int=>pos=>rat

(display-default-varnames)

;; a: 	rat
;; kj: 	int yprod int
;; k: 	int
;; p: 	pos
;; n: 	nat

;; ppn (pretty print with names) shows the internal conversions
;; (coercions)

(ppn (pt "n+p"))
;; (n NatPlus (PosToNat p))

(ppn (pt "n+k"))
;; ((NatToInt n) IntPlus k)

(ppn (pt "n+a"))
;; (((NatToInt n) RatConstr 1) RatPlus a)

(ppn (pt "p+k"))
;; ((IntPos p) IntPlus k)

(ppn (pt "p+a"))
;; (((IntPos p) RatConstr 1) RatPlus a)

(ppn (pt "k+a"))

(display-pconst "PosToNat")

;; PosToNat
;;   comprules
;; 0	PosToNat 1	Succ Zero
;; 1	PosToNat(SZero p)	NatDouble(PosToNat p)
;; 2	PosToNat(SOne p)	Succ(PosToNat(SZero p))

(display-pconst "NatToPos")

;; NatToPos
;;   comprules
;; 0	NatToPos n	(GRec nat pos)([n]n)n NatToPosStep

(display-pconst "NatToInt")

;; NatToInt
;;   comprules
;; 0	Zero	0
;; 1	Succ n	IntS n

(ppn (pt "Succ Zero+2"))
;; ((Succ Zero) NatPlus (PosToNat 2))

(ppn (pt "Succ Zero+IntPos 2"))
;; ((NatToInt (Succ Zero)) IntPlus (IntPos 2))

(ppn (pt "Succ Zero+(2#3)"))

;; (((NatToInt (Succ Zero)) RatConstr 1)
;;   RatPlus
;;   ((IntPos 2) RatConstr 3))

(pp (pt "Succ Zero+(2#3)"))
;; Succ Zero+(2#3)

(pp (nt (pt "Succ Zero+(2#3)")))
;; 5#3

(ppn (nt (pt "Succ Zero+(2#3)")))
;; ((IntPos 5) RatConstr 3)

;; 2.  Equality of rationals
;; =========================

(display-pconst "RatEqv")

;; RatEqv
;;   comprules
;; 0	(k#p)==(j#q)	k*q=j*p
;;   rewrules
;; 0	a==a	True
;; 1	~a+a==0	True
;; 2	a+ ~a==0	True
;; 3	a+c==b+c	a==b
;; 4	a+b==a+c	b==c
;; 5	RatUDiv a==RatUDiv b	a==b
;; 6	(p#q)*a==(p#q)*b	a==b
;; 7	a*(p#q)==b*(p#q)	a==b
;; 8	~a== ~b	a==b
;; 9	(IntN p#q)*a==(IntN p#q)*b	a==b
;; 10	a*(IntN p#q)==b*(IntN p#q)	a==b

(search-about "Rat" "Eqv")

;; Theorems with name containing Rat and Eqv
;; RatEqvUMinusInj
;; all a,b (~a== ~b)=(a==b)
;; RatEqvTimesCancelR
;; all a,b,c(0<abs c -> a*c==b*c -> a==b)
;; RatEqvTimesCancelL
;; all a,b,c(0<abs a -> a*b==a*c -> b==c)
;; RatEqvUDivInj
;; all a,b (RatUDiv a==RatUDiv b)=(a==b)
;; RatEqvPlusCancelL
;; all a,b,c(a+b==a+c -> b==c)
;; RatEqvPlusCancelR
;; all a,b,c(a+c==b+c -> a==b)
;; RatEqvConstrPlus
;; all k,j,p (k+j#p)==(k#p)+(j#p)
;; RatEqvPlusMinusRev
;; all a,b a+b+ ~b==a
;; RatEqvPlusMinus
;; all a,b a+ ~b+b==a
;; RatEqvCompat
;; all a,b,c,d(a==b -> c==d -> (a==c)=(b==d))
;; RatEqvTrans
;; all a,b,c(a==b -> b==c -> a==c)
;; RatEqvConstrTimes
;; all k,p,q (k#p)==(k*q#p*q)
;; RatEqvSym
;; all a,b(a==b -> b==a)
;; No global assumptions with name containing Rat and Eqv

;; 3.  Commands
;; ============

;; use, use-with
;; assume
;; assert, cut
;; inst-with-to
;; intro, elim
;; simp, simp-with
;; ind, cases

;; 4.  Totality
;; ============

(search-about 'all "All" "Total")

;; ...
;; AllTotalIntro
;; allnc alpha^(Total alpha^ -> (Pvar alpha)alpha^) -> 
;; all alpha (Pvar alpha)alpha

;; AllTotalElim
;; all alpha (Pvar alpha)alpha -> 
;; allnc alpha^(Total alpha^ -> (Pvar alpha)alpha^)

;; AllncTotalIntro
;; allnc alpha^(TotalNc alpha^ -> (Pvar alpha)alpha^) -> 
;; allnc alpha (Pvar alpha)alpha

;; AllncTotalElim
;; allnc alpha (Pvar alpha)alpha -> 
;; allnc alpha^(TotalNc alpha^ -> (Pvar alpha)alpha^)

(term-to-t-deg (pt "n+m"))
;; 1

(term-to-t-deg (pt "n^ +m"))
;; 0

;; 5.  Computational content
;; =========================

(display-idpc "TotalNat" "TotalNatNc")

;; TotalNat	with content of type nat
;; 	TotalNatZero:	TotalNat Zero
;; 	TotalNatSucc:	allnc n^(TotalNat n^ -> TotalNat(Succ n^))

;; TotalNatNc	non-computational
;; 	TotalNatNcZero:	TotalNatNc Zero
;; TotalNatNcSucc:	allnc n^(TotalNatNc n^ -> TotalNatNc(Succ n^))

(display-idpc "ExR")

;; ExR	with content of type identity
;; InitExR: allnc alpha^((Pvar alpha)alpha^ -> exr alpha^0 (Pvar alpha)alpha^0)

(display-idpc "ExNc")

;; ExNc	non-computational
;;   InitExNc: allnc alpha^((Pvar alpha)^ alpha^ ->
;; 		         exnc alpha^0 (Pvar alpha)^ alpha^0)

(pp "ExRTotalIntro")
;; exr alpha^(TotalNc alpha^ andr (Pvar alpha)alpha^) -> 
;; exr alpha (Pvar alpha)alpha

(pp "ExNcTotalIntro")
;; exnc alpha^(Total alpha^ andnc (Pvar alpha)alpha^) -> 
;; exnc alpha (Pvar alpha)alpha