From 192884dae520029b152a3f69989e51cc8af158ce Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 19 Nov 2005 12:16:40 +0000 Subject: [PATCH] some renaming --- .../{ac_defs.ma => class_defs.ma} | 50 +++++++-------- .../PREDICATIVE-TOPOLOGY/domain_defs.ma | 64 +++++++++++++++++++ .../contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma | 30 --------- .../{subsets_defs.ma => subset_defs.ma} | 25 ++++++-- 4 files changed, 109 insertions(+), 60 deletions(-) rename helm/matita/contribs/PREDICATIVE-TOPOLOGY/{ac_defs.ma => class_defs.ma} (67%) create mode 100644 helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma delete mode 100644 helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma rename helm/matita/contribs/PREDICATIVE-TOPOLOGY/{subsets_defs.ma => subset_defs.ma} (64%) diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma similarity index 67% rename from helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma rename to helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma index b375c69ad..10a5ae34c 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma @@ -14,9 +14,9 @@ (* Project started Wed Oct 12, 2005 ***************************************) -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs". +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs". -include "coq.ma". +include "../../library/logic/connectives.ma". (* ACZEL CATEGORIES: - We use typoids with a compatible membership relation @@ -27,43 +27,43 @@ include "coq.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 aceq predicate given inside the category. Then we prove the + of the csub1 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 *) -record AC: Type \def { - ac: Type; - acin: ac \to Prop; - aceq: ac \to ac \to Prop +record Class: Type \def { + class: Type; + cin : class \to Prop; + csub1: class \to class \to Prop }. -coercion ac. +coercion class. -inductive eq (A:AC) (a:A): A \to Prop \def - | eq_refl: acin ? a \to eq ? a a - | eq_sing_r: \forall b,c. - eq ? a b \to acin ? c \to aceq ? b c \to eq ? a c - | eq_sing_l: \forall b,c. - eq ? a b \to acin ? c \to aceq ? c b \to eq ? a c. +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 A,a,b. eq ? a b \to acin A a \land acin A b. -intros; elim H; clear H; clear b; +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 A,b,a,c. - eq A b c \to eq ? a b \to eq ? a c. -intros 5; elim H; clear H; clear c; +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 A,b,a,c. - eq A c b \to eq ? a b \to eq ? a c. -intros 5; elim H; clear H; clear b; +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 @@ -72,14 +72,14 @@ intros 5; elim H; clear H; clear b; ]. qed. -theorem eq_sym: \forall A,a,b. eq A a b \to eq A b a. +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 A,b,a,c. - eq A a b \to eq ? a c \to eq ? b c. +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 ]. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma new file mode 100644 index 000000000..821002e68 --- /dev/null +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/domain_defs.ma @@ -0,0 +1,64 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/domain_defs". + +include "class_defs.ma". + +(* QUANTIFICATION DOMAINS + - These are the categories on which we allow quantification + - We set up single quantifiers, parametric on the domain, so they + already have the properties that usually are axiomatized inside the + 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. + +(*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). + +notation < "hvbox(\iall ident i opt (: ty) break . p)" + right associative with precedence 20 +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). + +notation < "hvbox(\iexist ident i opt (: ty) break . p)" + right associative with precedence 20 +for @{ 'iexist ${default + @{\lambda ${ident i} : $ty. $p)} + @{\lambda ${ident i} . $p}}}. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma deleted file mode 100644 index cbe4f567a..000000000 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma +++ /dev/null @@ -1,30 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/qd_defs". - -include "ac_defs.ma". - -(* QUANTIFICATION DOMAINS -*) - -record QD: Type \def { - qd: AC -}. - -coercion qd. - -(* se togli il D da acin D a non ce la fa ancora *) -inductive iall (D:QD) (P:D \to Prop) : Prop \def - | iall_intro: (\forall a:D. acin D a \to P a) \to iall D P. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma similarity index 64% rename from helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma rename to helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma index 010595e09..2ae2471db 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma @@ -12,17 +12,32 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/subsets_defs". +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs". -include "qd_defs.ma". +include "domain_defs.ma". (* SUBSETS - We use predicative subsets coded as propositional functions according to G.Sambin and S.Valentini "Toolbox" *) -definition Subset \def \forall (D:QD). D \to Prop. +definition Subset \def \lambda (D:Domain). D \to Prop. -alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". +(* 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. -definition stop \def \lambda (D:QD). \lambda (a:D). True. + +(* 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. + + + +(* full subset: "subset top" *) +definition stop \def \lambda (D:Domain). \lambda (_:D). True. + +coercion stop. + +(* empty subset: "subset bottom" *) +definition sbot \def \lambda (D:Domain). \lambda (_:D). False. \ No newline at end of file -- 2.39.2