Subset.v

(**
This file is part of the Elfic library

Copyright (C) Boldo, Clément, Faissole, Martin, Mayero

This library is free software; you can redistribute it and/or
modify it under the terms of the GNU Lesser General Public
License as published by the Free Software Foundation; either
version 3 of the License, or (at your option) any later version.

This library is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
COPYING file for more details.
*)

(** Operations on subsets (definitions and properties).

  Subsets of the type U are represented by their belonging function,
  of type U -> Prop.

  Most of the properties are tautologies that can be found on Wikipedia:
  https://en.wikipedia.org/wiki/List_of_set_identities_and_relations *)

From Coq Require Import Classical.
From Coq Require Import PropExtensionality FunctionalExtensionality.


Section Base_Def1.

Context {U : Type}. (* Universe. *)

(** Nullary constructors of subsets. *)

Definition emptyset : U -> Prop := fun _ => False.
Definition fullset : U -> Prop := fun _ => True.

(** Unary constructor of subsets. *)

Variable a : U. (* Element. *)

Definition singleton : U -> Prop := fun x => x = a.

(** Unary predicates on subsets. *)

Variable A : U -> Prop. (* Subset. *)

Definition empty : Prop := forall x, A x -> False.
Definition full : Prop := forall x, A x.

(** Unary operation on subsets. *)

Definition compl : U -> Prop := fun x => ~ A x.

(** Binary predicates on subsets. *)

Variable B : U -> Prop. (* Subset. *)

Definition incl : Prop := forall x, A x -> B x.
Definition same : Prop := forall x, A x <-> B x.

Definition disj : Prop :=forall x, A x -> B x -> False.

(** Binary operations on subsets. *)

Definition union : U -> Prop := fun x => A x \/ B x.
Definition inter : U -> Prop := fun x => A x /\ B x.

End Base_Def1.


Section Base_Def2.

Context {U : Type}. (* Universe. *)

(** Sesquary operation on subsets. *)

Variable A : U -> Prop. (* Subset. *)
Variable a : U. (* Element. *)

Definition add : U -> Prop := union A (singleton a).

(** More binary operation on subsets. *)

Variable B : U -> Prop. (* Subset. *)

Definition diff : U -> Prop := inter A (compl B).

(** Ternary predicate on subsets. *)

Variable C : U -> Prop. (* Subset. *)

Definition partition : Prop := A = union B C /\ disj B C.

End Base_Def2.


Section Base_Def3.

Context {U : Type}. (* Universe. *)

(** Binary constructor of subsets. *)

Variable a b : U. (* Elements. *)

Definition pair : U -> Prop := add (singleton a) b.

(** More binary operation on subsets. *)

Variable A B : U -> Prop. (* Subsets. *)

Definition sym_diff : U -> Prop := union (diff A B) (diff B A).

End Base_Def3.


Section Base_Def4.

Context {U1 U2 : Type}. (* Universes. *)

Variable A1 : U1 -> Prop. (* Subset. *)
Variable A2 : U2 -> Prop. (* Subset. *)

Definition prod : U1 * U2 -> Prop :=
  inter (fun x => A1 (fst x)) (fun x => A2 (snd x)).

Definition swap : forall {U : Type}, (U1 * U2 -> U) -> U2 * U1 -> U :=
  fun U f x => f (snd x, fst x).

End Base_Def4.


Ltac subset_unfold :=
  unfold partition, disj, same, incl, full, empty, (* Predicates. *)
      pair,
      swap, prod, sym_diff, diff, add, inter, union, compl, (* Operators. *)
      singleton, fullset, emptyset. (* Constructors. *)

Ltac subset_auto :=
  subset_unfold; try tauto; try easy.


Section Prop_Facts.

Context {U : Type}. (* Universe. *)

(** Extensionality of subsets. *)

Lemma subset_ext :
  forall (A B : U -> Prop),
    same A B -> A = B.
Proof.
intros.
apply functional_extensionality;
    intros x; now apply propositional_extensionality.
Qed.

Lemma subset_ext_equiv :
  forall (A B : U -> Prop),
    A = B <-> incl A B /\ incl B A.
Proof.
intros; split.
intros H; split; now rewrite H.
intros [H1 H2]; apply subset_ext; split; [apply H1 | apply H2].
Qed.

(** Facts about emptyset and fullset. *)

Lemma empty_emptyset :
  forall (A : U -> Prop),
    empty A <-> A = emptyset.
Proof.
intros; split; intros H.
intros; apply subset_ext; intros x; split; try easy; intros; now apply (H x).
now rewrite H.
Qed.

Lemma full_fullset :
  forall (A : U -> Prop),
    full A <-> A = fullset.
Proof.
intros; split; intros H.
now apply subset_ext.
now rewrite H.
Qed.

(** Facts about singleton. *)

Lemma singleton_in :
  forall a : U, singleton a a.
Proof.
subset_auto.
Qed.

Lemma singleton_out :
  forall a x : U, x <> a -> compl (singleton a) x.
Proof.
subset_auto.
Qed.