+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
(* 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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+
+(* APPLICATIONS *******************************************************)
+
+definition u0_i: ∀T:Type[0]. T → T ≝
+ λT,a. a.
+
+definition u0_k: ∀T,U:Type[0]. T → U → T ≝
+ λT,U,a,b. 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).
(* *)
(**************************************************************************)
-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];
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.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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".
+
+(* CLASSES FROM DATA TYPES ********************************************)
+
+definition u0_data: Type[0] → u0_class ≝
+ λT. mk_u0_class T (u0_full T) (eq T).
+
+(* Basic properties ***************************************************)
+
+lemma u0_class_data: ∀T. is_u0_class (u0_data T).
+/2 width=1 by mk_is_u0_class/ qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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".
-
-(* RELATIONS **********************************************************)
-
-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 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)
-}.
-*)
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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-.
projects / helm.git / commitdiff