From: Ferruccio Guidi Date: Sat, 19 Nov 2005 12:16:40 +0000 (+0000) Subject: some renaming X-Git-Tag: V_0_7_2_3~31 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=192884dae520029b152a3f69989e51cc8af158ce;p=helm.git some renaming --- diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma deleted file mode 100644 index b375c69ad..000000000 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma +++ /dev/null @@ -1,86 +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 *) -(* *) -(**************************************************************************) - -(* Project started Wed Oct 12, 2005 ***************************************) - -set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs". - -include "coq.ma". - -(* ACZEL CATEGORIES: - - We use typoids with a compatible membership relation - - The category is intended to be the domain of the membership relation - - The membership relation is necessary because we need to regard the - domain of a propositional function (ie a predicative subset) as a - quantification domain and therefore as a category, but there is no - 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 - 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 -}. - -coercion ac. - -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. - -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; - [ 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; - [ 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; - [ 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 A,a,b. eq A a b \to eq A b a. -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. -intros. -lapply eq_sym; [|||| apply H ]. -apply eq_trans; [| auto | auto ]. -qed. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma new file mode 100644 index 000000000..10a5ae34c --- /dev/null +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma @@ -0,0 +1,86 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* Project started Wed Oct 12, 2005 ***************************************) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_defs". + +include "../../library/logic/connectives.ma". + +(* ACZEL CATEGORIES: + - We use typoids with a compatible membership relation + - The category is intended to be the domain of the membership relation + - The membership relation is necessary because we need to regard the + domain of a propositional function (ie a predicative subset) as a + quantification domain and therefore as a category, but there is no + 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 + properties of the equality that usually are axiomatized inside the + category structure. This makes categories easier to use +*) + +record Class: Type \def { + class: Type; + cin : class \to Prop; + csub1: 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. 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/subset_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma new file mode 100644 index 000000000..2ae2471db --- /dev/null +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/subset_defs". + +include "domain_defs.ma". + +(* SUBSETS + - We use predicative subsets coded as propositional functions + according to G.Sambin and S.Valentini "Toolbox" +*) + +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 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 diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma deleted file mode 100644 index 010595e09..000000000 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subsets_defs.ma +++ /dev/null @@ -1,28 +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/subsets_defs". - -include "qd_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. - -alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". - -definition stop \def \lambda (D:QD). \lambda (a:D). True.