ac2e7867 - 6.5610-project

Authored by: Anthony Wang
Authored at: 2026-05-07 21:22:29 -0400
Committed by: Anthony Wang
Committed at: 2026-05-07 21:22:29 -0400
Signature: View
-----BEGIN SSH SIGNATURE----- U1NIU0lHAAAAAQAAADMAAAALc3NoLWVkMjU1MTkAAAAg8Ms9qQOcB6WoVNS51AHxfRPvJz /x6RXeMaql4lvTraUAAAADZ2l0AAAAAAAAAAZzaGE1MTIAAABTAAAAC3NzaC1lZDI1NTE5 AAAAQA8/DchYR4Er+U/7HweHN+fJHfnZTB6su47t2Bybn9yPUciNQsN1mleyQmX1BiKHQU XDWzLZh4AQyYAQDjtpzwA= -----END SSH SIGNATURE-----
Object name: ac2e7867082d0393b24e46148b74251dd259489b
Parent: 9fb51f49

Delete Lurk files for old type checker I kept the demo directory though

Changes

7 changed files (+0/-215)

a.lurk (deleted)
- @@ -1,59 +0,0 @@
  - ;; lists the relevant bindings - !(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)))) - - ;; Get ith element of list - !(defrec geti (lambda (xs i) (if (= i 0) (car xs) (geti (cdr xs) (- i 1))))) - - ;; NEED defrec instead of def for recursive functions - ;; TODO: Implement nats - !(defrec check (lambda (env term typ) - ;; Variable - (if (= (car term) 10n) - (eq typ (geti env (arg1 term))) - ;; Lambda - (if (and (= (car term) 11n) (= (car typ) 1n)) - (and (eq (arg2 typ) (arg1b term)) - (check (cons (arg1 typ) env) (arg1a term) (arg1b term))) - ;; Application - (if (and (= (car term) 12n) (= (car (arg1b term)) 1n)) - (and (eq (arg1 (arg1b term)) (arg2b term)) (and (eq (arg2 (arg1b term)) typ) - (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) - ;; And - (if (and (= (car term) 13n) (= (car typ) 2n)) - (and (eq (arg1b term) (arg1 typ)) (and (eq (arg2b term) (arg2 typ)) - (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) - ;; And1 - (if (and (= (car term) 14n) (= (car (arg1b term)) 2n)) - (and (eq (arg1 (arg1b term)) typ) - (check env (arg1a term) (arg1b term))) - ;; And2 - (if (and (= (car term) 15n) (= (car (arg1b term)) 2n)) - (and (eq (arg2 (arg1b term)) typ) - (check env (arg1a term) (arg1b term))) - ;; Or - (if (and (= (car term) 16n) (= (car typ) 3n)) - (and (or (eq (arg1b term) (arg1 typ)) (eq (arg1b term) (arg2 typ))) - (check env (arg1a term) (arg1b term))) - ;; False elim - (if (and (= (car term) 20n) (eq (car (arg1b term)) 5n)) - t - nil)))))))))) -
files/not_ab_imp_not_a_proof (deleted)
files/not_ab_imp_not_a_protocol (deleted)
files/not_not_not_a_imp_not_a_proof (deleted)
files/not_not_not_a_imp_not_a_protocol (deleted)
protocol.lurk (deleted)
- @@ -1,78 +0,0 @@
  - ;; load muLean - ;; !(load "a.lurk") - - ;; !(def statement (list 1n (list 1n (list 3n (list 0n 0n) (list 0n 1n)) '(5n)) (list 1n (list 0n 0n) '(5n)))) - - !(def not_ab_imp_not_a_solution (list 11n (cons (list 11n (cons (list 12n (cons (list 10n 1) (list 1n (list 3n (list 0n 0n) (list 0n 1n)) '(5n))) (cons (list 16n (cons (list 10n 0) (list 0n 0n))) (list 3n (list 0n 0n) (list 0n 1n)))) '(5n))) (list 1n (list 0n 0n) '(5n))))) - - !(def comm_term_test (hide #0x2903850943570 not_ab_imp_not_a_solution)) - - ;; (eval (emit ( - ;; list 'check nil (list 'open 'comm_term_test) 'statement - ;; )) (current-env)) - - !(defprotocol not_ab_imp_not_a_protocol (comm_term) - (cons - ;; claim definition - (cons (cons - ;; expression - ;; needs to be a quoted syntax tree - (list 'check nil (list 'open comm_term) 'statement) - ;; environment - (letrec ( - (arg1 (lambda (x) (car (cdr x)))) - (arg1a (lambda (x) (car (arg1 x)))) - (arg1b (lambda (x) (cdr (arg1 x)))) - (arg2 (lambda (x) (car (cdr (cdr x))))) - (arg2a (lambda (x) (car (arg2 x)))) - (arg2b (lambda (x) (cdr (arg2 x)))) - (and (lambda (x y) (if x (if y t nil) nil))) - (or (lambda (x y) (if x t (if y t nil)))) - (geti (lambda (xs i) (if (= i 0) (car xs) (geti (cdr xs) (- i 1))))) - (check (lambda (env term typ) - ;; Variable - (if (= (car term) 10n) - (eq typ (geti env (arg1 term))) - ;; Lambda - (if (and (= (car term) 11n) (= (car typ) 1n)) - (and (eq (arg2 typ) (arg1b term)) - (check (cons (arg1 typ) env) (arg1a term) (arg1b term))) - ;; Application - (if (and (= (car term) 12n) (= (car (arg1b term)) 1n)) - (and (eq (arg1 (arg1b term)) (arg2b term)) (and (eq (arg2 (arg1b term)) typ) - (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) - ;; And - (if (and (= (car term) 13n) (= (car typ) 2n)) - (and (eq (arg1b term) (arg1 typ)) (and (eq (arg2b term) (arg2 typ)) - (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) - ;; And1 - (if (and (= (car term) 14n) (= (car (arg1b term)) 2n)) - (and (eq (arg1 (arg1b term)) typ) - (check env (arg1a term) (arg1b term))) - ;; And2 - (if (and (= (car term) 15n) (= (car (arg1b term)) 2n)) - (and (eq (arg2 (arg1b term)) typ) - (check env (arg1a term) (arg1b term))) - ;; Or - (if (and (= (car term) 16n) (= (car typ) 3n)) - (and (or (eq (arg1b term) (arg1 typ)) (eq (arg1b term) (arg2 typ))) - (check env (arg1a term) (arg1b term))) - ;; False elim - (if (and (= (car term) 20n) (eq (car (arg1b term)) 5n)) - t - nil)))))))))) - - (statement (list 1n (list 1n (list 3n (list 0n 0n) (list 0n 1n)) '(5n)) (list 1n (list 0n 0n) '(5n)))) - ) (current-env)) - ) - ;; expected output - t ) - ;; post-verification predicate - nil) - :description "¬(A ∨ B) → ¬A") - - !(dump-expr not_ab_imp_not_a_protocol "files/not_ab_imp_not_a_protocol") - !(defq not_ab_imp_not_a_protocol_loaded !(load-expr "files/not_ab_imp_not_a_protocol")) - !(prove-protocol not_ab_imp_not_a_protocol_loaded "files/not_ab_imp_not_a_proof" comm_term_test) - !(inspect "10662522c024b18140b63a5159dc46cdc268e367a5a2a08b0d9e486b9b6201") - !(verify-protocol not_ab_imp_not_a_protocol_loaded "files/not_ab_imp_not_a_proof")
protocol2.lurk (deleted)
- @@ -1,78 +0,0 @@
  - ;; load muLean - ;; !(load "a.lurk") - - ;; !(def statement (list 1n (list 1n (list 3n (list 0n 0n) (list 0n 1n)) '(5n)) (list 1n (list 0n 0n) '(5n)))) - - !(def not_not_not_a_imp_not_a_solution (list 11n (cons (list 11n (cons (list 12n (cons (list 10n 1) (list 1n (list 1n (list 1n (list 0n 0n) '(5n)) '(5n)) '(5n))) (cons (list 12n (cons (list 11n (cons (list 11n (cons (list 12n (cons (list 10n 0) (list 1n (list 0n 0n) '(5n))) (cons (list 10n 1) (list 0n 0n))) '(5n))) (list 1n (list 1n (list 0n 0n) '(5n)) '(5n)))) (list 1n (list 0n 0n) (list 1n (list 1n (list 0n 0n) '(5n)) '(5n)))) (cons (list 10n 0) (list 0n 0n))) (list 1n (list 1n (list 0n 0n) '(5n)) '(5n)))) '(5n))) (list 1n (list 0n 0n) '(5n))))) - - !(def comm_term_test (hide #0x2903850943570 not_not_not_a_imp_not_a_solution)) - - ;; (eval (emit ( - ;; list 'check nil (list 'open 'comm_term_test) 'statement - ;; )) (current-env)) - - !(defprotocol not_not_not_a_imp_not_a_protocol (comm_term) - (cons - ;; claim definition - (cons (cons - ;; expression - ;; needs to be a quoted syntax tree - (list 'check nil (list 'open comm_term) 'statement) - ;; environment - (letrec ( - (arg1 (lambda (x) (car (cdr x)))) - (arg1a (lambda (x) (car (arg1 x)))) - (arg1b (lambda (x) (cdr (arg1 x)))) - (arg2 (lambda (x) (car (cdr (cdr x))))) - (arg2a (lambda (x) (car (arg2 x)))) - (arg2b (lambda (x) (cdr (arg2 x)))) - (and (lambda (x y) (if x (if y t nil) nil))) - (or (lambda (x y) (if x t (if y t nil)))) - (geti (lambda (xs i) (if (= i 0) (car xs) (geti (cdr xs) (- i 1))))) - (check (lambda (env term typ) - ;; Variable - (if (= (car term) 10n) - (eq typ (geti env (arg1 term))) - ;; Lambda - (if (and (= (car term) 11n) (= (car typ) 1n)) - (and (eq (arg2 typ) (arg1b term)) - (check (cons (arg1 typ) env) (arg1a term) (arg1b term))) - ;; Application - (if (and (= (car term) 12n) (= (car (arg1b term)) 1n)) - (and (eq (arg1 (arg1b term)) (arg2b term)) (and (eq (arg2 (arg1b term)) typ) - (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) - ;; And - (if (and (= (car term) 13n) (= (car typ) 2n)) - (and (eq (arg1b term) (arg1 typ)) (and (eq (arg2b term) (arg2 typ)) - (and (check env (arg1a term) (arg1b term)) (check env (arg2a term) (arg2b term))))) - ;; And1 - (if (and (= (car term) 14n) (= (car (arg1b term)) 2n)) - (and (eq (arg1 (arg1b term)) typ) - (check env (arg1a term) (arg1b term))) - ;; And2 - (if (and (= (car term) 15n) (= (car (arg1b term)) 2n)) - (and (eq (arg2 (arg1b term)) typ) - (check env (arg1a term) (arg1b term))) - ;; Or - (if (and (= (car term) 16n) (= (car typ) 3n)) - (and (or (eq (arg1b term) (arg1 typ)) (eq (arg1b term) (arg2 typ))) - (check env (arg1a term) (arg1b term))) - ;; False elim - (if (and (= (car term) 20n) (eq (car (arg1b term)) 5n)) - t - nil)))))))))) - - (statement (list 1n (list 1n (list 1n (list 1n (list 0n 0n) '(5n)) '(5n)) '(5n)) (list 1n (list 0n 0n) '(5n)))) - ) (current-env)) - ) - ;; expected output - t ) - ;; post-verification predicate - nil) - :description "¬¬¬A → ¬A") - - !(dump-expr not_not_not_a_imp_not_a_protocol "files/not_not_not_a_imp_not_a_protocol") - !(defq not_not_not_a_imp_not_a_protocol_loaded !(load-expr "files/not_not_not_a_imp_not_a_protocol")) - !(prove-protocol not_not_not_a_imp_not_a_protocol_loaded "files/not_not_not_a_imp_not_a_proof" comm_term_test) - !(inspect "10662522c024b18140b63a5159dc46cdc268e367a5a2a08b0d9e486b9b6201") - !(verify-protocol not_not_not_a_imp_not_a_protocol_loaded "files/not_not_not_a_imp_not_a_proof")