From 174ee1889b5c91ef5339c718d7657ed0e5da21e8 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 24 Sep 2015 14:03:26 +0000 Subject: [PATCH] first constructions with classes --- .../matita/contribs/limits/etc/Class/defs.etc | 69 --------------- .../contribs/limits/notation/equiv_3.ma | 23 +++++ matita/matita/contribs/limits/preamble.ma | 6 ++ .../limits/{u0_predicates.ma => u0_apps.ma} | 29 ++----- matita/matita/contribs/limits/u0_class.ma | 52 +++++++++-- .../limits/{etc/Class/eq.etc => u0_data.ma} | 33 ++----- matita/matita/contribs/limits/u0_exp.ma | 35 ++++++++ matita/matita/contribs/limits/u0_preds.ma | 86 +++++++++++++++++++ 8 files changed, 208 insertions(+), 125 deletions(-) delete mode 100644 matita/matita/contribs/limits/etc/Class/defs.etc create mode 100644 matita/matita/contribs/limits/notation/equiv_3.ma rename matita/matita/contribs/limits/{u0_predicates.ma => u0_apps.ma} (56%) rename matita/matita/contribs/limits/{etc/Class/eq.etc => u0_data.ma} (54%) create mode 100644 matita/matita/contribs/limits/u0_exp.ma create mode 100644 matita/matita/contribs/limits/u0_preds.ma diff --git a/matita/matita/contribs/limits/etc/Class/defs.etc b/matita/matita/contribs/limits/etc/Class/defs.etc deleted file mode 100644 index 429a6a17f..000000000 --- a/matita/matita/contribs/limits/etc/Class/defs.etc +++ /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/notation/equiv_3.ma b/matita/matita/contribs/limits/notation/equiv_3.ma new file mode 100644 index 000000000..f7afbc1eb --- /dev/null +++ b/matita/matita/contribs/limits/notation/equiv_3.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION (equivalence relation) ************************************) + +notation > "hvbox(a break ∼ term 46 b)" + non associative with precedence 45 + for @{ 'Equiv ? $a $b }. + +notation < "hvbox(term 46 a break maction (∼) (∼\sub t) term 46 b)" + non associative with precedence 45 + for @{ 'Equiv $t $a $b }. diff --git a/matita/matita/contribs/limits/preamble.ma b/matita/matita/contribs/limits/preamble.ma index 4741d33dc..47724701b 100644 --- a/matita/matita/contribs/limits/preamble.ma +++ b/matita/matita/contribs/limits/preamble.ma @@ -17,3 +17,9 @@ (* Project taken over by "lambdadelta" and restarted Sun Sept 20, 2015 ****) include "basics/logic.ma". +include "../lambdadelta/ground_2/notation/xoa/false_0.ma". +include "../lambdadelta/ground_2/notation/xoa/true_0.ma". + +interpretation "logical false" 'false = False. + +interpretation "logical true" 'true = True. diff --git a/matita/matita/contribs/limits/u0_predicates.ma b/matita/matita/contribs/limits/u0_apps.ma similarity index 56% rename from matita/matita/contribs/limits/u0_predicates.ma rename to matita/matita/contribs/limits/u0_apps.ma index 13650cfde..9ad43fb25 100644 --- a/matita/matita/contribs/limits/u0_predicates.ma +++ b/matita/matita/contribs/limits/u0_apps.ma @@ -14,28 +14,13 @@ include "preamble.ma". -(* RELATIONS **********************************************************) +(* APPLICATIONS *******************************************************) -definition u0_predicate1: Type[0] → Type[1] ≝ λT.T → Prop. +definition u0_i: ∀T:Type[0]. T → T ≝ + λT,a. a. -definition u0_predicate2: Type[0] → Type[1] ≝ λT.T → u0_predicate1 T. +definition u0_k: ∀T,U:Type[0]. T → U → T ≝ + λT,U,a,b. a. -definition u1_predicate1: Type[1] → Type[2] ≝ λT.T → Prop. - -definition u0_quantifier: Type[0] → Type[2] ≝ λT. u1_predicate1 (u0_predicate1 T). - -record is_u0_reflexive (T:Type[0]) (All:u0_quantifier T) (R:u0_predicate2 T): Prop ≝ -{ - u0_refl: All (λa. R a a) -}. - -record can_u0_replace1 (T:Type[0]) (All:u0_quantifier T) (Q:u0_predicate2 T) (R:u0_predicate1 T): Prop ≝ -{ - u0_repl1: All (λa. R a → All (λb. Q b a → R b)) -}. -(* -record can_u0_replac2 (T:Type[0]) (All:u0_quantifier T) (Q:u0_predicate2 T) (R:u0_predicate2 T): Prop ≝ -{ - u0_reflexivity: All (λa. R a a) -}. -*) +definition u0_s: ∀T,U1,U2:Type[0]. (T → U1 → U2) → (T → U1) → (T → U2) ≝ + λT,U1,U2,f,g,a. f a (g a). diff --git a/matita/matita/contribs/limits/u0_class.ma b/matita/matita/contribs/limits/u0_class.ma index 49c715a01..37168bb82 100644 --- a/matita/matita/contribs/limits/u0_class.ma +++ b/matita/matita/contribs/limits/u0_class.ma @@ -12,9 +12,17 @@ (* *) (**************************************************************************) -include "u0_predicates.ma". +include "notation/equiv_3.ma". +include "u0_preds.ma". +include "u0_apps.ma". -(* CLASSES ************************************************************) +(* CLASS **************************************************************) +(* - a class is defined as a category in the sense of Per Martin-Lof + - a membership predicate defines the domain of the category + - an equivalence relation on the domain defines equality in the category + - a function between classes is an application respecting + - both membership and equality +*) record u0_class: Type[1] ≝ { u0_class_t :> Type[0]; @@ -22,13 +30,41 @@ record u0_class: Type[1] ≝ { u0_class_eq: u0_predicate2 u0_class_t }. -interpretation "u0 class membership" 'mem a C = (u0_class_in C a). +interpretation "u0 class membership" 'mem a D = (u0_class_in D a). -definition u0_class_all: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∀a. a ∈ C → P a. +interpretation "u0 class equivalence" 'Equiv D a1 a2 = (u0_class_eq D a1 a2). -definition u0_class_ex: ∀C:u0_class. u0_quantifier C ≝ λC,P. ∃a. a ∈ C ∧ P a. +record is_u0_class (D:u0_class): Prop ≝ { + u0_class_refl: u0_refl D (u0_class_in D) (u0_class_eq D); + u0_class_repl: u0_repl2 D (u0_class_in D) (u0_class_eq D) (u0_class_eq D) +}. + +record u0_fun (D,C:u0_class): Type[0] ≝ { + u0_fun_a :1> D → C +}. -record is_u0_class (C:u0_class): Prop ≝ { - u0_class_repl1: can_u0_replace1 C (u0_class_all C) (u0_class_eq C) (u0_class_in C); - u0_class_refl : is_u0_reflexive C (u0_class_all C) (u0_class_eq C) +record is_u0_fun (D,C) (f:u0_fun D C): Prop ≝ { + u0_fun_hom1: u0_hom1 D (u0_class_in D) C f (u0_class_in D) (u0_class_in C); + u0_fun_hom2: u0_hom2 D (u0_class_in D) C f (u0_class_eq D) (u0_class_eq C) }. + +definition u0_id (D): u0_fun D D ≝ + mk_u0_fun D D (u0_i D). + +(* Basic properties ***************************************************) + +(* auto width 7 in the next lemmas is due to automatic η expansion *) +lemma u0_class_sym: ∀D. is_u0_class D → u0_sym D (u0_class_in D) (u0_class_eq D). +#D #HD @u0_refl_repl_sym /2 width=7 by u0_class_repl, u0_class_refl/ qed-. + +lemma u0_class_trans: ∀D. is_u0_class D → u0_trans D (u0_class_in D) (u0_class_eq D). +#D #HD @u0_refl_repl_trans /2 width=7 by u0_class_repl, u0_class_refl/ qed-. + +lemma u0_class_conf: ∀D. is_u0_class D → u0_conf D (u0_class_in D) (u0_class_eq D). +#D #HD @u0_refl_repl_conf /2 width=7 by u0_class_repl, u0_class_refl/ qed-. + +lemma u0_class_div: ∀D. is_u0_class D → u0_div D (u0_class_in D) (u0_class_eq D). +#D #HD @u0_refl_repl_div /2 width=7 by u0_class_repl, u0_class_refl/ qed-. + +lemma u0_fun_id: ∀D. is_u0_class D → is_u0_fun D D (u0_id D). +/2 width=1 by mk_is_u0_fun/ qed. diff --git a/matita/matita/contribs/limits/etc/Class/eq.etc b/matita/matita/contribs/limits/u0_data.ma similarity index 54% rename from matita/matita/contribs/limits/etc/Class/eq.etc rename to matita/matita/contribs/limits/u0_data.ma index 003365bf4..150f38d2d 100644 --- a/matita/matita/contribs/limits/etc/Class/eq.etc +++ b/matita/matita/contribs/limits/u0_data.ma @@ -12,33 +12,14 @@ (* *) (**************************************************************************) -include "Class/defs.ma". +include "u0_class.ma". -(* CLASSES: - - Here we prove the standard properties of the equality. -*) +(* CLASSES FROM DATA TYPES ********************************************) -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. +definition u0_data: Type[0] → u0_class ≝ + λT. mk_u0_class T (u0_full T) (eq T). -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. +(* Basic properties ***************************************************) -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. +lemma u0_class_data: ∀T. is_u0_class (u0_data T). +/2 width=1 by mk_is_u0_class/ qed. diff --git a/matita/matita/contribs/limits/u0_exp.ma b/matita/matita/contribs/limits/u0_exp.ma new file mode 100644 index 000000000..1943af03f --- /dev/null +++ b/matita/matita/contribs/limits/u0_exp.ma @@ -0,0 +1,35 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "u0_class.ma". + +(* EXPONENTIAL CLASS **************************************************) + +definition u0_exp_eq (D,C): u0_predicate2 (u0_fun D C) ≝ + λf,g. (u0_xeq … (u0_class_in D) … (u0_class_eq C) f g). + +definition u0_exp (D,C): u0_class ≝ + mk_u0_class (u0_fun D C) (is_u0_fun …) (u0_exp_eq D C). + +definition u0_proj1 (D1,D2): u0_fun D1 (u0_exp D2 D1) ≝ + mk_u0_fun … (λa. mk_u0_fun … (u0_k … a)). + +(* Basic properties ***************************************************) + +lemma u0_class_exp: ∀D,C. is_u0_class C → is_u0_class (u0_exp D C). +/4 width=7 by mk_is_u0_class, u0_class_refl, u0_class_repl, u0_fun_hom1/ qed. + +lemma u0_fun_proj1: ∀D2,D1. is_u0_class D1 → is_u0_fun … (u0_proj1 D1 D2). +#D2 #D1 #HD1 @mk_is_u0_fun /3 width=1 by mk_is_u0_fun, u0_class_refl/ +qed. diff --git a/matita/matita/contribs/limits/u0_preds.ma b/matita/matita/contribs/limits/u0_preds.ma new file mode 100644 index 000000000..e39c1814e --- /dev/null +++ b/matita/matita/contribs/limits/u0_preds.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 *) +(* *) +(**************************************************************************) + +include "preamble.ma". + +(* PREDICATES *********************************************************) + +definition u0_predicate1: Type[0] → Type[1] ≝ λT.T → Prop. + +definition u0_predicate2: Type[0] → Type[1] ≝ λT.T → u0_predicate1 T. + +definition u1_predicate1: Type[1] → Type[2] ≝ λT.T → Prop. + +definition u1_predicate2: Type[1] → Type[2] ≝ λT.T → u1_predicate1 T. + +definition u0_full: ∀T:Type[0]. u0_predicate1 T ≝ λT,a. ⊤. + +definition u0_empty: ∀T:Type[0]. u0_predicate1 T ≝ λT,a. ⊥. + +definition u0_quantifier: Type[0] → Type[2] ≝ λT. u1_predicate2 (u0_predicate1 T). + +definition u0_all: ∀T:Type[0]. u0_quantifier T ≝ λT,I,P. ∀a. I a → P a. + +definition u0_ex: ∀T:Type[0]. u0_quantifier T ≝ λT,I,P. ∃a. I a ∧ P a. + +definition u0_refl (T:Type[0]) (I:u0_predicate1 T) (P:u0_predicate2 T): Prop ≝ + u0_all T I (λa. P a a). + +definition u0_sym (T:Type[0]) (I:u0_predicate1 T) (P:u0_predicate2 T): Prop ≝ + u0_all T I (λa1. u0_all T I (λa2. P a2 a1 → P a1 a2)). + +definition u0_trans (T:Type[0]) (I:u0_predicate1 T) (P:u0_predicate2 T): Prop ≝ + u0_all T I (λa1. u0_all T I (λa. P a1 a → (u0_all T I (λa2. P a a2 → P a1 a2)))). + +definition u0_conf (T:Type[0]) (I:u0_predicate1 T) (P:u0_predicate2 T): Prop ≝ + u0_all T I (λa. u0_all T I (λa1. P a a1 → (u0_all T I (λa2. P a a2 → P a1 a2)))). + +definition u0_div (T:Type[0]) (I:u0_predicate1 T) (P:u0_predicate2 T): Prop ≝ + u0_all T I (λa1. u0_all T I (λa. P a1 a → (u0_all T I (λa2. P a2 a → P a1 a2)))). + +definition u0_repl2 (T:Type[0]) (I:u0_predicate1 T) (Q:u0_predicate2 T) (P:u0_predicate2 T): Prop ≝ + u0_all T I (λa1. u0_all T I (λa2. P a1 a2 → u0_all T I (λb1. u0_all T I (λb2. Q b1 a1 → Q b2 a2 → P b1 b2)))). + +definition u0_hom1 (T:Type[0]) (I:u0_predicate1 T) (U:Type[0]) (f:T → U) (P:u0_predicate1 T) (Q:u0_predicate1 U) : Prop ≝ + u0_all T I (λa. P a → Q (f a)). + +definition u0_hom2 (T:Type[0]) (I:u0_predicate1 T) (U:Type[0]) (f:T → U) (P:u0_predicate2 T) (Q:u0_predicate2 U) : Prop ≝ + u0_all T I (λa1. u0_all T I (λa2. P a1 a2 → Q (f a1) (f a2))). + +definition u0_xeq (T:Type[0]) (I:u0_predicate1 T) (U:Type[0]) (Q:u0_predicate2 U): u0_predicate2 (T → U) ≝ + λf,g. u0_all T I (λa. Q (f a) (g a)). + +(* Basic properties ***************************************************) + +lemma u0_refl_repl_sym: ∀T,I,P. u0_refl T I P → u0_repl2 T I P P → u0_sym T I P. +normalize /3 width=7 by/ qed-. + +lemma u0_refl_repl_trans: ∀T,I,P. u0_refl T I P → u0_repl2 T I P P → u0_trans T I P. +normalize /3 width=7 by/ qed-. + +lemma u0_refl_repl_conf: ∀T,I,P. u0_refl T I P → u0_repl2 T I P P → u0_conf T I P. +#T #I #P +(* +/3 width=1 by (u0_refl_repl_trans T I P), (u0_refl_repl_sym T I P)/ +*) +#H1 #H2 #a #Ha #a1 #Ha1 #Haa1 +@(u0_refl_repl_trans T I P) /2 width=7 by/ +@(u0_refl_repl_sym T I P) /2 width=7 by/ +qed-. + +lemma u0_refl_repl_div: ∀T,I,P. u0_refl T I P → u0_repl2 T I P P → u0_div T I P. +#T #I #P #H1 #H2 #a1 #Ha1 #a #Ha #Ha1a #a2 #Ha2 #Ha2a +@(u0_refl_repl_trans T I P … a) /2 width=7 by/ +@(u0_refl_repl_sym T I P) /2 width=7 by/ +qed-. -- 2.39.2