matita/library/algebra/CoRN/SetoidInc.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
   8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU Lesser General Public License Version 2.1         *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 set "baseuri" "cic:/matita/algebra/CoRN/SetoidInc".
  16 include "algebra/CoRN/SetoidFun.ma".
  17
  18 (* $Id: CSetoidInc.v,v 1.3 2004/04/22 14:49:43 lcf Exp $ *)
  19
  20 (* printing included %\ensuremath{\subseteq}% #&sube;# *)
  21
  22 (* Section inclusion. *)
  23
  24 (* Inclusion
  25
  26 Let [S] be a setoid, and [P], [Q], [R] be predicates on [S]. *)
  27
  28 (* Variable S : CSetoid. *)
  29
  30 definition included : \forall S : CSetoid. \forall P,Q : S \to Type. Type \def
  31    \lambda S : CSetoid. \lambda P,Q : S \to Type.
  32    \forall x : S. P x \to Q x.
  33
  34 (* Section Basics. *)
  35
  36 (* Variables P Q R : S -> CProp. *)
  37 lemma included_refl : \forall S : CSetoid. \forall P : S \to Type.
  38   included S P P.
  39 intros.
  40 unfold.
  41 intros.
  42 assumption.
  43 qed.
  44
  45 lemma included_trans : \forall S : CSetoid. \forall P,Q,R : S \to Type.
  46   included S P Q \to included S Q R \to included S P R.
  47 intros.
  48 unfold.
  49 intros.
  50 apply i1.
  51 apply i.
  52 assumption.
  53 qed.
  54
  55 lemma included_conj : \forall S : CSetoid. \forall P,Q,R : S \to Type.
  56  included S P Q \to included S P R \to included S P (conjP S Q R).
  57 intros 4.
  58 unfold included.
  59 intros;
  60 unfold.
  61 split [apply f.assumption|apply f1.assumption]
  62 qed.
  63
  64 lemma included_conj' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
  65   included S (conjP S P Q) P.
  66   intros.
  67 exact (prj1 S P Q).
  68 qed.
  69
  70 lemma included_conj'' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
  71  included S (conjP S P Q) Q.
  72  intros.
  73 exact (prj2 S P Q).
  74 qed.
  75
  76 lemma included_conj_lft : \forall S : CSetoid. \forall P,Q,R : S \to Type.
  77   included S R (conjP S P Q) -> included S R P.
  78 intros 4.
  79 unfold included.
  80 unfold conjP.intros (f1 x H2).
  81 elim (f1 x ); assumption.
  82 qed.
  83
  84 lemma included_conj_rht : \forall S : CSetoid. \forall P,Q,R : S \to Type.
  85   included S R (conjP S P Q) \to included S R Q.
  86   intros 4.
  87   unfold included.
  88   unfold conjP.
  89 intros (H1 x H2).
  90 elim (H1 x); assumption.
  91 qed.
  92 lemma included_extend : \forall S : CSetoid. \forall P,Q,R : S \to Type.
  93   \forall H : \forall x. P x \to Type.
  94  included S R (extend S P H) \to included S R P.
  95 intros 4.
  96 intros (H0 H1).
  97 unfold.
  98 unfold extend in H1.
  99 intros.
 100 elim (H1 x);assumption.
 101 qed.
 102
 103
 104 (* End Basics. *)
 105
 106 (*
 107 %\begin{convention}% Let [I,R:S->CProp] and [F G:(PartFunct S)], and denote
 108 by [P] and [Q], respectively, the domains of [F] and [G].
 109 %\end{convention}%
 110 *)
 111
 112 (* Variables F G : (PartFunct S). *)
 113
 114 (* begin hide *)
 115 (* Let P := Dom F. *)
 116 (* Let Q := Dom G. *)
 117 (* end hide *)
 118
 119 (* Variable R : S -> CProp. *)
 120 lemma included_FComp : \forall S : CSetoid. \forall F,G: PartFunct S.
 121 \forall R : S \to Type.
 122   included S R (UP ? F) \to (\forall x: S. \forall Hx. (R x) \to UQ ? G (pfpfun ? F x Hx)) \to
 123   included S R (pfdom ? (Fcomp ? F G)).
 124 intros (S F G R HP HQ).
 125 unfold Fcomp.
 126 simplify.
 127 unfold included. intros (x Hx).
 128 apply (existT ? ? (HP x Hx)).
 129 apply HQ.
 130 assumption.
 131 qed.
 132
 133 lemma included_FComp': \forall S : CSetoid. \forall F,G: PartFunct S.
 134 \forall R : S \to Type.
 135 included S R (pfdom ? (Fcomp ? F G)) \to included S R (UP ? F).
 136 intros (S F G R H).
 137 unfold Fcomp in H.
 138 simplify in H.
 139 unfold. intros (x Hx).
 140 elim (H x Hx);
 141 assumption.
 142 qed.
 143
 144 (* End inclusion. *)
 145
 146 (* Implicit Arguments included [S].
 147
 148 Hint Resolve included_refl included_FComp : included.
 149
 150 Hint Immediate included_trans included_FComp' : included. *)