SET EQUALITY

-type defines propositional equality between sets, leveraging the Z3 SMT solver to enforce equivalence of predicates over real numbers, including equations and inequalities. It ensures rigorous set identity in analysis.

In this system, connects type theory to classical mathematics by reducing set equality to logical equivalence, validated mechanically via Z3.

Formation

(-Formation). Set equality is a proposition asserting that two sets are equal, defined by predicate equivalence.

type exp =
  | SetEq of exp * exp  (* S =s T *)

Introduction

(-Introduction). Equality between sets and is introduced by proving , enforced by Z3.

let set_eq (s : exp) (t : exp) : exp =
  SetEq (s, t)

Elimination

(-Elimination). If , then for any , membership implies , and vice versa, validated by Z3.

let reduce env ctx = function
  | SetEq (Set (Lam (x1, Real, p1)), Set (Lam (x2, Real, p2))) ->
      smt_verify_iff ctx_z3 p1 p2
  | _ -> ...

Computation

(-Computation). The Z3 solver reduces to if is unsatisfiable when negated, otherwise .

let smt_verify_iff ctx p q =
  let solver = Solver.mk_solver ctx None in
  let p_z3 = z3_of_exp ctx p in
  let q_z3 = z3_of_exp ctx q in
  let not_iff = Boolean.mk_not ctx (Boolean.mk_iff ctx p_z3 q_z3) in
  Solver.add solver [not_iff];
  match Solver.check solver [] with
    | Solver.UNSATISFIABLE -> True
    | Solver.SATISFIABLE -> False
    | _ -> failwith "Z3 returned UNKNOWN"

Uniqueness

(-Uniqueness). As a proposition, is 0-truncated; all proofs of equality are equivalent in .

Theorems

(Extensionality). Two sets are equal if and only if their predicates are logically equivalent, as verified by Z3 over real arithmetic.

(Z3 Soundness). If Z3 returns for , then and are equal in the classical sense over .

let test_set_eq_correct =
  let s1 = Set (Lam ("x", Real, RealIneq (Lte, Var "x", One))) in
  let s2 = Set (Lam ("x", Real, Or (RealIneq (Lt, Var "x", One), RealIneq (Eq, Var "x", One)))) in
  SetEq (s1, s2)  (* Z3 proves True *)