From: coquand Date: Mon, 4 Jan 2016 16:58:17 +0000 (+0100) Subject: added an example with ordinals X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=1bdd2243a433acef164707a97c3a3fe29496a07e;p=cubicaltt.git added an example with ordinals --- diff --git a/examples/ordinal.ctt b/examples/ordinal.ctt new file mode 100644 index 0000000..3e2721a --- /dev/null +++ b/examples/ordinal.ctt @@ -0,0 +1,103 @@ +module ordinal where + +import prelude + +-- from the JSL 89 paper of Stan Wainer + +data nat = zero | succ (n:nat) + +data ord = zero | succ (n:ord) | lim (f : nat -> ord) + +data ord2 = zero | succ (n:ord2) | lim (f : nat -> ord2) | lim2 (f : ord -> ord2) + +inj0 : nat -> ord = split + zero -> zero + succ n -> succ (inj0 n) + +G1 : ord -> nat -> nat = split + zero -> \ (x:nat) -> zero + succ z -> \ (x:nat) -> succ (G1 z x) + lim f -> \ (x:nat) -> G1 (f x) x + +G2 : ord2 -> nat -> ord = split + zero -> \ (x:nat) -> zero + succ z -> \ (x:nat) -> succ (G2 z x) + lim f -> \ (x:nat) -> G2 (f x) x + lim2 f -> \ (x:nat) -> lim (\ (n:nat) -> G2 (f (inj0 n)) x) + +and (A B : U) : U = (_:A) * B + +O2 (n:nat) : ord2 -> U = split + zero -> Unit + succ z -> O2 n z + lim f -> (p:nat) -> O2 n (f p) + lim2 f -> (x:ord) -> and (O2 n (f x)) (Id ord (G2 (f x) n) (G2 (f (inj0 (G1 x n))) n)) + +inj12 : ord -> ord2 = split + zero -> zero + succ z -> succ (inj12 z) + lim f -> lim (\ (n:nat) -> inj12 (f n)) + +H1 : ord -> nat -> nat = split + zero -> \ (x:nat) -> x + succ z -> \ (x:nat) -> H1 z (succ x) + lim f -> \ (x:nat) -> H1 (f x) x + +H2 : ord2 -> ord -> ord = split + zero -> \ (x:ord) -> x + succ z -> \ (x:ord) -> H2 z (succ x) + lim f -> \ (x:ord) -> lim (\ (n:nat) -> H2 (f n) x) + lim2 f -> \ (x:ord) -> H2 (f x) x + +collapsing (n:nat) : + (x:ord2) (y:ord) -> O2 n x -> Id nat (G1 (H2 x y) n) (H1 (G2 x n) (G1 y n)) = split + zero -> \ (y:ord) (h:O2 n zero) -> G1 y n + succ z -> \ (y:ord) (h:O2 n (succ z)) -> collapsing n z (succ y) h + lim f -> \ (y:ord) (h:O2 n (lim f)) -> collapsing n (f n) y (h n) + lim2 f -> \ (y:ord) (h:O2 n (lim2 f)) -> + let + rem : Id ord (G2 (f y) n) (G2 (f (inj0 (G1 y n))) n) = (h y).2 + rem1 : Id nat (G1 (H2 (f y) y) n) (H1 (G2 (f y) n) (G1 y n)) = collapsing n (f y) y (h y).1 + in comp (Id nat (G1 (H2 (f y) y) n) (H1 (rem@i) (G1 y n))) rem1 [] + +-- an application + +omega : ord = lim inj0 + +omega1 : ord2 = lim2 inj12 + +lemOmega1 (n:nat) : O2 n omega1 = \ (x:ord) -> (rem x,rem1 x) + where rem : (x:ord) -> O2 n (inj12 x) = split + zero -> tt + succ z -> rem z + lim f -> \ (p:nat) -> rem (f p) + rem1 : (x:ord) -> Id ord (G2 (inj12 x) n) (G2 (inj12 (inj0 (G1 x n))) n) = split + zero -> zero + succ z -> succ ((rem1 z)@i) + lim f -> rem1 (f n) + +corr1 (n:nat) : Id nat (G1 (H2 omega1 omega) n) (H1 (G2 omega1 n) (G1 omega n)) = + collapsing n omega1 omega (lemOmega1 n) + +lem : (n p:nat) -> Id nat (G1 (inj0 n) p) n = split + zero -> \ (p:nat) -> zero + succ q -> \ (p:nat) -> succ (lem q p@i) + +lem1 (n:nat) : Id nat (G1 omega n) n = lem n n + +lem2 : (n p:nat) -> Id ord (G2 (inj12 (inj0 n)) p) (inj0 n) = split + zero -> \ (p:nat) -> inj0 zero + succ q -> \ (p:nat) -> succ (lem2 q p@i) + +test (n:nat) : ord = G2 omega1 n + +lem3 (n:nat) : Id ord (G2 (inj12 (inj0 n)) n) (inj0 n) = lem2 n n + +lem4 (n:nat) : Id nat (H1 (G2 omega1 n) n) (H1 omega n) = + H1 (lem3 n@i) n + +-- the G1 and H1 hierarchy coincides: G1 (H2 omega1 omega) and H1 omega are the same function + +corr2 : Id (nat -> nat) (G1 (H2 omega1 omega)) (H1 omega) = + \ (n:nat) -> comp (<_>nat) (H1 (G2 omega1 n) ((lem1 n)@i)) [(i=0) -> corr1 n@-j,(i=1) -> lem4 n] +