mirror of
https://github.com/Kindelia/Kind2.git
synced 2024-08-15 18:20:26 +03:00
Move benchmarks out, update README
This commit is contained in:
Victor Maia
parent
42d9b12f3f
commit
1cca987277
@ -1,6 +1,6 @@
|
||||
[package]
|
||||
name = "kind2"
|
||||
version = "0.2.69"
|
||||
version = "0.2.70"
|
||||
edition = "2021"
|
||||
description = "A pure functional functional language that uses the HVM."
|
||||
repository = "https://github.com/Kindelia/Kind2"
|
||||
|
||||
84
README.md
84
README.md
@ -1,62 +1,64 @@
|
||||
Kind2
|
||||
=====
|
||||
|
||||
Kind2 is a pure functional, lazy, non-garbage-collected, general-purpose,
|
||||
dependently typed programming language focusing on performance and usability. It
|
||||
features a blazingly fast type-checker based on **optimal
|
||||
[normalization-by-evaluation](https://en.wikipedia.org/wiki/Normalisation_by_evaluation)**. It can also
|
||||
compile programs to [HVM](https://github.com/kindelia/hvm) and [Kindelia](https://github.com/kindelia/kindelia),
|
||||
and can be used to prove and verify mathematical theorems.
|
||||
**Kind2** is a **functional programming language** and **proof assistant**.
|
||||
|
||||
It is a complete rewrite of [Kind1](https://github.com/kindelia/kind-legacy), based on
|
||||
[HVM](https://github.com/kindelia/hvm), a **lazy**, **non-garbage-collected** and **massively parallel** virtual
|
||||
machine. In [our benchmarks](https://github.com/kindelia/functional-benchmarks), its type-checker outperforms every
|
||||
alternative proof assistant by a far margin, and its programs can offer exponential speedups over Haskell's GHC. Kind2
|
||||
unleashes the [inherent parallelism of the Lambda
|
||||
Calculus](https://github.com/VictorTaelin/Symmetric-Interaction-Calculus) to become the ultimate programming language of
|
||||
the next century.
|
||||
|
||||
**Welcome to the inevitable parallel, functional future of computers!**
|
||||
|
||||
Examples
|
||||
--------
|
||||
|
||||
Pure functions can be defined using an equational notation that resembles [Haskell](https://www.haskell.org/):
|
||||
Pure functions are defined via equations, as in [Haskell](https://www.haskell.org/):
|
||||
|
||||
```idris
|
||||
List.map <a: Type> <b: Type> (x: (List a)) (f: (x: a) b) : (List b)
|
||||
List.map a b (Nil t) f = (Nil b)
|
||||
List.map a b (Cons t x xs) f = (Cons b (f x) (List.map xs f))
|
||||
```javascript
|
||||
// Applies a function to every element of a list
|
||||
map <a> <b> (list: List a) (f: a -> b) : List b
|
||||
map a b Nil f = Nil
|
||||
map a b (Cons head tail) f = Cons (f x) (map tail f)
|
||||
```
|
||||
|
||||
Mathematical theorems can be proved via inductive reasoning, as in [Idris](https://www.idris-lang.org/) and [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php):
|
||||
Side-effective programs are written via monadic monads, resembling [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
|
||||
|
||||
```idris
|
||||
Nat.commutes (a: Nat) (b: Nat) : (Nat.add a b) == (Nat.add b a)
|
||||
Nat.commutes Zero b = (Nat.comm.a b)
|
||||
Nat.commutes (Succ a) b =
|
||||
let e0 = (Equal.apply @x(Succ x) (Nat.commutes a b))
|
||||
let e1 = (Equal.mirror (Nat.commutes.b b a))
|
||||
(Equal.chain e0 e1)
|
||||
```
|
||||
|
||||
Normal programs can be written in a monadic syntax that is inspired by [Rust](https://www.rust-lang.org/) and [TypeScript](https://www.typescriptlang.org/):
|
||||
|
||||
```idris
|
||||
Main : (IO (Result () String)) {
|
||||
ask limit = (IO.prompt "Enter limit:")
|
||||
```javascript
|
||||
// Prints the double of every numbet up to a limit
|
||||
Main : IO (Result () String) {
|
||||
ask limit = IO.prompt "Enter limit:"
|
||||
for x in (List.range limit) {
|
||||
(IO.print "{} * 2 = {}" x (Nat.double x))
|
||||
IO.print "{} * 2 = {}" x (Nat.double x)
|
||||
}
|
||||
return (Ok ())
|
||||
return Ok ()
|
||||
}
|
||||
```
|
||||
|
||||
Theorems can be proved inductivelly, as in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php) and [Idris](https://www.idris-lang.org/):
|
||||
|
||||
```javascript
|
||||
// Black Friday Theorem. Proof that, for every Nat n: n * 2 / 2 == n.
|
||||
black_friday_theorem (n: Nat) : Equal Nat (Nat.half (Nat.double n)) n
|
||||
black_friday_theorem Nat.zero = Equal.refl
|
||||
black_friday_theorem (Nat.succ n) = Equal.apply (x => Nat.succ x) (black_friday_theorem n)
|
||||
```
|
||||
|
||||
For more examples, check the [Wikind](https://github.com/kindelia/wikind).
|
||||
|
||||
Installation
|
||||
------------
|
||||
Usage
|
||||
-----
|
||||
|
||||
Install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
|
||||
First, install [Rust](https://www.rust-lang.org/tools/install) first, then enter:
|
||||
|
||||
```
|
||||
cargo install kind2
|
||||
```
|
||||
|
||||
Enter `kind2` on the terminal to make sure it worked.
|
||||
|
||||
Usage
|
||||
-----
|
||||
Then, use any of the commands below:
|
||||
|
||||
Command | Usage | Note
|
||||
---------- | ------------------------- | --------------------------------------------------------------
|
||||
@ -64,9 +66,13 @@ Check | `kind2 check file.kind2` | Checks all definitions.
|
||||
Eval | `kind2 eval file.kind2` | Runs using the type-checker's evaluator.
|
||||
Run | `kind2 run file.kind2` | Runs using HVM's evaluator, on Rust-mode.
|
||||
To-HVM | `kind2 to-hvm file.kind2` | Generates a [.hvm](https://github.com/kindelia/hvm) file. Can then be compiled to C.
|
||||
To-KDL | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to Kindelia.
|
||||
To-KDL | `kind2 to-kdl file.kind2` | Generates a [.kdl](https://github.com/kindelia/kindelia) file. Can then be deployed to [Kindelia](https://github.com/kindelia/kindelia).
|
||||
|
||||
Benchmarks
|
||||
----------
|
||||
Executables can be generated via HVM:
|
||||
|
||||
In preliminary [benchmarks](/bench), Kind2's type-checker has outperformed Agda, Idris by 90x to 900x, which is an expressive difference. That said, we only tested a few small programs, so there isn't enough data to draw a conclusion yet. We're working on a more extensive benchmark suite.
|
||||
```
|
||||
kind2 to-hvm file.kind2
|
||||
hvm compile file.hvm
|
||||
clang -O2 file.c -o file
|
||||
./file
|
||||
```
|
||||
|
||||
@ -1,239 +0,0 @@
|
||||
CBool : Type
|
||||
CBool = (B : Type) -> B -> B -> B
|
||||
|
||||
toBool : CBool -> Bool
|
||||
toBool = \b => b Bool True False
|
||||
|
||||
ctrue : CBool
|
||||
ctrue = \b, t, f => t
|
||||
|
||||
and : CBool -> CBool -> CBool
|
||||
and = \a, b, bb, t, f => a bb (b bb t f) f
|
||||
|
||||
CNat : Type
|
||||
CNat = (n : Type) -> (n -> n) -> n -> n
|
||||
|
||||
add : CNat -> CNat -> CNat
|
||||
add = \a, b, n, s, z => a n s (b n s z)
|
||||
|
||||
cmul : CNat -> CNat -> CNat
|
||||
cmul = \a, b, n, s => a n (b n s)
|
||||
|
||||
suc : CNat -> CNat
|
||||
suc = \a, n, s, z => s (a n s z)
|
||||
|
||||
CEq : {A : Type} -> A -> A -> Type
|
||||
CEq = \x, y => (P : A -> Type) -> P x -> P y
|
||||
|
||||
crefl : {A : Type} -> {x : A} -> CEq {A} x x
|
||||
crefl = \p, px => px
|
||||
|
||||
n2 : CNat
|
||||
n2 = \n, s, z => s (s z)
|
||||
|
||||
n3 : CNat
|
||||
n3 = \n, s, z => s (s (s z))
|
||||
|
||||
n4 : CNat
|
||||
n4 = \n, s, z => s (s (s (s z)))
|
||||
|
||||
n5 : CNat
|
||||
n5 = \n, s, z => s (s (s (s (s z))))
|
||||
|
||||
n10 : CNat
|
||||
n10 = cmul n2 n5
|
||||
|
||||
n10b : CNat
|
||||
n10b = cmul n5 n2
|
||||
|
||||
n15 : CNat
|
||||
n15 = add n10 n5
|
||||
|
||||
n15b : CNat
|
||||
n15b = add n10b n5
|
||||
|
||||
n18 : CNat
|
||||
n18 = add n15 n3
|
||||
|
||||
n18b : CNat
|
||||
n18b = add n15b n3
|
||||
|
||||
n19 : CNat
|
||||
n19 = add n15 n4
|
||||
|
||||
n19b : CNat
|
||||
n19b = add n15b n4
|
||||
|
||||
n20 : CNat
|
||||
n20 = cmul n2 n10
|
||||
|
||||
n20b : CNat
|
||||
n20b = cmul n2 n10b
|
||||
|
||||
n21 : CNat
|
||||
n21 = suc n20
|
||||
|
||||
n21b : CNat
|
||||
n21b = suc n20b
|
||||
|
||||
n22 : CNat
|
||||
n22 = suc n21
|
||||
|
||||
n22b : CNat
|
||||
n22b = suc n21b
|
||||
|
||||
n23 : CNat
|
||||
n23 = suc n22
|
||||
|
||||
n23b : CNat
|
||||
n23b = suc n22b
|
||||
|
||||
n100 : CNat
|
||||
n100 = cmul n10 n10
|
||||
|
||||
n100b : CNat
|
||||
n100b = cmul n10b n10b
|
||||
|
||||
n10k : CNat
|
||||
n10k = cmul n100 n100
|
||||
|
||||
n10kb : CNat
|
||||
n10kb = cmul n100b n100b
|
||||
|
||||
n100k : CNat
|
||||
n100k = cmul n10k n10
|
||||
|
||||
n100kb : CNat
|
||||
n100kb = cmul n10kb n10b
|
||||
|
||||
n1M : CNat
|
||||
n1M = cmul n10k n100
|
||||
|
||||
n1Mb : CNat
|
||||
n1Mb = cmul n10kb n100b
|
||||
|
||||
n5M : CNat
|
||||
n5M = cmul n1M n5
|
||||
|
||||
n5Mb : CNat
|
||||
n5Mb = cmul n1Mb n5
|
||||
|
||||
n10M : CNat
|
||||
n10M = cmul n5M n2
|
||||
|
||||
n10Mb : CNat
|
||||
n10Mb = cmul n5Mb n2
|
||||
|
||||
Tree : Type
|
||||
Tree = (T : Type) -> (T -> T -> T) -> T -> T
|
||||
|
||||
leaf : Tree
|
||||
leaf = \t, n, l => l
|
||||
|
||||
node : Tree -> Tree -> Tree
|
||||
node = \t1, t2, t, n, l => n (t1 t n l) (t2 t n l)
|
||||
|
||||
fullTree : CNat -> Tree
|
||||
fullTree = \n => n Tree (\t => node t t) leaf
|
||||
|
||||
-- full tree with given trees at bottom level
|
||||
fullTreeWithLeaf : Tree -> CNat -> Tree
|
||||
fullTreeWithLeaf = \bottom, n => n Tree (\t => node t t) bottom
|
||||
|
||||
forceTree : Tree -> CBool
|
||||
forceTree = \t => t CBool and ctrue
|
||||
|
||||
t15 : Tree
|
||||
t15 = fullTree n15
|
||||
t15b : Tree
|
||||
t15b = fullTree n15b
|
||||
t18 : Tree
|
||||
t18 = fullTree n18
|
||||
t18b : Tree
|
||||
t18b = fullTree n18b
|
||||
t19 : Tree
|
||||
t19 = fullTree n19
|
||||
t19b : Tree
|
||||
t19b = fullTree n19b
|
||||
t20 : Tree
|
||||
t20 = fullTree n20
|
||||
t20b : Tree
|
||||
t20b = fullTree n20b
|
||||
t21 : Tree
|
||||
t21 = fullTree n21
|
||||
t21b : Tree
|
||||
t21b = fullTree n21b
|
||||
t22 : Tree
|
||||
t22 = fullTree n22
|
||||
t22b : Tree
|
||||
t22b = fullTree n22b
|
||||
t23 : Tree
|
||||
t23 = fullTree n23
|
||||
t23b : Tree
|
||||
t23b = fullTree n23b
|
||||
|
||||
-- CNat conversion
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
convn1M : CEq Main.n1M Main.n1Mb
|
||||
convn1M = crefl
|
||||
|
||||
-- convn5M : CEq Main.n5M Main.n5Mb
|
||||
-- convn5M = crefl
|
||||
|
||||
-- convn10M : CEq Main.n10M Main.n10Mb
|
||||
-- convn10M = crefl
|
||||
|
||||
-- Full tree conversion
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- convt15 : CEq Main.t15 Main.t15b
|
||||
-- convt15 = crefl
|
||||
-- convt18 : CEq Main.t18 Main.t18b
|
||||
-- convt18 = crefl
|
||||
-- convt19 : CEq Main.t19 Main.t19b
|
||||
-- convt19 = crefl
|
||||
-- convt20 : CEq Main.t20 Main.t20b
|
||||
-- convt20 = crefl
|
||||
-- convt21 : CEq Main.t21 Main.t21b
|
||||
-- convt21 = crefl
|
||||
-- convt22 : CEq Main.t22 Main.t22b
|
||||
-- convt22 = crefl
|
||||
-- convt23 : CEq Main.t23 Main.t23b
|
||||
-- convt23 = crefl
|
||||
|
||||
-- Full meta-containing tree conversion
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- convmt15 : CEq Main.t15b (fullTreeWithLeaf ? Main.n15 )
|
||||
-- convmt15 = crefl
|
||||
-- convmt18 : CEq Main.t18b (fullTreeWithLeaf ? Main.n18 )
|
||||
-- convmt18 = crefl
|
||||
-- convmt19 : CEq Main.t19b (fullTreeWithLeaf ? Main.n19 )
|
||||
-- convmt19 = crefl
|
||||
-- convmt20 : CEq Main.t20b (fullTreeWithLeaf ? Main.n20 )
|
||||
-- convmt20 = crefl
|
||||
-- convmt21 : CEq Main.t21b (fullTreeWithLeaf ? Main.n21 )
|
||||
-- convmt21 = crefl
|
||||
-- convmt22 : CEq Main.t22b (fullTreeWithLeaf ? Main.n22 )
|
||||
-- convmt22 = crefl
|
||||
-- convmt23 : CEq Main.t23b (fullTreeWithLeaf ? Main.n23 )
|
||||
-- convmt23 = crefl
|
||||
|
||||
-- Full tree forcing
|
||||
--------------------------------------------------------------------------------
|
||||
|
||||
-- forcet15 : CEq (toBool (forceTree Main.t15)) True
|
||||
-- forcet15 = crefl
|
||||
-- forcet18 : CEq (toBool (forceTree Main.t18)) True
|
||||
-- forcet18 = crefl
|
||||
-- forcet19 : CEq (toBool (forceTree Main.t19)) True
|
||||
-- forcet19 = crefl
|
||||
-- forcet20 : CEq (toBool (forceTree Main.t20)) True
|
||||
-- forcet20 = crefl
|
||||
-- forcet21 : CEq (toBool (forceTree Main.t21)) True
|
||||
-- forcet21 = crefl
|
||||
--forcet22 : CEq (toBool (forceTree Main.t22)) True
|
||||
--forcet22 = crefl
|
||||
-- forcet23 : CEq (toBool (forceTree Main.t23)) True
|
||||
-- forcet23 = crefl
|
||||
@ -1,156 +0,0 @@
|
||||
Bool : Type
|
||||
True : Bool
|
||||
False : Bool
|
||||
|
||||
CBool : Type
|
||||
CBool = (t: Type) t -> t -> t
|
||||
|
||||
CBool.to_bool (x : CBool) : Bool
|
||||
CBool.to_bool x = (x Bool True False)
|
||||
|
||||
CTrue : CBool
|
||||
CTrue = p => t => f => t
|
||||
|
||||
CFalse : CBool
|
||||
CFalse = p => t => f => f
|
||||
|
||||
And (a: CBool) (b: CBool) : CBool
|
||||
And a b = p => t => f => (a p (b p t f) f)
|
||||
|
||||
CNat : Type
|
||||
CNat = (n: Type) (n -> n) -> n -> n
|
||||
|
||||
Add (a: CNat) (b: CNat) : CNat
|
||||
Add a b = n => s => z => (a n s (b n s z))
|
||||
|
||||
CMul (a: CNat) (b: CNat) : CNat
|
||||
CMul a b = n => s => (a n (b n s))
|
||||
|
||||
Suc (a: CNat) : CNat
|
||||
Suc a = n => s => z => (s (a n s z))
|
||||
|
||||
CEqual (t: Type) (a: t) (b: t) : Type
|
||||
CEqual t a b = (p: t -> Type) (p a) -> (p b)
|
||||
|
||||
CRefl (t: Type) (x: t) : (CEqual t x x)
|
||||
CRefl t x = p => px => px
|
||||
|
||||
N0 : CNat
|
||||
N0 = n => s => z => z
|
||||
|
||||
N2 : CNat
|
||||
N2 = n => s => z => (s (s z))
|
||||
|
||||
N3 : CNat
|
||||
N3 = n => s => z => (s (s (s z)))
|
||||
|
||||
N4 : CNat
|
||||
N4 = n => s => z => (s (s (s (s z))))
|
||||
|
||||
N5 : CNat
|
||||
N5 = n => s => z => (s (s (s (s (s z)))))
|
||||
|
||||
N10 : CNat
|
||||
N10 = (CMul N2 N5)
|
||||
|
||||
N10b : CNat
|
||||
N10b = (CMul N5 N2)
|
||||
|
||||
N15 : CNat
|
||||
N15 = (Add N10 N5)
|
||||
|
||||
N15b : CNat
|
||||
N15b = (Add N10b N5)
|
||||
|
||||
N18 : CNat
|
||||
N18 = (Add N15 N3)
|
||||
|
||||
N18b : CNat
|
||||
N18b = (Add N15b N3)
|
||||
|
||||
N19 : CNat
|
||||
N19 = (Add N15 N4)
|
||||
|
||||
N19b : CNat
|
||||
N19b = (Add N15b N4)
|
||||
|
||||
N20 : CNat
|
||||
N20 = (CMul N2 N10)
|
||||
|
||||
N20b : CNat
|
||||
N20b = (CMul N2 N10b)
|
||||
|
||||
N21 : CNat
|
||||
N21 = (Suc N20)
|
||||
|
||||
N21b : CNat
|
||||
N21b = (Suc N20b)
|
||||
|
||||
N22 : CNat
|
||||
N22 = (Suc N21)
|
||||
|
||||
N22b : CNat
|
||||
N22b = (Suc N21b)
|
||||
|
||||
N23 : CNat
|
||||
N23 = (Suc N22)
|
||||
|
||||
N23b : CNat
|
||||
N23b = (Suc N22b)
|
||||
|
||||
N100 : CNat
|
||||
N100 = (CMul N10 N10)
|
||||
|
||||
N100b : CNat
|
||||
N100b = (CMul N10b N10b)
|
||||
|
||||
N10k : CNat
|
||||
N10k = (CMul N100 N100)
|
||||
|
||||
N10kb : CNat
|
||||
N10kb = (CMul N100b N100b)
|
||||
|
||||
N100k : CNat
|
||||
N100k = (CMul N10k N10)
|
||||
|
||||
N100kb : CNat
|
||||
N100kb = (CMul N10kb N10b)
|
||||
|
||||
N1M : CNat
|
||||
N1M = (CMul N10k N100)
|
||||
|
||||
N1Mb : CNat
|
||||
N1Mb = (CMul N10kb N100b)
|
||||
|
||||
N5M : CNat
|
||||
N5M = (CMul N1M N5)
|
||||
|
||||
N5Mb : CNat
|
||||
N5Mb = (CMul N1Mb N5)
|
||||
|
||||
N10M : CNat
|
||||
N10M = (CMul N5M N2)
|
||||
|
||||
N10Mb : CNat
|
||||
N10Mb = (CMul N5Mb N2)
|
||||
|
||||
CTree : Type
|
||||
CTree = (t: Type) (t -> t -> t) -> t -> t
|
||||
|
||||
CLeaf : CTree
|
||||
CLeaf = t => n => l => l
|
||||
|
||||
CNode (t1: CTree) (t2: CTree) : CTree
|
||||
CNode t1 t2 = t => n => l => (n (t1 t n l) (t2 t n l))
|
||||
|
||||
FullCTree (n: CNat) : CTree
|
||||
FullCTree n = (n CTree (t => CNode t t) CLeaf)
|
||||
|
||||
Num : CNat
|
||||
Num = N2
|
||||
|
||||
Force (n: CNat) : Bool
|
||||
Force n = (n Bool (x => x) True)
|
||||
|
||||
Main : (CEqual CNat N1M N1Mb)
|
||||
Main = (CRefl CNat N1M)
|
||||
@ -1,25 +0,0 @@
|
||||
data Nat : Set where
|
||||
z : Nat
|
||||
s : Nat -> Nat
|
||||
|
||||
data The : (x : Nat) -> Set where
|
||||
val : (x : Nat) -> The x
|
||||
|
||||
add : Nat -> Nat -> Nat
|
||||
add a (s b) = s (add a b)
|
||||
add a z = a
|
||||
|
||||
mul : Nat -> Nat -> Nat
|
||||
mul a (s b) = add a (mul a b)
|
||||
mul a z = z
|
||||
|
||||
exp : Nat -> Nat -> Nat
|
||||
exp a (s b) = mul a (exp a b)
|
||||
exp a z = s z
|
||||
|
||||
nul : Nat -> Nat
|
||||
nul (s a) = (nul a)
|
||||
nul z = z
|
||||
|
||||
work : The (nul (exp (s (s (s z))) (s (s (s (s (s (s (s (s z))))))))))
|
||||
work = val z
|
||||
@ -1,26 +0,0 @@
|
||||
data NAT : Type where
|
||||
Z : NAT
|
||||
S : NAT -> NAT
|
||||
|
||||
data The : NAT -> Type where
|
||||
Val : (x : NAT) -> The x
|
||||
|
||||
add : NAT -> NAT -> NAT
|
||||
add a (S b) = S (add a b)
|
||||
add a Z = a
|
||||
|
||||
mul : NAT -> NAT -> NAT
|
||||
mul a (S b) = add a (mul a b)
|
||||
mul a Z = Z
|
||||
|
||||
exp : NAT -> NAT -> NAT
|
||||
exp a (S b) = mul a (exp a b)
|
||||
exp a Z = S Z
|
||||
|
||||
nul : NAT -> NAT
|
||||
nul (S a) = nul a
|
||||
nul Z = Z
|
||||
|
||||
work : The (nul (exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))
|
||||
work = Val Z
|
||||
|
||||
@ -1,26 +0,0 @@
|
||||
Nat : Type
|
||||
Z : Nat
|
||||
S (pred: Nat) : Nat
|
||||
|
||||
The (x: Nat) : Type
|
||||
Val (x: Nat) : (The x)
|
||||
|
||||
Add (a: Nat) (b: Nat) : Nat
|
||||
Add a (S b) = (S (Add a b))
|
||||
Add a (Z) = a
|
||||
|
||||
Mul (a: Nat) (b: Nat) : Nat
|
||||
Mul a (S b) = (Add a (Mul a b))
|
||||
Mul a (Z) = (Z)
|
||||
|
||||
Exp (a: Nat) (b: Nat) : Nat
|
||||
Exp a (S b) = (Mul a (Exp a b))
|
||||
Exp a (Z) = (S Z)
|
||||
|
||||
Nul (n: Nat) : Nat
|
||||
Nul (S a) = (Nul a)
|
||||
Nul (Z) = (Z)
|
||||
|
||||
Work : (The (Nul (Exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z))))))))))) {
|
||||
(Val Z)
|
||||
}
|
||||
@ -1,25 +0,0 @@
|
||||
inductive NAT where
|
||||
| Z : NAT
|
||||
| S : NAT -> NAT
|
||||
|
||||
inductive The : NAT -> Type where
|
||||
| val : (x : NAT) -> The x
|
||||
|
||||
def add : NAT -> NAT -> NAT
|
||||
| a, NAT.S b => NAT.S (add a b)
|
||||
| a, NAT.Z => a
|
||||
|
||||
def mul : NAT -> NAT -> NAT
|
||||
| a, NAT.S b => add a (mul a b)
|
||||
| _, NAT.Z => NAT.Z
|
||||
|
||||
def exp : NAT -> NAT -> NAT
|
||||
| a, NAT.S b => mul a (exp a b)
|
||||
| _, NAT.Z => NAT.S NAT.Z
|
||||
|
||||
def nul : NAT -> NAT
|
||||
| NAT.S a => nul a
|
||||
| NAT.Z => NAT.Z
|
||||
|
||||
def work : The (nul (exp (NAT.S (NAT.S (NAT.S NAT.Z))) (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S (NAT.S NAT.Z))))))))))
|
||||
:= @The.val NAT.Z
|
||||
@ -1,36 +0,0 @@
|
||||
Inductive Nat : Type :=
|
||||
| Z
|
||||
| S : Nat -> Nat.
|
||||
|
||||
(* Inductive The : Nat -> Type :=
|
||||
| val : forall (x : Nat), The x. *)
|
||||
|
||||
Inductive The : Nat -> Prop :=
|
||||
| val (x : Nat) : The x.
|
||||
|
||||
Fixpoint add (m : Nat) (n : Nat) : Nat :=
|
||||
match m, n with
|
||||
| m, Z => m
|
||||
| m, (S n) => S (add m n)
|
||||
end.
|
||||
|
||||
Fixpoint mul (m : Nat) (n : Nat) : Nat :=
|
||||
match m, n with
|
||||
| m, Z => Z
|
||||
| m, (S n) => (add m (mul m n))
|
||||
end.
|
||||
|
||||
Fixpoint exp (m : Nat) (n : Nat) : Nat :=
|
||||
match m, n with
|
||||
| m, Z => (S Z)
|
||||
| m, (S n) => (mul m (exp m n))
|
||||
end.
|
||||
|
||||
Fixpoint nul (n : Nat) : Nat :=
|
||||
match n with
|
||||
| Z => Z
|
||||
| (S n) => nul n
|
||||
end.
|
||||
|
||||
Definition work : The (nul (exp (S (S (S Z))) (S (S (S (S (S (S (S (S Z)))))))))) :=
|
||||
val Z.
|
||||
Loading…
Reference in New Issue
Block a user