1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/algebra/CoRN/SetoidInc".
16 include "algebra/CoRN/SetoidFun.ma".
18 (* $Id: CSetoidInc.v,v 1.3 2004/04/22 14:49:43 lcf Exp $ *)
20 (* printing included %\ensuremath{\subseteq}% #⊆# *)
22 (* Section inclusion. *)
26 Let [S] be a setoid, and [P], [Q], [R] be predicates on [S]. *)
28 (* Variable S : CSetoid. *)
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.
36 (* Variables P Q R : S -> CProp. *)
37 lemma included_refl : \forall S : CSetoid. \forall P : S \to Type.
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.
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).
61 split [apply f.assumption|apply f1.assumption]
64 lemma included_conj' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
65 included S (conjP S P Q) P.
70 lemma included_conj'' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
71 included S (conjP S P Q) Q.
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.
80 unfold conjP.intros (f1 x H2).
81 elim (f1 x ); assumption.
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.
90 elim (H1 x); assumption.
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.
100 elim (H1 x);assumption.
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].
112 (* Variables F G : (PartFunct S). *)
115 (* Let P := Dom F. *)
116 (* Let Q := Dom G. *)
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).
127 unfold included. intros (x Hx).
128 apply (existT ? ? (HP x Hx)).
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).
139 unfold. intros (x Hx).
146 (* Implicit Arguments included [S].
148 Hint Resolve included_refl included_FComp : included.
150 Hint Immediate included_trans included_FComp' : included. *)