zenith/examples/tree_eval.zkt at main · bridgekat/zenith · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
[
  Bool ≔ [B : Type, t : B, f : B] → B,
  true ≔ [B, t, f] ↦ t : Bool,
  false ≔ [B, t, f] ↦ f : Bool,
  and ≔ [a, b, B, t, f] ↦ a B (b B t f) f : [a : Bool, b : Bool] → Bool,
  Nat ≔ [N : Type, s : [n : N] → N, z : N] → N,
  add ≔ [a, b, n, s, z] ↦ a n s (b n s z) : [a : Nat, b : Nat] → Nat,
  mul ≔ [a, b, n, s] ↦ a n (b n s) : [a : Nat, b : Nat] → Nat,
  suc ≔ [a, n, s, z] ↦ s (a n s z) : [a : Nat] → Nat,
  Eq ≔ [A, x, y] ↦ [P : [a : A] → Type, h : P x] → P y : [A : Type, x : A, y : A] → Type,
  refl ≔ [A, x, P, h] ↦ h : [A : Type, x : A] → Eq A x x,
  n2 ≔ [N, s, z] ↦ s (s z) : Nat,
  n3 ≔ [N, s, z] ↦ s (s (s z)) : Nat,
  n4 ≔ [N, s, z] ↦ s (s (s (s z))) : Nat,
  n5 ≔ [N, s, z] ↦ s (s (s (s (s z)))) : Nat,
  n10 ≔ mul n2 n5,
  n10b ≔ mul n5 n2,
  n15 ≔ add n10 n5,
  n15b ≔ add n10b n5,
  n18 ≔ add n15 n3,
  n18b ≔ add n15b n3,
  n19 ≔ add n15 n4,
  n19b ≔ add n15b n4,
  n20 ≔ mul n2 n10,
  n20b ≔ mul n2 n10b,
  n21 ≔ suc n20,
  n21b ≔ suc n20b,
  n22 ≔ suc n21,
  n22b ≔ suc n21b,
  n23 ≔ suc n22,
  n23b ≔ suc n22b,
  n100 ≔ mul n10 n10,
  n100b ≔ mul n10b n10b,
  n10k ≔ mul n100 n100,
  n10kb ≔ mul n100b n100b,
  n100k ≔ mul n10k n10,
  n100kb ≔ mul n10kb n10b,
  n1M ≔ mul n10k n100,
  n1Mb ≔ mul n10kb n100b,
  n5M ≔ mul n1M n5,
  n5Mb ≔ mul n1Mb n5,
  n10M ≔ mul n5M n2,
  n10Mb ≔ mul n5Mb n2,
  Tree ≔ [T : Type, node : [left : T, right : T] → T, leaf : T] → T,
  leaf ≔ [T, n, l] ↦ l : Tree,
  node ≔ [left, right, T, n, l] ↦ n (left T n l) (right T n l) : [left : Tree, right : Tree] → Tree,
  fullTree ≔ [n] ↦ n Tree ([t] ↦ node t t) leaf : [n : Nat] → Tree,
  fullTreeWithLeaf ≔ [bottom, n] ↦ n Tree ([t] ↦ node t t) bottom : [bottom : Tree, n : Nat] → Tree,
  forceTree ≔ [t] ↦ t Bool and true : [t : Tree] → Bool,
  t15 ≔ fullTree n15,
  t15b ≔ fullTree n15b,
  t18 ≔ fullTree n18,
  t18b ≔ fullTree n18b,
  t19 ≔ fullTree n19,
  t19b ≔ fullTree n19b,
  t20 ≔ fullTree n20,
  t20b ≔ fullTree n20b,
  t21 ≔ fullTree n21,
  t21b ≔ fullTree n21b,
  t22 ≔ fullTree n22,
  t22b ≔ fullTree n22b,
  t23 ≔ fullTree n23,
  t23b ≔ fullTree n23b
]
  forceTree t23