FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

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

diff --git a/helm/software/matita/contribs/limits/Class/defs.ma b/helm/software/matita/contribs/limits/Class/defs.ma
index a0b07ccee53bcd7bd1b1cf50404adecea371365f..429a6a17fc128b4371c9fe4b5c379d124eb2122c 100644 (file)
--- a/helm/software/matita/contribs/limits/Class/defs.ma
+++ b/helm/software/matita/contribs/limits/Class/defs.ma
@@ -14,7 +14,7 @@
 
 include "preamble.ma".
 
-(* ACZEL CATEGORIES:
+(* 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
@@ -27,56 +27,43 @@ include "preamble.ma".
 *) 
 
 record Class: Type ≝ {
-   class:> Type;
-   cin: class → Prop;
-   ces: class → class \to Prop
+   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
 }.
 
-(* default inhabitance predicates *)
-definition true_f ≝ λ(X:Type). λ(_:X). True.
-definition false_f ≝ λ(X:Type). λ(_:X). False.
+(* equality predicate *******************************************************)
 
-(* equality predicate *)
 inductive ceq (C:Class): class C → class C → Prop ≝
-   | ceq_refl : ∀c. cin ? c → ceq ? c c
-   | ceq_trans: ∀c1,c,c2. cin ? c1 → ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
-   | ceq_conf : ∀c1,c,c2. cin ? c1 → ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
+   | 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
 .
-(*
-(* external universal quantification *)
-inductive call (C:Class) (P:C \to Prop) : Prop ≝
-   | call_intro: (\forall c. cin ? c \to P c) \to call C P.
-
-inductive call2 (C1,C2:Class) (P:C1 \to C2 \to Prop) : Prop \def
-   | call2_intro: 
-      (\forall c1,c2. cin ? c1 \to cin ? c2 \to P c1 c2) \to call2 C1 C2 P.
-*)
-(* notations **************************************************************)
-(*
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "external for all" 'xforall \eta.x =
-  (cic:/matita/limits/Class/defs/call.ind#xpointer(1/1) _ x).
-
-notation < "hvbox(\xforall ident i opt (: ty) break . p)"
-  right associative with precedence 20
-for @{ 'xforall ${default
-  @{\lambda ${ident i} : $ty. $p}
-  @{\lambda ${ident i} . $p}}}.
-
-notation > "\forall list1 ident x sep , opt (: T). term 19 Px"
-  with precedence 20
-  for ${ default
-          @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}:$T.$acc)} } }
-          @{ ${ fold right @{$Px} rec acc @{'xforall (λ${ident x}.$acc)} } }
-       }.
-
-(*CSC: the URI must disappear: there is a bug now *)
-interpretation "external for all 2" 'xforall2 \eta.x \eta.y =
-  (cic:/matita/limits/Class/defs/call2.ind#xpointer(1/1) _ _ x y).
-
-notation > "hvbox(\xforall ident i1 opt (: ty1) ident i2 opt (: ty2) break . p)"
-  with precedence 20
-for @{ 'xforall2 ${default
-  @{\lambda ${ident i1} : $ty1. \lambda ${ident i2} : $ty2. $p}
-  @{\lambda ${ident i1}, ${ident i2}. $p}}}.
-*)
+
+(* 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.