Require Import Arith.
Require Import List.

(* Type: sets are just lists of natural numbers *)
Definition set := list nat.

(* Value: the empty set *)
Definition empty_set : set := nil.

(* Function: whether two natural numbers are equal *)
Fixpoint nat_eq (a b:nat) {struct a} : bool :=
  match a,b with
  | O,O => true
  | S n, S m => nat_eq n m
  | _,_ => false
  end.

(* Function: set membership: Is "a" within "x" ? *)
Fixpoint set_mem (a:nat) (x:set) {struct x} : bool :=
  match x with
  | nil => false
  | a1 :: x1 =>
     if nat_eq a a1 then true else set_mem a x1
  end.

(* Function: set union is concatenation (we don't worry about duplicates in the set; they'll be ignored) *)
Definition set_union (x y:set) : set := x ++ y.

(* Function: set intersection filters the first set based on membership in the second *)
Fixpoint set_inter (x:set) : set -> set :=
  match x with
  | nil => fun y => nil
  | a1 :: x1 =>
      fun y =>
        if set_mem a1 y then a1 :: set_inter x1 y else set_inter x1 y
  end.

(* Predicate: defines the subset relationship *)
Inductive set_leq : set -> set -> Prop :=
  leq_c : forall (s1 s2:set), 
    (forall x, (set_mem x s1 = true -> set_mem x s2 = true)) -> set_leq s1 s2.

(* Lemma: Subset is reflexive *)
Lemma leq_id : forall s, set_leq s s.
(* XXX prove this *) Admitted. 

(* Lemma: membership in a union implies membership in one half of the union or the other *)
Lemma split_union : forall x s1 s2, 
  set_mem x (set_union s1 s2) = true -> (set_mem x s1 = true \/ set_mem x s2 = true).
(* XXX prove this *) Admitted.

(* Lemma: membership in a set implies membership in a union including that set *)
Lemma join_union : forall x s1 s2,
  set_mem x s1 = true \/ set_mem x s2 = true -> set_mem x (set_union s1 s2) = true.
(* XXX prove this *) Admitted.

(* Lemma: specialization of join_union *)
Lemma mem_union_left : forall x s1 s2,
  set_mem x s1 = true -> set_mem x (set_union s1 s2) = true.
(* XXX prove this using join_union *) Admitted.

(* Lemma: specialization of join_union *)
Lemma mem_union_right : forall x s1 s2,
  set_mem x s2 = true -> set_mem x (set_union s1 s2) = true.
(* XXX prove this using join_union *) Admitted.

(* Lemma: subset is preserved by union (i.e., is monotonic) *)
Lemma leq_union : forall s1 s2 s3 s4, 
  set_leq s1 s2 -> set_leq s3 s4 -> set_leq (set_union s1 s3) (set_union s2 s4).
(* XXX prove this using split_union, mem_union_left, and mem_union_right *) Admitted.

(* Lemma: subset is preserved by intersection (i.e., is monotonic) *)
Lemma leq_inter : forall s1 s2 s3 s4,
  set_leq s1 s2 -> set_leq s3 s4 -> set_leq (set_inter s1 s3) (set_inter s2 s4).
(* XXX prove this.  Try to follow a similar structure as for union. *)  Admitted.

(* The language of set functions *)
Inductive setfun : Set :=
  | f_var : setfun
  | f_const : set -> setfun
  | f_union : setfun -> setfun -> setfun
  | f_inter : setfun -> setfun -> setfun.

(* The semantics of set functions: a function e applied to a set x yields some set *)
Fixpoint evals (e:setfun) (x:set) {struct e} : set :=
  match e with
  | f_var => x
  | f_const s => s
  | f_union s1 s2 => set_union (evals s1 x) (evals s2 x)
  | f_inter s1 s2 => set_inter (evals s1 x) (evals s2 x)
  end.

(* Lemma: set functions are monotonic *)
Lemma evals_mono : forall (e:setfun) (s1 s2:set), set_leq s1 s2 -> set_leq (evals e s1) (evals e s2).
(* Prove this using leq_union, leq_inter, by induction on e *)
  induction e.
Admitted.