Use field elements instead of strings for variable names

Changes

2 changed files (+13/-28)

• Main.lean
  • @@ -11,7 +11,7 @@ TODO: Equality
    -/ inductive Typ /-- New named type -/ - | new : String → Typ + | new : Nat → Typ /-- Function type -/ | fn : Typ → Typ → Typ -- All types below are inductive
  • @@ -55,7 +55,7 @@ inductive Term
    | fls_elim : Term × Typ → Term def Typ.toString : Typ → String - | new α => s!"(list 0n \"{α}\")" + | new α => s!"(list 0n {α}n)" | fn α β => s!"(list 1n {α.toString} {β.toString})" | prod α β => s!"(list 2n {α.toString} {β.toString})" | sum α β => s!"(list 3n {α.toString} {β.toString})"
  • @@ -120,44 +120,29 @@ theorem false_empty : check (.ofList []) t .fls == false := by
    sorry -- TODO: Implement eval so we can state 2 + 2 = 4 - -- def eval env (venv : Std.HashMap String Term) t τ (h : check env t τ) (henv : ∀ x, x ∈ venv.keys → x ∈ env.keys) : Term × Typ := - -- match t, τ with - -- | .var x, _ => - -- (venv[x]'(by sorry), env[x]'(by sorry)) - -- | .lam f (b, β'), .fn α β => - -- (.lam f (eval (env.insert f α) venv b β (by sorry) (by sorry)), .fn α β) - -- | .app (f, .fn α β) (a, α'), β' => - -- let (a', α'') := eval env venv a α h henv - -- let (f', _) := eval env venv f (.fn α β) h henv - -- match f' with - -- | .lam x (b, β'') => eval (env.insert x α) (venv.insert x a') b β (by sorry) (by sorry) - -- | _ => nofun - -- | .and (a, α) (b, β), τ => - -- (.and (eval env venv a α (by sorry) henv) (eval env venv b β (by sorry) henv), τ) - - - def a_imp_a := (Term.lam "a" (.var "a", .new "A"), Typ.fn (.new "A") (.new "A")) + + def a_imp_a := (Term.lam "a" (.var "a", .new 0), Typ.fn (.new 0) (.new 0)) #guard check (.ofList []) a_imp_a.1 a_imp_a.2 #eval IO.println a_imp_a /-- A → B → B ∧ A -/ - def a_imp_b_imp_ba := (Term.lam "a" (.lam "b" (.and (.var "b", .new "B") (.var "a", .new "A"), .prod (.new "B") (.new "A")), .fn (.new "B") (.prod (.new "B") (.new "A"))), Typ.fn (.new "A") (.fn (.new "B") (.prod (.new "B") (.new "A")))) + def a_imp_b_imp_ba := (Term.lam "a" (.lam "b" (.and (.var "b", .new 1) (.var "a", .new 0), .prod (.new 1) (.new 0)), .fn (.new 1) (.prod (.new 1) (.new 0))), Typ.fn (.new 0) (.fn (.new 1) (.prod (.new 1) (.new 0)))) #guard check (.ofList []) a_imp_b_imp_ba.1 a_imp_b_imp_ba.2 #eval IO.println a_imp_b_imp_ba /-- A ∧ B → B ∧ A -/ - def ab_imp_ba := (Term.lam "ab" (.and (.and2 (.var "ab", .prod (.new "A") (.new "B")), .new "B") (.and1 (.var "ab", .prod (.new "A") (.new "B")), .new "A"), .prod (.new "B") (.new "A")), Typ.fn (.prod (.new "A") (.new "B")) (.prod (.new "B") (.new "A"))) + def ab_imp_ba := (Term.lam "ab" (.and (.and2 (.var "ab", .prod (.new 0) (.new 1)), .new 1) (.and1 (.var "ab", .prod (.new 0) (.new 1)), .new 0), .prod (.new 1) (.new 0)), Typ.fn (.prod (.new 0) (.new 1)) (.prod (.new 1) (.new 0))) #guard check (.ofList []) ab_imp_ba.1 ab_imp_ba.2 #eval IO.println ab_imp_ba /-- ¬(A ∨ B) → ¬A -/ - def not_ab_imp_not_a := (Term.lam "f" (.lam "a" (.app (.var "f", .fn (.sum (.new "A") (.new "B")) .fls) (.or (.var "a", .new "A"), .sum (.new "A") (.new "B")), .fls), .fn (.new "A") .fls), Typ.fn (.fn (.sum (.new "A") (.new "B")) .fls) (.fn (.new "A") .fls)) + def not_ab_imp_not_a := (Term.lam "f" (.lam "a" (.app (.var "f", .fn (.sum (.new 0) (.new 1)) .fls) (.or (.var "a", .new 0), .sum (.new 0) (.new 1)), .fls), .fn (.new 0) .fls), Typ.fn (.fn (.sum (.new 0) (.new 1)) .fls) (.fn (.new 0) .fls)) #guard check (.ofList []) not_ab_imp_not_a.1 not_ab_imp_not_a.2
• main.lurk
  • @@ -56,19 +56,19 @@
    nil)))))))))) ; Autogenerated by Main.lean - !(def a_imp_a (cons (list 11n 'a (cons (list 10n 'a) (list 0n "A"))) (list 1n (list 0n "A") (list 0n "A")))) + !(def a_imp_a (cons (list 11n 'a (cons (list 10n 'a) (list 0n 0n))) (list 1n (list 0n 0n) (list 0n 0n)))) (check (empty-env) (car a_imp_a) (cdr a_imp_a)) - !(def a_imp_b_imp_ba (cons (list 11n 'a (cons (list 11n 'b (cons (list 13n (cons (list 10n 'b) (list 0n "B")) (cons (list 10n 'a) (list 0n "A"))) (list 2n (list 0n "B") (list 0n "A")))) (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A"))))) (list 1n (list 0n "A") (list 1n (list 0n "B") (list 2n (list 0n "B") (list 0n "A")))))) + !(def a_imp_b_imp_ba (cons (list 11n 'a (cons (list 11n 'b (cons (list 13n (cons (list 10n 'b) (list 0n 1n)) (cons (list 10n 'a) (list 0n 0n))) (list 2n (list 0n 1n) (list 0n 0n)))) (list 1n (list 0n 1n) (list 2n (list 0n 1n) (list 0n 0n))))) (list 1n (list 0n 0n) (list 1n (list 0n 1n) (list 2n (list 0n 1n) (list 0n 0n)))))) (check (empty-env) (car a_imp_b_imp_ba) (cdr a_imp_b_imp_ba)) - !(def ab_imp_ba (cons (list 11n 'ab (cons (list 13n (cons (list 15n (cons (list 10n 'ab) (list 2n (list 0n "A") (list 0n "B")))) (list 0n "B")) (cons (list 14n (cons (list 10n 'ab) (list 2n (list 0n "A") (list 0n "B")))) (list 0n "A"))) (list 2n (list 0n "B") (list 0n "A")))) (list 1n (list 2n (list 0n "A") (list 0n "B")) (list 2n (list 0n "B") (list 0n "A"))))) + !(def ab_imp_ba (cons (list 11n 'ab (cons (list 13n (cons (list 15n (cons (list 10n 'ab) (list 2n (list 0n 0n) (list 0n 1n)))) (list 0n 1n)) (cons (list 14n (cons (list 10n 'ab) (list 2n (list 0n 0n) (list 0n 1n)))) (list 0n 0n))) (list 2n (list 0n 1n) (list 0n 0n)))) (list 1n (list 2n (list 0n 0n) (list 0n 1n)) (list 2n (list 0n 1n) (list 0n 0n))))) (check (empty-env) (car ab_imp_ba) (cdr ab_imp_ba)) - !(def not_ab_imp_not_a (cons (list 11n 'f (cons (list 11n 'a (cons (list 12n (cons (list 10n 'f) (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n))) (cons (list 16n (cons (list 10n 'a) (list 0n "A"))) (list 3n (list 0n "A") (list 0n "B")))) '(5n))) (list 1n (list 0n "A") '(5n)))) (list 1n (list 1n (list 3n (list 0n "A") (list 0n "B")) '(5n)) (list 1n (list 0n "A") '(5n))))) + !(def not_ab_imp_not_a (cons (list 11n 'f (cons (list 11n 'a (cons (list 12n (cons (list 10n 'f) (list 1n (list 3n (list 0n 0n) (list 0n 1n)) '(5n))) (cons (list 16n (cons (list 10n 'a) (list 0n 0n))) (list 3n (list 0n 0n) (list 0n 1n)))) '(5n))) (list 1n (list 0n 0n) '(5n)))) (list 1n (list 1n (list 3n (list 0n 0n) (list 0n 1n)) '(5n)) (list 1n (list 0n 0n) '(5n))))) (check (empty-env) (car not_ab_imp_not_a) (cdr not_ab_imp_not_a))
  • @@ -76,14 +76,14 @@
    !(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) + (cons (cons (list 'check (empty-env) term (cdr not_ab_imp_not_a)) (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)) + !(prove-protocol not_ab_imp_not_a_protocol "protocol-proof" (car 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