SET INTERSECTION

-type constructs the intersection of two sets, forming a set of elements common to both based on the conjunction of their predicates. It is vital for defining measurable sets and refining domains in analysis.

In this system, complements , leveraging and with Z3 verification to ensure precise set operations.

Formation

(-Formation). The intersection of two sets forms a new set containing elements in both and .

type exp =
  | Intersect of exp * exp  (* S ∩ T *)

Introduction

(-Introduction). The intersection of and is introduced as .

let intersect_sets (s : exp) (t : exp) : exp =
  Intersect (s, t)

Elimination

(-Elimination). Membership in holds if an element satisfies both ’s and ’s predicates.

let reduce env ctx = function
  | App (Intersect (Set (Lam (x1, _, p)), Set (Lam (x2, _, q))), a) ->
      And (subst x1 a p, subst x2 a q)
  | _ -> ...

Computation

(-Computation). Applying to an element reduces to a conjunction, verifiable by Z3 for specific predicates.

let infer env ctx (Intersect (s, t)) =
  check env ctx s (Set a); check env ctx t (Set a); Set a

Uniqueness

(-Uniqueness). The intersection is uniquely determined by its predicate, equal to another set if , provable via .

let equal env ctx (Intersect (s1, t1)) (Intersect (s2, t2)) =
  equal env ctx s1 s2 && equal env ctx t1 t2

Theorems

(Associativity). Intersection is associative: , provable by predicate equivalence.

(Measure Subadditivity). For a measure and sets , , reflecting inclusion.

let measure_subadditivity (mu : exp) (s : exp) (t : exp) =
  RealIneq (Lte, App (mu, Intersect (s, t)),
                RealMin (App (mu, s), App (mu, t)))