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

import Std.Data.HashMap

-- A type checker for simply typed lambda calculus (equivalent to propositional logic)

/--
Types in our toy language

We use Greek letters for variables with type `Typ`
-/
inductive Typ
  /-- New named type -/
  | new : String → Typ
  /-- Function type -/
  | fn : Typ → Typ → Typ
  /-- Product type -/
  | prod : Typ → Typ → Typ
  /-- Sum type -/
  | sum : Typ → Typ → Typ
  /-- False (no terms of this type) -/
  | fls : Typ
deriving BEq

/-- Terms in our toy language -/
inductive Term
  /-- Variable -/
  | var : String → Term
  /-- Lambda -/
  | lam : String → Typ × Term → Term
  /-- Function application -/
  | app : Typ × Term → Typ × Term → Term
  /-- Construct a product -/
  | and : Typ × Term → Typ × Term → Term
  /-- Get first element of product -/
  | and1 : Typ × Term → Term
  /-- Get second element of product -/
  | and2 : Typ × Term → Term
  /-- Construct a sum -/
  | or : Typ × Term → Term

-- TODO: Convert `Term` into Lurk s-expression

/--
The type checker!

TODO: Port to Lurk
-/
def check (env : Std.HashMap String Typ) : Typ → Term → Bool
  | τ, .var x =>
    (· == τ) <$> env[x]? |>.getD false
  | .fn α β, .lam x (β', b) =>
    β' == β && check (env.insert x α) β' b
  | τ, .app (.fn α β, f) (α', x) =>
    α' == α && β == τ && check env (.fn α β) f && check env α' x
  | .prod α β, .and (α', x) (β', y) =>
    α' == α && β' == β && check env α' x && check env β' y
  | τ, .and1 (.prod α β, x) =>
    τ == α && check env (.prod α β) x
  | τ, .and2 (.prod α β, y) =>
    τ == β && check env (.prod α β) y
  | .sum α β, .or (γ, z) =>
    (γ == α ∨ γ == β) && check env γ z
  | _, _ => false

-- theorem false_empty (h : ∀ x, (_ : x ∈ env.keys) → env[x]'(by grind) != .fls) : check env .fls t == false := by
--   cases t <;> try grind [check]

/-- A → B → B ∧ A -/
def a_imp_b_imp_ba := (Typ.fn (.new "A") (.fn (.new "B") (.prod (.new "B") (.new "A"))), Term.lam "a" (.fn (.new "B") (.prod (.new "B") (.new "A")), .lam "b" (.prod (.new "B") (.new "A"), .and (.new "B", .var "b") (.new "A", .var "a"))))

#guard check (.ofList []) a_imp_b_imp_ba.1 a_imp_b_imp_ba.2

/-- A ∧ B → B ∧ A -/
def ab_imp_ba := (Typ.fn (.prod (.new "A") (.new "B")) (.prod (.new "B") (.new "A")), Term.lam "ab" (.prod (.new "B") (.new "A"), .and (.new "B", .and2 (.prod (.new "A") (.new "B"), .var "ab")) (.new "A", .and1 (.prod (.new "A") (.new "B"), .var "ab"))))

#guard check (.ofList []) ab_imp_ba.1 ab_imp_ba.2

/-- ¬(A ∨ B) → ¬A -/
def not_ab_imp_not_a := (Typ.fn (.fn (.sum (.new "A") (.new "B")) .fls) (.fn (.new "A") .fls), Term.lam "f" (.fn (.new "A") .fls, .lam "x" (.fls, .app (.fn (.sum (.new "A") (.new "B")) .fls, .var "f") (.sum (.new "A") (.new "B"), .or (.new "A", .var "x")))))

#guard check (.ofList []) not_ab_imp_not_a.1 not_ab_imp_not_a.2