From: Anders Mörtberg Date: Thu, 20 Oct 2016 20:56:59 +0000 (-0400) Subject: comments X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e0b38ce0c42c2fac26ff0bde1ad851441610717a;p=cubicaltt.git comments --- diff --git a/examples/binnat.ctt b/examples/binnat.ctt index e9dca3a..f156ef0 100644 --- a/examples/binnat.ctt +++ b/examples/binnat.ctt @@ -1,3 +1,15 @@ +-- This file defines binary natural numbers are prove that they are +-- isomorphic to unary natural numbers and by univalence we get a path +-- in the universe between these two types. +-- +-- We then define a "doubling structure" with an operation for +-- computing 2*x and prove that the doubling structure for binary +-- numbers is isomorphic to the one for unary. This is then used to +-- transport a proof that 2^20 * 1024 = 2^5 * 2^15 * 1024 from binary +-- to unary numbers. This computation is instant for binary numbers +-- but impossible for unary, hence this illustrates how univalence can +-- be used to do program and data refinements. +-- module binnat where import nat @@ -128,6 +140,7 @@ doublesN : nat -> nat -> nat = split zero -> \(m:nat) -> m suc n -> \(m:nat) -> doublesN n (doubleN m) +-- 1024 = 2^8 * 2^2 = 2^10 n1024 : nat = doublesN (add four four) four doubleBinN : binN -> binN = split @@ -162,8 +175,6 @@ iter (A : U) : nat -> (A -> A) -> A -> A = split zero -> \(f:A->A) (z:A) -> z suc n -> \(f:A->A) (z:A) -> f (iter A n f z) -ten : nat = add five five - -- Compute: 2^n * x doubles (D : Double) (n : nat) (x : carrier D) : carrier D = iter (carrier D) n (double D) x @@ -175,8 +186,7 @@ propDouble (D : Double) : U -- The property we want to prove that takes long to typecheck: -- 2^10 * 1024 = 2^5 * (2^5 * 1024) --- propN : propDouble DoubleN --- propN = refl N (doublesN ten n1024) +-- propN : propDouble DoubleN = refl nat (doublesN n20 n1024) -- With binary numbers it is instant propBin : propDouble DoubleBinN = <_> doublesBinN n20 (elt DoubleBinN) @@ -215,4 +225,4 @@ propDoubleImpl : propDouble DoubleBinN -> propDouble DoubleN = goal : propDouble DoubleN = propDoubleImpl propBin -transparent_all \ No newline at end of file +transparent_all diff --git a/examples/bool.ctt b/examples/bool.ctt index 485c0b5..396982a 100644 --- a/examples/bool.ctt +++ b/examples/bool.ctt @@ -1,3 +1,4 @@ +-- Booleans module bool where import hedberg