---- Z
(Nat 0)
n.
(Nat n)
------- S
(Nat (S n))
---- even-0
(Even 0)
n.
(Even n)
-------- odd
(Odd (S n))
n.
(Odd n)
------- even
(Even (S n))
---- Unit
(Data U)
a. b.
(Data a) (Data b)
---- Pair
(Data (A a b))
x.
-------- Znatt
(natt x 0)
n.x.
(natt x n)
-------- sucnatt
(natt x (S n))
---- M-Empty
(M "")
s.
(M "$s")
-------- M-Surround
(M "( $s )")
s1.s2.
(M "$s1")
(M "$s2")
--------- M-Juxtapose
(M "$s1 $s2")
s.
(L "$s")
-------- N-Surr
(N "( $s )")
---- L-Empty
(L "")
s1.s2.
(N "$s1")
(L "$s2")
--------- L-Juxtapose
(L "$s1 $s2")
s. (N "$s")
--------N-L
(L "$s")
s. sn |- ?
x.y.
(/\ x y)
-------- AE1
x
x.y.
(/\ x y)
-------- AE2
y
x.y.
x
y
---- AI
(/\ x y)
---- Z
(Nat 0)
n.
(Nat n)
------- S
(Nat (S n))
P.n.
(Nat n)
(P 0)
[k. (P k) |- (P (S k))]
----------------------- ind
(P n)
---- e-z
(Even 0)
n.
(Even n)
-------- e-SS
(Even (S (S n)))
P.n.
(Even n)
(P 0)
[k. (P k) |- (P (S (S k)))]
--------------------------- E-ind
(P n)
a.
---- refl
(= a a)
a. b. f.
(= a b) (f a)
-------- eq-ap
(f b)
a.
-------- eqab
(= (A a) (B a))
Gentzen
x.y.
(/\ x y)
--------
(/\ y x)
x.y. asm |- by (AI ((x. x. \1) y x) ((x. x. x) y x)) {
|- ?
|- ?}
a.
(Even a)
-------
(Nat a)
a. asm |- ?
a.
(Nat a)
-------
(Nat (S (S a)))
a. asm |- ?
a. b. f.
(= a b)
-------
(= (f a) (f b))
a. b. f. asm |- ?
a. b. c.
(= a b)
(= b c)
------- eq-trans
(= a c)
a. b. c. ab bc |- ?
------- A0B0
(= (A 0) (B 0))
|- ?
x. y.
-------------------- neq-constructors
(not (= (@Z x) (@S y)))
x. y. |- ?
x. y.
(= (@S x) (@S y))
-------------- S-inj
(= x y)
x. y. eq |- ?
x.
[P. (P (fst x))]
----------------
(r (fst (fst x)))
x. asm |- by (asm ((x. x. r (fst x)) x)) {}
String
Basic
---- M-Empty
("" M)
s.
("$s" M)
------- M-Surround
("($s)" M)
s1. s2.
("$s1" M) ("$s2" M)
------- M-Juxtapose
("$s1 $s2" M)
---- paren
("( ) ( ( ) )" M)
|- by (M-Juxtapose "( )" "( ( ) )") {
|- by (M-Surround "") {
|- by (M-Empty) {}}
|- by (M-Surround "( )") {
|- by (M-Surround "") {
|- by (M-Empty) {}}}}
s. ("$s" L)
-----N-Surr
("($s)" N)
-----L-Empty
("" L)
s1. s2.
("$s1" N) ("$s2" L)
-----L-Juxtapose
("$s1 $s2" L)
s. ("$s" N)
--------N-L
("$s" L)
s. sn |- by (L-Juxtapose s "") {
|- by (sn) {}
|- by (L-Empty) {}
}
s1.s2. ("$s1" L) ("$s2" L)
--------------------- lexp-juxt
("$s1 $s2" L)
s1. s2. s1L s2L |- ?
s. ("$s" M)
----------- mexp-lexp
("$s" L)
s. sM |- ?
s. ("$s" L)
----------- mexp-lexp
("$s" M)
s. sL |- elim (L_mutualInduct sL "" "$s" "" M M) {
|- by (M-Empty) {}
s1.s2. 0 1 2 3 |- elim (M-Juxtapose 2 "$s1" "$s2") {
|- by (3) {}}
s. 0 1 |- elim (M-Surround 1 "$s") {}}
s. n.
--------- string-prod
(Parse "$s * $n" (Prod s nat(n)))
s1.
---------- eval-prod-Z
(Eval (Prod s1 nat(0)) "")
s1. s1n. n.
(Eval (Prod s1 nat(n)) s1n)
----------- eval-prod-S
(Eval (Prod s1 nat(n + 1)) "$s1$s1n")
s. ast. res.
(Parse s ast)
(Eval ast res)
--------------- program-eval
(PEval s res)
------------- foo-3
(PEval "foo * 3" "foo foo foo")
|- ?
n. (Type n Nat)
------------ Var
(Var n)
------------ Sig-Empty
(Sig Empty)
f. n. sig. (Sig sig)
------------ Sig-Cons
(Sig (Cons (f nat(n)) sig))
f. n. sig.
(Sig sig)
------------ InSig-Head
(InSig (f nat(n)) (Cons (f nat(n)) sig))
f. n. g. sig.
(Sig sig)
(InSig (f nat(n)) sig)
------------ InSig-Next
(InSig (f nat(n)) (Cons g (f nat(n))))
v. sig. (Sig sig) (Var v)
------------ Term-Var
(Term sig (Var v))
a. sig. (Sig sig) (InSig (a nat(0)) sig)
------------ Term-Const
(Term sig (Const a))
sig.
------------ Term-List-0
(TermList sig nat(0) Empty)
f. n. t. ts. sig. (Term sig t) (TermList nat(n) ts)
------------ Term-List-n
(TermList sig nat(n + 1) (Cons t ts))
f. n. ts. sig. (Sig sig) (InSig (f nat(n)) sig) (TermList sig nat(n) ts)
------------ Term-Func
(Term sig (Func f ts))
------------- penips
(Term (Cons (f nat(2)) (Cons (a nat(0)) Empty)) (Func f (Cons (Const a) (Cons (Var nat(1)) Empty))))
|- ?
a.
-------- Eq
(Eq a a)
s.
(Eq length("$s") nat(1))
---------------------- Singleton
("$s" Singleton)
----------- Palindrome-Empty
("" Palindrome)
c. ("$c" Singleton)
------------ Palindrome-Single
("$c" Palindrome)
c. s. ("$c" Singleton) ("$s" Palindrome)
------------ Palindrome-Add
("$c $s $c" Palindrome)
------------------ dlads
("a b c b a" Palindrome)
|- ?
a.
-------------- eq-refl
(Eq a a)
a. b. (Eq a b)
-------------- eq-sym
(Eq b a)
a. b. c. (Eq a b) (Eq "$b" c)
-------------- eq-trans-weird
(Eq a c)
-------------- eq-a-comp
(Eq "a" Foo)
------------- eq-a-c
(Eq "a" "a")
|- ?