#Logic

#Architecture

#Kernel (LCF Architecture)

///|
struct Thm {
  hyps : Array[Term] // hypotheses (assumptions)
  concl : Term // conclusion
}

#Primitive Inference Rules

refl t                                      |- t = t
assume phi                             phi |- phi
eqMp   (A1 |- phi = psi) (A2 |- phi)  A1 U A2 |- psi
absThm v (A |- t = u)                  A |- (\v. t) = (\v. u)
appThm (A1 |- f = g) (A2 |- x = y)    A1 U A2 |- f x = g y
deductAntisym (A1 |- phi) (A2 |- psi)  (A1\{psi}) U (A2\{phi}) |- phi = psi
termSubst sigma (A |- phi)             A[sigma] |- phi[sigma]
typeSubst sigma (A |- phi)             A[sigma] |- phi[sigma]
betaConv (\v. t) u                          |- (\v. t) u = t[u/v]
defineConst c t                             |- c = t

#Examples

///|
test "kernel: refl, assume, eqMp" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let p = @terms.mk_var("p", @types.bool_ty())

  // |- p = p
  let th_eq = @logic.Kernel::refl(p)
  assert_eq(th_eq.hyps.length(), 0)

  // p |- p
  let th_p = @logic.Kernel::assume_(p)
  assert_eq(th_p.hyps.length(), 1)

  // eqMp (|- p = p) (p |- p) => p |- p
  let th = @logic.Kernel::eqMp(th_eq, th_p)
  assert_true(th.concl == p)
}

///|
test "kernel: betaConv reduces a lambda application" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let x = @terms.mk_var("x", a)
  let y = @terms.mk_var("y", a)

  // |- (\x. x) y = y
  let th = @logic.Kernel::betaConv(@terms.Term::mk_abs(x, x), y)
  let (_, rhs) = @terms.Term::dest_eq(th.concl)
  assert_true(rhs == y)
}

///|
test "kernel: defineConst registers a constant" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let x = @terms.mk_var("x", a)
  let body = @terms.Term::mk_abs(x, x)

  // |- my_id = (\x. x)
  let th = @logic.Kernel::defineConst("my_id", body)
  assert_eq(th.hyps.length(), 0)
  let (lhs, rhs) = @terms.Term::dest_eq(th.concl)
  assert_true(lhs is Const(_, _))
  assert_true(rhs.aconv(body))
}

#BoolSyntax (Connectives and Quantifiers)

• mk_* -- builds the formula
• dest_* -- takes it apart
• is_* -- tests whether a term has that form

///|
test "BoolSyntax: implication and negation" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let p = @terms.mk_var("p", @types.bool_ty())
  let q = @terms.mk_var("q", @types.bool_ty())

  // Build p ==> q
  let imp = @logic.BoolSyntax::mk_imp(p, q)
  assert_true(@logic.BoolSyntax::is_imp(imp))
  let (ant, conseq) = @logic.BoolSyntax::dest_imp(imp)
  assert_true(ant == p)
  assert_true(conseq == q)

  // Build ~p, then dest_neg returns the inner term
  let neg = @logic.BoolSyntax::mk_neg(p)
  assert_true(@logic.BoolSyntax::is_neg(neg))
  assert_true(@logic.BoolSyntax::dest_neg(neg) == p)
}

///|
test "BoolSyntax: quantifiers are applied to abstractions" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let bool_ty = @types.bool_ty()
  let x = @terms.mk_var("x", bool_ty)
  let p = @terms.mk_var("p", bool_ty)

  // forall x. x ==> p  is  App(forall_inst, Abs(x, x ==> p))
  let body = @logic.BoolSyntax::mk_imp(x, p)
  let fa = @logic.BoolSyntax::mk_forall(x, body)
  assert_true(fa is App(_, _))
  assert_true(fa.type_of() == bool_ty)

  // exist x. x ==> p
  let ex = @logic.BoolSyntax::mk_exists(x, body)
  assert_true(ex is App(_, _))
}

#Equal (Derived Equality Rules)

///|
test "Equal: sym and trans" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let x = @terms.mk_var("x", a)
  let y = @terms.mk_var("y", a)
  let z = @terms.mk_var("z", a)

  // x = y |- x = y
  let th_xy = @logic.Kernel::assume_(@terms.Term::mk_eq(x, y))

  // sym: x = y |- y = x
  let sym_th = @logic.Equal::sym(th_xy)
  let (lhs, rhs) = @terms.Term::dest_eq(sym_th.concl)
  assert_true(lhs == y)
  assert_true(rhs == x)

  // trans: {x = y, y = z} |- x = z
  let th_yz = @logic.Kernel::assume_(@terms.Term::mk_eq(y, z))
  let trans_th = @logic.Equal::trans(th_xy, th_yz)
  let (tl, tr) = @terms.Term::dest_eq(trans_th.concl)
  assert_true(tl == x)
  assert_true(tr == z)
}

///|
test "Equal: alpha produces a theorem from alpha-convertible terms" {
  @types.Type::reset_table()
  @terms.Term::reset_table()
  let a = @types.mk_var("'a")
  let x = @terms.mk_var("x", a)
  let y = @terms.mk_var("y", a)

  // \x. x  and  \y. y  are alpha-equivalent
  let t1 = @terms.Term::mk_abs(x, x)
  let t2 = @terms.Term::mk_abs(y, y)

  // |- (\x. x) = (\y. y)
  let th = @logic.Equal::alpha(t1, t2)
  assert_eq(th.hyps.length(), 0)
  assert_true(@terms.Term::is_eq(th.concl))
}