/*
Represent sets as predicates, that is, functions to bool.
*/

import Base

opaque union Set<T> {
  char_fun(fn (T) -> bool)
}

opaque fun rep<T>(S : Set<T>) {
  switch S {
    case char_fun(f) { f }
  }
}

opaque fun set_of_pred<T>(f : fn T -> bool) {
  char_fun(f)
}

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

opaque fun empty_set<T>() {
  char_fun(λx:T{false})
}

opaque fun single<V>(x : V) {
  char_fun(fun y:V {x = y})
}

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

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

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

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

theorem single_member: <T> all x:T.  x ∈ single(x)
proof
  arbitrary T:type
  arbitrary x:T
  expand single | operator ∈ | rep.
end

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

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

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

theorem empty_no_members: all T:type. all x:T.
  not (x ∈ ∅)
proof
  arbitrary T:type
  arbitrary x:T
  suppose x_in_empty: x ∈ ∅
  evaluate in x_in_empty
end

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

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

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
  
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

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

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

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

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

// Testing alternative asci symbols
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

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

// testing alternate syntax for ∅
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

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

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

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

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 ∪
    replace rep_char_fun<T>.
  }
  expand operator ∈ in x_A
end

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

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

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