From d468b38f538a7c7d4ace666c1c41931621e8f28c Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 10 Jan 2006 18:07:01 +0000 Subject: [PATCH] cle introduced; ceq fixed --- .../PREDICATIVE-TOPOLOGY/class_defs.ma | 17 ++++---- .../contribs/PREDICATIVE-TOPOLOGY/class_eq.ma | 41 ++++++------------- .../contribs/PREDICATIVE-TOPOLOGY/class_le.ma | 28 +++++++++++++ .../contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma | 8 +++- .../PREDICATIVE-TOPOLOGY/subset_defs.ma | 8 ++-- 5 files changed, 59 insertions(+), 43 deletions(-) create mode 100644 helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_le.ma diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma index acd73c4ba..17a53f64f 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma @@ -38,13 +38,14 @@ definition false_f \def \lambda (X:Type). \lambda (_:X). False. record Class: Type \def { class:> Type; - cin : class \to Prop; - cle1 : class \to class \to Prop + cin: class \to Prop; + cle1: class \to class \to Prop }. -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. +inductive cle (C:Class) (c1:C): C \to Prop \def + | cle_refl: cin ? c1 \to cle ? c1 c1 + | ceq_sing: \forall c2,c3. + cle ? c1 c2 \to cin ? c3 \to cle1 ? c2 c3 \to cle ? c1 c3. + +inductive ceq (C:Class) (c1:C) (c2:C): Prop \def + | ceq_intro: cle ? c1 c2 \to cle ? c2 c1 \to ceq ? c1 c2. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma index 5c53b9459..cfcb57293 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_eq.ma @@ -14,42 +14,25 @@ set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/class_eq". -include "class_defs.ma". +include "class_le.ma". theorem ceq_cl: \forall C,c1,c2. ceq ? c1 c2 \to cin C c1 \land cin C c2. -intros; elim H; clear H; clear c2; - [ auto | decompose H2; auto | decompose H2; auto ]. +intros; elim H; clear H. +lapply cle_cl to H1 using H; clear H1; decompose H; +lapply cle_cl to H2 using H; clear H2; decompose H. +auto. qed. -theorem ceq_trans: \forall C,c2,c1,c3. - ceq C c2 c3 \to ceq ? c1 c2 \to ceq ? c1 c3. -intros 5; elim H; clear H; clear c3; - [ auto - | apply ceq_sing_r; [||| apply H4 ]; auto - | apply ceq_sing_l; [||| apply H4 ]; auto - ]. +theorem ceq_refl: \forall C,c. cin C c \to ceq ? c c. +intros; apply ceq_intro; auto. qed. -theorem ceq_conf_rev: \forall C,c2,c1,c3. - ceq C c3 c2 \to ceq ? c1 c2 \to ceq ? c1 c3. -intros 5; elim H; clear H; clear c2; - [ auto - | lapply ceq_cl; [ decompose Hletin |||| apply H1 ]. - apply H2; apply ceq_sing_l; [||| apply H4 ]; auto - | lapply ceq_cl; [ decompose Hletin |||| apply H1 ]. - apply H2; apply ceq_sing_r; [||| apply H4 ]; auto - ]. +theorem ceq_trans: \forall C,c2,c1,c3. + ceq C c2 c3 \to ceq ? c1 c2 \to ceq ? c1 c3. +intros; elim H; elim H1; clear H; clear H1. +apply ceq_intro; apply cle_trans; [|auto|auto||auto|auto]. qed. theorem ceq_sym: \forall C,c1,c2. ceq C c1 c2 \to ceq C c2 c1. -intros; -lapply ceq_cl; [ decompose Hletin |||| apply H ]. -auto. -qed. - -theorem ceq_conf: \forall C,c2,c1,c3. - ceq C c1 c2 \to ceq ? c1 c3 \to ceq ? c2 c3. -intros. -lapply ceq_sym; [|||| apply H ]. -apply ceq_trans; [| auto | auto ]. +intros; elim H; clear H.; auto. qed. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_le.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_le.ma new file mode 100644 index 000000000..a688ec63b --- /dev/null +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_le.ma @@ -0,0 +1,28 @@ +(**************************************************************************) +(* ___ *) +(* ||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/class_le". + +include "class_defs.ma". + +theorem cle_cl: \forall C,c1,c2. cle ? c1 c2 \to cin C c1 \land cin C c2. +intros; elim H; clear H; clear c2; + [| decompose H2 ]; auto. +qed. + +theorem cle_trans: \forall C,c1,c2. cle C c1 c2 \to + \forall c3. cle ? c3 c1 \to cle ? c3 c2. +intros 4; elim H; clear H; clear c2; + [| apply ceq_sing; [||| apply H4 ]]; auto. +qed. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma index ab8d4d9cf..c840fbdaf 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/coa_defs.ma @@ -21,7 +21,7 @@ include "domain_data.ma". *) record COA: Type \def { - coa:> Class; (* carrier *) + coa:> Class; (* carrier *) le: coa \to coa \to Prop; (* inclusion *) ov: coa \to coa \to Prop; (* overlap *) sup: \forall (D:Domain). (D \to coa) \to coa; (* supremum *) @@ -54,4 +54,8 @@ definition bsup: \forall (P:COA). P \to P \to P \def inf_ov: forall p q, ov p q -> ov p (inf QDBool (bool_family _ p q)) properness: ov zero zero -> False; distributivity: forall I p q, id _ (inf QDBool (bool_family _ (sup I p) q)) (sup I (fun i => (inf QDBool (bool_family _ (p i) q)))); -*) \ No newline at end of file +*) + +inductive pippo : Prop \def + | Pippo: let x \def zero in zero = x \to pippo. + \ 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 cf981362c..5d872040a 100644 --- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/subset_defs.ma @@ -51,16 +51,16 @@ definition sover: \forall D. Subset D \to Subset D \to Prop \def (* 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 +(* the domain built upon a subset (not an implicit coercion) *) +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)). -coercion cic:/matita/PREDICATIVE-TOPOLOGY/subset_defs/domain_of_subset.con. - (* the full subset of a domain *) coercion stop. -- 2.39.2