From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 16 Jan 2007 12:18:09 +0000 (+0000)
Subject: Added SetoidInc.m
X-Git-Tag: make_still_working~6525
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a04ff90485bcb7d800538914d0df76eeb414f6c9;p=helm.git

Added SetoidInc.m
---

diff --git a/helm/software/matita/library/algebra/CoRN/SetoidInc.ma b/helm/software/matita/library/algebra/CoRN/SetoidInc.ma
new file mode 100644
index 000000000..5bf067087
--- /dev/null
+++ b/helm/software/matita/library/algebra/CoRN/SetoidInc.ma
@@ -0,0 +1,150 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
+(*      ||A||       E.Tassi, S.Zacchiroli                                 *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU Lesser General Public License Version 2.1         *)
+(*                                                                        *)
+(**************************************************************************)
+
+set "baseuri" "cic:/matita/algebra/CoRN/SetoidInc".
+include "algebra/CoRN/SetoidFun.ma".
+
+(* $Id: CSetoidInc.v,v 1.3 2004/04/22 14:49:43 lcf Exp $ *)
+
+(* printing included %\ensuremath{\subseteq}% #&sube;# *)
+
+(* Section inclusion. *)
+
+(* Inclusion
+
+Let [S] be a setoid, and [P], [Q], [R] be predicates on [S]. *)
+
+(* Variable S : CSetoid. *)
+
+definition included : \forall S : CSetoid. \forall P,Q : S \to Type. Type \def
+   \lambda S : CSetoid. \lambda P,Q : S \to Type.
+   \forall x : S. P x \to Q x.
+
+(* Section Basics. *)
+
+(* Variables P Q R : S -> CProp. *)
+lemma included_refl : \forall S : CSetoid. \forall P : S \to Type. 
+  included S P P.
+intros.
+unfold.
+intros.
+assumption.
+qed.
+
+lemma included_trans : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+  included S P Q \to included S Q R \to included S P R.
+intros.
+unfold.
+intros.
+apply i1.
+apply i.
+assumption.
+qed.
+
+lemma included_conj : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ included S P Q \to included S P R \to included S P (conjP S Q R).
+intros 4.
+unfold included.
+intros;
+unfold.
+split [apply f.assumption|apply f1.assumption]
+qed.
+
+lemma included_conj' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+  included S (conjP S P Q) P.
+  intros.
+exact (prj1 S P Q).
+qed.
+
+lemma included_conj'' : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+ included S (conjP S P Q) Q.
+ intros.
+exact (prj2 S P Q).
+qed.
+
+lemma included_conj_lft : \forall S : CSetoid. \forall P,Q,R : S \to Type.
+  included S R (conjP S P Q) -> included S R P.
+intros 4.
+unfold included.
+unfold conjP.intros (f1 x H2).
+elim (f1 x ); assumption.
+qed.
+
+lemma included_conj_rht : \forall S : CSetoid. \forall P,Q,R : S \to Type. 
+  included S R (conjP S P Q) \to included S R Q.
+  intros 4.
+  unfold included.
+  unfold conjP.
+intros (H1 x H2).
+elim (H1 x); assumption.
+qed.
+lemma included_extend : \forall S : CSetoid. \forall P,Q,R : S \to Type.  
+  \forall H : \forall x. P x \to Type.
+ included S R (extend S P H) \to included S R P.
+intros 4.
+intros (H0 H1).
+unfold.
+unfold extend in H1.
+intros.
+elim (H1 x);assumption.
+qed.
+
+
+(* End Basics. *)
+
+(*
+%\begin{convention}% Let [I,R:S->CProp] and [F G:(PartFunct S)], and denote
+by [P] and [Q], respectively, the domains of [F] and [G].
+%\end{convention}%
+*)
+
+(* Variables F G : (PartFunct S). *)
+
+(* begin hide *)
+(* Let P := Dom F. *)
+(* Let Q := Dom G. *)
+(* end hide *)
+
+(* Variable R : S -> CProp. *)
+lemma included_FComp : \forall S : CSetoid. \forall F,G: PartFunct S. 
+\forall R : S \to Type.
+  included S R (UP ? F) \to (\forall x: S. \forall Hx. (R x) \to UQ ? G (pfpfun ? F x Hx)) \to 
+  included S R (pfdom ? (Fcomp ? F G)).
+intros (S F G R HP HQ).
+unfold Fcomp.
+simplify.
+unfold included. intros (x Hx).
+apply (existT ? ? (HP x Hx)).
+apply HQ.
+assumption.
+qed.
+
+lemma included_FComp': \forall S : CSetoid. \forall F,G: PartFunct S. 
+\forall R : S \to Type.
+included S R (pfdom ? (Fcomp ? F G)) \to included S R (UP ? F).
+intros (S F G R H).
+unfold Fcomp in H.
+simplify in H.
+unfold. intros (x Hx).
+elim (H x Hx);
+assumption.
+qed.
+
+(* End inclusion. *) 
+
+(* Implicit Arguments included [S].
+
+Hint Resolve included_refl included_FComp : included.
+
+Hint Immediate included_trans included_FComp' : included. *)