helm/software/matita/contribs/limits/Class/defs.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "preamble.ma".
  16
  17 (* CLASSES:
  18    - We use typoids with a compatible membership relation
  19    - The category is intended to be the domain of the membership relation
  20    - The membership relation is necessary because we need to regard the
  21      domain of a propositional function (ie a predicative subset) as a
  22      quantification domain and therefore as a category, but there is no
  23      type in CIC representing the domain of a propositional function
  24    - We set up a single equality predicate, parametric on the category,
  25      defined as the reflexive, symmetic, transitive and compatible closure
  26      of the "ces" (class equality step) predicate given inside the category.
  27 *)
  28
  29 record Class: Type ≝ {
  30    class     :> Type;
  31    cin       :  class → Prop;
  32    ces       :  class → class → Prop;
  33    ces_cin_fw:  ∀c1,c2. cin c1 → ces c1 c2 → cin c2;
  34    ces_cin_bw:  ∀c1,c2. cin c1 → ces c2 c1 → cin c2
  35 }.
  36
  37 (* equality predicate *******************************************************)
  38
  39 inductive ceq (C:Class): class C → class C → Prop ≝
  40    | ceq_refl : ∀c. ceq ? c c
  41    | ceq_trans: ∀c1,c,c2. ces ? c1 c → ceq ? c c2 → ceq ? c1 c2
  42    | ceq_conf : ∀c1,c,c2. ces ? c c1 → ceq ? c c2 → ceq ? c1 c2
  43 .
  44
  45 (* default inhabitance predicates *******************************************)
  46
  47 definition true_f ≝ λX:Type. λ_:X. True.
  48
  49 definition false_f ≝ λX:Type. λ_:X. False.
  50
  51 (* default foreward compatibilities *****************************************)
  52
  53 theorem const_fw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x1 x2 → A.
  54 intros; autobatch.
  55 qed.
  56
  57 definition true_fw ≝ const_fw True.
  58
  59 definition false_fw ≝ const_fw False.
  60
  61 (* default backward compatibilities *****************************************)
  62
  63 theorem const_bw: ∀A:Prop. ∀X:Type. ∀P:X→X→Prop. ∀x1,x2. A → P x2 x1 → A.
  64 intros; autobatch.
  65 qed.
  66
  67 definition true_bw ≝ const_bw True.
  68
  69 definition false_bw ≝ const_bw False.