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

import Base

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

/*
  The Deduce parser translates
  ∅
  into
  char_fun(λx{false})
*/

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

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

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

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

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
  definition {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
  definition {operator ∈, single, rep}
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)
  definition rep
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 definition {operator∪, operator∈} and replace rep_char_fun<T>
  cases prem
  case xA: x ∈ A {
    conclude rep(A)(x) by definition operator∈ in xA
  }
  case xB: x ∈ B {
    conclude rep(B)(x) by definition 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>
  definition {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 .
  suffices char_fun(fun x:T{(rep(A)(x) or rep(∅ : Set<T>)(x))}) = A  by definition operator ∪
  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 definition rep
      rewrite eq
    }
  }
end

theorem empty_union: all T:type. all A:Set<T>.
  @char_fun<T>(λx{false}) ∪ 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 definition operator ∪
  switch A {
    case char_fun(f) {
      suffices char_fun(λx{f(x)} : fn T->bool) = char_fun(f)  by definition rep
      have eq: (λx{f(x)} : fn T->bool) = f  by extensionality arbitrary x:T.
      rewrite 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 definition 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 definition rep
	  have fg_gf: (λx{(f(x) or g(x))} : fn T->bool) = λx{(g(x) or f(x))}
	    by extensionality arbitrary x:T 
	       rewrite or_sym[f(x),g(x)]
	  rewrite 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>
  definition {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 definition {operator ∈, operator ∪} and replace rep_char_fun<T>
  definition 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 definition 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 definition {operator ∈, rep} in
                     rewrite A_f | B_g in
                     (conjunct 0 of prem)[x]
               have gx_to_fx: if g(x) then f(x)
                  by definition {operator ∈, rep} in
                     rewrite A_f | B_g in
                     (conjunct 1 of prem)[x]
               apply iff_equal[f(x),g(x)]
               to fx_to_gx, gx_to_fx
          rewrite f_g
	}
      }
    }
  }
end