- character: we adjusted some "autobatch" parameters

[helm.git] / helm / software / matita / contribs / limits / Subset / defs.ma

diff --git a/helm/software/matita/contribs/limits/Subset/defs.ma b/helm/software/matita/contribs/limits/Subset/defs.ma
index 6dbab4b39de63ed4fceed84f9ee07f5ac5fa63ac..729bdaba94cf87b1c779d9809628e7359cd63f7c 100644 (file)
--- a/helm/software/matita/contribs/limits/Subset/defs.ma
+++ b/helm/software/matita/contribs/limits/Subset/defs.ma
@@ -15,44 +15,124 @@
 include "Domain/defs.ma".
 
 (* SUBSETS
-   - We use predicative subsets coded as propositional functions
-     according to G.Sambin and S.Valentini "Toolbox".
+   - We use predicative subsets encoded as propositional functions
+     according to Sambin/Valentini "Toolbox".
 *)
 
-definition Subset ≝ λD:Domain. D → Prop.
+record Subset (D:Domain): Type ≝ {
+   subset       :1> D → Prop;
+   ces_subset_fw:   ∀d1,d2. subset d1 → ces ? d1 d2 → subset d2;
+   ces_subset_bw:   ∀d1,d2. subset d1 → ces ? d2 d1 → subset d2
+}.
 
-(* subset membership (epsilon) *)
-definition sin : ∀D. Subset D → D → Prop ≝
-   λD:Domain. λU,d. cin D d ∧ U d.
+(* subset membership (epsilon) ********************************************)
 
-(* subset top (full subset) *)
-definition stop ≝ λD:Domain. true_f D.
+definition sin: ∀D. Subset D → D → Prop ≝
+   λD. λU:Subset D. λd. cin D d ∧ U d.
 
-coercion stop.
+theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d.
+ unfold sin; intros; autobatch.
+qed.
 
-(* subset bottom (empty subset) *)
-definition sbot ≝ λD:Domain. false_f D.
+theorem sin_e1: ∀D. ∀U:Subset D. ∀d. sin ? U d → cin D d.
+ intros; decompose; autobatch.
+qed.
+
+theorem sin_e2: ∀D. ∀U:Subset D. ∀d. sin ? U d → U d.
+ intros; decompose; autobatch.
+qed.
+
+(* the domain built upon a subset *****************************************)
+
+theorem ces_sin_fw: ∀D,U,d1,d2. sin D U d1 → ces ? d1 d2 → sin D U d2.
+ intros; 
+ apply sin_i; 
+ [ autobatch
+ | apply (ces_subset_fw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ]. 
+qed.
+
+theorem ces_sin_bw: ∀D,U,d1,d2. sin D U d1 → ces ? d2 d1 → sin D U d2.
+ intros; 
+ apply sin_i; 
+ [ autobatch
+ | apply (ces_subset_bw D U d1); [ apply sin_e2; autobatch | autobatch ] (**)
+ ]. 
+qed.
+
+definition domain_of_subset: ∀D. Subset D → Domain ≝
+   λD:Domain. λU.
+   mk_Domain (mk_Class D (sin D U) (ces D) (ces_sin_fw ? ?) (ces_sin_bw ? ?)).
+
+coercion domain_of_subset.
+
+(* subset top (full subset) ***********************************************)
+
+definition stop: ∀D. Subset D ≝
+   λD. mk_Subset D (true_f ?) (true_fw ? ?) (true_bw ? ?).
+
+coercion stop nocomposites.
+
+(* subset bottom (empty subset) *******************************************)
+
+definition sbot: ∀D. Subset D ≝
+   λD. mk_Subset D (false_f ?) (false_fw ? ?) (false_bw ? ?).
+
+(* subset and (binary intersection) ***************************************)
+
+theorem ces_sand_fw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d1 d2 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sand_bw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∧ U2 d1 → ces ? d2 d1 → U1 d2 ∧ U2 d2.
+ intros; decompose; apply conj;
+ [ apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
 
-(* subset and (binary intersection) *)
 definition sand: ∀D. Subset D → Subset D → Subset D ≝
-   λD,U1,U2,d. U1 d ∧ U2 d. 
+   λD,U1,U2. 
+   mk_Subset D (λd. U1 d ∧ U2 d) (ces_sand_fw ? U1 U2) (ces_sand_bw ? U1 U2).
+
+(* subset or (binary union) ***********************************************)
+
+theorem ces_sor_fw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d1 d2 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_fw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_fw D U2 d1); autobatch
+ ].
+qed.
+
+theorem ces_sor_bw:
+   ∀D. ∀U1,U2:Subset D. ∀d1,d2. U1 d1 ∨ U2 d1 → ces ? d2 d1 → U1 d2 ∨ U2 d2.
+ intros; decompose;
+ [ apply or_introl; apply (ces_subset_bw D U1 d1); autobatch (**)
+ | apply or_intror; apply (ces_subset_bw D U2 d1); autobatch
+ ].
+qed.
 
-(* subset or (binary union) *)
 definition sor: ∀D. Subset D → Subset D → Subset D ≝
-   λD,U1,U2,d. U1 d ∨ U2 d.
+   λD,U1,U2. 
+   mk_Subset D (λd. U1 d ∨ U2 d) (ces_sor_fw ? U1 U2) (ces_sor_bw ? U1 U2).
+
+(* subset less or equal (inclusion) ***************************************)
 
-(* subset less or equal (inclusion) *) 
 definition sle: ∀D. Subset D → Subset D → Prop ≝
-   λD,U1,U2. \iforall d. U1 d → U2 d. 
+   λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d. 
+
+(* subset overlap *********************************************************)
 
-(* subset overlap *) 
 definition sover: ∀D. Subset D → Subset D → Prop ≝
-   λD,U1,U2. \iexists d. U1 d ∧ U2 d. 
+   λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d. 
 
-(* the class of the subsets of a domain *)
-definition subsets_of_domain ≝
-   λD. mk_Class (Subset D) (true_f ?) (sle ?). 
+(* the class of the subsets of a domain ***********************************)
 
-(* the domain built upon a subset *)
-definition domain_of_subset: ∀D. Subset D → Domain ≝
-   λD:Domain. λU. mk_Domain (mk_Class D (sin D U) (ces D)).
+definition power: Domain → Class ≝
+   λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?).