add some files from chris course
This commit is contained in:
parent
4380c7c126
commit
e4d7f2e22d
|
|
@ -0,0 +1,86 @@
|
|||
nat: type.
|
||||
z: nat.
|
||||
s: nat -> nat.
|
||||
|
||||
%{
|
||||
>>> bogus: nat.
|
||||
|
||||
}%
|
||||
|
||||
even: nat -> type.
|
||||
odd: nat -> type.
|
||||
|
||||
even/z: even z.
|
||||
even/s: even (s N) <- odd N.
|
||||
|
||||
odd/s: odd (s N) <- even N.
|
||||
|
||||
%solve - : even (s (s (s (s z)))).
|
||||
%{
|
||||
>>> %solve - : even bogus.
|
||||
hw.elf:19.2-19.23 Error:
|
||||
No solution to %solve found
|
||||
|
||||
>>> %solve - : even (s (s (s z))).
|
||||
No solution to %solve found
|
||||
|
||||
|
||||
>>> %solve even (s (s (s (s z)))).
|
||||
OK
|
||||
- : even (s (s (s (s z)))) = even/s (odd/s (even/s (odd/s even/z))).
|
||||
}%
|
||||
|
||||
% Standalone even
|
||||
even': nat -> type.
|
||||
even'/z: even' z.
|
||||
even'/s: even' (s (s N)) <- even' N.
|
||||
|
||||
|
||||
% =========================================
|
||||
% even' N -> even N
|
||||
% =========================================
|
||||
|
||||
even'-impl-even: even' N -> even N -> type.
|
||||
%mode even'-impl-even +X1 -X2.
|
||||
|
||||
even'-impl-even/z : even'-impl-even
|
||||
even'/z
|
||||
even/z.
|
||||
|
||||
even'-impl-even/s : even'-impl-even
|
||||
(even'/s (D1': even' N))
|
||||
(even/s (odd/s D1))
|
||||
<- even'-impl-even D1' D1.
|
||||
|
||||
% =========================================
|
||||
% even N -> even' N
|
||||
% =========================================
|
||||
|
||||
even-impl-even': even N -> even' N -> type.
|
||||
%mode even-impl-even' +X1 -X2.
|
||||
|
||||
even-impl-even'/z : even-impl-even'
|
||||
even/z even'/z.
|
||||
|
||||
even-impl-even'/s: even-impl-even'
|
||||
(even/s (D1: odd N))
|
||||
(even'/s D2).
|
||||
|
||||
|
||||
% even-impl-even'/s: even-impl-even'
|
||||
% (even/s (D1: odd N))
|
||||
% D2
|
||||
% % (even'/s D2)
|
||||
% <- even-impl-even' (even/s D1) D3.
|
||||
|
||||
|
||||
% =========================================
|
||||
% Every nat is either even or odd
|
||||
% =========================================
|
||||
|
||||
nat-eod: nat -> type.
|
||||
nat-eod/e: nat-eod N <- even N.
|
||||
nat-eod/o: nat-eod N <- odd N.
|
||||
|
||||
step: nat-eod N -> nat-eod (s N).
|
||||
step/z: nat-eod z -> nat-eod (s z).
|
||||
|
|
@ -0,0 +1,45 @@
|
|||
nat: type.
|
||||
z: nat.
|
||||
s: nat -> nat.
|
||||
|
||||
even2: nat -> type.
|
||||
odd: nat -> type.
|
||||
|
||||
even2/z: even2 z.
|
||||
even2/s: even2 (s N) <- odd N.
|
||||
|
||||
odd/s: odd (s N) <- even2 N.
|
||||
|
||||
|
||||
% Standalone even
|
||||
even: nat -> type.
|
||||
even/z: even z.
|
||||
even/s: even (s (s N)) <- even N.
|
||||
|
||||
% =========================================
|
||||
% even2 N -> even N
|
||||
% =========================================
|
||||
|
||||
even2-impl-even: even2 N -> even N -> type.
|
||||
%mode even2-impl-even +X1 -X2.
|
||||
|
||||
even2-impl-even/z : even2-impl-even
|
||||
even2/z even/z.
|
||||
|
||||
even2-impl-even/s : even2-impl-even
|
||||
(even2/s (odd/s (D1: even2 N)))
|
||||
(even/s D2)
|
||||
<- even2-impl-even D1 D2.
|
||||
|
||||
% =========================================
|
||||
% Every nat is either even or odd
|
||||
% =========================================
|
||||
|
||||
nat-eod: nat -> type.
|
||||
nat-eod/e: nat-eod N <- even N.
|
||||
nat-eod/o: nat-eod N <- odd N.
|
||||
|
||||
step: nat-eod N -> nat-eod (s N).
|
||||
step/z: nat-eod z -> nat-eod (s z).
|
||||
|
||||
% ∃X, X + 1 = 2
|
||||
|
|
@ -0,0 +1,82 @@
|
|||
% 30-Jan-2024
|
||||
|
||||
nat: type.
|
||||
z: nat.
|
||||
s: nat -> nat.
|
||||
|
||||
% Make twelf output use N as name for vals of nat in output
|
||||
%name nat N.
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
even: nat -> type.
|
||||
even/z: even z.
|
||||
even/s: even (s (s N)) <- even N.
|
||||
% even/s: even N -> even (s (s N)).
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
even2: nat -> type.
|
||||
odd: nat -> type.
|
||||
|
||||
odd/s: odd (s N) <- even2 N.
|
||||
|
||||
even2/z: even2 z.
|
||||
even2/s: even2 (s N) <- odd N.
|
||||
|
||||
%solve myEvenDeriv: even (s (s z)).
|
||||
% myEvenDeriv : even (s (s z)) = even/s even/z.
|
||||
|
||||
% %solve myEvenDeriv: even (s (s (s z))).
|
||||
% No solution to %solve found
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
even-implies-even2: even N -> even2 N -> type.
|
||||
%mode even-implies-even2 +X1 -X2.
|
||||
|
||||
even-implies-even2/z
|
||||
: even-implies-even2 even/z even2/z.
|
||||
|
||||
even-implies-even2/s
|
||||
: even-implies-even2
|
||||
(even/s (Deven: even N))
|
||||
(even2/s (odd/s Deven2))
|
||||
<- even-implies-even2 Deven (Deven2: even2 N).
|
||||
|
||||
%worlds () (even-implies-even2 _ _).
|
||||
%total D (even-implies-even2 D _).
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
even2-implies-even: even2 N -> even N -> type.
|
||||
%mode even2-implies-even +X1 -X2.
|
||||
|
||||
even2-implies-even/z
|
||||
: even2-implies-even even2/z even/z.
|
||||
|
||||
even2-implies-even/s
|
||||
: even2-implies-even
|
||||
(even2/s (Deven: even N))
|
||||
(even2/s (Deven: even2 N))
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
|
||||
% Yeah, unicode seems to be fine.
|
||||
% sml doesn't support unicode I guess. Apparently, twelf source treats
|
||||
% all non-ascii as lower-case letter
|
||||
ℕ: type.
|
||||
|
||||
|
||||
%%%%%%%%%%%%%%%%%%%%%%
|
||||
|
||||
plus: nat -> nat -> nat -> type.
|
||||
%mode plus +N1 +N2 -N3.
|
||||
plus/z: plus z N N.
|
||||
plus/s: plus (s N1) N2 (s N3) <- plus N1 N2 N3.
|
||||
|
||||
% Error
|
||||
% plus-comm: plus N1 (plus N2 N3) N4 -> plus (plus N1 N2) N3 N4 -> type.
|
||||
|
|
@ -0,0 +1 @@
|
|||
nat.elf
|
||||
|
|
@ -0,0 +1,52 @@
|
|||
% ---
|
||||
% nat
|
||||
% ===
|
||||
|
||||
nat: type.
|
||||
z: nat.
|
||||
s: nat -> nat.
|
||||
%name nat N.
|
||||
%freeze nat.
|
||||
|
||||
% -------------------
|
||||
% Maximum of two nats
|
||||
% ===================
|
||||
|
||||
max: nat -> nat -> nat -> type.
|
||||
%mode max +N1 +N2 -N3.
|
||||
max/z1: max z N N.
|
||||
max/z2: max N z N.
|
||||
max/s: max N M P -> max (s N) (s M) (s P).
|
||||
%worlds () (max _ _ _).
|
||||
%total N (max N _ _).
|
||||
|
||||
% --------------
|
||||
% Tree structure
|
||||
% ==============
|
||||
|
||||
tree: type.
|
||||
leaf: tree.
|
||||
node: tree -> tree -> tree.
|
||||
%freeze tree.
|
||||
%name tree T.
|
||||
|
||||
height: tree -> nat -> type.
|
||||
%mode height +T -N.
|
||||
|
||||
height/leaf: height leaf z.
|
||||
height/node: height (node L R) (s H)
|
||||
<- height L HL
|
||||
<- height L HR
|
||||
<- max HL HR H.
|
||||
|
||||
%worlds () (height _ _).
|
||||
%total T (height T _).
|
||||
|
||||
% --------
|
||||
% AVL tree
|
||||
% ========
|
||||
|
||||
avl: type.
|
||||
avlLeaf: avl.
|
||||
avlNode: nat -> tree -> tree -> avl.
|
||||
% nat is the balance factor
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
w2-live.elf
|
||||
hw.elf
|
||||
|
|
@ -0,0 +1,88 @@
|
|||
nat: type.
|
||||
z: nat.
|
||||
s: nat -> nat.
|
||||
%name nat N.
|
||||
%freeze nat.
|
||||
|
||||
max: nat -> nat -> nat -> type.
|
||||
%mode max +N1 +N2 -N3.
|
||||
max/z1: max z N N.
|
||||
max/z2: max N z N.
|
||||
max/s: max N M P -> max (s N) (s M) (s P).
|
||||
%worlds () (max _ _ _).
|
||||
%total N (max N _ _).
|
||||
%
|
||||
% As long as one of N1 and N2 get smaller.
|
||||
% A twelf feature that's not well-documented
|
||||
% %total [N1 N2] (max N1 N2 _).
|
||||
|
||||
|
||||
% A skeleton tree. ie, with no data.
|
||||
tree: type.
|
||||
leaf: tree.
|
||||
node: tree -> tree -> tree.
|
||||
%freeze tree.
|
||||
%name tree T.
|
||||
|
||||
height: tree -> nat -> type.
|
||||
%mode height +T -N.
|
||||
|
||||
height/leaf: height leaf z.
|
||||
height/node
|
||||
: height (node L R) (s H)
|
||||
<- height L HL
|
||||
<- height L HR
|
||||
<- max HL HR H.
|
||||
|
||||
%worlds () (height _ _).
|
||||
%total T (height T _).
|
||||
|
||||
|
||||
balanced: tree -> type.
|
||||
balanced/leaf: balanced leaf.
|
||||
balanced/node
|
||||
: balanced (node L R)
|
||||
<- height L H
|
||||
<- height R H.
|
||||
% Wow.. that's cool.
|
||||
|
||||
|
||||
% >>> %solve - : balanced (node leaf leaf).
|
||||
% OK
|
||||
% - : balanced (node leaf leaf) = balanced/node height/leaf height/leaf.
|
||||
|
||||
% >>> %solve - : balanced (node leaf (node leaf leaf)).
|
||||
% No solution to %solve found
|
||||
|
||||
tree1: tree = node leaf leaf.
|
||||
|
||||
% >>> %solve - : balanced tree1.
|
||||
% OK
|
||||
% - : balanced tree1 = balanced/node height/leaf height/leaf.
|
||||
|
||||
% >>> %solve - : balanced (node tree1 tree1).
|
||||
% OK
|
||||
% - : balanced (node tree1 tree1)
|
||||
% = balanced/node (height/node max/z1 height/leaf height/leaf)
|
||||
% (height/node max/z1 height/leaf height/leaf).
|
||||
|
||||
bbt: nat -> type.
|
||||
bLeaf: bbt z.
|
||||
bNode: bbt N -> bbt N -> bbt (s N).
|
||||
|
||||
%solve egtree1: bbt (s (s (s z))).
|
||||
|
||||
eqTree: bbt N -> bbt N -> type.
|
||||
%mode eqTree +T1 +T2.
|
||||
eqTree/bLeaf: eqTree bLeaf bLeaf.
|
||||
eqTree/bNode
|
||||
: eqTree (bNode L1 R1) (bNode L2 R2)
|
||||
<- eqTree L1 L2
|
||||
<- eqTree R1 R2.
|
||||
%worlds () (eqTree _ _).
|
||||
%total [T1 T2] (eqTree T1 T2).
|
||||
|
||||
|
||||
% % This doesn't work???? Even if it doesn't give error.
|
||||
% eqTree2: bbt N -> bbt N -> type.
|
||||
% eqTree2/i: eqTree2 N N.
|
||||
Loading…
Reference in New Issue