(** This module (Toolbox - subsets: relations) defines:
    - subset inclusion:        [SbE] (sub or equal)
    - subset overlap:          [SOv] (subset overlap)  not used in %\cite{SV}%
    - subset equality          [SEq] (subset equal) 
    
    and provides:
    - introduction and elimination rules for [SbE] and [SEq]
    - standard properties (reflexiivity, symmetry, transitivity) for [SbE] and [SEq]

% \hrule %
 
 We require Toolbox basics and the underlying theory.
  
 *)
Require Export tbs_base.

Section Subset_Relations_Definitions.

   Section subset_inclusion_overlap_equality.
   
(** Sub or equal: [(SbE S U V)] means $ U \sub_S V $. *)
      Definition SbE: (S:Set) (S -> Set) -> (S -> Set) -> Set.
      Intros S U V.
      Exact (a:S)(Eps S a U)->(Eps S a V).
      Defined.

(** Subset overlap: [(SOv S U V)] means $ U \meet_S V $ that is $ (\lex a \in S)\ a \e U \land a \e V $. *)
      Definition SOv: (S:Set) (S -> Set) -> (S -> Set) -> Set.
      Intros S U V. 
      Exact (LEx S [a](LAnd (Eps S a U) (Eps S a V))).
      Defined.      
(*
(** Sup or equal: [(SpE S U V)] means $ U \sup_S V $. *)
Definition SpE: (S:Set) (S -> Set) -> (S -> Set) -> Set.
Intros S U V. 
Exact (SbE S V U).
Defined.
*)

(** Subset equal: [(SEq S U V)] means $ U =_S V $. *)   
      Definition SEq: (S:Set) (S -> Set) -> (S -> Set) -> Set.
      Intros S U V. 
      Exact (a:S)(LIff (Eps S a U) (Eps S a V)).
      Defined.

   End subset_inclusion_overlap_equality.
(*   
Section subset_completion.

(** Subset complete: [(SCm S U V)] means $ (\lall a \in S)\ a \e U \lor a \e V $. *)
Definition SCm: (S:Set) (S -> Set) -> (S -> Set) -> Set.
Intros S U V.
Exact (a:S)(LOr (Eps S a U) (Eps S a V)).
Defined.

End subset_completion.
*)
End Subset_Relations_Definitions.

Section Subset_Relations_Results.

   Section subset_inclusion.

(** Sub or equal introduction: $ ((\lall a \in S)\ a \e U \limp a \e V) \limp U \sub V $. *)
      Theorem sbe_i: (S:Set; U,V:S-> Set) ((a:S) (Eps S a U) -> (Eps S a V)) -> (SbE S U V).
      Unfold SbE.      
      Intros.
      MApply '(H a).
      Qed.

(** Sub or equal elimination: $ a \e U \limp U \sub V \limp a \e V $. *)
      Theorem sbe_e: (S:Set; U,V:S -> Set; a:S) (Eps S a U) -> (SbE S U V) -> (Eps S a V).
      Unfold SbE.
      Intros.
      MApply '(H0 a).
      Qed.

(*      
Theorem sbe_i2: (S:Set; U,V:(S -> Set)) ((a:S) (U a) -> (V a)) -> (SbE S U V).
Intros.
MApply 'sbe_i.
MApply 'eps_c1_l.
MApply '(H a).
MApply 'eps_c1_r.
Qed.

Theorem sbe_e2: (S:Set; U,V:(S -> Set); a:S) (U a) -> (SbE S U V) -> (V a).
Intros.
MApply 'eps_c1_r.
MApply '(sbe_e S U).
MApply 'eps_c1_l.
Qed.
*)
(** Sub or equal reflexivity: $ U \sub U $. *) 
      Theorem sbe_r: (S:Set; U:S->Set) (SbE S U U).
      Intros.
      MApply 'sbe_i.
      Qed.

(** Sub or equal transitivity: $ U \sub W \limp W \sub V \limp U \sub V $. *) 
      Theorem sbe_t: (S:Set; W,U,V:S->Set) (SbE S U W) -> (SbE S W V) -> (SbE S U V).
      Intros.
      MApply 'sbe_i.
      MApply '(sbe_e S W).
      MApply '(sbe_e S U).
      Qed.
      
   End subset_inclusion.

   Section stop_sbot_sing_inclusion.

(** Subset top, sub or equal introduction: $ U \sub \stop $. *) 
      Theorem stop_sbe_i: (S:Set; U:S->Set) (SbE S U (STop S)).
      Intros.
      MApply 'sbe_i.
      MApply 'stop_eps_i.
      Qed.

(** Subset bottom, sub or equal introduction: $ \sbot \sub U $. *)
      Theorem sbot_sbe_i: (S:Set; U:S->Set) (SbE S (SBot S) U).
      Intros.
      MApply 'sbe_i.
      MCut 'Empty.
      Intros.
      MApply '(sbot_eps_e S a).
      MElim 'H0 'efq.
      Qed.

(** Singleton, sub or equal introduction: $ a \e U \limp \subset{a} \sub U $. *)
      Theorem sing_sbe_i: (S:Set; a:S; U:S->Set) (Eps S a U) -> (SbE S (Sing S a) U).
      Intros.
      MApply 'sbe_i.
      MCut '(Id S a a0).
      MApply 'sing_eps_e.
      MApply '(id_repl S a0 a).
      Qed.

(** Singleton, sub or equal elimination: $ \subset{a} \sub U \limp a \e U $. *)
      Theorem sing_sbe_e: (S:Set; a:S; U:S->Set) (SbE S (Sing S a) U) -> (Eps S a U).
      Intros.
      MApply '(sbe_e S (Sing S a)).
      MApply 'sing_eps_i.
      Qed.

(** Singleton, sub or equal criterion: $ a \e U \liff \subset{a} \sub U $. *)
      Theorem sing_sbe: (S:Set; a:S; U:S->Set) (LIff (Eps S a U) (SbE S (Sing S a) U)).
      Intros.
      MApply 'liff_i.
      MApply 'sing_sbe_i.
      MApply 'sing_sbe_e.
      Qed.

   End stop_sbot_sing_inclusion.
   
   Section subset_equality.

(** Set equal introduction: $ ((\lall a \in S)\ a \e U \limp a \e V) \limp ((\lall a \in S)\ a \e V \limp a \e U) \limp U = V $. *)
      Theorem seq_i: (S:Set; U,V:S->Set) ((a:S) (Eps S a U) -> (Eps S a V)) -> ((a:S) (Eps S a V) -> (Eps S a U)) -> (SEq S U V).
      Unfold SEq.
      Intros.
      MApply 'liff_i.
      MApply '(H a).
      MApply '(H0 a).
      Qed.

(** Set equal elimination 1: $ a \e U \limp U = V \limp a \e V $. *)
      Theorem seq_e1: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (SEq S U V) -> (Eps S a V).
      Unfold SEq.
      Intros.
      MApply '(liff_e1 (Eps S a U)).
      MApply '(H0 a).
      Qed.

(** Set equal elimination 2: $ a \e V \limp U = V \limp a \e U $. *)
      Theorem seq_e2: (S:Set; V,U:(S -> Set); a:S) (Eps S a V) -> (SEq S U V) -> (Eps S a U).
      Unfold SEq.
      Intros.
      MApply '(liff_e2 (Eps S a V)).
      MApply '(H0 a).
      Qed.

(*
Theorem seq_i2: (S:Set; U,V:(S -> Set)) ((a:S) (U a) -> (V a)) -> ((a:S) (V a) -> (U a)) -> (SEq S U V).
Intros.
MApply 'seq_i.
MApply 'eps_c1_l.
MApply '(H a).
MApply 'eps_c1_r.
MApply 'eps_c1_l.
MApply '(H0 a).
MApply 'eps_c1_r.
Qed.
*)
(** Set equal, sub or equal introduction: $ U \sub V \limp V \sub U \limp U = V $. *)
      Theorem seq_sbe_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SbE S V U) -> (SEq S U V).
      Intros.
      MApply 'seq_i.
      MApply '(sbe_e S U).
      MApply '(sbe_e S V).
      Qed.

(** Set equal, sub or equal elimination: $ U = V \limp U \sub V \land V \sub U $. *)
      Theorem seq_sbe_e: (S:Set; U,V:S->Set) (SEq S U V) -> (LAnd (SbE S U V) (SbE S V U)).
      Intros.
      MApply 'land_i.
      MApply 'sbe_i.
      MApply '(seq_e1 S U).
      MApply 'sbe_i.
      MApply '(seq_e2 S V).
      Qed.

(** Set equal, sub or equal criterion: $ U = V \liff U \sub V \land V \sub U $. *)
      Theorem seq_sbe: (S:Set; U,V:S->Set) (LIff (SEq S U V) (LAnd (SbE S U V) (SbE S V U))).
      Intros.
      MApply 'liff_i.
      MApply 'seq_sbe_e.
      MApply 'seq_sbe_i.
      MApply '(land_e2 (SbE S V U)).
      MApply '(land_e1 (SbE S U V)).
      Qed.

(** Subset equal reflexivity: $ U = U $. *) 
      Theorem seq_r: (S:Set; U:S->Set) (SEq S U U).
      Intros.
      MApply 'seq_i.
      Qed.

(** Subset equal transitivity: $ U = W \limp W = V \limp U = V $. *) 
      Theorem seq_t: (S:Set; W,U,V:S->Set) (SEq S U W) -> (SEq S W V) -> (SEq S U V).
      Intros.
      MApply 'seq_i.
      MApply '(seq_e1 S W).
      MApply '(seq_e1 S U).
      MApply '(seq_e2 S W).
      MApply '(seq_e2 S V).
      Qed.

(** Subset equal symmetry: $ U = V \limp V = U $. *) 
      Theorem seq_s: (S:Set; U,V:S-> Set) (SEq S U V) -> (SEq S V U).
      Intros.
      MApply 'seq_i.
      MApply '(seq_e2 S V).
      MApply '(seq_e1 S U).
      Qed.

   End subset_equality.

End Subset_Relations_Results.