From: Ferruccio Guidi Date: Sat, 4 Jun 2005 15:12:01 +0000 (+0000) Subject: a contribution about subset theory in an intuitionistic and predicative foundation X-Git-Tag: PRE_INDEX_1~70 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=65f400affe20fa3fe66b9a998ced5d6f64a23b45;p=helm.git a contribution about subset theory in an intuitionistic and predicative foundation --- diff --git a/helm/coq-contribs/SUBSETS/.cvsignore b/helm/coq-contribs/SUBSETS/.cvsignore new file mode 100644 index 000000000..419956872 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/.cvsignore @@ -0,0 +1 @@ +*.vo diff --git a/helm/coq-contribs/SUBSETS/.depend b/helm/coq-contribs/SUBSETS/.depend new file mode 100644 index 000000000..4229b4971 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/.depend @@ -0,0 +1,13 @@ +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 diff --git a/helm/coq-contribs/SUBSETS/Make b/helm/coq-contribs/SUBSETS/Make new file mode 100644 index 000000000..30cb09374 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/Make @@ -0,0 +1,14 @@ +# 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 diff --git a/helm/coq-contribs/SUBSETS/Makefile b/helm/coq-contribs/SUBSETS/Makefile new file mode 100644 index 000000000..45819834b --- /dev/null +++ b/helm/coq-contribs/SUBSETS/Makefile @@ -0,0 +1,196 @@ +############################################################################## +## 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 + diff --git a/helm/coq-contribs/SUBSETS/README b/helm/coq-contribs/SUBSETS/README new file mode 100644 index 000000000..caf37357d --- /dev/null +++ b/helm/coq-contribs/SUBSETS/README @@ -0,0 +1,45 @@ + + 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 and can be downloaded at: + + www.cs.unibo.it/cgi-bin/viewcvs.cgi/helm/coq-contribs/SUBSETS.tgz diff --git a/helm/coq-contribs/SUBSETS/Standard.v b/helm/coq-contribs/SUBSETS/Standard.v new file mode 100644 index 000000000..05f03f76e --- /dev/null +++ b/helm/coq-contribs/SUBSETS/Standard.v @@ -0,0 +1,5 @@ +Require Export st_base. +Require Export st_logic. +Require Export st_nat. +Require Export st_arith. + diff --git a/helm/coq-contribs/SUBSETS/Toolbox.v b/helm/coq-contribs/SUBSETS/Toolbox.v new file mode 100644 index 000000000..9217ef93c --- /dev/null +++ b/helm/coq-contribs/SUBSETS/Toolbox.v @@ -0,0 +1,12 @@ +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. diff --git a/helm/coq-contribs/SUBSETS/description b/helm/coq-contribs/SUBSETS/description new file mode 100644 index 000000000..ac4d053e9 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/description @@ -0,0 +1,13 @@ +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: diff --git a/helm/coq-contribs/SUBSETS/st_arith.v b/helm/coq-contribs/SUBSETS/st_arith.v new file mode 100644 index 000000000..800c74c48 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/st_arith.v @@ -0,0 +1,534 @@ +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. diff --git a/helm/coq-contribs/SUBSETS/st_base.v b/helm/coq-contribs/SUBSETS/st_base.v new file mode 100644 index 000000000..79b250724 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/st_base.v @@ -0,0 +1,185 @@ +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. diff --git a/helm/coq-contribs/SUBSETS/st_logic.v b/helm/coq-contribs/SUBSETS/st_logic.v new file mode 100644 index 000000000..0455d3877 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/st_logic.v @@ -0,0 +1,253 @@ +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. + + diff --git a/helm/coq-contribs/SUBSETS/st_nat.v b/helm/coq-contribs/SUBSETS/st_nat.v new file mode 100644 index 000000000..23081f9ff --- /dev/null +++ b/helm/coq-contribs/SUBSETS/st_nat.v @@ -0,0 +1,264 @@ +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. diff --git a/helm/coq-contribs/SUBSETS/tbs_base.v b/helm/coq-contribs/SUBSETS/tbs_base.v new file mode 100644 index 000000000..88e083b33 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/tbs_base.v @@ -0,0 +1,195 @@ +(** 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. diff --git a/helm/coq-contribs/SUBSETS/tbs_fin.v b/helm/coq-contribs/SUBSETS/tbs_fin.v new file mode 100644 index 000000000..cd618b889 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/tbs_fin.v @@ -0,0 +1,119 @@ +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. diff --git a/helm/coq-contribs/SUBSETS/tbs_fun.v b/helm/coq-contribs/SUBSETS/tbs_fun.v new file mode 100644 index 000000000..7d03a1b93 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/tbs_fun.v @@ -0,0 +1,208 @@ +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. + diff --git a/helm/coq-contribs/SUBSETS/tbs_op.v b/helm/coq-contribs/SUBSETS/tbs_op.v new file mode 100644 index 000000000..7a744762a --- /dev/null +++ b/helm/coq-contribs/SUBSETS/tbs_op.v @@ -0,0 +1,778 @@ +(** 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. diff --git a/helm/coq-contribs/SUBSETS/tbs_rel.v b/helm/coq-contribs/SUBSETS/tbs_rel.v new file mode 100644 index 000000000..c3f1957c1 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/tbs_rel.v @@ -0,0 +1,249 @@ +(** 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. + diff --git a/helm/coq-contribs/SUBSETS/tbs_rop.v b/helm/coq-contribs/SUBSETS/tbs_rop.v new file mode 100644 index 000000000..2abccd67c --- /dev/null +++ b/helm/coq-contribs/SUBSETS/tbs_rop.v @@ -0,0 +1,130 @@ +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. + diff --git a/helm/coq-contribs/SUBSETS/xt_fin.v b/helm/coq-contribs/SUBSETS/xt_fin.v new file mode 100644 index 000000000..694632494 --- /dev/null +++ b/helm/coq-contribs/SUBSETS/xt_fin.v @@ -0,0 +1,304 @@ +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. +