;; ueb04.scm

;; (load "~/git/minlog/init.scm")

;; adding the algebras
(add-algs "nat" '("Zero" "nat") '("Succ" "nat=>nat"))
(add-algs "BBin" '("BinNil" "BBin") '("BinBranch" "BBin=>BBin=>BBin"))

;; this will be needed
(define (make-numeric-term-wrt-nat n)
  (if (= n 0)
      (pt "Zero")
      (make-term-in-app-form
       (pt "Succ")
       (make-numeric-term-wrt-nat (- n 1)))))

;; add some default var-names
(add-var-name "n" "m" (py "nat"))
(add-var-name "t" "s" (py "BBin"))

;; display some terms
(pp (pt "Succ(Succ Zero)"))
(pp (pt "BinBranch BinNil (BinBranch BinNil BinNil)"))

;; can display algbras
(display-alg "BBin")
(display-alg "nat")

;; defined `qconstants are added by '(add-program-constanst
;; "contant-name" type), e.g.

(add-program-constant "NatPlus" (py "nat=>nat=>nat"))

;; computation rules are added by
;; (add-computation-rules "lhs1" "rhs1" "lhs2" "rhs2" ...), e.g.

(add-computation-rules "NatPlus n Zero" "n"
		       "NatPlus n (Succ m)" "Succ(NatPlus n m)")

;; can display the computation rules by
(display-pconst "NatPlus")

;; they are available as theorems, to search for theorems we use
;; (search-about ...).
(search-about 'all "NatPlus" "Comp")

;; eqd is (inductively defined) equality. Given a theorem of the form
;; 't0 eqd t1' and a goal of the form 'A(t0)' [or A(t1)] we can use
;; the (simp thm-name-or-formula) [or (simp "<-" thm-name-or-formula)]
;; to get the new goal 'A(t1)' ['A(t0)']. example see below

;; eqd is introduced by refl, i.e.
(set-goal "all t t eqd t")
(assume "t")
(intro 0)

;; properties of 'nat' and 'BBin' are proven using induction via the
;; (ind) command

;; NatZeroPlus
(set-goal "all n (NatPlus Zero n eqd n)")
;; eqd is equality.
(ind)
;; (pp "NatPlus0CompRule")
(simp "NatPlus0CompRule")
;; alternatively we could have used
;; (simp (pf "NatPlus Zero Zero eqd Zero"))
(intro 0)
(assume "n" "IH")
;; (pp "NatPlus1CompRule")
;; (simp "NatPlus1CompRule")
(ng #t)
;; (ng #t) automatically tries to normalize all terms in the goal as
;; much as possible [note that it will not always do what you want]
(simp "IH")
(intro 0)
(cdp)
;; can save theorem for later use
(save "NatZeroPlus")

;; can display types of rec-operators
(pp (term-to-type (pt "(Rec nat=>alpha)")))
(pp (term-to-type (pt "(Rec BBin=>alpha)")))

;; and corec-op
(pp (term-to-type (pt "(CoRec alpha=>nat)")))
(pp (term-to-type (pt "(CoRec alpha=>BBin)")))

;; exercise 20
;; a) LeafCounter
(add-program-constant "LeafCounterOne" (py "BBin=>nat"))
(add-program-constant "LeafCounterTwo" (py "BBin=>nat"))

(add-computation-rules
 "LeafCounterOne BinNil" ...
 "LeafCounterOne (BinBranch t s)" ...)

;; for the rec-op-def it is probably useful to define the
;; "step-function" separately
(add-program-constant "LeafCounterStep" (py "(BBin=>nat=>BBin=>nat=>nat)"))
(add-computation-rules ...)

(add-computation-rules
 "LeafCounterTwo t" "(Rec BBin=>nat)t Zero LeafCounterStep")

;;display all the theorems about the new consts
(search-about 'all "LeafCounter")

(set-goal "all t(LeafCounterOne t eqd LeafCounterTwo t)")
(ind)
;; ...

;; b) NatInf (we only define the corec-operator version)
(add-program-constant "NatInf" (py "nat"))

;; again, its useful to define the costep separately
(add-program-constant "NatInfCoStep" (py ...))

;; some notes on sums
(display-alg "uysum")
(display-alg "ysum")
;; to properly parse term, additional type info must be supplied
(pp (pt "(DummyL BBin)"))
;; (pp (pt "DummyL")) can't infer the type
;; furthermore
(pp (pt "(InR nat BBin) n"))
(pp (pt "(InL BBin nat) t"))

(add-computation-rules "NatInfCoStep unit" ...)

(add-computation-rules "NatInf" ...)

;; to unfold the corec-opeartor we use
(pp (aconst-to-formula (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))))
;; we use it with simp, e.g.
(set-goal
 "Succ Zero eqd (CoRec unit=>nat)Dummy ([unit] Inr ((InL nat unit) Zero))")
(simp (make-proof-in-aconst-form
       (alg-or-arrow-types-to-corec-aconst (py "unit=>nat"))))
(ng #t)
(intro 0)

;;
(set-goal "NatInf eqd Succ NatInf")
;; ...

;; exercise end

;; some more things provable by ind (if you want)
(set-goal "all n (NatPlus (Succ n) m eqd Succ (NatPlus n m))")
(set-goal "all n,m (NatPlus n m) eqd (NatPlus m n)")

;; and more
(add-program-constant "max" (py "nat=>nat=>nat"))
(add-computation-rules "max Zero n" "n"
		       "max n Zero" "n"
		       "max (Succ n) (Succ m)" "max n m")

(set-goal "all n,m max n m eqd max m n")

(add-program-constant "TreeHt" (py "BBin=>nat"))
(add-computation-rules "TreeHt BinNil" "Zero"
		       "TreeHt (BinBranch t s)" "max (TreeHt t) (TreeHt s)")

(set-goal "all t (TreeHt (BinBranch t BinNil) eqd Succ(TreeHt t))")
(set-goal "all t,s (TreeHt (BinBranch t s) eqd TreeHt (BinBranch s t))")