;;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 constants 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 24
;; 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))")