From 51ba598a5d034a2cb572c58f6db4937627e914a3 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 19 Nov 2005 17:58:50 +0000 Subject: [PATCH] some definitions about subsets --- .../PREDICATIVE-TOPOLOGY/class_defs.ma | 58 ++++--------------- .../PREDICATIVE-TOPOLOGY/domain_defs.ma | 17 +++--- .../PREDICATIVE-TOPOLOGY/subset_defs.ma | 39 ++++++++++--- 3 files changed, 51 insertions(+), 63 deletions(-) diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma index 10a5ae34c..ba1195619 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma @@ -27,60 +27,26 @@ include "../../library/logic/connectives.ma". type in CIC representing the domain of a propositional function - We set up a single equality predicate, parametric on the category, defined as the reflexive, symmetic, transitive and compatible closure - of the csub1 predicate given inside the category. Then we prove the + of the cle1 predicate given inside the category. Then we prove the properties of the equality that usually are axiomatized inside the category structure. This makes categories easier to use *) +definition true_f \def \lambda (X:Type). \lambda (_:X). True. + +definition false_f \def \lambda (X:Type). \lambda (_:X). False. + record Class: Type \def { class: Type; cin : class \to Prop; - csub1: class \to class \to Prop + cle1 : class \to class \to Prop }. coercion class. -inductive eq (C:Class) (c1:C): C \to Prop \def - | eq_refl: cin ? c1 \to eq ? c1 c1 - | eq_sing_r: \forall c2,c3. - eq ? c1 c2 \to cin ? c3 \to csub1 ? c2 c3 \to eq ? c1 c3 - | eq_sing_l: \forall c2,c3. - eq ? c1 c2 \to cin ? c3 \to csub1 ? c3 c2 \to eq ? c1 c3. - -theorem eq_cl: \forall C,c1,c2. eq ? c1 c2 \to cin C c1 \land cin C c2. -intros; elim H; clear H; clear c2; - [ auto | decompose H2; auto | decompose H2; auto ]. -qed. - -theorem eq_trans: \forall C,c2,c1,c3. - eq C c2 c3 \to eq ? c1 c2 \to eq ? c1 c3. -intros 5; elim H; clear H; clear c3; - [ auto - | apply eq_sing_r; [||| apply H4 ]; auto - | apply eq_sing_l; [||| apply H4 ]; auto - ]. -qed. - -theorem eq_conf_rev: \forall C,c2,c1,c3. - eq C c3 c2 \to eq ? c1 c2 \to eq ? c1 c3. -intros 5; elim H; clear H; clear c2; - [ auto - | lapply eq_cl; [ decompose Hletin |||| apply H1 ]. - apply H2; apply eq_sing_l; [||| apply H4 ]; auto - | lapply eq_cl; [ decompose Hletin |||| apply H1 ]. - apply H2; apply eq_sing_r; [||| apply H4 ]; auto - ]. -qed. - -theorem eq_sym: \forall C,c1,c2. eq C c1 c2 \to eq C c2 c1. -intros; -lapply eq_cl; [ decompose Hletin |||| apply H ]. -auto. -qed. - -theorem eq_conf: \forall C,c2,c1,c3. - eq C c1 c2 \to eq ? c1 c3 \to eq ? c2 c3. -intros. -lapply eq_sym; [|||| apply H ]. -apply eq_trans; [| auto | auto ]. -qed. +inductive ceq (C:Class) (c1:C): C \to Prop \def + | ceq_refl: cin ? c1 \to ceq ? c1 c1 + | ceq_sing_r: \forall c2,c3. + ceq ? c1 c2 \to cin ? c3 \to cle1 ? c2 c3 \to ceq ? c1 c3 + | ceq_sing_l: \forall c2,c3. + ceq ? c1 c2 \to cin ? c3 \to cle1 ? c3 c2 \to ceq ? c1 c3. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma index 821002e68..670211caf 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma @@ -23,20 +23,22 @@ include "class_defs.ma". domain structure. This makes domains easier to use *) - - record Domain: Type \def { qd: Class }. coercion qd. - - (* internal universal quantification *) inductive iall (D:Domain) (P:D \to Prop) : Prop \def | iall_intro: (\forall d:D. cin D d \to P d) \to iall D P. +(* internal existential quantification *) +inductive iex (D:Domain) (P:D \to Prop) : Prop \def + | iex_intro: \forall d:D. cin D d \land P d \to iex D P. +(* +(* notations **************************************************************) + (*CSC: the URI must disappear: there is a bug now *) interpretation "internal for all" 'iall \eta.x = (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/iall.ind#xpointer(1/1) _ x). @@ -47,12 +49,6 @@ for @{ 'iall ${default @{\lambda ${ident i} : $ty. $p)} @{\lambda ${ident i} . $p}}}. - - -(* internal existential quantification *) -inductive iex (D:Domain) (P:D \to Prop) : Prop \def - | iex_intro: \forall d:D. cin D d \land P d \to iex D P. - (*CSC: the URI must disappear: there is a bug now *) interpretation "internal exist" 'iexist \eta.x = (cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs/iex.ind#xpointer(1/1) _ x). @@ -62,3 +58,4 @@ notation < "hvbox(\iexist ident i opt (: ty) break . p)" for @{ 'iexist ${default @{\lambda ${ident i} : $ty. $p)} @{\lambda ${ident i} . $p}}}. +*) \ No newline at end of file diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma index 2ae2471db..87ecb2780 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma @@ -23,21 +23,46 @@ include "domain_defs.ma". definition Subset \def \lambda (D:Domain). D \to Prop. -(* subset inclusion *) -definition ssub: \forall D. Subset D \to Subset D \to Prop \def - \lambda D,U1,U2. \forall d. U1 d \to U2 d. +(* subset membership (epsilon) *) +definition sin : \forall D. Subset D \to D \to Prop \def + \lambda (D:Domain). \lambda U,d. cin D d \and U d. + +(* subset top (full subset) *) +definition stop \def \lambda (D:Domain). true_f D. + +(* subset bottom (empty subset) *) +definition sbot \def \lambda (D:Domain). false_f D. + +(* subset and (binary intersection) *) +definition sand: \forall D. Subset D \to Subset D \to Subset D \def + \lambda D,U1,U2,d. U1 d \land U2 d. +(* subset or (binary union) *) +definition sor: \forall D. Subset D \to Subset D \to Subset D \def + \lambda D,U1,U2,d. U1 d \lor U2 d. +(* subset less or equal (inclusion) *) +definition sle: \forall D. Subset D \to Subset D \to Prop \def + \lambda D,U1,U2. \forall d. U1 d \to U2 d. +(* (* subset overlap *) definition sover: \forall D. Subset D \to Subset D \to Prop \def \lambda D,U1,U2. \forall d. U1 d \to U2 d. +*) + +(* coercions **************************************************************) +(* the class of the subsets of a domain (not an implicit coercion) *) +definition class_of_subsets_of \def + \lambda D. mk_Class (Subset D) (true_f ?) (sle ?). +(* the domain built upon a subset *) +definition domain_of_subset: \forall D. (Subset D) \to Domain \def + \lambda (D:Domain). \lambda U. + mk_Domain (mk_Class D (sin D U) (cle1 D)). -(* full subset: "subset top" *) -definition stop \def \lambda (D:Domain). \lambda (_:D). True. +coercion domain_of_subset. +(* the full subset of a domain *) coercion stop. -(* empty subset: "subset bottom" *) -definition sbot \def \lambda (D:Domain). \lambda (_:D). False. \ No newline at end of file -- 2.39.2