From: Ferruccio Guidi Date: Sun, 20 Sep 2015 17:52:45 +0000 (+0000) Subject: old files (re)moved X-Git-Tag: make_still_working~692 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=34c69f5b13b3aafd36d2e8a7e36a96e0748c7938;p=helm.git old files (re)moved --- diff --git a/matita/matita/contribs/limits/Class/defs.ma b/matita/matita/contribs/limits/Class/defs.ma deleted file mode 100644 index 429a6a17f..000000000 --- a/matita/matita/contribs/limits/Class/defs.ma +++ /dev/null @@ -1,69 +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 *) -(* *) -(**************************************************************************) - -include "preamble.ma". - -(* CLASSES: - - 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 "ces" (class equality step) predicate given inside the category. -*) - -record Class: Type ≝ { - class :> Type; - cin : class → Prop; - ces : class → class → Prop; - ces_cin_fw: ∀c1,c2. cin c1 → ces c1 c2 → cin c2; - ces_cin_bw: ∀c1,c2. cin c1 → ces c2 c1 → cin c2 -}. - -(* equality predicate *******************************************************) - -inductive ceq (C:Class): class C → class C → Prop ≝ - | ceq_refl : ∀c. ceq ? c c - | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2 - | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2 -. - -(* default inhabitance predicates *******************************************) - -definition true_f ≝ λX:Type. λ_:X. True. - -definition false_f ≝ λX:Type. λ_:X. False. - -(* default foreward compatibilities *****************************************) - -theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A. -intros; autobatch. -qed. - -definition true_fw ≝ const_fw True. - -definition false_fw ≝ const_fw False. - -(* default backward compatibilities *****************************************) - -theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A. -intros; autobatch. -qed. - -definition true_bw ≝ const_bw True. - -definition false_bw ≝ const_bw False. diff --git a/matita/matita/contribs/limits/Class/eq.ma b/matita/matita/contribs/limits/Class/eq.ma deleted file mode 100644 index 003365bf4..000000000 --- a/matita/matita/contribs/limits/Class/eq.ma +++ /dev/null @@ -1,44 +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 *) -(* *) -(**************************************************************************) - -include "Class/defs.ma". - -(* CLASSES: - - Here we prove the standard properties of the equality. -*) - -theorem ceq_cin_fw: ∀C,c1,c2. ceq C c1 c2 → cin ? c1 → cin ? c2. -intros 4; elim H; clear H c1 c2; autobatch. -qed. - -theorem ceq_cin_bw: ∀C,c1,c2. ceq C c1 c2 → cin ? c2 → cin ? c1. -intros 4; elim H; clear H c1 c2; autobatch. -qed. - -theorem ceq_trans: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c2 c3 → ceq ? c1 c3. -intros 4; elim H; clear H c1 c2; autobatch. -qed. - -theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1. -intros; elim H; clear H c1 c2; autobatch. -qed. - -theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3. -intros; autobatch. -qed. - -theorem ceq_repl: ∀C,c1,c2. ceq C c1 c2 → - ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2. -intros; autobatch. -qed. diff --git a/matita/matita/contribs/limits/Domain/data.ma b/matita/matita/contribs/limits/Domain/data.ma deleted file mode 100644 index 690b9483d..000000000 --- a/matita/matita/contribs/limits/Domain/data.ma +++ /dev/null @@ -1,41 +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 *) -(* *) -(**************************************************************************) - -include "Domain/defs.ma". - -(* QUANTIFICATION DOMAINS - - Here we define some useful domains based on data types. -*) - -definition DBool: Domain ≝ - mk_Domain ( - mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?) - ). -(* -definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def - \lambda C,c0,c1,b. - match b in bool with - [ false \Rightarrow c0 - | true \Rightarrow c1 - ]. -*) -definition DVoid: Domain ≝ - mk_Domain ( - mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?) - ). -(* -definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def - \lambda C,v. - match v in void with []. -*) diff --git a/matita/matita/contribs/limits/Domain/defs.ma b/matita/matita/contribs/limits/Domain/defs.ma deleted file mode 100644 index f828ff1ae..000000000 --- a/matita/matita/contribs/limits/Domain/defs.ma +++ /dev/null @@ -1,38 +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 *) -(* *) -(**************************************************************************) - -include "Class/defs.ma". - -(* QUANTIFICATION DOMAINS - - These are the categories on which we allow quantification. - - We set up single quantifiers, parametric on the domain. -*) - -record Domain: Type ≝ { - domain:> Class -}. - -(* internal universal quantification *) -inductive dall (D:Domain) (P:D → Prop): Prop ≝ - | dall_intro: (∀d. cin ? d → P d) → dall D P -. - -interpretation "internal for all" 'iforall η.x = (dall ? x). - -(* internal existential quantification *) -inductive dex (D:Domain) (P:D → Prop): Prop ≝ - | dex_intro: ∀d. cin D d → P d → dex D P -. - -interpretation "internal exists" 'iexists η.x = (dex ? x). diff --git a/matita/matita/contribs/limits/Makefile b/matita/matita/contribs/limits/Makefile deleted file mode 100644 index a3e891435..000000000 --- a/matita/matita/contribs/limits/Makefile +++ /dev/null @@ -1,16 +0,0 @@ -include ../Makefile.defs - -DIR=$(shell basename $$PWD) - -$(DIR) all: - $(BIN)matitac -$(DIR).opt opt all.opt: - $(BIN)matitac.opt -clean: - $(BIN)matitaclean -clean.opt: - $(BIN)matitaclean.opt -depend: - $(BIN)matitadep -depend.opt: - $(BIN)matitadep.opt diff --git a/matita/matita/contribs/limits/Subset/defs.ma b/matita/matita/contribs/limits/Subset/defs.ma deleted file mode 100644 index 729bdaba9..000000000 --- a/matita/matita/contribs/limits/Subset/defs.ma +++ /dev/null @@ -1,138 +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 *) -(* *) -(**************************************************************************) - -include "Domain/defs.ma". - -(* SUBSETS - - We use predicative subsets encoded as propositional functions - according to Sambin/Valentini "Toolbox". -*) - -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. λU:Subset D. λd. cin D d ∧ U d. - -theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d. - unfold sin; intros; autobatch. -qed. - -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. - -definition sand: ∀D. Subset D → Subset D → Subset 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. - -definition sor: ∀D. Subset D → Subset D → Subset 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) ***************************************) - -definition sle: ∀D. Subset D → Subset D → Prop ≝ - λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d. - -(* subset overlap *********************************************************) - -definition sover: ∀D. Subset D → Subset D → Prop ≝ - λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d. - -(* the class of the subsets of a domain ***********************************) - -definition power: Domain → Class ≝ - λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?). diff --git a/matita/matita/contribs/limits/depends b/matita/matita/contribs/limits/depends deleted file mode 100644 index af2f6349f..000000000 --- a/matita/matita/contribs/limits/depends +++ /dev/null @@ -1,9 +0,0 @@ -preamble.ma datatypes/bool.ma datatypes/constructors.ma logic/connectives.ma -Class/eq.ma Class/defs.ma -Domain/defs.ma Class/defs.ma -Domain/data.ma Domain/defs.ma -Subset/defs.ma Domain/defs.ma -Class/defs.ma preamble.ma -datatypes/bool.ma -datatypes/constructors.ma -logic/connectives.ma diff --git a/matita/matita/contribs/limits/etc/Class/defs.etc b/matita/matita/contribs/limits/etc/Class/defs.etc new file mode 100644 index 000000000..429a6a17f --- /dev/null +++ b/matita/matita/contribs/limits/etc/Class/defs.etc @@ -0,0 +1,69 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "preamble.ma". + +(* CLASSES: + - 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 "ces" (class equality step) predicate given inside the category. +*) + +record Class: Type ≝ { + class :> Type; + cin : class → Prop; + ces : class → class → Prop; + ces_cin_fw: ∀c1,c2. cin c1 → ces c1 c2 → cin c2; + ces_cin_bw: ∀c1,c2. cin c1 → ces c2 c1 → cin c2 +}. + +(* equality predicate *******************************************************) + +inductive ceq (C:Class): class C → class C → Prop ≝ + | ceq_refl : ∀c. ceq ? c c + | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2 + | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2 +. + +(* default inhabitance predicates *******************************************) + +definition true_f ≝ λX:Type. λ_:X. True. + +definition false_f ≝ λX:Type. λ_:X. False. + +(* default foreward compatibilities *****************************************) + +theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A. +intros; autobatch. +qed. + +definition true_fw ≝ const_fw True. + +definition false_fw ≝ const_fw False. + +(* default backward compatibilities *****************************************) + +theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A. +intros; autobatch. +qed. + +definition true_bw ≝ const_bw True. + +definition false_bw ≝ const_bw False. diff --git a/matita/matita/contribs/limits/etc/Class/eq.etc b/matita/matita/contribs/limits/etc/Class/eq.etc new file mode 100644 index 000000000..003365bf4 --- /dev/null +++ b/matita/matita/contribs/limits/etc/Class/eq.etc @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Class/defs.ma". + +(* CLASSES: + - Here we prove the standard properties of the equality. +*) + +theorem ceq_cin_fw: ∀C,c1,c2. ceq C c1 c2 → cin ? c1 → cin ? c2. +intros 4; elim H; clear H c1 c2; autobatch. +qed. + +theorem ceq_cin_bw: ∀C,c1,c2. ceq C c1 c2 → cin ? c2 → cin ? c1. +intros 4; elim H; clear H c1 c2; autobatch. +qed. + +theorem ceq_trans: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c2 c3 → ceq ? c1 c3. +intros 4; elim H; clear H c1 c2; autobatch. +qed. + +theorem ceq_sym: ∀ C,c1,c2. ceq C c1 c2 → ceq ? c2 c1. +intros; elim H; clear H c1 c2; autobatch. +qed. + +theorem ceq_conf: ∀C,c1,c2. ceq C c1 c2 → ∀c3. ceq ? c1 c3 → ceq ? c2 c3. +intros; autobatch. +qed. + +theorem ceq_repl: ∀C,c1,c2. ceq C c1 c2 → + ∀d1. ceq ? c1 d1 → ∀d2. ceq ? c2 d2 → ceq ? d1 d2. +intros; autobatch. +qed. diff --git a/matita/matita/contribs/limits/etc/Domain/data.etc b/matita/matita/contribs/limits/etc/Domain/data.etc new file mode 100644 index 000000000..690b9483d --- /dev/null +++ b/matita/matita/contribs/limits/etc/Domain/data.etc @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Domain/defs.ma". + +(* QUANTIFICATION DOMAINS + - Here we define some useful domains based on data types. +*) + +definition DBool: Domain ≝ + mk_Domain ( + mk_Class bool (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?) + ). +(* +definition dbool_ixfam : \forall (C:Class). C \to C \to (DBool \to C) \def + \lambda C,c0,c1,b. + match b in bool with + [ false \Rightarrow c0 + | true \Rightarrow c1 + ]. +*) +definition DVoid: Domain ≝ + mk_Domain ( + mk_Class void (true_f ?) (eq ?) (true_fw ? ?) (true_bw ? ?) + ). +(* +definition dvoid_ixfam : \forall (C:Class). (DVoid \to C) \def + \lambda C,v. + match v in void with []. +*) diff --git a/matita/matita/contribs/limits/etc/Domain/defs.etc b/matita/matita/contribs/limits/etc/Domain/defs.etc new file mode 100644 index 000000000..f828ff1ae --- /dev/null +++ b/matita/matita/contribs/limits/etc/Domain/defs.etc @@ -0,0 +1,38 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Class/defs.ma". + +(* QUANTIFICATION DOMAINS + - These are the categories on which we allow quantification. + - We set up single quantifiers, parametric on the domain. +*) + +record Domain: Type ≝ { + domain:> Class +}. + +(* internal universal quantification *) +inductive dall (D:Domain) (P:D → Prop): Prop ≝ + | dall_intro: (∀d. cin ? d → P d) → dall D P +. + +interpretation "internal for all" 'iforall η.x = (dall ? x). + +(* internal existential quantification *) +inductive dex (D:Domain) (P:D → Prop): Prop ≝ + | dex_intro: ∀d. cin D d → P d → dex D P +. + +interpretation "internal exists" 'iexists η.x = (dex ? x). diff --git a/matita/matita/contribs/limits/etc/Subset/defs.etc b/matita/matita/contribs/limits/etc/Subset/defs.etc new file mode 100644 index 000000000..729bdaba9 --- /dev/null +++ b/matita/matita/contribs/limits/etc/Subset/defs.etc @@ -0,0 +1,138 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +include "Domain/defs.ma". + +(* SUBSETS + - We use predicative subsets encoded as propositional functions + according to Sambin/Valentini "Toolbox". +*) + +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. λU:Subset D. λd. cin D d ∧ U d. + +theorem sin_i: ∀D. ∀U:Subset D. ∀d. cin D d → U d → sin ? U d. + unfold sin; intros; autobatch. +qed. + +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. + +definition sand: ∀D. Subset D → Subset D → Subset 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. + +definition sor: ∀D. Subset D → Subset D → Subset 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) ***************************************) + +definition sle: ∀D. Subset D → Subset D → Prop ≝ + λD. λU1,U2:Subset D. \iforall d. U1 d → U2 d. + +(* subset overlap *********************************************************) + +definition sover: ∀D. Subset D → Subset D → Prop ≝ + λD. λU1,U2:Subset D. \iexists d. U1 d ∧ U2 d. + +(* the class of the subsets of a domain ***********************************) + +definition power: Domain → Class ≝ + λD. mk_Class (Subset D) (true_f ?) (sle ?) (true_fw ? ?) (true_bw ? ?). diff --git a/matita/matita/contribs/limits/etc/preamble.etc b/matita/matita/contribs/limits/etc/preamble.etc new file mode 100644 index 000000000..80713e416 --- /dev/null +++ b/matita/matita/contribs/limits/etc/preamble.etc @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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 ***************************************) +(* Project taken over by "formal_topology" and restarted Mon Apr 6, 2009 **) + +include "logic/connectives.ma". +include "datatypes/constructors.ma". +include "datatypes/bool.ma". + +(* notations **************************************************************) + +notation < "hvbox(\iforall ident i opt (: ty) break . p)" + right associative with precedence 20 +for @{ 'iforall ${ default + @{λ ${ident i}: $ty. $p} + @{λ ${ident i}. $p} +}}. + +notation > "\iforall list1 ident x sep , opt (: T). term 19 Px" + with precedence 20 +for ${ default + @{ ${ fold right @{$Px} rec acc @{'iforall (λ ${ident x} :$T . $acc)} } } + @{ ${ fold right @{$Px} rec acc @{'iforall (λ ${ident x} . $acc)} } } +}. + +notation < "hvbox(\iexists ident i opt (: ty) break . p)" + right associative with precedence 20 +for @{ 'iexists ${ default + @{λ ${ident i}: $ty. $p} + @{λ ${ident i}. $p} +}}. + +notation > "\iexists list1 ident x sep , opt (: T). term 19 Px" + with precedence 20 +for ${ default + @{ ${ fold right @{$Px} rec acc @{'iexists (λ ${ident x}: $T. $acc)} } } + @{ ${ fold right @{$Px} rec acc @{'iexists (λ ${ident x}. $acc)} } } +}. diff --git a/matita/matita/contribs/limits/preamble.ma b/matita/matita/contribs/limits/preamble.ma index 80713e416..4741d33dc 100644 --- a/matita/matita/contribs/limits/preamble.ma +++ b/matita/matita/contribs/limits/preamble.ma @@ -14,37 +14,6 @@ (* Project started Wed Oct 12, 2005 ***************************************) (* Project taken over by "formal_topology" and restarted Mon Apr 6, 2009 **) +(* Project taken over by "lambdadelta" and restarted Sun Sept 20, 2015 ****) -include "logic/connectives.ma". -include "datatypes/constructors.ma". -include "datatypes/bool.ma". - -(* notations **************************************************************) - -notation < "hvbox(\iforall ident i opt (: ty) break . p)" - right associative with precedence 20 -for @{ 'iforall ${ default - @{λ ${ident i}: $ty. $p} - @{λ ${ident i}. $p} -}}. - -notation > "\iforall list1 ident x sep , opt (: T). term 19 Px" - with precedence 20 -for ${ default - @{ ${ fold right @{$Px} rec acc @{'iforall (λ ${ident x} :$T . $acc)} } } - @{ ${ fold right @{$Px} rec acc @{'iforall (λ ${ident x} . $acc)} } } -}. - -notation < "hvbox(\iexists ident i opt (: ty) break . p)" - right associative with precedence 20 -for @{ 'iexists ${ default - @{λ ${ident i}: $ty. $p} - @{λ ${ident i}. $p} -}}. - -notation > "\iexists list1 ident x sep , opt (: T). term 19 Px" - with precedence 20 -for ${ default - @{ ${ fold right @{$Px} rec acc @{'iexists (λ ${ident x}: $T. $acc)} } } - @{ ${ fold right @{$Px} rec acc @{'iexists (λ ${ident x}. $acc)} } } -}. +include "basics/logic.ma".