1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103

;; Get second element of list (0-indexed)
!(def arg1 (lambda (x) (car (cdr x))))

;; Get left element of tuple at second position in list
!(def arg1a (lambda (x) (car (arg1 x))))

!(def arg1b (lambda (x) (cdr (arg1 x))))

;; Get third element of list
!(def arg2 (lambda (x) (car (cdr (cdr x)))))

!(def arg2a (lambda (x) (car (arg2 x))))

!(def arg2b (lambda (x) (cdr (arg2 x))))

;; Boolean and
!(def and (lambda (x y) (if x (if y t nil) nil)))

;; Boolean or
!(def or (lambda (x y) (if x t (if y t nil))))

;; NEED defrec instead of def for recursive functions
;; TODO: Implement nats
!(defrec check (lambda (env typ term)
  (if (= (car term) 10n)
    (eq typ (eval (arg1 term) env))
  (if (and (= (car typ) 1n) (= (car term) 11n))
    (and (eq (arg2 typ) (arg2a term))
      ;; Crazy eval magic
      (check (eval (list 'let (list (list (arg1 term) (list 'quote (arg1 typ)))) '(current-env)) env) (arg2a term) (arg2b term)))
  (if (and (= (car term) 12n) (= (car (arg1a term)) 1n))
    (and (eq (arg1 (arg1a term)) (arg2a term)) (and (eq (arg2 (arg1a term)) typ)
      (and (check env (arg1a term) (arg1b term))
        (check env (arg2a term) (arg2b term)))))
  (if (and (= (car typ) 2n) (= (car term) 13n))
    (and (eq (arg1a term) (arg1 typ)) (and (eq (arg2a term) (arg2 typ))
      (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term)))))
  (if (and (= (car term) 14n) (= (car (arg1a term)) 2n))
    (and (eq (arg1 (arg1a term)) typ)
      (check env (arg1a term) (arg1b term)))
  (if (and (= (car term) 15n) (= (car (arg1a term)) 2n))
    (and (eq (arg2 (arg1a term)) typ)
      (check env (arg1a term) (arg1b term)))
  (if (and (= (car typ) 3n) (= (car term) 16n))
    (and (or (eq (arg1a term) (arg1 typ)) (eq (arg1a term) (arg2 typ)))
      (check env (arg1a term) (arg1b term)))
  (if (and (= (car term) 20n) (eq (car (arg1a term))))
    t
  nil))))))))))

; Autogenerated by Main.lean
!(def a_imp_a (cons (list 1n (list 0n "A") (list 0n "A")) (list 11n 'a (cons (list 0n "A") (list 10n 'a)))))

(check (empty-env) (car a_imp_a) (cdr a_imp_a))

!(def a_imp_b_imp_ba (cons (list 1n (list 0n "A") (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A")))) (list 11n 'a (cons (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A"))) (list 11n 'b (cons (list 2n (list 0n "B") (list 0n "A")) (list 13n (cons (list 0n "B") (list 10n 'b)) (cons (list 0n "A") (list 10n 'a)))))))))

(check (empty-env) (car a_imp_b_imp_ba) (cdr a_imp_b_imp_ba))

!(def ab_imp_ba (cons (list 1n (list 2n (list 0n "A") (list 0n "B")) (list 2n (list 0n "B") (list 0n "A"))) (list 11n 'ab (cons (list 2n (list 0n "B") (list 0n "A")) (list 13n (cons (list 0n "B") (list 15n (cons (list 2n (list 0n "A") (list 0n "B")) (list 10n 'ab)))) (cons (list 0n "A") (list 14n (cons (list 2n (list 0n "A") (list 0n "B")) (list 10n 'ab)))))))))

(check (empty-env) (car ab_imp_ba) (cdr ab_imp_ba))

!(def not_ab_imp_not_a (cons (list 1n (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n)) (list 1n (list 0n "A") '(5n))) (list 11n 'f (cons (list 1n (list 0n "A") '(5n)) (list 11n 'x (cons '(5n) (list 12n (cons (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n)) (list 10n 'f)) (cons (list 3n (list 0n "A") (list 0n "B")) (list 16n (cons (list 0n "A") (list 10n 'x)))))))))))

(check (empty-env) (car not_ab_imp_not_a) (cdr not_ab_imp_not_a))

;; Currently broken
!(defprotocol not_ab_imp_not_a_protocol (term)
  (cons
    ;; claim definition
    (cons (cons (list 'check (empty-env) (car not_ab_imp_not_a) term) (current-env)) t)
    ;; post-verification predicate is not provided
    nil)
  :description "¬(A ∨ B) → ¬A")

!(dump-expr not_ab_imp_not_a_protocol "protocol")

!(prove-protocol not_ab_imp_not_a_protocol "protocol-proof" (cdr not_ab_imp_not_a))

;; ;; A protocol that requires knowledge of a hash that opens to a pair such that
;; ;; its components add up to 30. If the proof is accepted, further require that
;; ;; the first component of the pair be greater than 10.
;; !(defprotocol my-protocol (hash pair)
;;   (cons
;;     (if (= (+ (car pair) (cdr pair)) 30)
;;       (cons (cons (cons 'open (cons hash nil)) (empty-env)) pair)
;;       nil)
;;     (lambda () (> (car pair) 10)))
;;   :description "hash opens to a pair (a, b) s.t. a+b=30 and a>10")

;; ;; This is the prover's pair, whose hash is
;; ;; #c0x955f855f302a30ed988cc48685c442ebd98c8711e989fc64df8f27f52e1350
;; (commit '(13 . 17))

;; ;; Let's prove it and write the proof to the file protocol-proof
;; !(prove-protocol my-protocol
;;   "protocol-proof"
;;   #c0x955f855f302a30ed988cc48685c442ebd98c8711e989fc64df8f27f52e1350
;;   '(13 . 17))

;; ;; Now it can be verified
;; !(verify-protocol my-protocol "protocol-proof")