cle introduced; ceq fixed

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/class_defs.ma
index acd73c4ba686ca00ca9523bfd27130bc730df00a..17a53f64f57ec30e013bdb79d514d5002f6b6bef 100644 (file)
--- 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 5c53b94596d2be574982d277f33bcd799196239e..cfcb57293f6a066eced2e45621d9387398db64b9 100644 (file)
--- 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 (file)
index 0000000..a688ec6
--- /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 ab8d4d9cfd0ed78ea20c3c364bcdb53c4f904345..c840fbdaf7cddc972b4f3cdade571c5b2aa84dd4 100644 (file)
--- 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 cf981362c42f6808286f2417cac0869117c6f172..5d872040a403d9c9466424d9d956742eeb040a65 100644 (file)
--- 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.