--- /dev/null
+Toolbox.vo: Toolbox.v st_base.vo st_logic.vo st_nat.vo st_arith.vo Standard.vo xt_fin.vo tbs_base.vo tbs_rel.vo tbs_op.vo tbs_rop.vo tbs_fun.vo tbs_fin.vo
+tbs_fin.vo: tbs_fin.v tbs_fun.vo
+tbs_fun.vo: tbs_fun.v tbs_rop.vo
+tbs_rop.vo: tbs_rop.v tbs_op.vo
+tbs_op.vo: tbs_op.v tbs_rel.vo
+tbs_rel.vo: tbs_rel.v tbs_base.vo
+tbs_base.vo: tbs_base.v xt_fin.vo
+xt_fin.vo: xt_fin.v Standard.vo
+Standard.vo: Standard.v st_base.vo st_logic.vo st_nat.vo st_arith.vo
+st_arith.vo: st_arith.v st_nat.vo
+st_nat.vo: st_nat.v st_logic.vo
+st_logic.vo: st_logic.v st_base.vo
+st_base.vo: st_base.v
--- /dev/null
+# List of vernac files to compile
+st_base.v
+st_logic.v
+st_nat.v
+st_arith.v
+Standard.v
+xt_fin.v
+tbs_base.v
+tbs_rel.v
+tbs_op.v
+tbs_rop.v
+tbs_fun.v
+tbs_fin.v
+Toolbox.v
--- /dev/null
+##############################################################################
+## The Calculus of Inductive Constructions ##
+## ##
+## Projet Coq ##
+## ##
+## INRIA ENS-CNRS ##
+## Rocquencourt Lyon ##
+## ##
+## Coq V7 ##
+## ##
+## ##
+##############################################################################
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+
+#
+# This Makefile was generated by the command line :
+# coq_makefile -f Make -o Makefile
+#
+
+##########################
+# #
+# Variables definitions. #
+# #
+##########################
+
+CAMLP4LIB=`camlp4 -where`
+COQSRC=-I $(COQTOP)/kernel -I $(COQTOP)/lib \
+ -I $(COQTOP)/library -I $(COQTOP)/parsing -I $(COQTOP)/pretyping \
+ -I $(COQTOP)/proofs -I $(COQTOP)/syntax -I $(COQTOP)/tactics \
+ -I $(COQTOP)/toplevel -I $(CAMLP4LIB)
+ZFLAGS=$(OCAMLLIBS) $(COQSRC)
+OPT=
+COQFLAGS=-q $(OPT) $(COQLIBS)
+COQC=$(COQBIN)coqc
+GALLINA=gallina
+COQWEB=coqweb
+CAMLC=ocamlc -c
+CAMLOPTC=ocamlopt -c
+CAMLLINK=ocamlc
+CAMLOPTLINK=ocamlopt
+COQDEP=$(COQBIN)coqdep -c
+COQVO2XML=coq_vo2xml
+
+#########################
+# #
+# Libraries definition. #
+# #
+#########################
+
+OCAMLLIBS=-I .
+COQLIBS=-I .
+
+###################################
+# #
+# Definition of the "all" target. #
+# #
+###################################
+
+VFILES=st_base.v\
+ st_logic.v\
+ st_nat.v\
+ st_arith.v\
+ Standard.v\
+ xt_fin.v\
+ tbs_base.v\
+ tbs_rel.v\
+ tbs_op.v\
+ tbs_rop.v\
+ tbs_fun.v\
+ tbs_fin.v\
+ Toolbox.v
+VOFILES=$(VFILES:.v=.vo)
+VIFILES=$(VFILES:.v=.vi)
+GFILES=$(VFILES:.v=.g)
+HTMLFILES=$(VFILES:.v=.html)
+GHTMLFILES=$(VFILES:.v=.g.html)
+
+all: st_base.vo\
+ st_logic.vo\
+ st_nat.vo\
+ st_arith.vo\
+ Standard.vo\
+ xt_fin.vo\
+ tbs_base.vo\
+ tbs_rel.vo\
+ tbs_op.vo\
+ tbs_rop.vo\
+ tbs_fun.vo\
+ tbs_fin.vo\
+ Toolbox.vo
+
+spec: $(VIFILES)
+
+gallina: $(GFILES)
+
+html: $(HTMLFILES)
+
+gallinahtml: $(GHTMLFILES)
+
+all.ps: $(VFILES)
+ $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`
+
+all-gal.ps: $(GFILES)
+ $(COQWEB) -ps -o $@ `$(COQDEP) -sort -suffix .g $(VFILES)`
+
+xml:: .xml_time_stamp
+.xml_time_stamp: st_base.vo\
+ st_logic.vo\
+ st_nat.vo\
+ st_arith.vo\
+ Standard.vo\
+ xt_fin.vo\
+ tbs_base.vo\
+ tbs_rel.vo\
+ tbs_op.vo\
+ tbs_rop.vo\
+ tbs_fun.vo\
+ tbs_fin.vo\
+ Toolbox.vo
+ $(COQVO2XML) $(COQFLAGS) $(?:%.o=%)
+ touch .xml_time_stamp
+
+####################
+# #
+# Special targets. #
+# #
+####################
+
+.PHONY: all opt byte archclean clean install depend xml
+
+.SUFFIXES: .v .vo .vi .g .html .tex .g.tex .g.html
+
+.v.vo:
+ $(COQC) $(COQDEBUG) $(COQFLAGS) $*
+
+.v.vi:
+ $(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
+
+.v.g:
+ $(GALLINA) $<
+
+.v.tex:
+ $(COQWEB) $< -o $@
+
+.v.html:
+ $(COQWEB) -html $< -o $@
+
+.g.g.tex:
+ $(COQWEB) $< -o $@
+
+.g.g.html:
+ $(COQWEB) -html $< -o $@
+
+byte:
+ $(MAKE) all "OPT="
+
+opt:
+ $(MAKE) all "OPT=-opt"
+
+include .depend
+
+depend:
+ rm .depend
+ $(COQDEP) -i $(COQLIBS) *.v *.ml *.mli >.depend
+ $(COQDEP) $(COQLIBS) -suffix .html *.v >>.depend
+
+xml::
+
+install:
+ mkdir -p `$(COQC) -where`/user-contrib
+ cp -f *.vo `$(COQC) -where`/user-contrib
+
+Makefile: Make
+ mv -f Makefile Makefile.bak
+ $(COQBIN)coq_makefile -f Make -o Makefile
+
+clean:
+ rm -f *.cmo *.cmi *.cmx *.o *.vo *.vi *.g *~
+ rm -f all.ps all-gal.ps $(HTMLFILES) $(GHTMLFILES)
+
+archclean:
+ rm -f *.cmx *.o
+
+# WARNING
+#
+# This Makefile has been automagically generated by coq_makefile
+# Edit at your own risks !
+#
+# END OF WARNING
+
--- /dev/null
+
+ Contribution Padova/SUBSETS
+ ============================
+
+This directory contains a formalization in Coq of the content of this paper
+describing a theory of subsets on a intuitionistic a predicative foundation:
+
+G.Sambin, S.Valentini:
+Building up a toolbox for Martin-Lof's type theory: subset theory.
+In Proc. of Twenty-five years of constructive type theory,
+Oxford U.P. (1998) pp. 221-244.
+
+Author & Date: Ferruccio Guidi
+ Department of Computer Science, University of Bologna
+ March 2005
+E-mail : fguidi@cs.unibo.it
+WWW : http://www.cs.unibo.it/~fguidi
+
+Installation procedure:
+-----------------------
+
+ To get this contribution compiled, type
+
+ make
+
+ or
+
+ make opt
+
+ The main modules produced by the compilation are:
+
+ Toolbox provides the theory of subsets and its prerequisites
+
+ Base provides just the prerequisites
+
+Description:
+------------
+
+Further information on this contribution:
+-----------------------------------------
+
+ The latest version of this development is maintained in the CVS repository
+ of the HELM project <helm.cs.unibo.it> and can be downloaded at:
+
+ www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/SUBSETS.tgz
--- /dev/null
+Require Export st_base.
+Require Export st_logic.
+Require Export st_nat.
+Require Export st_arith.
+
--- /dev/null
+Require Export st_base.
+Require Export st_logic.
+Require Export st_nat.
+Require Export st_arith.
+Require Export Standard.
+Require Export xt_fin.
+Require Export tbs_base.
+Require Export tbs_rel.
+Require Export tbs_op.
+Require Export tbs_rop.
+Require Export tbs_fun.
+Require Export tbs_fin.
--- /dev/null
+Name: toolbox
+Title: A theory of subsets on an intuitionistic and predicative foundation
+Author: Ferruccio Guidi
+Email: fguidi@cs.unibo.it
+Homepage: http://www.cs.unibo.it/~fguidi
+Institution: Department of Computer Science, University of Bologna
+Address: Mura Anteo Zamboni 7, 40127 Bologna, ITALY
+Date: March 31, 2005
+Description:
+Url:
+Keywords: subsets, toolbox
+Version: 7.3.1
+Require:
--- /dev/null
+Require Export st_nat.
+
+Section Arith_Functions.
+
+ Section head_tail_append.
+
+ Variable S:Set.
+(*
+Definition hd: (List S) -> (List S) := (listrec S [_](List S) (empty ?) [_;_](fr ? (empty ?))).
+*)
+ Definition hde: S -> (List S) -> S := [a](listrec S [_]S a [_;_;a]a).
+
+ Definition tl: (List S) -> (List S) := (listrec S [_](List S) (empty ?) [v;_;_]v).
+
+ Definition app: (List S) -> (List S) -> (List S) := [v](listrec S [_](List S) v [_;p;a](fr S p a)).
+
+ Definition app_three: (List S) -> (List S) -> (List S) -> (List S) := [v,w](app (app v w)).
+(*
+Definition bs_app: (ListS S) -> N -> (List S) := (bs_iter (List S) (empty S) app).
+
+Definition rbs_app: (ListS S)->N->(List S) := (rbs_iter (List S) (empty S) app).
+*)
+ Definition LIn: S -> (List S) -> Set := [a;l](LEx (List S) [v](LEx (List S) [w](Id (List S) (app (fr S v a) w) l))).
+
+ End head_tail_append.
+
+ Section slicing.
+
+ Variable S:Set; n:N; v:(List S).
+
+ Definition lskip: N -> (List S) -> (List S) := (natrec [_](List S)->(List S) [w]w [_;p;w](p (tl ? w))).
+(*
+Definition lfirst: N -> (List S) -> (List S) := (natrec [_](List S)->(List S) [_](empty S) [_;p;w](app ? (p (tl ? w)) (hd ? w))).
+
+Definition lslice: N -> N -> (List S) -> (List S) := [m;n;v](lfirst n (lskip m v)).
+
+Definition lix: N -> (List S) -> (List S) := [n;v](hd S (lskip n v)).
+
+Definition lixe: S -> N -> (List S) -> S := [a;n;v](hde S a (lskip n v)).
+
+Definition llen: (List S) -> N := (listrec S [_]N zero [_;p;_](succ p)).
+*)
+ End slicing.
+
+ Section arithmetic.
+
+ Definition pred: N -> N := (tl One).
+
+ Definition add: N -> N -> N := (app One).
+
+ Definition add_three: N -> N -> N -> N := (app_three One).
+(*
+Definition bs_add: NS -> N -> N := (bs_app One).
+
+Definition rbs_add:NS->N->N := (rbs_app One).
+*)
+ Definition sub: N -> N -> N := [m;n](lskip One n m).
+(*
+Definition sub_t: N -> N -> N -> N := [m,n](sub (sub m n)).
+
+Definition absv: N -> N -> N := [m;n](plus (minus m n) (minus n m)).
+*)
+ End arithmetic.
+
+End Arith_Functions.
+
+Section Arith_Hints.
+
+ Section arith_fold.
+(*
+Theorem bs_app_fold: (n:N; S:Set; ls:(ListS S); P:(List S)->Set) (P (bs_app S ls n)) -> (P (bs_iter (List S) (empty S) (app S) ls n)).
+Intros.
+Assumption.
+Qed.
+*)
+ Theorem pred_fold: (n:N; P:N->Set) (P (pred n)) -> (P (tl One n)).
+ Intros.
+ Assumption.
+ Qed.
+(*
+Theorem add_fold: (m,n:N; P:N->Set) (P (add m n)) -> (P (app One m n)).
+Intros.
+Apply (id_repl N (app One m n) (add m n)).
+Apply id_r.
+Assumption.
+Qed.
+
+Theorem bs_add_fold: (n:N; ns:NS; P:N->Set) (P (bs_add ns n)) -> (P (bs_app One ns n)).
+Intros.
+Assumption.
+Qed.
+*)
+ End arith_fold.
+
+End Arith_Hints.
+
+Section Arith_Results.
+
+ Section head_tail_results.
+
+ Theorem fr_ini1: (S:Set; a,b:S; v,w:(List S)) (Id (List S) (fr S v a) (fr S w b)) -> (Id (List S) v w).
+ Intros.
+ MApply '(id_repl (List S) v (tl S (fr S v a))).
+ MApply '(id_repl (List S) w (tl S (fr S w b))).
+ MApply '(id_comp (List S)).
+ Qed.
+
+ Theorem fr_ini2: (S:Set; v,w:(List S); a,b:S) (Id (List S) (fr S v a) (fr S w b)) -> (Id S a b).
+ Intros.
+ MApply '(id_repl S a (hde S a (fr S v a))).
+ MApply '(id_repl S b (hde S a (fr S w b))).
+ MApply '(id_comp (List S)).
+ Qed.
+(*
+Theorem hd_hde_id: (S:Set; a:S; v:(List S)) (GT (llen S v) zero) -> (Id (List S) (hd S v) (fr S (empty S) (hde S a v))).
+Intros S a v.
+MElim 'v 'listrec.
+MApply '(gt_false zero).
+Qed.
+
+Theorem tl_len: (S:Set; v:(List S)) (Id N (llen S (tl S v)) (pred (llen S v))).
+Intros.
+MElim 'v 'listrec.
+Qed.
+*)
+ Theorem app_empty: (S:Set; v:(List S)) (Id (List S) (app S (empty S) v) v).
+ Intros.
+ MElim 'v 'listrec.
+ MApply '(id_comp (List S) (List S) [v:?](fr S v s)).
+ Qed.
+(*
+Theorem app_ass: (S:Set; u,v,w:(List S)) (Id (List S) (app S (app S u v) w) (app S u (app S v w))).
+Intros.
+MElim 'w 'listrec.
+MApply '(id_comp (List S) (List S) [v:?](fr S v y)).
+Qed.
+*)
+ Theorem lin_i: (S:Set; v,w,l:(List S); a:S) (Id (List S) (app S (fr S v a) w) l) -> (LIn S a l).
+ Intros.
+ Unfold LIn.
+ MApply '(lex_i (List S) v).
+ MApply '(lex_i (List S) w).
+ Qed.
+
+ Theorem lin_e: (S:Set; a:S; l:(List S); P:Set) (LIn S a l) -> ((v,w:(List S)) (Id (List S) (app S (fr S v a) w) l) -> P) -> P.
+ Intros.
+ MElim 'H 'lex_e.
+ MElim 'y 'lex_e.
+ MApply '(H0 a0 a1).
+ Qed.
+
+ Theorem lin_fr_i: (S:Set; a,b:S; l:(List S)) (LOr (LIn S a l) (Id S a b)) -> (LIn S a (fr S l b)).
+ Intros.
+ MElim 'H '(when (LIn S a l) (Id S a b)).
+ MApply '(lin_e S a l).
+ MApply '(id_repl (List S) l (app S (fr S v a) w)).
+ MApply '(lin_i S v (fr S w b)).
+ MApply '(id_repl S b a).
+ MApply '(lin_i S l (empty S)).
+ Qed.
+
+ End head_tail_results.
+(*
+Section slicing_results.
+
+Theorem lskip_empty: (S:Set; n:N) (Id (List S) (lskip S n (empty S)) (empty S)).
+Intros.
+MElim 'n 'natrec.
+Qed.
+
+Theorem lskip_tl: (S:Set; n:N; v:(List S)) (Id (List S) (lskip S n (tl S v)) (tl S (lskip S n v))).
+Intros S n.
+MElim 'n 'natrec.
+MElim 'v 'listrec.
+(MApply '(id_repl ? (lskip S n0 (empty S)) (empty S)); MApply 'id_comm).
+MApply 'lskip_empty.
+MApply '(H l).
+Qed.
+
+Theorem lixe_empty: (n:N; S:Set; a:S) (Id S (lixe S a n (empty S)) a).
+Intros.
+MElim 'n 'natrec.
+Qed.
+
+Theorem lixe_app_v: (S:Set; a,b:S; w,v:(List S); n:N) (GT (llen S v) n) -> (Id S (lixe S a n (app S w v)) (lixe S b n v)).
+Intros S a b w v.
+(Elim v using listrec; MSimpl).
+Intros.
+MApply '(gt_false n).
+Intros l H y n.
+MElim 'n 'natrec.
+(Unfold lixe; Simpl).
+Fold (lixe S a n0 (app S w l)) (lixe S b n0 l). (**)
+MApply '(H n0).
+Qed.
+
+Theorem lixe_le: (S:Set; a:S; v:(List S); n:N) (LE (llen S v) n) -> (Id S (lixe S a n v) a).
+Intros S a v.
+(Elim v using listrec; Simpl).
+Intros n.
+MElim 'n 'natrec.
+MApply 'lixe_empty.
+Intros l H y n.
+MElim 'n 'natrec.
+MApply '(le_false (succ (llen S l))).
+(Unfold lixe; Simpl).
+Fold (lixe S a n0 l). (**)
+MApply '(H n0).
+Qed.
+
+Theorem lslice_lix: (S:Set; k:N; v:(List S)) (Id (List S) (lslice S k one v) (lix S k v)).
+Intros.
+Unfold lslice lfirst.
+MSimpl.
+MApply 'app_empty.
+Qed.
+
+End slicing_results.
+*)
+ Section arithmetics_results.
+
+ Theorem succ_ini: (m,n:N) (Id N (succ m) (succ n)) -> (Id N m n).
+ Intros.
+ MApply '(fr_ini1 One tt tt).
+ Qed.
+
+ Theorem sub_succ: (m,n:N) (LE m n) ->
+ (Id N (sub (succ n) m) (succ (sub n m))).
+ Intros m.
+ Elim m using natrec.
+ Intros.
+ MSimpl.
+ Intros m' H n.
+ MElim 'n 'natrec.
+ MApply '(le_false m').
+ MApply '(H n0).
+ Qed.
+(*
+Theorem succ_pred: (n:N) (GT n zero) -> (Id N (succ (pred n)) n).
+Intros n.
+MElim 'n 'natrec.
+MApply '(gt_false zero).
+Qed.
+*)
+ Theorem add_zero: (n:N) (Id N (add zero n) n).
+ Intros.
+ Unfold N add zero.
+ MApply 'app_empty.
+ Qed.
+(*
+Theorem add_ass: (l,m,n:N) (Id N (add (add l m) n) (add l (add m n))).
+Intros.
+Unfold N add.
+MApply 'app_ass.
+Qed.
+*)
+ Theorem add_succ: (m,n:N) (Id N (add (succ m) n) (succ (add m n))).
+ Intros.
+ (MElim 'n 'natrec; Apply succ_fold). (**)
+ MApply '(id_comp N).
+ Qed.
+
+ Theorem add_comm: (m,n:N) (Id N (add m n) (add n m)).
+ Intros m.
+ MElim 'm 'natrec.
+ MApply 'add_zero.
+ MApply '(id_trans ? (succ (add n n0))).
+ MApply 'add_succ.
+ Apply succ_fold. (**)
+ MApply '(id_comp N).
+ MApply '(H n0).
+ Qed.
+(*
+Theorem add_pred: (n,m:N) (GT n zero) -> (Id N (succ (add (pred n) m)) (add n m)).
+Intros n m.
+MElim 'm 'natrec.
+MApply 'succ_pred.
+(Apply succ_fold; Apply succ_fold). (**)
+MApply '(id_comp N).
+MApply 'H.
+Qed.
+*)
+ Theorem le_comp_pred: (m,n:N) (LE m n) -> (LE (pred m) (pred n)).
+ Intros m.
+ Elim m using natrec.
+ Intros.
+ MApply 'le_wf.
+ Intros m' H n.
+ MElim 'n 'natrec.
+ MApply '(le_false m').
+ Qed.
+
+ Theorem le_add: (m,n:N) (LE m (add m n)).
+ Intros.
+ MElim 'n 'natrec.
+ MApply 'le_r.
+ MApply '(le_trans (add m n0)).
+ Apply succ_fold. (**)
+ MApply 'le_succ.
+ Qed.
+
+ Theorem le_comp_add: (m1,m2,n:N) (LE m1 m2) -> (LE (add m1 n) (add m2 n)).
+ Intros m1 m2 n.
+ MElim 'n 'natrec.
+ (Apply succ_fold; Apply succ_fold). (**)
+ MApply 'le_comp_succ.
+ MApply 'H.
+ Qed.
+
+ Theorem le_comp_add2: (m,n1,n2:N) (LE n1 n2) -> (LE (add m n1) (add m n2)).
+ Intros.
+ MApply '(id_repl N (add m n1) (add n1 m)).
+ MApply 'add_comm.
+ MApply '(id_repl N (add m n2) (add n2 m)).
+ MApply 'add_comm.
+ MApply 'le_comp_add.
+ Qed.
+
+ Theorem gt_comp_add2: (m,n1,n2:N) (GT n1 n2) -> (GT (add m n1) (add m n2)).
+ Intros.
+ MApply 'le_gt.
+ MApply '(id_repl N (succ (add m n2)) (add m (succ n2))).
+ MApply 'le_comp_add2.
+ MApply 'gt_le.
+ Qed.
+
+ Theorem le_comp_sub: (n,m1,m2:N) (LE m1 m2) -> (LE (sub m1 n) (sub m2 n)).
+ Intros n.
+ MElim 'n 'natrec.
+ MApply '(H (pred m1) (pred m2)).
+ MApply 'le_comp_pred.
+ Qed.
+
+ Theorem gt_comp_sub: (m1,m2,n:N) (LE n m2) -> (GT m1 m2) -> (GT (sub m1 n) (sub m2 n)).
+ Intros.
+ MApply 'le_gt.
+ MApply '(id_repl N (succ (sub m2 n)) (sub (succ m2) n)).
+ MApply 'sub_succ.
+ MApply 'le_comp_sub.
+ MApply gt_le.
+ Qed.
+(*
+Theorem le_zero_add: (m,n:N) (LE (add n m) zero) -> (Id N n zero).
+Intros.
+MApply 'le_zero.
+MApply '(le_trans (add n m)).
+MApply 'le_add.
+Qed.
+
+Theorem sub_pred_l: (n,m:N) (Id N (sub (pred m) n) (pred (sub m n))).
+Intros.
+Unfold N sub pred.
+MApply 'lskip_tl.
+Qed.
+*)
+ Theorem sub_zero: (n,m:N) (LE m n) -> (Id N (sub m n) zero).
+ Intros n.
+ Elim n using natrec.
+ Intros.
+ MSimpl.
+ MApply 'le_zero.
+ Intros n' H m.
+ Elim m using natrec.
+ Intros.
+ MSimpl.
+ MApply '(H zero).
+ Intros m' H1 H2.
+ MSimpl.
+ MApply '(H m').
+ Qed.
+
+ Theorem succ_pred_e: (m,n:N) (Id N m (succ n)) -> (Id N (pred m) n).
+ Intros m.
+ Elim m using natrec.
+ Intros.
+ MApply '(n_false n).
+ Intros m' H n H2.
+ MSimpl.
+ MApply 'succ_ini.
+ Qed.
+
+ Theorem add_sub_e: (n,m2,m1:N) (Id N m1 (add m2 n)) -> (Id N (sub m1 m2) n).
+ Intros n.
+ Elim n using natrec.
+ MSimpl.
+ Intros.
+ MApply 'sub_zero.
+ MApply '(id_repl N m2 m1).
+ MApply 'le_r.
+ Intros n' H m2.
+ Elim m2 using natrec.
+ Intros.
+ MSimpl.
+ MApply '(id_repl N (succ n') (add zero (succ n'))).
+ MApply 'add_zero.
+ Intros m2' H1 m1 H2.
+ MSimpl.
+ MApply 'pred_fold. (**)
+ MApply '(H1 (pred m1)).
+ Simpl in H2.
+ Fold (succ (add (succ m2') n')) in H2. (**)
+ MApply '(id_repl N (add m2' (succ n')) (add (succ m2') n')).
+ MApply '(add_succ m2' n').
+ MApply 'succ_pred_e.
+ Qed.
+
+ Theorem sub_add: (m,n:N) (Id N (sub (add m n) n) m).
+ Intros.
+ MApply 'add_sub_e.
+ MApply 'add_comm.
+ Qed.
+
+ Theorem gt_add_di: (a,m,n:N) (GT (add m n) a) ->
+ (LOr (GT m a) (GT n (sub a m))).
+ Intros.
+ MApply '(lor_e (LE m a) (GT m a)).
+ MCut '(GT n (sub a m)).
+ MApply '(id_repl N n (sub (add n m) m)).
+ MApply 'sub_add.
+ MApply 'gt_comp_sub.
+ MApply '(id_repl N (add n m) (add m n)).
+ MApply 'add_comm.
+ MApply 'in_r.
+ MApply 'in_l.
+ MApply 'le_di.
+ Qed.
+(*
+Theorem app_llen: (S:Set; w,v:(List S)) (Id N (llen S (app S w v)) (add (llen S w) (llen S v))).
+Intros.
+MElim 'v 'listrec.
+Apply succ_fold. (**)
+MApply '(id_comp N).
+Qed.
+
+Theorem bsapp_llen: (S:Set; vs:N->(List S); n:N) (Id N (llen S (bs_app S vs n)) (bs_add [n](llen S (vs n)) n)).
+Intros.
+MElim 'n 'natrec.
+MApply '(id_repl ? (bs_add [n:N](llen S (vs n)) n0) (llen S (bs_app S vs n0))).
+MApply 'app_llen.
+Qed.
+
+Theorem rbsapp_llen: (S:Set; vs:N->(List S); n:N) (Id N (llen S (rbs_app S vs n)) (rbs_add [n](llen S (vs n)) n)).
+Intros.
+Unfold rbs_add rbs_app rbs_iter.
+Apply bs_app_fold.
+Apply bs_app_fold.
+Apply bs_add_fold. (**)
+MApply 'bsapp_llen.
+Qed.
+
+Theorem lskip_llen: (S:Set; v:(List S); n:N) (Id N (llen S (lskip S n v)) (sub (llen S v) n)).
+Intros.
+MElim 'n 'natrec.
+Fold (pred (llen S v)). (**)
+MApply '(id_trans ? (pred (llen S (lskip S n0 v)))).
+MApply '(id_repl ? (lskip S n0 (tl S v)) (tl S (lskip S n0 v))).
+(MApply 'id_comm; MApply 'lskip_tl).
+MApply 'tl_len.
+MApply '(id_trans ? (pred (sub (llen S v) n0))).
+MApply '(id_comp N).
+(MApply 'id_comm; MApply 'sub_pred_l).
+Qed.
+
+Theorem lskip_le: (S:Set; v:(List S); n:N) (LE (llen S v) n) -> (Id N (llen S (lskip S n v)) zero).
+Intros.
+MApply '(id_trans ? (sub (llen S v) n)).
+MApply 'lskip_llen.
+MApply 'sub_zero.
+Qed.
+
+Theorem lslice_succ_r: (S:Set; v:(List S); k,n:N) (Id (List S) (lslice S k (succ n) v) (app S (lslice S (succ k) n v) (lix S k v))).
+Intros.
+(Unfold lslice lix; MSimpl).
+MApply '(id_repl ? (tl S (lskip S k v)) (lskip S k (tl S v))).
+MApply 'lskip_tl.
+Qed.
+
+Theorem lslice_succ_l: (S:Set; v:(List S); n,k:N) (Id (List S) (lslice S k (succ n) v) (app S (lix S (add k n) v) (lslice S k n v))).
+Intros S v n.
+MElim 'n 'natrec.
+MApply 'lslice_lix.
+MApply '(id_repl ? (succ (add k n0)) (add (succ k) n0)).
+MApply 'add_succ.
+MApply '(id_repl ? (lslice S k (succ n0) v) (app S (lslice S (succ k) n0 v) (lix S k v))).
+(MApply 'id_comm; MApply 'lslice_succ_r).
+MApply '(id_repl ? (lslice S k (succ (succ n0)) v) (app S (lslice S (succ k) (succ n0) v) (lix S k v))).
+(MApply 'id_comm; MApply 'lslice_succ_r).
+MApply '(id_trans (List S) (app S (app S (lix S (add (succ k) n0) v) (lslice S (succ k) n0 v)) (lix S k v))).
+MApply '(id_comp (List S) (List S) [u:?](app S u (lix S k v))).
+MApply '(H (succ k)).
+Apply succ_fold. (**)
+MApply '(id_repl N (succ (add k n0)) (add (succ k) n0)).
+MApply 'add_succ.
+MApply 'app_ass.
+Qed.
+
+Theorem lslice_add: (S:Set; v:(List S); k,m,n:N) (Id (List S) (lslice S k (add m n) v) (app S (lslice S (add k m) n v) (lslice S k m v))).
+Intros.
+MElim 'n 'natrec.
+MApply '(id_repl ? (lslice S (add k m) zero v) (empty S)).
+(MApply 'id_comm; MApply 'app_empty).
+MApply '(id_trans ? (app S (lix S (add k (add m n0)) v) (lslice S k (add m n0) v))).
+Apply succ_fold. (**)
+MApply 'lslice_succ_l.
+MApply '(id_repl ? (lslice S (add k m) (succ n0) v) (app S (lix S (add (add k m) n0) v) (lslice S (add k m) n0 v))).
+(MApply 'id_comm; MApply 'lslice_succ_l).
+MApply '(id_trans ? (app S (lix S (add (add k m) n0) v) (app S (lslice S (add k m) n0 v) (lslice S k m v)))).
+MApply '(id_repl ? (add k (add m n0)) (add (add k m) n0)).
+MApply 'add_ass.
+MApply '(id_comp (List S) (List S) [w](app S (lix S (add (add k m) n0) v) w)).
+(MApply 'id_comm; MApply 'app_ass).
+Qed.
+
+Theorem lslice_bsadd: (S:Set; v:(List S); k:N; ms:NS; n:N) (Id (List S) (lslice S k (bs_add ms n) v) (bs_app S [m](lslice S (add k (bs_add ms m)) (ms m) v) n)).
+Intros.
+(MElim 'n 'natrec; Fold (add (ms n0) (bs_add ms n0))).
+MApply '(id_repl ? (bs_app S [m:N](lslice S (add k (bs_add ms m)) (ms m) v) n0) (lslice S k (bs_add ms n0) v)).
+MApply '(id_repl ? (add (ms n0) (bs_add ms n0)) (add (bs_add ms n0) (ms n0))).
+MApply 'add_comm.
+MApply 'lslice_add.
+Qed.
+
+Theorem lslice_rbsadd: (S:Set; v:(List S); k:N; ms:NS; n:N) (Id (List S) (lslice S k (rbs_add ms n) v) (rbs_app S [m](lslice S (add k (bs_add ms m)) (ms m) v) n)).
+Intros.
+Unfold rbs_add rbs_app rbs_iter.
+Apply bs_app_fold.
+Apply bs_app_fold.
+Apply bs_add_fold. (**)
+MApply 'lslice_bsadd.
+Qed.
+*)
+End arithmetics_results.
+
+End Arith_Results.
--- /dev/null
+Section Base_Definitions.
+
+ Section inductive_sets.
+
+ Inductive Set Empty := .
+
+ Inductive Set List [S:Set] := empty: (List S) | fr: (List S) -> S -> (List S).
+
+ Inductive Id [S:Set; a:S]: S -> Set := id_r: (Id S a a).
+
+ Inductive Set Pi [S:Set; P:S->Set] := abst: ((a:S) (P a)) -> (Pi S P).
+
+ Inductive Set Sigma [S:Set; P:S->Set] := pair: (a:S) (P a) -> (Sigma S P).
+
+ Inductive Set Plus [S,T:Set] := in_l : S -> (Plus S T) | in_r : T -> (Plus S T).
+(*
+Inductive SId [A:Set] : Set -> Set := sid_r: (SId A A).
+*)
+ End inductive_sets.
+
+ Section eliminators.
+
+ Definition efq := Empty_rec.
+
+ Definition listrec := List_rec.
+
+ Definition idrec := Id_rec.
+
+ Definition fsplit := Pi_rec.
+
+ Definition psplit := Sigma_rec.
+
+ Definition when := Plus_rec.
+
+ Definition EmptyFam := Empty_rect.
+
+ Definition ListFam := List_rect.
+
+ Definition IdFam := Id_rect.
+
+ Definition PiFam := Pi_rect.
+
+ Definition SigmaFam := Sigma_rect.
+
+ Definition PlusFam := Plus_rect.
+
+ Definition ap: (S:Set; P:S->Set) (Pi S P) -> (a:S) (P a).
+ Intros.
+ Elim H.
+ Intros.
+ Apply (p a).
+ Defined.
+
+ Definition sp: (S:Set; P:S->Set) (Sigma S P) -> S.
+ Intros.
+ Elim H.
+ Intros.
+ Assumption.
+ Defined.
+
+ Definition sq: (S:Set; P:S->Set; p:(Sigma S P)) (P (sp S P p)).
+ Intros.
+ Elim p.
+ Intros.
+ Unfold sp.
+ Simpl.
+ Assumption.
+ Defined.
+
+ End eliminators.
+
+ Section functions.
+
+ Definition id: (S:Set) S -> S.
+ Intros.
+ Assumption.
+ Defined.
+
+ Definition comp: (R,S,T:Set) (R -> S) -> (S -> T) -> (R -> T).
+ Intros.
+ Apply H0.
+ Apply H.
+ Assumption.
+ Defined.
+
+ End functions.
+
+End Base_Definitions.
+
+Section Base_Results.
+
+ Section general_results.
+
+ Theorem mcut: (S,T:Set) S -> (S -> T) -> T.
+ Intros.
+ Apply H0.
+ Assumption.
+ Qed.
+
+ End general_results.
+
+ Section ID_results.
+
+ Theorem id_repl: (S:Set; a,b:S; P:S->Set) (Id ? b a) -> (P b) -> (P a).
+ Intros.
+ Elim H.
+ Assumption.
+ Qed.
+
+ Theorem id_comm: (S:Set; a,b:S) (Id ? b a) -> (Id ? a b).
+ Intros.
+ Apply (id_repl S a b).
+ Assumption.
+ Apply id_r.
+ Qed.
+
+ Theorem id_trans: (S:Set; c,a,b:S) (Id S a c) -> (Id S c b) -> (Id S a b).
+ Intros.
+ Apply (id_repl S b c).
+ Assumption.
+ Assumption.
+ Qed.
+
+ Theorem id_comp: (S,T:Set; f:S->T; a,b:S) (Id S a b) -> (Id T (f a) (f b)).
+ Intros.
+ Apply (id_repl ? b a).
+ Assumption.
+ Apply id_r.
+ Qed.
+
+ Axiom id_ext: (S,T:Set; f,g:S->T) ((a:S) (Id T (f a) (g a))) -> (Id S->T f g).
+
+ End ID_results.
+(*
+Section SID_results.
+
+Theorem sid_repl: (A,B:Set; P:Set->Set) (SId B A) -> (P B) -> (P A).
+Intros.
+Elim H.
+Assumption.
+Qed.
+
+Theorem sid_comp: (P:Set->Set; A,B:Set) (SId A B) -> (SId (P A) (P B)).
+Intros.
+Apply (sid_repl B A).
+Assumption.
+Apply sid_r.
+Qed.
+
+Axiom sid_ext: (S:Set; P:(S->Set)->Set; Q,R:S->Set) ((a:S) (SId (Q a) (R a))) -> (SId (P Q) (P R)).
+
+End SID_results.
+*)
+ Section indipendence.
+
+ Axiom list_p4: (S:Set; l:(List S); a:S) (Id (List S) (empty S) (fr S l a)) -> Empty.
+
+ Axiom plus_p4: (S:Set; a:S; T:Set; b:T) (Id (Plus S T) (in_l S T a) (in_r S T b)) -> Empty.
+(*
+Axiom id_ctt: (S:Set) (P:(a:S)(Id S a a) -> Set) ((a:S) (P a (id_r S a))) -> (a:S; p:(Id S a a)) (P a p).
+*)
+ End indipendence.
+
+End Base_Results.
+
+Tactic Definition MTrivial := Try Apply id_r; (* Try Apply sid_r; *)
+(*|*) Try Assumption; Try Apply id_comm;
+ Try Assumption; Try Apply id_comm.
+
+Tactic Definition MFold := Idtac.
+
+Tactic Definition MRed := Idtac.
+
+Tactic Definition MAuto := MTrivial; MFold; MRed.
+
+Tactic Definition MSimpl := Simpl; MAuto.
+
+Tactic Definition MElim v e := Pattern v; Elim v using e; Simpl;
+ Intros; MAuto.
+
+Tactic Definition MApply t := Apply t; Intros; MTrivial.
+
+Tactic Definition MCut t := MApply '(mcut t).
+
+Tactic Definition UnIntros T t := Apply (mcut T); Try Assumption; Clear t.
--- /dev/null
+Require Export st_base.
+
+Section Logic_Sets.
+
+ Section logic_aliases.
+(*
+Definition All := Pi.
+*)
+ Definition LEx := Sigma.
+
+ Definition LBot := Empty.
+
+ Definition LOr := Plus.
+
+ Definition LImp: Set -> Set -> Set := [S,T](Pi S [_:S]T).
+
+ Definition LAnd: Set -> Set -> Set := [S,T](Sigma S [_:S]T).
+
+ Definition LNot: Set -> Set := [S](LImp S LBot).
+
+ Definition LTop: Set := (LNot LBot).
+
+ Definition LIff: Set -> Set -> Set := [S,T](LAnd (LImp S T) (LImp T S)).
+
+ Definition limp_i: (S,T:Set) (S -> T) -> (LImp S T).
+ Intros.
+ MApply '(abst S [_]T H).
+ Defined.
+
+ Definition limp_e: (S,T:Set) (LImp S T) -> (S->T).
+ Intros.
+ MApply '(ap S [_:S]T H H0).
+ Defined.
+
+ Definition land_i: (S,T:Set) S -> T -> (LAnd S T).
+ Intros.
+ MApply '(pair S [_:S]T H H0).
+ Defined.
+
+ Definition land_e2: (T,S:Set) (LAnd S T) -> S.
+ Intros.
+ MElim H psplit.
+ Defined.
+
+ Definition land_e1: (S,T:Set) (LAnd S T) -> T.
+ Intros.
+ MElim H psplit.
+ Defined.
+(*
+Definition all_e: (S:Set; a:S; P:S->Set) (All S P) -> (P a) := [S;a;P,f](ap S P f a).
+*)
+ Definition lex_i: (S:Set; a:S; P:S->Set) (P a) -> (LEx S P).
+ Intros.
+ MApply '(pair S P a H).
+ Defined.
+
+ Definition lex_e: (S:Set; P:S->Set; P0:(LEx S P)->Set) ((a:S; y:(P a)) (P0 (lex_i S a P y))) -> (s:(LEx S P)) (P0 s).
+ Intros.
+ MElim s psplit.
+ MApply '(H a p).
+ Defined.
+
+ End logic_aliases.
+
+ Section unit.
+
+ Definition One: Set := (List Empty).
+
+ Definition tt: One := (empty Empty).
+
+ Definition onerec: (P:One->Set) (P tt) -> (u:One) (P u).
+ Intros.
+ MElim 'u 'listrec.
+ MElim 's 'efq.
+ Defined.
+
+ Definition OneFam: (P:One->Type) (P tt) -> (u:One) (P u).
+ Intros.
+ MElim 'u 'ListFam.
+ MElim 's 'EmptyFam.
+ Defined.
+
+ End unit.
+
+ Section booleans.
+
+ Definition Boole: Set := (Plus One One).
+
+ Definition false: Boole := (in_l One One tt).
+
+ Definition true: Boole := (in_r One One tt).
+
+ Definition ite: (P:Boole->Set) (P false) -> (P true) -> (b:Boole) (P b).
+ Intros.
+ MElim 'b 'when.
+ MElim 's 'onerec.
+ MElim 't 'onerec.
+ Defined.
+
+ Definition BooleFam: (P:Boole->Type)
+ (P false) -> (P true) -> (b:Boole) (P b).
+ Intros.
+ MElim 'b 'PlusFam.
+ MElim 's 'OneFam.
+ MElim 't 'OneFam.
+ Defined.
+(*
+Definition BF: Set -> Set -> Boole -> Set := (BooleFam [_]Set).
+
+Definition Two: Set := Boole.
+*)
+ End booleans.
+
+End Logic_Sets.
+
+Section Logic_Hints.
+(*
+Section logic_fold.
+
+Theorem Top_fold: (P:Set->Set) (P Top) -> (P (Imp Bot Bot)).
+Intros.
+Apply (sid_repl (Imp Bot Bot) Top).
+Apply sid_r.
+Assumption.
+Qed.
+
+End logic_fold.
+*)
+ Section logic_red.
+
+ Theorem LTop_red: LTop.
+ Unfold LTop LNot.
+ Apply limp_i.
+ Intros.
+ Assumption.
+ Qed.
+(*
+Theorem Top_And_red: (A:Set) A -> (And Top A).
+Intros.
+Apply and_i.
+Apply Top_red.
+Assumption.
+Qed.
+*)
+ End logic_red.
+
+End Logic_Hints.
+
+Section Logic_Results.
+
+ Section boole_indipendence.
+
+ Axiom lor_p4: (A,B:Set; a:A; b:B)
+ (Id (LOr A B) (in_l A B a) (in_r A B b)) -> Empty.
+
+ Axiom boole_p4: (Id Boole false true) -> Empty. (**)
+
+ End boole_indipendence.
+
+ Section logic_results.
+
+ Theorem lor_e: (A,B,C:Set) (A -> C) -> (B -> C) -> (LOr A B) -> C.
+ Intros.
+ MApply '(when A B [_:?]C).
+ MApply '(H s).
+ MApply '(H0 t).
+ Qed.
+
+ Theorem lnot_i: (S:Set) (S -> LBot) -> (LNot S).
+ Intros.
+ Unfold LNot.
+ MApply 'limp_i.
+ MApply 'H.
+ Qed.
+
+ Theorem lnot_e: (S:Set) (LNot S) -> S -> LBot.
+ Unfold LNot.
+ Intros.
+ MApply '(limp_e S).
+ Qed.
+
+ Theorem liff_i: (A,B:Set) (A -> B) -> (B -> A) -> (LIff A B).
+ Intros.
+ Unfold LIff.
+ (MApply land_i; MApply limp_i).
+ MApply H.
+ MApply H0.
+ Qed.
+
+ Theorem liff_e1: (A,B:Set) A -> (LIff A B) -> B.
+ Unfold LIff.
+ Intros.
+ MApply '(limp_e A).
+ MApply '(land_e2 (LImp B A)).
+ Qed.
+
+ Theorem liff_e2: (B,A:Set) B -> (LIff A B) -> A.
+ Unfold LIff.
+ Intros.
+ MApply '(limp_e B).
+ MApply '(land_e1 (LImp A B)).
+ Qed.
+(*
+Theorem iff_trans: (C,A,B:Set) (Iff A C) -> (Iff C B) -> (Iff A B).
+Intros.
+MApply iff_i.
+MApply (iff_e1 C).
+MApply (iff_e1 A).
+MApply (iff_e2 C).
+MApply (iff_e2 B).
+Qed.
+
+Theorem iff_sym: (A,B:Set) (Iff B A) -> (Iff A B).
+Intros.
+MApply iff_i.
+MApply (iff_e2 A).
+MApply (iff_e1 B).
+Qed.
+*)
+ Theorem lnot_liff_lbot: (A:Set) (LIff A (LNot A)) -> LBot.
+ Intros.
+ MApply '(lnot_e (LNot A)).
+ MApply 'lnot_i.
+ MApply '(lnot_e A).
+ MApply '(liff_e2 (LNot A)).
+ MApply 'lnot_i.
+ MApply '(lnot_e A).
+ MApply '(liff_e1 A).
+ Qed.
+(*
+Theorem imp_r: (A:Set) (Imp A A).
+Intros.
+MApply imp_i.
+Qed.
+
+Theorem imp_trans: (C,A,B:Set) (Imp A C) -> (Imp C B) -> (Imp A B).
+Intros.
+MApply imp_i.
+MApply (imp_e C).
+MApply (imp_e A).
+Qed.
+
+Theorem all_sigma_l: (S:Set; T:S->Set; P:(Sigma S T)->Set) ((a:S; b:(T a)) (P (pair S T a b))) -> (p:(Sigma S T)) (P p).
+Intros.
+MElim p psplit.
+Apply (H a y).
+Qed.
+*)
+ End logic_results.
+
+End Logic_Results.
+
+
--- /dev/null
+Require Export st_logic.
+
+Section Nat_Sets.
+
+ Section natural_numbers.
+
+ Definition N: Set := (List One).
+
+ Definition zero: N := (empty One).
+
+ Definition succ: N -> N := [n](fr One n tt).
+
+ Definition natrec: (P:N->Set) (P zero) ->
+ ((n:N) (P n) -> (P (succ n))) -> (n:N)(P n).
+ Intros.
+ MElim 'n 'listrec.
+ MElim 's 'onerec.
+ MApply '(H0 l).
+ Defined.
+
+ Definition NatFam: (P:N->Type) (P zero) ->
+ ((n:N) (P n) -> (P (succ n))) -> (n:N)(P n).
+ Intros.
+ MElim 'n 'ListFam.
+ MElim 's 'OneFam.
+ MApply '(X0 l).
+ Defined.
+
+ Definition one: N := (succ zero).
+(*
+Definition two:N := (succ one).
+*)
+ End natural_numbers.
+(*
+Section sequences.
+
+Definition ListS := [S:Set](N -> (List S)).
+
+Definition BooleS: Set := N -> Boole.
+
+Definition NS := N -> N.
+
+Definition trues:BooleS := [_]true.
+
+End sequences.
+*)
+End Nat_Sets.
+
+Section Nat_Functions.
+(*
+Section bounded_iteration.
+
+Variable S:Set; e:S; f:S->S->S.
+
+Definition bs_iter: (N -> S) -> N -> S := [s](natrec [_]S e [m](f (s m))).
+
+Definition rbs_iter: (N -> S) -> N -> S := [s;n](bs_iter s (succ n)).
+
+End bounded_iteration.
+
+Section nat_boolean_eq.
+
+Variable S:Set.
+
+Definition n_id: N -> N -> Boole := (natrec [_]N->Boole (natrec [_]Boole true [_;_]false)
+ [_;pm'](natrec [_]Boole false [n';_](pm' n'))).
+
+Definition ifeq: N -> N -> S -> S -> S := [m,n;a;b](ite [_]S b a (n_id m n)).
+
+Definition ifz: N -> S -> S -> S := [n;a;b](natrec [_]S a [_;_]b n).
+
+End nat_boolean_eq.
+*)
+ Section less_equal.
+
+ Definition b_le: N -> N -> Boole := (natrec [_]N->Boole [n]true [m';p](natrec [_]Boole false [n';_](p n'))).
+
+ Definition LE: N -> N -> Set := [m,n](Id Boole (b_le m n) true).
+
+ Definition GT: N -> N -> Set := [m,n](Id Boole (b_le m n) false).
+
+ End less_equal.
+
+End Nat_Functions.
+
+Section Nat_Hints.
+
+ Section nat_fold.
+
+ Theorem succ_fold: (n:N; P:N->Set) (P (succ n)) -> (P (fr One n tt)).
+ Intros.
+ Assumption.
+ Qed.
+(*
+Theorem LE_fold: (m,n:N; P:Set->Set) (P (LE m n)) -> (P (Id Boole (b_le m n) true)).
+Intros.
+Assumption.
+Qed.
+*)
+ End nat_fold.
+
+End Nat_Hints.
+
+Section Nat_Results.
+
+ Section nat_indipendence.
+
+ Theorem n_p4: (n:N) (Id N zero (succ n)) -> Empty.
+ Intros.
+ MApply '(list_p4 One n tt).
+ Qed.
+
+ Theorem n_false: (n:N; P:Set) (Id N zero (succ n)) -> P.
+ Intros.
+ MCut 'Empty.
+ MApply '(n_p4 n).
+ MElim 'H0 'efq.
+ Qed.
+
+ End nat_indipendence.
+
+ Section b_le_results.
+
+ Theorem le_wf: (n:N) (LE zero n).
+ Intros.
+ Unfold LE.
+ MApply 'id_r.
+ Qed.
+
+ Theorem le_comp_succ: (m,n:N) (LE m n) -> (LE (succ m) (succ n)).
+ Intros.
+ Assumption.
+ Qed.
+(*
+Theorem le_ssucc: (m,n:N) (LE (succ m) (succ n)) -> (LE m n).
+Intros.
+Assumption.
+Qed.
+*)
+ Theorem le_false: (n:N; P:Set) (LE (succ n) zero) -> P.
+ Intros n P.
+ Unfold LE.
+ MSimpl.
+ Intros.
+ MCut 'Empty.
+ MApply 'boole_p4.
+ MElim 'H0 'efq.
+ Qed.
+
+ Theorem le_r: (n:N) (LE n n).
+ Intros.
+ MElim 'n 'natrec.
+ MApply 'le_wf.
+ Qed.
+
+ Theorem le_succ: (n:N) (LE n (succ n)).
+ Intros.
+ MElim 'n 'natrec.
+ MApply 'le_wf.
+ Qed.
+
+ Theorem le_zero: (n:N) (LE n zero) -> (Id N n zero).
+ Intros n.
+ MElim 'n 'natrec.
+ MApply '(le_false n0).
+ Qed.
+
+ Theorem le_trans: (b,c,a:N) (LE a b) -> (LE b c) -> (LE a c).
+ Intros b.
+ Elim b using natrec.
+ Intros c a.
+ MElim 'a 'natrec.
+ MApply '(le_false n).
+ Intros b' H c.
+ Elim c using natrec.
+ Intros.
+ MApply '(le_false b').
+ Intros c' H' a.
+ MElim 'a 'natrec.
+ MApply 'le_comp_succ.
+ MCut '(LE n b').
+ MCut '(LE b' c').
+ MApply '(H c' n).
+ Qed.
+
+ Theorem gt_wf: (n:N) (GT (succ n) zero).
+ Intros.
+ Unfold GT.
+ MApply 'id_r.
+ Qed.
+
+ Theorem gt_comp_succ: (m,n:N) (GT m n) -> (GT (succ m) (succ n)).
+ Intros.
+ Assumption.
+ Qed.
+
+ Theorem gt_false: (n:N; P:Set) (GT zero n) -> P.
+ Intros n P.
+ Unfold GT.
+ MSimpl.
+ Intros.
+ MCut 'Empty.
+ MApply 'boole_p4.
+ MElim 'H0 'efq.
+ Qed.
+
+ Theorem le_gt: (m,n:N) (LE (succ n) m) -> (GT m n).
+ Intros m.
+ Elim m using natrec.
+ Intros.
+ MApply '(le_false n).
+ Intros m' H n.
+ Elim n using natrec.
+ Intros.
+ MApply 'gt_wf.
+ Intros n' H1 H2.
+ MApply 'gt_comp_succ.
+ MApply '(H n').
+ Qed.
+
+ Theorem gt_le: (m,n:N) (GT m n) -> (LE (succ n) m).
+ Intros m.
+ Elim m using natrec.
+ Intros.
+ MApply '(gt_false n).
+ Intros m' H n.
+ MElim 'n natrec.
+ MApply 'le_comp_succ.
+ MApply 'le_wf.
+ MApply 'le_comp_succ.
+ MApply '(H n0).
+ Qed.
+
+ Theorem le_gt_trans: (b,c,a:N) (LE b a) -> (GT b c) -> (GT a c).
+ Intros.
+ MApply 'le_gt.
+ MApply '(le_trans b).
+ MApply 'gt_le.
+ Qed.
+
+ Theorem boole_di: (b:Boole) (LOr (Id Boole b true) (Id Boole b false)).
+ Intros.
+ MElim 'b 'ite.
+ MApply 'in_r.
+ MApply 'in_l.
+ Qed.
+
+ Theorem le_di: (m,n:N) (LOr (LE m n) (GT m n)).
+ Intros.
+ Unfold LE GT.
+ MApply '(boole_di (b_le m n)).
+ Qed.
+(*
+Theorem ble_trip: (m,n:N; P:N->Set) ((n:N) (LE n m) -> (P n)) -> ((n:N) (GT n m) -> (P n)) -> (P n).
+Intros.
+MApply '(or_e (LE n m) (GT n m)).
+MApply '(H n).
+MApply '(H0 n).
+MApply 'ble_tri.
+Qed.
+*)
+ End b_le_results.
+
+End Nat_Results.
--- /dev/null
+(** This module (Toolbox - subsets: basics) defines:
+ - subset membership: [Eps] (epsilon)
+ - empty subset: [SBot] (subset bottom)
+ - full subset: [STop] (subset top)
+ - singleton: [Sing] (singleton)
+ - relative universal quantifier: [RAll] (relative all)
+ - relative existential quantifier: [REx] (relative exists)
+
+ and provides:
+ - introduction and elimination rules for the defined constants
+ - epsilon conditions: [eps_1], [eps_2]
+ - alternative form of epsilon with sigma: [eps2]
+
+% \hrule %
+
+ We require the support for finite sets and finite domain functions ([xt_fin])
+ that includes the basic type theory (the [st] package).
+
+ *)
+Require Export xt_fin.
+
+Section Subset_Definitions.
+
+ Section subset_membership.
+
+(** Epsilon: [(Eps S a U)] corresponds to $ a \e_S U $. *)
+ Definition Eps: (S:Set) S -> (S -> Set) -> Set.
+ Intros S a U.
+ Exact (LAnd (U a) (Id S a a)).
+ Defined.
+
+ End subset_membership.
+
+ Section subset_constants.
+
+(** Subset bottom: [(SBot S)] corresponds to $ \sbot_S $. *)
+ Definition SBot: (S:Set) S -> Set.
+ Intros.
+ Exact LBot.
+ Defined.
+
+(** Subset top: [(STop S)] corresponds to $ \stop_S $, %{\ie}% to $S$ as a subset of itself. *)
+ Definition STop: (S:Set) S -> Set.
+ Intros.
+ Exact LTop.
+ Defined.
+
+(** Singleton: [(Sing S a)] corresponds to $ \subset{a} $. *)
+ Definition Sing: (S:Set) S -> (S -> Set).
+ Intros S a b.
+ Exact (Id S a b).
+ Defined.
+
+ End subset_constants.
+
+ Section relative_quantification.
+
+(** Relative all: [(RAll S U P)] corresponds to $ (\lall x \e U) P(x) $. *)
+ Definition RAll: (S:Set) (S -> Set) -> (S -> Set) -> Set.
+ Intros S U P.
+ Exact (a:S) (Eps S a U) -> (P a).
+ Defined.
+
+(** Relative exists: [(REx S U P)] corresponds to $ (\lex x \e U) P(x) $. *)
+ Definition REx: (S:Set) (S -> Set) -> (S -> Set) -> Set.
+ Intros S U P.
+ Exact (LEx S [a](LAnd (Eps S a U) (P a))).
+ Defined.
+
+ End relative_quantification.
+
+End Subset_Definitions.
+
+Section Subset_Results.
+
+ Section epsilon_conditions.
+
+(** Epsilon elimination: $ a \e U \limp U(a) $. *)
+ Theorem eps_e: (S:Set; a:S; U:S->Set) (Eps S a U) -> (U a).
+ Unfold Eps.
+ Intros.
+ MApply '(land_e2 (Id S a a)).
+ Qed.
+
+(** Epsilon introduction: $ U(a) \limp a \e U $. *)
+ Theorem eps_i: (S:Set; a:S; U:S->Set) (U a) -> (Eps S a U).
+ Unfold Eps.
+ Intros.
+ MApply 'land_i.
+ Qed.
+
+(** Epsilon condition 1: $ a \e U \liff U(a) $. *)
+ Theorem eps_1: (S:Set; U:(S -> Set)) (a:S)(LIff (Eps S a U) (U a)).
+ Intros.
+ MApply 'liff_i.
+ MApply '(eps_e S a).
+ MApply 'eps_i.
+ Qed.
+
+(** Epsilon condition 2: $ a \e_S U \limp a \in S $. *)
+ Theorem eps_2: (S:Set; a:S; U:(S -> Set)) (Eps S a U) -> S.
+ Intros.
+ Exact a.
+ Qed.
+
+(** Epsilon in sigma form: $ a \e_S U \liff (\lex z \in (\Sigma x \in S) U) Id(S, p(z), a) $. *)
+ Theorem eps2: (S:Set; a:S; U:(S -> Set)) (LIff (Eps S a U) (LEx (Sigma S U) [z](Id S (sp S U z) a))).
+ Intros.
+ MApply 'liff_i.
+ MCut '(U a).
+ MApply 'eps_e.
+ MApply '(lex_i (Sigma S U) (pair S U a H0)).
+ MApply 'eps_i.
+ MElim 'H 'lex_e.
+ MApply '(id_repl ? a (sp S U a0)).
+ MElim 'a0 psplit.
+ Qed.
+
+ End epsilon_conditions.
+
+ Section subset_top_bottom.
+
+(** Subset top, epsilon introduction: $ a \e \stop $. *)
+ Theorem stop_eps_i: (S:Set; a:S) (Eps S a (STop S)).
+ Intros.
+ MApply 'eps_i.
+ Unfold STop.
+ MApply 'LTop_red.
+ Qed.
+
+(** Subset bottom, epsilon elimination: $ a \e \sbot \limp \lbot $. *)
+ Theorem sbot_eps_e: (S:Set; a:S) (Eps S a (SBot S)) -> LBot.
+ Intros.
+ MApply '(eps_e S a).
+ Qed.
+
+ End subset_top_bottom.
+
+ Section singleton.
+
+(** Singleton, epsilon introduction: $ Id(S, a, b) \limp b \e \subset{a} $. *)
+ Theorem sing_eps_i: (S:Set; b,a:S) (Id S a b) -> (Eps S b (Sing S a)).
+ Intros.
+ MApply 'eps_i.
+ Qed.
+
+(** Singleton, epsilon elimination: $ b \e \subset{a} \limp Id(S, a, b) $. *)
+ Theorem sing_eps_e: (S:Set; a,b:S) (Eps S b (Sing S a)) -> (Id S a b).
+ Intros.
+ MApply 'eps_e.
+ Qed.
+
+ End singleton.
+
+ Section relative_universal.
+
+(** Relative all introduction: $ ((\lall a \in S)\ a \e U \limp P(a)) \limp (\lall x \e U) P(x) $. *)
+ Theorem rall_i: (S:Set; U:S->Set; P:S->Set) ((a:S) (Eps S a U) -> (P a)) -> (RAll S U P).
+ Unfold RAll.
+ Intros.
+ MApply '(H a).
+ Qed.
+
+(** Relative all elimination: $ a \e U \limp (\lall x \e U) P(x) \limp P(a) $. *)
+ Theorem rall_e: (S:Set; a:S; U:S->Set; P:S->Set) (Eps S a U) -> (RAll S U P) -> (P a).
+ Intros.
+ Unfold RAll in H0.
+ MApply '(H0 a).
+ Qed.
+
+ End relative_universal.
+
+ Section relative_existential.
+
+(** Relative exists introduction: $ a \e U \limp P(a) \limp (\lex x \e U) P(x) $. *)
+ Theorem rex_i: (S:Set; a:S; U:S->Set; P:S->Set) (Eps S a U) -> (P a) -> (REx S U P).
+ Intros.
+ Unfold REx.
+ MApply '(lex_i S a).
+ MApply 'land_i.
+ Qed.
+
+(** Relative exists elimination: $ ((\lall a \in S)\ a \e U \limp P(a) \limp T) \limp (\lex x \e U) P(x) \limp T $. *)
+ Theorem rex_e: (S:Set; U:S->Set; P:S->Set; T:Set) ((a:S) (Eps S a U) -> (P a) -> T) -> (REx S U P) -> T.
+ Intros.
+ Unfold REx in H0.
+ MElim 'H0 'lex_e.
+ MApply '(H a).
+ MApply '(land_e2 (P a)).
+ MApply '(land_e1 (Eps S a U)).
+ Qed.
+
+ End relative_existential.
+
+End Subset_Results.
--- /dev/null
+Require Export tbs_fun.
+
+Section Subset_Finite_Definitions.
+
+ Section subsets_from_lists.
+
+ Definition SList: (S:Set) (List S) -> (S -> Set) := [S](ListFam S [_](S->Set) (SBot S) [_;p;a](SOr S p (Sing S a))).
+
+ End subsets_from_lists.
+
+ Section subset_finite_predicate.
+
+ Definition WFin: (S:Set) (S -> Set) -> Set := [S;U](LEx (FDF S) [z](SbE S U (FDFImg S z))).
+(*
+Definition SFin: (S:Set) (S -> Set) -> Set := [S;U](Ex (FDF S) [z](SEq S U (FDFImg S z))).
+*)
+ End subset_finite_predicate.
+(*
+Section subset_finite_quantification.
+
+Definition FAll: (S:Set) ((Part S) -> Set) -> Set := [S;P](z:(FDF S))(P (SFImg S z)).
+
+Definition FEx: (S:Set) ((Part S) -> Set) -> Set := [S;P](Ex (FDF S) [z](P (SFImg S z))).
+
+End subset_finite_quantification.
+*)
+End Subset_Finite_Definitions.
+
+Section Subset_Finite_Results.
+
+ Section subset_list.
+
+ Theorem slist_eps_i: (S:Set; a:S; l:(List S)) (LIn S a l) -> (Eps S a (SList S l)).
+ Intros S a l.
+ MElim l listrec.
+ MCut Empty.
+ Apply (lin_e S a (empty S)).
+ Assumption.
+ Intros v w.
+ MElim w listrec.
+ MApply '(list_p4 S v a).
+ MApply '(list_p4 S (app S (fr S v a) l0) s).
+ MElim H0 efq.
+ Apply (lin_e S a (fr S l0 s)).
+ Assumption.
+ Intros v w.
+ MElim w listrec.
+ MApply 'sor_eps_i1.
+ MApply 'sing_eps_i.
+ MApply '(fr_ini2 S l0 v).
+ MApply 'sor_eps_i2.
+ MApply 'H.
+ MApply '(lin_i S v l1).
+ MApply '(fr_ini1 S s0 s).
+ Qed.
+
+
+ Theorem slist_xfdfl: (S:Set; n:N; v:(Fin n)->S) (SbE S (Img (Fin n) S v) (SList S (xfdf_list S n v))).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'slist_eps_i.
+ MApply '(img_eps_e (Fin n) S v a).
+ MApply '(id_repl S a (v i)).
+ MApply 'xfdfl_lin.
+ Qed.
+
+ Theorem slist_fdfl: (S:Set; v:(FDF S)) (SbE S (FDFImg S v) (SList S (fdfl S v))).
+ Intros.
+ MApply '(id_repl (List S) (fdfl S v) (xfdf_list S (fdf_n S v) (fdf_f S v))).
+ MElim 'v '(fdf_e S).
+ Unfold FDFImg.
+ MApply 'slist_xfdfl.
+ Qed.
+
+ End subset_list.
+
+ Section weakly_finite.
+
+ Theorem wfin_i: (S:Set; v:(FDF S); U:S->Set) (SbE S U (FDFImg S v)) -> (WFin S U).
+ Intros.
+ Unfold WFin.
+ MApply '(lex_i (FDF S) v).
+ Qed.
+
+ Theorem wfin_e: (S:Set; U:S->Set; P:Set) (WFin S U) -> ((v:(FDF S)) (SbE S U (FDFImg S v)) -> P) -> P.
+ Intros.
+ MElim 'H 'lex_e.
+ MApply '(H0 a).
+ Qed.
+
+ Theorem wfin_sand: (S:Set; U,V:S->Set) (WFin S U) -> (WFin S (SAnd S U V)).
+ Intros.
+ MApply '(wfin_e S U).
+ MApply '(wfin_i S v).
+ MApply '(sbe_t S U).
+ MApply 'sand_sbe_e2.
+ Qed.
+
+ Theorem wfin_sor: (S:Set; U,V:S->Set) (WFin S U) -> (WFin S V) -> (WFin S (SOr S U V)).
+ Intros.
+ MApply '(wfin_e S U).
+ MApply '(wfin_e S V).
+ MApply '(wfin_i S (fdf_add S v v0)).
+ MApply '(sbe_t S (SOr S (FDFImg S v) (FDFImg S v0))).
+ MApply 'sor_sbe_c.
+ MApply 'img_fdf_add_i.
+ Qed.
+
+ Theorem wfin_list: (S:Set; U:S->Set) (WFin S U) -> (LEx (List S) [v](SbE S U (SList S v))).
+ Intros.
+ MApply '(wfin_e S U).
+ MApply '(lex_i (List S) (fdfl S v)).
+ MApply '(sbe_t S (FDFImg S v)).
+ MApply 'slist_fdfl.
+ Qed.
+
+ End weakly_finite.
+
+End Subset_Finite_Results.
--- /dev/null
+Require Export tbs_rop.
+
+Section Subset_From_Functions_Definitions.
+
+ Section image_subset.
+
+ Definition Img: (I,S:Set) (I -> S) -> (S -> Set) := [I,S;f;a] (LEx I [i](Id S (f i) a)).
+
+ Definition FDFImg: (S:Set) (FDF S) -> (S -> Set) := [S;v](Img (Fin (fdf_n S v)) S (fdf_f S v)).
+
+ End image_subset.
+
+ Section relative_image_domain_subset.
+
+ Definition RImg: (I,S:Set) (I -> S) -> (I -> Set) -> (S -> Set) := [I,S;f;T;a](REx I T [i](Id S (f i) a)).
+
+ Definition RDom: (I,S:Set) (I -> S) -> (S -> Set) -> (I -> Set) := [I,S;f;U;i](REx S U [a](Id S (f i) a)).
+
+ End relative_image_domain_subset.
+
+End Subset_From_Functions_Definitions.
+
+Section Subset_From_Functions_Results.
+
+ Section image.
+
+ Theorem img_eps_i: (I:Set; i:I; S:Set; a:S; f:I->S) (Id S (f i) a) -> (Eps S a (Img I S f)).
+ Intros.
+ MApply 'eps_i.
+ Unfold Img.
+ MApply '(lex_i I i).
+ Qed.
+
+ Theorem img_eps_e: (I,S:Set; f:I->S; a:S; P:Set) (Eps S a (Img I S f)) -> ((i:I) (Id S (f i) a) -> P) -> P.
+ Intros.
+ MCut '(LEx I [i](Id S (f i) a)).
+ Fold (Img I S f a).
+ MApply 'eps_e.
+ MElim 'H1 'lex_e.
+ MApply '(H0 a0).
+ Qed.
+
+ Theorem img_seq: (S:Set; U:(S -> Set)) (SEq S U (Img (Sigma S U) S (sp S U))).
+ Intros.
+ MApply 'seq_i.
+ MCut '(U a).
+ MApply 'eps_e.
+ MApply '(img_eps_i (Sigma S U) (pair S U a H0)).
+ MApply 'eps_i.
+ MApply '(img_eps_e (Sigma S U) S (sp S U) a).
+ MApply '(id_repl S a (sp S U i)).
+ MElim 'i 'psplit.
+ Qed.
+
+ Theorem img_sbe_i: (I,J,S:Set; f:I->S; g:J->S) (LEx I->J [h](i:I)(Id S (f i) (g (h i)))) -> (SbE S (Img I S f) (Img J S g)).
+ Intros.
+ MElim 'H 'lex_e.
+ MApply 'sbe_i.
+ MApply '(img_eps_e I S f a0).
+ MApply '(img_eps_i J (a i)).
+ MApply '(id_repl S a0 (f i)).
+ MApply 'id_comm.
+ MApply '(y i).
+ Qed.
+
+ Theorem img_xfdf_add_i: (S:Set; m:N; v:(Fin m)->S; n:N; w:(Fin n)->S) (SbE S (SOr S (Img (Fin m) S v) (Img (Fin n) S w)) (Img (Fin (add m n)) S (xfdf_add S m v n w))).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply 'img_sbe_i.
+ MApply '(lex_i (Fin m)->(Fin (add m n)) (fil m n)).
+ MApply 'id_comm.
+ MApply 'xfdfa_fil.
+ MApply 'img_sbe_i.
+ MApply '(lex_i (Fin n)->(Fin (add m n)) (fir m n)).
+ MApply 'id_comm.
+ MApply 'xfdfa_fir.
+ Qed.
+
+ End image.
+
+ Section fdf_image.
+
+ Theorem fdfimg_eps_i: (S:Set; v:(FDF S); i:(Fin (fdf_n S v)); a:S) (Id S (fdf_f S v i) a) -> (Eps S a (FDFImg S v)).
+ Intros.
+ Unfold FDFImg.
+ MApply '(img_eps_i (Fin (fdf_n S v)) i).
+ Qed.
+
+ Theorem fdfimg_eps_e: (S:Set; v:(FDF S); a:S; P:Set) (Eps S a (FDFImg S v)) -> ((i:(Fin (fdf_n S v))) (Id S (fdf_f S v i) a) -> P) -> P.
+ Intros.
+ MApply '(img_eps_e (Fin (fdf_n S v)) S (fdf_f S v) a).
+ MApply '(H0 i).
+ Qed.
+
+ Theorem img_fdf_add_i: (S:Set; v,w:(FDF S)) (SbE S (SOr S (FDFImg S v) (FDFImg S w)) (FDFImg S (fdf_add S v w))).
+ Intros.
+ Unfold FDFImg fdf_add.
+ MSimpl.
+ MApply 'img_xfdf_add_i.
+ Qed.
+
+ End fdf_image.
+
+ Section relative_image.
+
+ Theorem rimg_eps_i: (I:Set; i:I; T:I->Set) (Eps I i T) -> (S:Set; a:S; f:I->S) (Id S (f i) a) -> (Eps S a (RImg I S f T)).
+ Intros.
+ MApply 'eps_i.
+ Unfold RImg.
+ MApply '(rex_i I i).
+ Qed.
+
+ Theorem rimg_eps_e: (I,S:Set; a:S; T:I->Set; f:I->S; P:Set) ((i:I) (Eps I i T) -> (Id S (f i) a) -> P) -> (Eps S a (RImg I S f T)) -> P.
+ Intros.
+ Unfold RImg in H0.
+ MCut '(REx I T [i:I](Id S (f i) a)).
+ MApply '(eps_e S a).
+ MApply '(rex_e I T [i:I](Id S (f i) a)).
+ MApply '(H a0).
+ Qed.
+
+ Theorem rimg_sbe: (I,S:Set; f:I->S; U,V:I->Set) (SbE I U V) -> (SbE S (RImg I S f U) (RImg I S f V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(rimg_eps_e I S a U f).
+ MApply '(rimg_eps_i I i).
+ MApply '(sbe_e I U).
+ Qed.
+
+ Theorem rimg_sing_i: (I,S:Set; f:I->S; T:I->Set) (SbE S (SREx I T S [i;_](Sing S (f i))) (SREx S (RImg I S f T) S [a;_](Sing S a))).
+ Intros.
+ MApply 'sbe_i.
+ MCut '(LEx I [i:I](REps (T i) S a [_:?](Sing S (f i)))).
+ MApply '(srex_eps_e I T S a [i:I; _:(T i)](Sing S (f i))).
+ MElim 'H0 'lex_e.
+ MApply '(srex_eps_i S (f a0)).
+ MApply '(reps_e (T a0) S a [_:(T a0)](Sing S (f a0))).
+ MCut '(RImg I S f T (f a0)).
+ MApply 'eps_e.
+ MApply '(rimg_eps_i I a0).
+ MApply 'eps_i.
+ MApply '(reps_i (RImg I S f T (f a0)) H2).
+ Qed.
+
+ Theorem rimg_sing_e: (I,S:Set; f:I->S; T:I->Set) (SbE S (SREx S (RImg I S f T) S [a;_](Sing S a)) (SREx I T S [i;_](Sing S (f i)))).
+ Intros.
+ MApply 'sbe_i.
+ MCut '(LEx S [a0:?](REps (RImg I S f T a0) S a [_:?](Sing S a0))).
+ MApply '(srex_eps_e S (RImg I S f T) S a [a0:S; _:(RImg I S f T a0)](Sing S a0)).
+ MElim 'H0 'lex_e.
+ MApply '(reps_e (RImg I S f T a0) S a [_:(RImg I S f T a0)](Sing S a0)).
+ MCut '(Eps S a0 (RImg I S f T)).
+ MApply 'eps_i.
+ MApply '(rimg_eps_e I S a0 T f).
+ MApply '(srex_eps_i I i0).
+ MCut '(T i0).
+ MApply 'eps_e.
+ MApply '(reps_i (T i0) H5).
+ MApply 'sing_eps_i.
+ MApply '(id_repl S (f i0) a0).
+ MApply 'sing_eps_e.
+ Qed.
+
+ Theorem rimg_sing: (I,S:Set; f:I->S; T:I->Set) (SEq S (SREx I T S [i;_](Sing S (f i))) (SREx S (RImg I S f T) S [a;_](Sing S a))).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'rimg_sing_i.
+ MApply 'rimg_sing_e.
+ Qed.
+
+ Theorem rimg_srex: (I,S:Set; f:I->S; T:I->Set) (SEq S (SREx I T S [i;_](Sing S (f i))) (RImg I S f T)).
+ Intros.
+ MApply '(seq_t S (SREx S (RImg I S f T) S [a:S; _:(RImg I S f T a)](Sing S a))).
+ MApply 'rimg_sing.
+ MApply 'srex_sing.
+ Qed.
+
+ Theorem rimg_img_i: (I,S:Set; f:I->S; T:I->Set) (SbE S (Img (Sigma I T) S [x](f (sp I T x))) (RImg I S f T)).
+ Intros.
+ MApply 'sbe_i.
+ Apply (img_eps_e (Sigma I T) S [x:(Sigma I T)](f (sp I T x)) a).
+ Assumption.
+ Intros p.
+ MElim 'p 'psplit.
+ MApply '(rimg_eps_i I a0).
+ MApply 'eps_i.
+ Qed.
+
+ Theorem rimg_img_e: (I,S:Set; f:I->S; T:I->Set) (SbE S (RImg I S f T) (Img (Sigma I T) S [x](f (sp I T x)))).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(rimg_eps_e I S a T f).
+ MCut '(T i).
+ MApply 'eps_e.
+ MApply '(img_eps_i (Sigma I T) (pair I T i H2)).
+ Qed.
+
+ Theorem rimg_img: (I,S:Set; f:I->S; T:I->Set) (SEq S (Img (Sigma I T) S [x](f (sp I T x))) (RImg I S f T)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'rimg_img_i.
+ MApply 'rimg_img_e.
+ Qed.
+
+ End relative_image.
+
+End Subset_From_Functions_Results.
+
--- /dev/null
+(** This module (Toolbox - subsets: operations) defines:
+ - subset binary intersection: [SAnd] (subset and)
+ - subset binary union: [SOr] (subset or)
+ - subset implication: [SImp] (subset implies)
+ - subset opposite: [SNot] (subset not)
+ - subset infinitary intersection: [SAll] (subset all)
+ - subset infinitary union: [SEx] (subset exists)
+
+ and provides:
+ - introduction and elimination rules for the defined constants
+ - standard properties (idempotency, commutativity, associativity, compatibility, distributivity) for the defined constants
+ - Cantor's diagonalization theorem: [cantor_diag]
+
+% \hrule %
+
+ We require Toolbox relations and the underlying theory.
+
+ *)
+Require Export tbs_rel.
+
+Section Subset_Operations_Definitions.
+
+ Section finitary_subset_operations.
+
+(** Subset and: [(SAnd S U V)] corresponds to $ U \sand_S V $. *)
+ Definition SAnd: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
+ Intros S U V a.
+ Exact (LAnd (U a) (V a)).
+ Defined.
+
+(** Subset or: [(SOr S U V)] corresponds to $ U \sor_S V $. *)
+ Definition SOr: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
+ Intros S U V a.
+ Exact (LOr (U a) (V a)).
+ Defined.
+
+(** Subset implies: [(SImp S U V)] corresponds to $ U \simp_S V $. *)
+ Definition SImp: (S:Set) (S -> Set) -> (S -> Set) -> (S -> Set).
+ Intros S U V a.
+ Exact (U a)->(V a).
+ Defined.
+
+(** Subset not: [(SNot S U)] corresponds to $ \snot_S U $. *)
+ Definition SNot: (S:Set) (S -> Set) -> (S -> Set).
+ Intros S U a.
+ Exact (LNot (U a)).
+ Defined.
+
+ End finitary_subset_operations.
+
+ Section infinitary_subset_operations.
+
+(** Subset all: [(SAll I S F)] corresponds to $ \bigsand_S\subset{F(i) \st i \in I} $. *)
+ Definition SAll: (I,S:Set) (I -> S -> Set) -> (S -> Set).
+ Intros I S F a.
+ Exact (i:I)(F i a).
+ Defined.
+
+(** Subset exists: [(SEx I S F)] corresponds to $ \bigsor_S\subset{F(i) \st i \in I} $. *)
+ Definition SEx: (I,S:Set) (I -> S -> Set) -> (S -> Set).
+ Intros I S F a.
+ Exact (LEx I [i](F i a)).
+ Defined.
+
+ End infinitary_subset_operations.
+
+End Subset_Operations_Definitions.
+
+Section Subset_Operations_Results.
+
+ Section subset_binary_intersection.
+
+(** Subset and, epsilon introduction: $ a \e U \limp a \e V \limp a \e U \sand V $. *)
+ Theorem sand_eps_i: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a V) -> (Eps S a (SAnd S U V)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SAnd.
+ MApply 'land_i.
+ MApply 'eps_e.
+ MApply 'eps_e.
+ Qed.
+
+(** Subset and, epsilon elimination 2: $ a \e U \sand V \limp a \e U $. *)
+ Theorem sand_eps_e2: (S:Set; V,U:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a U).
+ Intros.
+ MApply 'eps_i.
+ MApply '(land_e2 (V a)).
+ Fold (SAnd S U V a).
+ MApply 'eps_e.
+ Qed.
+
+(** Subset and, epsilon elimination 1: $ a \e U \sand V \limp a \e V $. *)
+ Theorem sand_eps_e1: (S:Set; U,V:S->Set; a:S) (Eps S a (SAnd S U V)) -> (Eps S a V).
+ Intros.
+ MApply 'eps_i.
+ MApply '(land_e1 (U a)).
+ Fold (SAnd S U V a).
+ MApply 'eps_e.
+ Qed.
+
+(** Subset and, epsilon criterion: $ a \e U \land a \e V \liff a \e U \sand V $ *)
+ Theorem sand_eps: (S:Set; U,V:S->Set; a:S) (LIff (LAnd (Eps S a U) (Eps S a V)) (Eps S a (SAnd S U V))).
+ Intros.
+ MApply 'liff_i.
+ MApply 'sand_eps_i.
+ MApply '(land_e2 (Eps S a V)).
+ MApply '(land_e1 (Eps S a U)).
+ MApply 'land_i.
+ MApply '(sand_eps_e2 S V).
+ MApply '(sand_eps_e1 S U).
+ Qed.
+
+(** Subset and, sub or equal elimination 2: $ U \sand V \sub U $. *)
+ Theorem sand_sbe_e2: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) U).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(sand_eps_e2 S V).
+ Qed.
+
+(** Subset and, sub or equal elimination 1: $ U \sand V \sub V $. *)
+ Theorem sand_sbe_e1: (S:Set; U,V:S->Set) (SbE S (SAnd S U V) V).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(sand_eps_e1 S U).
+ Qed.
+
+(** Subset and, sub or equal introduction: $ W \sub U \limp W \sub V \limp W \sub U \sand V $. *)
+ Theorem sand_sbe_i: (S:Set; W,U,V:S->Set) (SbE S W U) -> (SbE S W V) -> (SbE S W (SAnd S U V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sand_eps_i.
+ MApply '(sbe_e S W).
+ MApply '(sbe_e S W).
+ Qed.
+
+(** Subset and, sub or equal compatibility 2: $ U \sub V \limp U \sand W \sub V \sand W $. *)
+ Theorem sand_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S U W) (SAnd S V W)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply '(sbe_t S U).
+ MApply 'sand_sbe_e2.
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Subset and, sub or equal subset top: $ U \sub \stop \sand U $. *)
+ Theorem sand_sbe_stop: (S:Set; U:S->Set) (SbE S U (SAnd S (STop S) U)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'stop_sbe_i.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset and, sub or equal idempotency: $ U \sub U \sand U $. *)
+ Theorem sand_sbe_r: (S:Set; U:S->Set) (SbE S U (SAnd S U U)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'sbe_r.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset and, idempotency $ U \sand U = U $. *)
+ Theorem sand_r: (S:Set; U:S->Set) (SEq S (SAnd S U U) U).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sand_sbe_e2.
+ MApply 'sand_sbe_r.
+ Qed.
+
+(** Subset and, sub or equal commutativity: $ V \sand U \sub U \sand V $. *)
+ Theorem sand_sbe_s: (S:Set; U,V:S->Set) (SbE S (SAnd S V U) (SAnd S U V)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'sand_sbe_e1.
+ MApply 'sand_sbe_e2.
+ Qed.
+
+(** Subset and, commutativity: $ V \sand U = U \sand V $. *)
+ Theorem sand_s: (S:Set; U,V:S->Set) (SEq S (SAnd S V U) (SAnd S U V)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sand_sbe_s.
+ MApply 'sand_sbe_s.
+ Qed.
+
+(** Subset and, sub or equal associativity 1: $ U \sand (V \sand W) \sub (U \sand V) \sand W $. *)
+ Theorem sand_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'sand_sbe_i.
+ MApply 'sand_sbe_e2.
+ MApply '(sbe_t S (SAnd S V W)).
+ MApply 'sand_sbe_e1.
+ MApply 'sand_sbe_e2.
+ MApply '(sbe_t S (SAnd S V W)).
+ MApply 'sand_sbe_e1.
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Subset and, sub or equal associativity 2: $ (U \sand V) \sand W \sub U \sand (V \sand W) $. *)
+ Theorem sand_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SAnd S (SAnd S U V) W) (SAnd S U (SAnd S V W))).
+ Intros.
+ MApply '(sbe_t S (SAnd S W (SAnd S U V))).
+ MApply 'sand_sbe_s.
+ MApply '(sbe_t S (SAnd S (SAnd S V W) U)).
+ MApply '(sbe_t S (SAnd S (SAnd S W U) V)).
+ MApply 'sand_sbe_a1.
+ MApply '(sbe_t S (SAnd S V (SAnd S W U))).
+ MApply 'sand_sbe_s.
+ MApply 'sand_sbe_a1.
+ MApply 'sand_sbe_s.
+ Qed.
+
+(** Subset and, associativity: $ U \sand (V \sand W) = (U \sand V) \sand W $. *)
+ Theorem sand_a: (S:Set; U,V,W:S->Set) (SEq S (SAnd S U (SAnd S V W)) (SAnd S (SAnd S U V) W)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sand_sbe_a1.
+ MApply 'sand_sbe_a2.
+ Qed.
+
+(** Subset and, sub or equal compatibility 1: $ U \sub V \limp W \sand U \sub W \sand V $. *)
+ Theorem sand_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SAnd S W U) (SAnd S W V)).
+ Intros.
+ MApply '(sbe_t S (SAnd S U W)).
+ MApply 'sand_sbe_s.
+ MApply '(sbe_t S (SAnd S V W)).
+ MApply 'sand_sbe_c2.
+ MApply 'sand_sbe_s.
+ Qed.
+
+(** Subset and, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sand W \sub V \sand X $. *)
+ Theorem sand_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SAnd S U W) (SAnd S V X)).
+ Intros.
+ MApply '(sbe_t S (SAnd S V W)).
+ MApply 'sand_sbe_c2.
+ MApply 'sand_sbe_c1.
+ Qed.
+
+ End subset_binary_intersection.
+
+ Section subset_binary_union.
+
+(** Subset or, epsilon introduction 2: $ a \e U \limp a \e U \sor V $. *)
+ Theorem sor_eps_i2: (S:Set; U,V:S->Set; a:S) (Eps S a U) -> (Eps S a (SOr S U V)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SOr.
+ MApply 'in_l.
+ MApply 'eps_e.
+ Qed.
+
+(** Subset or, epsilon introduction 1: $ a \e V \limp a \e U \sor V $. *)
+ Theorem sor_eps_i1: (S:Set; U,V:S->Set; a:S) (Eps S a V) -> (Eps S a (SOr S U V)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SOr.
+ MApply 'in_r.
+ MApply 'eps_e.
+ Qed.
+
+(** Subset or, epsilon elimination: $ (a \e U \limp T) \limp (a \e V \limp T) \limp a \e U \sor V \limp T $. *)
+ Theorem sor_eps_e: (S:Set; a:S; U,V:S->Set; T:Set) ((Eps S a U) -> T) -> ((Eps S a V) -> T) -> (Eps S a (SOr S U V)) -> T.
+ Intros.
+ MCut '(SOr S U V a).
+ MApply 'eps_e.
+ MApply '(lor_e (U a) (V a)).
+ MApply 'H.
+ MApply 'eps_i.
+ MApply 'H0.
+ MApply 'eps_i.
+ Qed.
+
+(** Subset or, epsilon criterion: $ a \e U \lor a \e V \liff a \e U \sor V $. *)
+ Theorem sor_eps: (S:Set; U,V:S->Set; a:S) (LIff (LOr (Eps S a U) (Eps S a V)) (Eps S a (SOr S U V))).
+ Intros.
+ MApply 'liff_i.
+ MApply '(lor_e (Eps S a U) (Eps S a V)).
+ MApply 'sor_eps_i2.
+ MApply 'sor_eps_i1.
+ MApply '(sor_eps_e S a U V).
+ MApply 'in_l.
+ MApply 'in_r.
+ Qed.
+
+(** Subset or, sub or equal introduction 2: $ U \sub U \sor V $. *)
+ Theorem sor_sbe_i2: (S:Set; U,V:S->Set) (SbE S U (SOr S U V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sor_eps_i2.
+ Qed.
+
+(** Subset or, sub or equal introduction 1: $ V \sub U \sor V $. *)
+ Theorem sor_sbe_i1: (S:Set; U,V:S->Set) (SbE S V (SOr S U V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sor_eps_i1.
+ Qed.
+
+(** Subset or, sub or equal elimination: $ U \sub W \limp V \sub W \limp U \sor V \sub W $. *)
+ Theorem sor_sbe_e: (S:Set; W,U,V:S->Set) (SbE S U W) -> (SbE S V W) -> (SbE S (SOr S U V) W).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(sor_eps_e S a U V).
+ MApply '(sbe_e S U).
+ MApply '(sbe_e S V).
+ Qed.
+
+(** Subset or, sub or equal compatibility 2: $ U \sub V \limp U \sor W \sub V \sor W $. *)
+ Theorem sor_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S U W) (SOr S V W)).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply '(sbe_t S V).
+ MApply 'sor_sbe_i2.
+ MApply 'sor_sbe_i1.
+ Qed.
+
+(** Subset or, sub or equal idempotency: $ U \sor U \sub U $. *)
+ Theorem sor_sbe_r: (S:Set; U:S->Set) (SbE S (SOr S U U) U).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply 'sbe_r.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset or, idempotency: $ U \sor U = U $. *)
+ Theorem sor_r: (S:Set; U:S->Set) (SEq S (SOr S U U) U).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sor_sbe_r.
+ MApply 'sor_sbe_i2.
+ Qed.
+
+(** Subset or, sub or equal commutativity: $ V \sor U \sub U \sor V $. *)
+ Theorem sor_sbe_s: (S:Set; U,V:S->Set) (SbE S (SOr S V U) (SOr S U V)).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply 'sor_sbe_i1.
+ MApply 'sor_sbe_i2.
+ Qed.
+
+(** Subset or, commutativity: $ V \sor U = U \sor V $. *)
+ Theorem sor_s: (S:Set; U,V:S->Set) (SEq S (SOr S V U) (SOr S U V)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sor_sbe_s.
+ MApply 'sor_sbe_s.
+ Qed.
+
+(** Subset or, sub or equal associativity 1: $ U \sor (V \sor W) \sub (U \sor V) \sor W $. *)
+ Theorem sor_sbe_a1: (S:Set; U,V,W:S->Set) (SbE S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
+ Intros.
+ MApply 'sor_sbe_e.
+ MApply '(sbe_t S (SOr S U V)).
+ MApply 'sor_sbe_i2.
+ MApply 'sor_sbe_i2.
+ MApply 'sor_sbe_e.
+ MApply '(sbe_t S (SOr S U V)).
+ MApply 'sor_sbe_i1.
+ MApply 'sor_sbe_i2.
+ MApply 'sor_sbe_i1.
+ Qed.
+
+(** Subset or, sub or equal associativity 2: $ (U \sor V) \sor W \sub U \sor (V \sor W) $. *)
+ Theorem sor_sbe_a2: (S:Set; U,V,W:S->Set) (SbE S (SOr S (SOr S U V) W) (SOr S U (SOr S V W))).
+ Intros.
+ MApply '(sbe_t S (SOr S W (SOr S U V))).
+ MApply 'sor_sbe_s.
+ MApply '(sbe_t S (SOr S (SOr S V W) U)).
+ MApply '(sbe_t S (SOr S (SOr S W U) V)).
+ MApply 'sor_sbe_a1.
+ MApply '(sbe_t S (SOr S V (SOr S W U))).
+ MApply 'sor_sbe_s.
+ MApply 'sor_sbe_a1.
+ MApply 'sor_sbe_s.
+ Qed.
+
+(** Subset or, associativity: $ U \sor (V \sor W) = (U \sor V) \sor W $. *)
+ Theorem sor_a: (S:Set; U,V,W:S->Set) (SEq S (SOr S U (SOr S V W)) (SOr S (SOr S U V) W)).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sor_sbe_a1.
+ MApply 'sor_sbe_a2.
+ Qed.
+
+(** Subset or, sub or equal compatibility 1: $ U \sub V \limp W \sor U \sub W \sor V $. *)
+ Theorem sor_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SOr S W U) (SOr S W V)).
+ Intros.
+ MApply '(sbe_t S (SOr S U W)).
+ MApply 'sor_sbe_s.
+ MApply '(sbe_t S (SOr S V W)).
+ MApply 'sor_sbe_c2.
+ MApply 'sor_sbe_s.
+ Qed.
+
+(** Subset or, sub or equal compatibility: $ U \sub V \limp W \sub X \limp U \sor W \sub V \sor X $. *)
+ Theorem sor_sbe_c: (S:Set; U,V,W,X:S->Set) (SbE S U V) -> (SbE S W X) -> (SbE S (SOr S U W) (SOr S V X)).
+ Intros.
+ MApply '(sbe_t S (SOr S V W)).
+ MApply 'sor_sbe_c2.
+ MApply 'sor_sbe_c1.
+ Qed.
+
+ End subset_binary_union.
+
+ Section subset_implication.
+
+(** Subset implies, epsilon introduction: $ (a \e U \limp a \e V) \limp a \e U \simp V $. *)
+ Theorem simp_eps_i: (S:Set; U,V:S->Set; a:S) ((Eps S a U) -> (Eps S a V)) -> (Eps S a (SImp S U V)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SImp.
+ Intros.
+ MApply 'eps_e.
+ MApply 'H.
+ MApply 'eps_i.
+ Qed.
+
+(** Subset implies, epsilon elimination: $ a \e U \simp V \limp a \e U \limp a \e V $. *)
+ Theorem simp_eps_e: (S:Set; U,V:S->Set; a:S) (Eps S a (SImp S U V)) -> (Eps S a U) -> (Eps S a V).
+ Intros.
+ MApply 'eps_i.
+ Apply (mcut (U a)).
+ MApply 'eps_e.
+ MApply '(eps_e S a).
+ Qed.
+
+(** Subset implies, epsilon criterion: $ a \e U \simp V \liff (a \e U \limp a \e V) $. *)
+ Theorem simp_eps: (S:Set; U,V:S->Set; a:S) (LIff (Eps S a (SImp S U V)) (Eps S a U) -> (Eps S a V)).
+ Intros.
+ MApply 'liff_i.
+ MApply '(simp_eps_e S U).
+ MApply 'simp_eps_i.
+ MApply 'H.
+ Qed.
+
+(** Subset implies, sub or equal elimination: $ W \sub U \simp V \limp W \sand U \sub V $. *)
+ Theorem simp_sbe_e: (S:Set; U,V,W:S->Set) (SbE S W (SImp S U V)) -> (SbE S (SAnd S W U) V).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(simp_eps_e S U).
+ MApply '(sbe_e S W).
+ MApply '(sand_eps_e2 S U).
+ MApply '(sand_eps_e1 S W).
+ Qed.
+
+(** Subset implies, sub or equal introduction: $ W \sand U \sub V \limp W \sub U \simp V $. *)
+ Theorem simp_sbe_i: (S:Set; U,V,W:S->Set) (SbE S (SAnd S W U) V) -> (SbE S W (SImp S U V)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'simp_eps_i.
+ MApply '(sbe_e S (SAnd S W U)).
+ MApply 'sand_eps_i.
+ Qed.
+
+(** Subset implies, sub or equal compatibility 2: $ V \sub U \limp U \simp W \sub V \simp W $. *)
+ Theorem simp_sbe_c2: (S:Set; U,V,W:S->Set) (SbE S V U) -> (SbE S (SImp S U W) (SImp S V W)).
+ Intros.
+ MApply 'simp_sbe_i.
+ MApply '(sbe_t S (SAnd S (SImp S U W) U)).
+ MApply 'sand_sbe_c1.
+ MApply 'simp_sbe_e.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset implies, sub or equal compatibility 2: $ U \sub V \limp W \simp U \sub W \simp V $. *)
+ Theorem simp_sbe_c1: (S:Set; U,V,W:S->Set) (SbE S U V) -> (SbE S (SImp S W U) (SImp S W V)).
+ Intros.
+ MApply 'simp_sbe_i.
+ MApply '(sbe_t S U).
+ MApply 'simp_sbe_e.
+ MApply 'sbe_r.
+ Qed.
+
+(** Subset implies, subset top elimination: $ \stop \sub U \simp V \limp U \sub V $. *)
+ Theorem simp_stop_e: (S:Set; U,V:S->Set) (SbE S (STop S) (SImp S U V)) -> (SbE S U V).
+ Intros.
+ MApply '(sbe_t S (SAnd S (STop S) U)).
+ MApply 'sand_sbe_stop.
+ MApply 'simp_sbe_e.
+ Qed.
+
+(** Subset implies, subset top introduction: $ U \sub V \limp \stop \sub U \simp V $. *)
+ Theorem simp_stop_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SbE S (STop S) (SImp S U V)).
+ Intros.
+ MApply 'simp_sbe_i.
+ MApply '(sbe_t S U).
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Subset implies, subset top criterion: $ \stop \sub U \simp V \liff U \sub V $. *)
+ Theorem simp_stop: (S:Set; U,V:S->Set) (LIff (SbE S (STop S) (SImp S U V)) (SbE S U V)).
+ Intros.
+ MApply 'liff_i.
+ MApply 'simp_stop_e.
+ MApply 'simp_stop_i.
+ Qed.
+
+ End subset_implication.
+
+ Section subset_negation.
+
+(** Subset not, epsilon introduction: $ \lnot (a \e U) \limp a \e \snot U $. *)
+ Theorem snot_eps_i: (S:Set; U:S->Set; a:S) (LNot (Eps S a U)) -> (Eps S a (SNot S U)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SNot.
+ MApply 'lnot_i.
+ MApply '(lnot_e (Eps S a U)).
+ MApply 'eps_i.
+ Qed.
+
+(** Subset not, epsilon elimination: $ a \e \snot U \limp \lnot (a \e U) $. *)
+ Theorem snot_eps_e: (S:Set; U:S->Set; a:S) (Eps S a (SNot S U)) -> (LNot (Eps S a U)).
+ Unfold SNot.
+ Intros.
+ MApply 'lnot_i.
+ MApply '(lnot_e (U a)).
+ MApply '(eps_e S a [a0:S](LNot (U a0))).
+ MApply 'eps_e.
+ Qed.
+
+(** Subset not, epsilon criterion: $ \lnot (a \e U) \liff a \e \snot U $. *)
+ Theorem snot_eps: (S:Set; U:S->Set; a:S) (LIff (LNot (Eps S a U)) (Eps S a (SNot S U))).
+ Intros.
+ MApply 'liff_i.
+ MApply 'snot_eps_i.
+ MApply 'snot_eps_e.
+ Qed.
+
+(** Subset not, subset implication compatibility: $ \snot U = U \simp \sbot $. *)
+ Theorem snot_simp_c: (S:Set; U:S->Set) (SEq S (SNot S U) (SImp S U (SBot S))).
+ Intros.
+ MApply 'seq_i.
+ MApply 'simp_eps_i.
+ MCut 'Empty.
+ MApply '(lnot_e (Eps S a U)).
+ MApply 'snot_eps_e.
+ MElim 'H1 'efq.
+ MApply 'snot_eps_i.
+ MApply 'lnot_i.
+ MApply '(sbot_eps_e S a).
+ MApply '(simp_eps_e S U).
+ Qed.
+
+ End subset_negation.
+
+ Section subset_infinitary_intersection.
+
+(** Subset all, epsilon introduction: $ ((\lall i \in I)\ a \e F(i)) \limp a \e \bigsand\subset{F(i) \st i \in I} $. *)
+ Theorem sall_eps_i: (I,S:Set; F:(I->S->Set); a:S) ((i:I) (Eps S a (F i))) -> (Eps S a (SAll I S F)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SAll.
+ Intros.
+ MApply 'eps_e.
+ MApply '(H i).
+ Qed.
+
+(** Subset all, epsilon elimination: $ a \e \bigsand\subset{F(i) \st i \in I} \limp (\lall i \in I)\ a \e F(i) $. *)
+ Theorem sall_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SAll I S F)) -> (i:I) (Eps S a (F i)).
+ Intros.
+ MApply 'eps_i.
+ Apply (mcut (i:I)(F i a)).
+ MApply '(eps_e S a).
+ Intros.
+ MApply '(H0 i).
+ Qed.
+
+(** Subset all, epsilon criterion: $ a \e \bigsand\subset{F(i) \st i \in I} \liff (\lall i \in I)\ a \e F(i) $. *)
+ Theorem sall_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SAll I S F)) (i:I) (Eps S a (F i))).
+ Intros.
+ MApply 'liff_i.
+ MApply '(sall_eps_e I).
+ MApply 'sall_eps_i.
+ MApply '(H i).
+ Qed.
+
+(** Subset all, sub or equal elimination: $ (\lall i \in I)\ \bigsand\subset{F(i) \st i \in I} \sub F(i) $. *)
+ Theorem sall_sbe_e: (I,S:Set; F:(I->S->Set); i:I) (SbE S (SAll I S F) (F i)).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(sall_eps_e I).
+ Qed.
+
+(** Subset all, sub or equal introduction: $ ((\lall i \in I)\ W \sub F(i)) \limp W \sub \bigsand\subset{F(i) \st i \in I} $. *)
+ Theorem sall_sbe_i: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S W (F i))) -> (SbE S W (SAll I S F)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sall_eps_i.
+ MApply '(sbe_e S W).
+ MApply 'H.
+ Qed.
+
+ End subset_infinitary_intersection.
+
+ Section subset_infinitary_union.
+
+(** Subset exists, epsilon introduction: $ ((\lex i \in I)\ a \e F(i)) \limp a \e \bigsor\subset{F(i) \st i \in I} $. *)
+ Theorem sex_eps_i: (I,S:Set; F:(I->S->Set); a:S) (LEx I [i](Eps S a (F i))) -> (Eps S a (SEx I S F)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SEx.
+ MElim 'H 'lex_e.
+ MApply '(lex_i I a0).
+ MApply 'eps_e.
+ Qed.
+
+(** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \limp (\lex i \in I)\ a \e F(i) $. *)
+ Theorem sex_eps_e: (I,S:Set; F:(I->S->Set); a:S) (Eps S a (SEx I S F)) -> (LEx I [i](Eps S a (F i))).
+ Intros.
+ MCut '(SEx I S F a).
+ MApply 'eps_e.
+ MElim 'H0 'lex_e.
+ MApply '(lex_i I a0).
+ MApply 'eps_i.
+ Qed.
+
+(** Subset exists, epsilon elimination: $ a \e \bigsor\subset{F(i) \st i \in I} \liff (\lex i \in I)\ a \e F(i) $. *)
+ Theorem sex_eps: (I,S:Set; F:(I->S->Set); a:S) (LIff (Eps S a (SEx I S F)) (LEx I [i](Eps S a (F i)))).
+ Intros.
+ MApply 'liff_i.
+ MApply 'sex_eps_e.
+ MApply 'sex_eps_i.
+ Qed.
+
+(** Subset exists, sub or equal introduction: $ (\lall i \in I)\ F(i) \sub \bigsor\subset{F(i) \st i \in I} $. *)
+ Theorem sex_sbe_i: (I,S:Set; F:(I->S->Set); i:I) (SbE S (F i) (SEx I S F)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sex_eps_i.
+ MApply '(lex_i I i).
+ Qed.
+
+(** Subset exists, sub or equal elimination: $ ((\lall i \in I)\ F(i) \sub W) \limp \bigsor\subset{F(i) \st i \in I} \sub W $. *)
+ Theorem sex_sbe_e: (I,S:Set; F:(I->S->Set); W:S->Set) ((i:I)(SbE S (F i) W)) -> (SbE S (SEx I S F) W).
+ Intros.
+ MApply 'sbe_i.
+ MCut '(LEx I [i:I](Eps S a (F i))).
+ MApply 'sex_eps_e.
+ MElim 'H1 'lex_e.
+ MApply '(sbe_e S (F a0)).
+ MApply 'H.
+ Qed.
+
+ End subset_infinitary_union.
+
+ Section subset_frame.
+
+(** Frame, subset and introduction: $ U \sub V \limp U \sand V = U $. *)
+ Theorem frame_sand_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SAnd S U V) U).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'sand_sbe_e2.
+ MApply '(sbe_t S (SAnd S U U)).
+ MApply 'sand_sbe_r.
+ MApply 'sand_sbe_c1.
+ Qed.
+
+(** Frame, subset and elimination: $ U \sand V = U \limp U \sub V $. *)
+ Theorem frame_sand_e: (S:Set; U,V:S->Set) (SEq S (SAnd S U V) U) -> (SbE S U V).
+ Intros.
+ MApply '(sbe_t S (SAnd S U V)).
+ MApply '(land_e1 (SbE S (SAnd S U V) U)).
+ MApply 'seq_sbe_e.
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Frame, subset or introduction: $ U \sub V \limp U \sor V = V $. *)
+ Theorem frame_sor_i: (S:Set; U,V:S->Set) (SbE S U V) -> (SEq S (SOr S U V) V).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply '(sbe_t S (SOr S V V)).
+ MApply 'sor_sbe_c2.
+ MApply 'sor_sbe_r.
+ MApply 'sor_sbe_i1.
+ Qed.
+
+(** Frame, subset or elimination: $ U \sor V = V \limp U \sub V $. *)
+ Theorem frame_sor_e: (S:Set; U,V:S->Set) (SEq S (SOr S U V) V) -> (SbE S U V).
+ Intros.
+ MApply '(sbe_t S (SOr S U V)).
+ MApply 'sor_sbe_i2.
+ MApply '(land_e2 (SbE S V (SOr S U V))).
+ MApply 'seq_sbe_e.
+ Qed.
+
+(** Frame, subset exists introduction: $ \bigsor\subset{F(i) \st i \in I} \sand W \sub \bigsor\subset{F(i) \sand W \st i \in I} $. *)
+ Theorem frame_sex_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'sex_eps_i.
+ MCut '(Eps S a (SEx I S F)).
+ MApply '(sand_eps_e2 S W).
+ MCut '(LEx I [i:I](Eps S a (F i))).
+ MApply 'sex_eps_e.
+ MElim 'H1 'lex_e.
+ MApply '(lex_i I a0).
+ MApply 'sand_eps_i.
+ MApply '(sand_eps_e1 S (SEx I S F)).
+ Qed.
+
+(** Frame, subset exists elimination: $ \bigsor\subset{F(i) \sand W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \sand W $. *)
+ Theorem frame_sex_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SEx I S [i]
+(SAnd S (F i) W)) (SAnd S (SEx I S F) W)).
+ Intros.
+ MApply 'sand_sbe_i.
+ MApply 'sex_sbe_e.
+ MApply '(sbe_t S (F i)).
+ MApply 'sand_sbe_e2.
+ MApply 'sex_sbe_i.
+ MApply 'sex_sbe_e.
+ MApply 'sand_sbe_e1.
+ Qed.
+
+(** Frame, subset exists distributivity: $ \bigsor\subset{F(i) \st i \in I} \sand W = \bigsor\subset{F(i) \sand W \st i \in I} $. *)
+ Theorem frame_sex_d: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SAnd S (SEx I S F) W) (SEx I S [i](SAnd S (F i) W))).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'frame_sex_i.
+ MApply 'frame_sex_e.
+ Qed.
+
+(** Frame, subset implies elimination: $ \bigsor\subset{F(i) \st i \in I} \simp W \sub \bigsand\subset{F(i) \simp W \st i \in I} $. *)
+ Theorem frame_simp_e: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
+ Intros.
+ MApply 'sall_sbe_i.
+ MApply 'simp_sbe_c2.
+ MApply 'sex_sbe_i.
+ Qed.
+
+(** Frame, subset implies introduction: $ \bigsand\subset{F(i) \simp W \st i \in I} \sub \bigsor\subset{F(i) \st i \in I} \simp W $. *)
+ Theorem frame_simp_i: (I,S:Set; F:(I->S->Set); W:S->Set) (SbE S (SAll I S [i](SImp S (F i) W)) (SImp S (SEx I S F) W)).
+ Intros.
+ MApply 'sbe_i.
+ MApply 'simp_eps_i.
+ MCut '(LEx I [i:I](Eps S a (F i))).
+ MApply 'sex_eps_e.
+ MElim 'H1 'lex_e.
+ MApply '(simp_eps_e S (F a0)).
+ MApply '(sall_eps_e I S [i:I](SImp S (F i) W)).
+ Qed.
+
+(** Frame, subset implies compatibility: $ \bigsor\subset{F(i) \st i \in I} \simp W = \bigsand\subset{F(i) \simp W \st i \in I} $. *)
+ Theorem frame_simp_c: (I,S:Set; F:(I->S->Set); W:S->Set) (SEq S (SImp S (SEx I S F) W) (SAll I S [i](SImp S (F i) W))).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'frame_simp_e.
+ MApply 'frame_simp_i.
+ Qed.
+
+ End subset_frame.
+
+ Section cantor_diagonalization.
+
+(** [(D S F)] is Cantor's subset $ D_F $. *)
+ Local D: (S:Set) (S -> S -> Set) -> (S -> Set).
+ Intros S F.
+ Exact (SNot S [a:S](F a a)).
+ Defined.
+
+(** Cantor's diagonalization: $ (\lall b \in S)\ \lnot (F(b) = D_F) $. *)
+ Theorem cantor_diag: (S:Set; F:S->S->Set) (b:S) (LNot (SEq S (F b) (D S F))).
+ Intros.
+ MApply 'lnot_i.
+ MCut '(LIff (Eps S b (F b)) (LNot (Eps S b (F b)))).
+ MApply 'liff_i.
+ MApply 'snot_eps_e.
+ Change (Eps S b (D S F)).
+ MApply '(seq_e1 S (F b)).
+ MApply '(seq_e2 S (D S F)).
+ Change (Eps S b (SNot S (F b))).
+ MApply 'snot_eps_i.
+ MApply '(lnot_liff_lbot (Eps S b (F b))).
+ Qed.
+
+ End cantor_diagonalization.
+
+End Subset_Operations_Results.
--- /dev/null
+(** 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.
+
--- /dev/null
+Require Export tbs_op.
+
+Section Subset_Relative_Operations_Definitions.
+
+ Section relative_membership.
+
+ Definition REps: (I,S:Set) S -> (I -> S -> Set) -> Set := [I,S;a;F](LEx I [i](Eps S a (F i))).
+
+ End relative_membership.
+
+ Section infinitary_subset_relative_operations.
+
+ Definition SRAll: (I:Set; T:I->Set; S:Set) ((i:I) (T i) -> (S -> Set)) -> (S -> Set) := [I;T;S;R;a](RAll I T [i](REps (T i) S a (R i))).
+
+ Definition SREx: (I:Set; T:I->Set; S:Set) ((i:I) (T i) -> (S -> Set)) -> (S -> Set) := [I;T;S;R;a](REx I T [i](REps (T i) S a (R i))).
+
+ End infinitary_subset_relative_operations.
+
+End Subset_Relative_Operations_Definitions.
+
+Section Subset_Relative_Operations_Results.
+
+ Section relative_epsilon_conditions.
+
+ Theorem reps_i: (I:Set; i:I; S:Set; a:S; F:I->S->Set) (Eps S a (F i)) -> (REps I S a F).
+ Intros.
+ Unfold REps.
+ MApply '(lex_i I i).
+ Qed.
+
+ Theorem reps_e: (I,S:Set; a:S; F:I->S->Set; P:Set) ((i:I) (Eps S a (F i)) -> P) -> (REps I S a F) -> P.
+ Intros.
+ Unfold REps in H0.
+ MElim 'H0 'lex_e.
+ MApply '(H a0).
+ Qed.
+
+ End relative_epsilon_conditions.
+
+ Section infinitary_relative_intersection.
+
+ Theorem srall_eps_i: (I:Set; T:I->Set; S:Set; a:S; R:(i:I)(T i)->(S->Set)) ((i:I) (REps (T i) S a (R i))) -> (Eps S a (SRAll I T S R)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SRAll.
+ MApply 'rall_i.
+ MApply '(H a0).
+ Qed.
+
+ Theorem srall_eps_e: (I:Set; i:I; T:I->Set) (T i) -> (S:Set; a:S; R:(i:I)(T i)->(S->Set)) (Eps S a (SRAll I T S R)) -> (REps (T i) S a (R i)).
+ Intros.
+ MCut '(SRAll I T S R a).
+ MApply 'eps_e.
+ Unfold SRAll in H1.
+ MApply '(rall_e I i T).
+ MApply 'eps_i.
+ Qed.
+
+ End infinitary_relative_intersection.
+
+ Section infinitary_relative_union.
+
+ Theorem srex_eps_i: (I:Set; i:I; S:Set; a:S; T:I->Set; R:(i:I)(T i)->(S->Set)) (REps (T i) S a (R i)) -> (Eps S a (SREx I T S R)).
+ Intros.
+ MApply 'eps_i.
+ Unfold SREx.
+ MApply '(rex_i I i).
+ MApply 'eps_i.
+ MApply '(reps_e (T i) S a (R i)).
+ Qed.
+
+ Theorem srex_eps_e: (I:Set; T:I->Set; S:Set; a:S; R:(i:I)(T i)->(S->Set)) (Eps S a (SREx I T S R)) -> (LEx I [i](REps (T i) S a (R i))).
+ Intros.
+ MCut '(SREx I T S R a).
+ MApply 'eps_e.
+ Unfold SREx in H0.
+ MApply '(rex_e I T [i:I](REps (T i) S a (R i))).
+ MApply '(lex_i I a0).
+ Qed.
+
+ Theorem srex_sbe: (I:Set; V,W:I->Set; S:Set; F:I->S->Set) (SbE I V W) -> (SbE S (SREx I V S [i;_](F i)) (SREx I W S [i;_](F i))).
+ Intros.
+ MApply 'sbe_i.
+ MCut '(LEx I [i:?](REps (V i) S a [_:?](F i))).
+ MApply '(srex_eps_e I V S a [i:?; _:(V i)](F i)).
+ MElim 'H1 'lex_e.
+ MApply '(srex_eps_i I a0).
+ MCut '(W a0).
+ MApply 'eps_e.
+ MApply '(sbe_e I V).
+ MApply 'eps_i.
+ MApply '(reps_e (V a0) S a [_:(V a0)](F a0)).
+ MApply '(reps_i (W a0) H2).
+ MApply '(reps_e (V a0) S a [_:(V a0)](F a0)).
+ Qed.
+
+ Theorem srex_sing_e: (S:Set; U:S->Set) (SbE S (SREx S U S [a;_](Sing S a)) U).
+ Intros.
+ MApply 'sbe_i.
+ MCut '(LEx S [b:?](REps (U b) S a [_:?](Sing S b))).
+ MApply '(srex_eps_e S U S a [a0:S; _:(U a0)](Sing S a0)).
+ MElim 'H0 'lex_e.
+ MApply '(reps_e (U a0) S a [_:(U a0)](Sing S a0)).
+ MCut '(Id S a0 a).
+ MApply 'sing_eps_e.
+ MApply '(id_repl S a a0).
+ MApply 'eps_i.
+ Qed.
+
+ Theorem srex_sing_i: (S:Set; U:S->Set) (SbE S U (SREx S U S [a;_](Sing S a))).
+ Intros.
+ MApply 'sbe_i.
+ MApply '(srex_eps_i S a).
+ MCut '(U a).
+ MApply 'eps_e.
+ MApply '(reps_i (U a) H0).
+ MApply 'sing_eps_i.
+ Qed.
+
+ Theorem srex_sing: (S:Set; U:S->Set) (SEq S (SREx S U S [a;_](Sing S a)) U).
+ Intros.
+ MApply 'seq_sbe_i.
+ MApply 'srex_sing_e.
+ MApply 'srex_sing_i.
+ Qed.
+
+ End infinitary_relative_union.
+
+End Subset_Relative_Operations_Results.
+
--- /dev/null
+Require Export Standard.
+
+Section Fin_Definitions.
+
+ Section finite_sets.
+
+ Definition Fin: N -> Set := (NatFam [_]Set Empty [_](LOr One)).
+
+(* Constructors: first element, next element *)
+ Definition ffe: (n:N) (Fin (succ n)).
+ Intros.
+ MApply '(in_l One (Fin n) tt).
+ Defined.
+
+ Definition fne: (n:N) (Fin n) -> (Fin (succ n)).
+ Intros.
+ MApply '(in_r One (Fin n)).
+ Defined.
+
+(* Eliminator *)
+ Definition finrec: (n:N; P:(Fin (succ n))->Set) (P (ffe n)) -> ((a:(Fin n))(P (fne n a))) -> (p:(Fin (succ n))) (P p).
+ Intros.
+ MElim 'p '(when One (Fin n)).
+ MElim 's 'onerec.
+ MApply '(H0 t).
+ Defined.
+
+(* Predecessor *)
+ Definition fpe: (n:N) (Fin (succ (succ n))) -> (Fin (succ n)).
+ Intros.
+ MElim 'H '(finrec (succ n)).
+ MApply '(ffe n).
+ Defined.
+
+(* Injection of (Fin (succ n)) in N *)
+ Definition fn: (n:N) (Fin (succ n)) -> N := (natrec [m](Fin (succ m))->N [_]zero [m;p](finrec (succ m) [_]N zero [a](succ (p a)))).
+(*
+ Intros n.
+ Elim n using natrec.
+ Intros.
+ Exact zero.
+ Intros.
+ Apply H.
+ Apply fpe.
+ Apply H0.
+*)
+
+(* Surjection of N in (Fin (succ n)): (ffe n) returned if m >= n *)
+ Definition nf: (n,m:N) (Fin (succ n)) := (natrec [m]N->(Fin (succ m)) [_](ffe zero) [n';p](natrec [_](Fin (succ (succ n'))) (ffe (succ n')) [m';p'](fne (succ n') (p m')))).
+
+(* Left injection of (Fin m) -> (Fin (add m n)) *)
+ Definition fil: (m,n:N) (Fin m) -> (Fin (add m n)) :=
+ (natrec [m](n:N) (Fin m) -> (Fin (add m n))
+ [n](efq [_](Fin (add zero n)))
+ [m';_](natrec [n](Fin (succ m')) -> (Fin (add (succ m') n))
+ [a]a [n';_;a](nf (add (succ m') n') (fn m' a)))).
+
+(* Right injection of (Fin n) -> (Fin (add m n)) *)
+ Definition fir: (m,n:N) (Fin n) -> (Fin (add m n)) :=
+ [m](natrec [n](Fin n) -> (Fin (add m n))
+ (efq [_](Fin m))
+ [n';_;a](nf (add m n') (add (fn n' a) m))).
+
+ End finite_sets.
+
+ Section explicit_finite_domain_functions.
+
+ Definition xfdf_list: (S:Set; n:N) ((Fin n) -> S) -> (List S) := [S](natrec [m]((Fin m)->S)->(List S) [_](empty S) [m;p;f](fr S (p [k](f (fne m k))) (f (ffe m)))).
+
+ Definition xfdf_add': (S:Set; m:N) ((Fin (succ m))->S) -> (n:N) ((Fin (succ n))->S) -> (Fin (add_three (succ m) n one)) -> S :=
+ [S;m;v;n;w;a](ite [_]S (w (nf n (sub (fn (add (succ m) n) a) (succ m))))
+ (v (nf m (fn (add (succ m) n) a)))
+ (b_le (fn (add (succ m) n) a) m)).
+
+ Definition xfdf_add: (S:Set; m:N) ((Fin m)->S) -> (n:N) ((Fin n)->S) -> (Fin (add m n)) -> S :=
+ [S](natrec [m]((Fin m)->S) -> (n:N) ((Fin n)->S) -> (Fin (add m n)) -> S
+ [_](natrec [n]((Fin n)->S) -> (Fin (add zero n)) -> S
+ [w]w [n';_;w;a](w (nf n' (fn (add zero n') a))))
+ [m';_;v](natrec [n]((Fin n)->S) -> (Fin (add (succ m') n)) -> S
+ [_]v [n';_](xfdf_add' S m' v n'))).
+
+ End explicit_finite_domain_functions.
+
+ Section finite_domain_functions.
+
+ Definition FDF: Set -> Set := [S](Sigma N [n](Fin n)->S).
+
+ Definition fdf_i: (S:Set; n:N) ((Fin n)->S) -> (FDF S) := [S](pair N [n](Fin n)->S).
+
+ Definition fdf_e: (S:Set; P:(FDF S)->Set) ((n:N; f:(Fin n)->S) (P (fdf_i S n f))) -> (v:(FDF S))(P v) :=
+ [S:Set](psplit N [n](Fin n)->S).
+
+ Definition fdf_n: (S:Set) (FDF S) -> N := [S](fdf_e S [_]N [a;_]a).
+
+ Definition fdf_f: (S:Set; v:(FDF S)) (Fin (fdf_n S v)) -> S := [S](fdf_e S [p](Fin (fdf_n S p))->S [_;p]p).
+
+ Definition fdf_empty: (S:Set) (FDF S) := [S](fdf_i S zero (efq [_]S)).
+
+ Definition fdf_fr: (S:Set) (FDF S) -> S -> (FDF S) := [S;v;a](fdf_i S (succ (fdf_n S v)) (when One (Fin (fdf_n S v)) [_]S [_]a (fdf_f S v))).
+(*
+ Definition lfdf: (S:Set) (List S) -> (FDF S) := [S](listrec S [_](FDF S) (fdf_empty S) [_](fdf_fr S)).
+*)
+ Definition fdfl: (S:Set) (FDF S) -> (List S) := [S](fdf_e S [_](List S) (xfdf_list S)).
+
+ Definition fdf_add: (S:Set) (FDF S) -> (FDF S) -> (FDF S) := [S;v;w](fdf_i S (add (fdf_n S v) (fdf_n S w)) (xfdf_add S (fdf_n S v) (fdf_f S v) (fdf_n S w) (fdf_f S w))).
+
+ End finite_domain_functions.
+
+End Fin_Definitions.
+
+Section Fin_Results.
+
+ Section fin_results.
+
+(* Immediate result used for reference
+ Theorem fpe_fne: (n:N; a:(Fin (succ n))) (Id (Fin (succ n)) (fpe n (fne (succ n) a)) a).
+*)
+ Theorem fne_ini: (n:N; a,b:(Fin n)) (Id (Fin (succ n)) (fne n a) (fne n b)) -> (Id (Fin n) a b).
+ Intros n.
+ Elim n using natrec.
+ Intros.
+ MElim a efq.
+ Intros.
+ MApply '(id_repl (Fin (succ n0)) a (fpe n0 (fne (succ n0) a))).
+ MApply '(id_repl (Fin (succ n0)) b (fpe n0 (fne (succ n0) b))).
+ MApply '(id_comp (Fin (succ (succ n0))) (Fin (succ n0)) (fpe n0)).
+ Qed.
+
+ Theorem fn_le: (n:N; a:(Fin (succ n))) (LE (fn n a) n).
+ Intros n.
+ Elim n using natrec; Intros.
+ MApply 'le_r.
+ MElim 'a '(finrec (succ n0)).
+ MApply 'le_wf.
+ MApply 'le_comp_succ.
+ MApply '(H a0).
+ Qed.
+
+ Theorem nfn': (n:N; a:(Fin (succ n)); m:N) (LE m n) -> (Id (Fin (succ n)) (nf n m) a) -> (Id N (fn n a) m).
+ Intros n.
+ Elim n using natrec.
+ Intros; Simpl.
+ MApply 'id_comm.
+ MApply '(le_zero m).
+ Intros n' H a m.
+ Elim a using (finrec (succ n')).
+ MElim 'm 'natrec.
+ MCut 'Empty.
+ Unfold fne in H2.
+ MApply '(lor_p4 One (Fin (succ n')) tt (nf n' n0)).
+ MElim 'H3 'efq.
+ Intros a'.
+ Elim m using natrec.
+ Simpl.
+ Intros.
+ MCut 'Empty.
+ MApply '(lor_p4 One (Fin (succ n')) tt a').
+ MElim 'H2 'efq.
+ Intros.
+ Simpl.
+ MApply '(id_comp N).
+ Change (Id N (fn n' a') n0).
+ MApply '(H a' n0).
+ Simpl in H2.
+ Change (Id (Fin (succ (succ n'))) (fne (succ n') (nf n' n0)) (fne (succ n') a')) in H2.
+ MApply 'fne_ini.
+ Qed.
+
+ Theorem nfn: (n:N; m:N) (LE m n) -> (Id N (fn n (nf n m)) m).
+ Intros.
+ MApply 'nfn'.
+ Qed.
+
+ Theorem fnf_fne: (n:N; a:(Fin n)) (Id (Fin (succ n)) (nf n (fn n (fne n a))) (fne n a)).
+ Intros n.
+ Elim n using natrec; Intros.
+ MElim 'a 'efq.
+ Elim a using (finrec n0); Intros.
+ MElim 'n0 'natrec.
+ MSimpl.
+ MApply '(id_comp (Fin (succ n0))).
+ MApply '(H a0).
+ Qed.
+
+ Theorem fnf: (n:N; a:(Fin (succ n))) (Id (Fin (succ n)) (nf n (fn n a)) a).
+ Intros.
+ Elim a using (finrec n); Intros.
+ MElim 'n 'natrec.
+ MApply 'fnf_fne.
+ Qed.
+
+ End fin_results.
+
+ Section xfdf_results.
+
+ Theorem xfdfl_lin: (S:Set; n:N; a:(Fin n); v:(Fin n)->S) (LIn S (v a) (xfdf_list S n v)).
+ Intros S n.
+ Elim n using natrec; Intros.
+ MElim a efq.
+ MSimpl.
+ MApply 'lin_fr_i.
+ MElim 'a '(finrec n0).
+ MApply 'in_r.
+ MApply 'in_l.
+ MApply '(H a0 [k:(Fin n0)](v (fne n0 k))).
+ Qed.
+
+ Theorem xfdfa_fil: (S:Set; m:N; a:(Fin m); v:(Fin m)->S; n:N; w:(Fin n)->S) (Id S (xfdf_add S m v n w (fil m n a)) (v a)).
+ Intros S m.
+ Elim m using natrec.
+ Intros a.
+ Elim a using efq.
+ Intros m' H a v n.
+ Elim n using natrec.
+ Intros.
+ MApply 'id_r.
+ Intros n' H0 w.
+ Simpl.
+ MCut '(LE (fn m' a) (add (succ m') n')).
+ MApply '(le_trans m').
+ MApply 'fn_le.
+ MApply '(id_repl N (add (succ m') n') (add_three m' n' one)).
+ MApply 'id_comm.
+ MApply '(add_succ m' n').
+ MApply '(le_add m' (succ n')).
+ Unfold xfdf_add'.
+ MApply '(id_repl Boole (b_le (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) m') true).
+ MApply 'id_comm.
+ Fold (LE (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) m').
+ MApply '(id_repl N (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) (fn m' a)).
+ MApply 'id_comm.
+ MApply 'nfn.
+ MApply 'fn_le.
+ Simpl.
+ MApply '(id_comp (Fin (succ m'))).
+ MApply '(id_repl N (fn (add (succ m') n') (nf (add (succ m') n') (fn m' a))) (fn m' a)).
+ MApply 'id_comm.
+ MApply 'nfn.
+ MApply 'fnf.
+ Qed.
+
+ Theorem xfdfa_fir: (S:Set; m:N; v:(Fin m)->S; n:N; a:(Fin n); w:(Fin n)->S) (Id S (xfdf_add S m v n w (fir m n a)) (w a)).
+ Intros S m.
+ Elim m using natrec.
+ Intros v n.
+ Elim n using natrec.
+ Intros a.
+ Elim a using efq.
+ Intros n' H a w.
+ MSimpl.
+ MApply '(id_comp (Fin (succ n'))).
+ MApply '(id_repl N (fn (add zero n') (nf (add zero n') (fn n' a))) (fn n' a)).
+ MApply 'id_comm.
+ MApply 'nfn.
+ MApply '(le_trans n').
+ MApply 'fn_le.
+ MApply '(id_repl N (add zero n') n').
+ MApply '(add_comm n' zero).
+ MApply 'le_r.
+ MApply 'fnf.
+ Intros m' H v n.
+ Elim n using natrec.
+ Intros a.
+ Elim a using efq.
+ Intros n' H' a w.
+ (MSimpl; Apply succ_fold). (**)
+ MCut '(LE (succ (add (fn n' a) m')) (add (succ m') n')).
+ MApply '(id_repl N (add (succ m') n') (succ (add m' n'))).
+ MApply 'id_comm.
+ MApply 'add_succ.
+ MApply 'le_comp_succ.
+ MApply '(id_repl N (add m' n') (add n' m')).
+ MApply 'add_comm.
+ MApply 'le_comp_add.
+ MApply 'fn_le.
+ Unfold xfdf_add'.
+ MApply '(id_repl Boole (b_le (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m')))) m') false).
+ MApply 'id_comm.
+ Fold (GT (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m')))) m').
+ MApply 'le_gt.
+ MApply '(id_repl N (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m')))) (succ (add (fn n' a) m'))).
+ MApply 'id_comm.
+ MApply 'nfn.
+ MApply 'le_comp_succ.
+ MApply '(id_repl N (add (fn n' a) m') (add m' (fn n' a))).
+ MApply 'add_comm.
+ MApply 'le_add.
+ MSimpl.
+ MApply 'pred_fold.
+ MApply '(id_comp (Fin (succ n'))).
+ MApply '(id_repl N (sub (pred (fn (add (succ m') n') (nf (add (succ m') n') (succ (add (fn n' a) m'))))) m') (fn n' a)).
+ MApply 'id_comm.
+ MApply 'add_sub_e.
+ MApply 'succ_pred_e.
+ MApply '(id_repl N (add m' (fn n' a)) (add (fn n' a) m')).
+ MApply 'add_comm.
+ MApply 'nfn.
+ MApply 'fnf.
+ Qed.
+
+ End xfdf_results.
+
+End Fin_Results.
+
projects / helm.git / commitdiff