/*
  Sets represented extensionally as predicates, that is, functions
  from elements to bool.

  The concrete predicate representation is opaque, so clients reason
  through membership, subset, union, intersection, and extensionality
  lemmas rather than by depending on the representation directly.
*/

import Base

// ============================================================
// Representation
// ============================================================

// A `Set` is represented opaquely by its characteristic predicate.
opaque union Set<T> {
  char_fun(fn (T) -> bool)
}

// Reveal the characteristic predicate inside the implementation.
opaque fun rep<T>(S : Set<T>) {
  switch S {
    case char_fun(f) { f }
  }
}

// Build a set from a predicate.
opaque fun set_of_pred<T>(f : fn T -> bool) {
  char_fun(f)
}

/*
  The Deduce parser translates
  ∅
  into
  empty_set()
*/

// The empty set — its characteristic predicate is constantly `false`.
opaque fun empty_set<T>() {
  char_fun(λx:T{false})
}

// Singleton set containing exactly `x`.
opaque fun single<V>(x : V) {
  char_fun(fun y:V {x = y})
}

// Set union.
opaque fun operator ∪ <E>(P: Set<E>, Q: Set<E>) {
  char_fun(fun x:E { rep(P)(x) or rep(Q)(x) })
}

// Set intersection.
opaque fun operator ∩ <T>(P : Set<T>, Q : Set<T>) {
  char_fun(fun x:T { rep(P)(x) and rep(Q)(x) })
}

// Membership.
opaque fun operator ∈ <T>(x : T, S : Set<T>) {
  rep(S)(x)
}

// Subset relation.
fun operator ⊆ <T>(P : Set<T>, Q : Set<T>) {
  all x:T. if x ∈ P then x ∈ Q
}

// ============================================================
// Singleton membership
// ============================================================

// `x` is a member of the singleton containing `x`.
theorem single_member: <T> all x:T.  x ∈ single(x)
proof
  arbitrary T:type
  arbitrary x:T
  expand single | operator ∈ | rep.
end

// Membership in `single(x)` forces equality with `x`.
theorem single_equal: all T:type. all x:T, y:T.
    if y ∈ single(x) then x = y
proof
  arbitrary T:type
  arbitrary x:T, y:T
  suppose y_in_x: y ∈ single(x)
  evaluate in y_in_x
end

// Boolean-equality form: `y ∈ single(x)` is `x = y`.
theorem single_equal_equal: all T:type. all x:T, y:T.
    (y ∈ single(x)) = (x = y)
proof
  arbitrary T:type
  arbitrary x:T, y:T
  expand operator ∈ | single | rep.
end

// `single(x)` is the set built from the equality predicate `λy. x = y`.
theorem single_pred: all T:type. all x:T.
  set_of_pred(fun y:T { x = y}) = single(x)
proof
  arbitrary T:type
  arbitrary x:T
  evaluate
end

// ============================================================
// Empty set
// ============================================================

// Nothing is a member of the empty set.
theorem empty_no_members: all T:type. all x:T.
  not (x ∈ ∅)
proof
  arbitrary T:type, x:T
  suppose x_in_empty: x ∈ ∅
  evaluate in x_in_empty
end

// Boolean form: membership in `∅` simplifies to `false`. Registered `auto`.
theorem empty_member_false: all T:type. all x:T.
  (x ∈ ∅) = false
proof
  arbitrary T:type, x:T
  apply eq_false to empty_no_members<T>[x]
end

auto empty_member_false

// ============================================================
// `rep` and `set_of_pred` laws
// ============================================================

// `rep` is the left inverse of the `char_fun` constructor.
theorem rep_char_fun: all T:type, f: fn T -> bool. rep(char_fun(f)) = f
proof
  arbitrary T:type, f:(fn T -> bool)
  expand rep.
end

// `rep` recovers the predicate that was wrapped by `set_of_pred`.
theorem rep_set_of_pred: all T:type, f: fn T -> bool. rep(set_of_pred(f)) = f
proof
  arbitrary T:type, f:(fn T -> bool)
  evaluate
end

// `set_of_pred` is injective — equal sets come from equal predicates.
theorem set_of_pred_equal_fwd: all T:type, f: fn T -> bool, g:fn T -> bool.
  if set_of_pred(f) = set_of_pred(g) then f = g
proof  
  arbitrary T:type, f:(fn T -> bool), g:(fn T -> bool)
  expand set_of_pred
  assume prem
  injective char_fun
  prem
end
  
// Converse: `set_of_pred` is a function — equal predicates yield equal sets.
theorem set_of_pred_equal_bkwd: all T:type, f: fn T -> bool, g:fn T -> bool.
  if f = g then set_of_pred(f) = set_of_pred(g)
proof
  arbitrary T:type, f:(fn T -> bool), g:(fn T -> bool)
  assume: f = g
  replace (recall f = g).
end

// Both directions together — `set_of_pred(f) = set_of_pred(g)` iff `f = g`.
theorem set_of_pred_equal: all T:type, f: fn T -> bool, g:fn T -> bool.
  set_of_pred(f) = set_of_pred(g) ⇔ f = g
proof
  arbitrary T:type, f:(fn T -> bool), g:(fn T -> bool)
  set_of_pred_equal_fwd<T>, set_of_pred_equal_bkwd<T>
end

// Membership in `set_of_pred(f)` reduces to `f(x)`.
theorem member_set_of_pred: all T:type, x:T, f: fn T -> bool.
  if x ∈ set_of_pred(f) then f(x)
proof
  arbitrary T:type, x:T, f:(fn T -> bool)
  evaluate
end

// Union of two `set_of_pred` sets is the `set_of_pred` of the disjunction.
theorem union_set_of_pred: all T:type, f: fn T -> bool, g:fn T -> bool.
  set_of_pred(f) ∪ set_of_pred(g) = set_of_pred(fun x { f(x) or g(x) })
proof
  arbitrary T:type, f:(fn T -> bool), g:(fn T -> bool)
  expand set_of_pred | operator∪
  evaluate
end

// ============================================================
// Union
// ============================================================

// Introduction rule — `x ∈ A` or `x ∈ B` implies `x ∈ A ∪ B`.
theorem union_member: all T:type. all x:T, A:Set<T>, B:Set<T>.
  if x ∈ A or x ∈ B
  then x ∈ (A ∪ B)
proof
  arbitrary T:type
  arbitrary x:T, A:Set<T>, B:Set<T>
  suppose prem: x ∈ A or x ∈ B
  suffices rep(A)(x) or rep(B)(x) by {
    expand operator∪ | operator∈
    replace rep_char_fun<T>.
  }
  cases prem
  case xA: x ∈ A {
    conclude rep(A)(x) by expand operator∈ in xA
  }
  case xB: x ∈ B {
    conclude rep(B)(x) by expand operator∈ in xB
  }
end

// Elimination rule — `x ∈ A ∪ B` implies `x ∈ A or x ∈ B`.
// Also exercises the ASCII syntax (`in`, `|`) for the same operators.
theorem member_union: all T:type. all x:T, A:Set<T>, B:Set<T>.
  if x in (A | B)
  then x in A or x in B
proof
  arbitrary T:type
  arbitrary x:T, A:Set<T>, B:Set<T>
  suppose x_AB: x in (A | B)
  suffices __ by evaluate
  evaluate in x_AB
end

// Boolean-equality form combining the intro and elim rules. Registered `auto`.
theorem member_union_equal: all T:type. all x:T, A:Set<T>, B:Set<T>.
  x ∈ (A ∪ B) = (x ∈ A or x ∈ B)
proof
  arbitrary T:type
  arbitrary x:T, A:Set<T>, B:Set<T>
  expand operator∈ | operator∪ | rep.
end

// `∅` is the right identity for union. Also exercises the `.0.` ASCII form for `∅`.
// Registered `auto`.
theorem union_empty: all T:type. all A:Set<T>.
  A ∪ .0. = A
proof
  arbitrary T:type
  arbitrary A:Set<T>
  suffices A ∪ @char_fun<T>(λ_{false}) = A   by evaluate
  suffices char_fun(fun x:T{(rep(A)(x) or rep(∅ : Set<T>)(x))}) = A
    by evaluate
  switch A {
    case char_fun(f) {
      have eq: (λy{f(y)} : fn T->bool) = f   by extensionality arbitrary x:T.
      suffices char_fun(λx{f(x)} : fn T->bool) = char_fun(f)   by evaluate
      replace eq.
    }
  }
end

auto union_empty

// `∅` is also the left identity for union. Registered `auto`.
theorem empty_union: all T:type. all A:Set<T>.
  @empty_set<T>() ∪ A = A
proof
  arbitrary T:type
  arbitrary A:Set<T>
  suffices char_fun(fun x:T{(rep(∅ : Set<T>)(x) or rep(A)(x))}) = A
    by evaluate
  switch A {
    case char_fun(f) {
      suffices char_fun(λx{f(x)} : fn T->bool) = char_fun(f)  by evaluate
      have eq: (λx{f(x)} : fn T->bool) = f  by extensionality arbitrary x:T.
      replace eq.
    }
  }
end

auto empty_union

// Union is commutative.
theorem union_sym: all T:type. all A:Set<T>, B:Set<T>.
  A ∪ B = B ∪ A
proof
  arbitrary T:type
  arbitrary A:Set<T>, B:Set<T>
  suffices @char_fun<T>(λx{(rep(A)(x) or rep(B)(x))})
             = char_fun(λx{(rep(B)(x) or rep(A)(x))})
    by expand operator ∪.
  switch A {
    case char_fun(f) {
      switch B {
        case char_fun(g) {
          suffices @char_fun<T>(λx{(f(x) or g(x))}) = char_fun(λx{(g(x) or f(x))})
            by expand rep.
          have fg_gf: (λx{(f(x) or g(x))} : fn T->bool) = λx{(g(x) or f(x))}
            by extensionality arbitrary x:T 
          replace or_sym[f(x),g(x)].
          replace fg_gf.
        }
      }
    }
  }
end

// Union is associative — also registered below via `associative operator ∪`.
theorem union_assoc: all T:type. all A:Set<T>, B:Set<T>, C:Set<T>.
  (A ∪ B) ∪ C = A ∪ (B ∪ C)
proof
  arbitrary T:type
  arbitrary A:Set<T>, B:Set<T>, C:Set<T>
  expand operator ∪ | rep.
end

associative operator ∪ <T> in Set<T>

// `x ∈ A` lifts to `x ∈ A ∪ B` for any `B`.
theorem in_left_union:
  all T:type. all B:Set<T>. all x:T, A: Set<T>.
  if x ∈ A then x ∈ (A ∪ B)
proof
  arbitrary T:type
  arbitrary B:Set<T>
  arbitrary x:T, A: Set<T>
  suppose x_A: x ∈ A
  suffices rep(A)(x) or rep(B)(x) by {
    expand operator ∈ | operator∪ | rep.
  }
  expand operator ∈ in x_A
end

// `x ∈ B` lifts to `x ∈ A ∪ B` for any `A`.
theorem in_right_union:
  all T:type. all A: Set<T>. all x:T, B:Set<T>.
  if x ∈ B then x ∈ (A ∪ B)
proof
  arbitrary T:type
  arbitrary A: Set<T>
  arbitrary x:T, B:Set<T>
  suppose x_B: x ∈ B
  conclude x ∈ A ∪ B   by apply union_member<T>[x,A,B] to x_B
end

// ============================================================
// Subset and set equality
// ============================================================

// Antisymmetry of `⊆` — two-way containment implies set equality.
theorem subset_equal:
  all T:type. all A:Set<T>, B:Set<T>.
  if A ⊆ B and B ⊆ A
  then A = B
proof
  suffices all T:type. all A:Set<T>, B:Set<T>.
    if (all x:T. (if x ∈ A then x ∈ B)) and (all x:T. (if x ∈ B then x ∈ A))
    then A = B
        by expand operator⊆.
  arbitrary U:type
  arbitrary A:Set<U>, B:Set<U>
  suppose prem
  switch A {
    case char_fun(f) suppose A_f {
      switch B {
        case char_fun(g) suppose B_g {
          have f_g: f = g by {
            extensionality
            arbitrary x:U
            have fx_to_gx: if f(x) then g(x) by {
              expand operator ∈ | rep in
              replace A_f | B_g in
              (conjunct 0 of prem)[x]
            }
            have gx_to_fx: if g(x) then f(x) by {
              expand operator ∈ | rep in
              replace A_f | B_g in
              (conjunct 1 of prem)[x]
            }
            apply iff_equal[f(x),g(x)]
            to fx_to_gx, gx_to_fx
          }
          replace f_g.
        }
      }
    }
  }
end

// Extensionality — sets with the same members are equal.
theorem member_equal: all T:type, A:Set<T>, B:Set<T>.
  if (all x:T. x ∈ A ⇔ x ∈ B) then A = B
proof
  arbitrary T:type, A:Set<T>, B:Set<T>
  assume prem
  suffices A ⊆ B and B ⊆ A by subset_equal
  have fwd: A ⊆ B by {
    expand operator⊆
    prem
  }
  have bkwd: B ⊆ A by {
    expand operator⊆
    prem
  }
  fwd, bkwd
end


// ============================================================
// Singleton ≠ empty
// ============================================================

// A singleton is never empty. Registered `auto`.
theorem single_empty_false: all T:type, x:T. (single(x) = ∅) = false
proof
  arbitrary T:type, x:T
  suffices not (single(x) = ∅) by eq_false [single(x) = ∅]
  assume eq
  have xx: x ∈ single(x) by single_member
  have xmt: x ∈ ∅ by replace eq in xx
  xmt
end

auto single_empty_false

auto single_equal_equal

// `single(x) ∪ S` always contains `x`, so it cannot be empty. Registered `auto`.
theorem single_union_empty_false: all T:type, x:T, S:Set<T>. (single(x) ∪ S = ∅) = false
proof
  arbitrary T:type, x:T, S:Set<T>
  suffices not (single(x) ∪ S = ∅) by eq_false [single(x) ∪ S = ∅]
  assume eq
  have x_x: x ∈ single(x) by single_member
  have x_xS: x ∈ single(x) ∪ S by replace member_union_equal x_x
  have xmt: x ∈ ∅ by replace eq in x_xS
  xmt
end

auto single_union_empty_false

// Mirror of `single_union_empty_false` with the singleton on the right. Registered `auto`.
theorem union_single_empty_false: all T:type, x:T, S:Set<T>. (S ∪ single(x) = ∅) = false
proof
  arbitrary T:type, x:T, S:Set<T>
  replace union_sym.
end

auto union_single_empty_false

auto member_union_equal