CoRN.algebra.CSetoidInc
Variable S : CSetoid.
Definition ⊆ (P Q : S → CProp) : CProp := ∀ x : S, P x → Q x.
Section Basics.
Variables P Q R : S → CProp.
Lemma included_refl : ⊆ P P.
Proof.
red in |- *; intros.
auto.
Qed.
Lemma included_trans : ⊆ P Q → ⊆ Q R → ⊆ P R.
Proof.
intros.
red in |- *; intros.
apply X0; apply X; auto.
Qed.
Lemma included_conj : ∀ P Q R, ⊆ P Q → ⊆ P R → ⊆ P (Conj Q R).
Proof.
intros.
red in |- *; red in X, X0.
intros; red in |- ×.
split.
apply X; assumption.
apply X0; assumption.
Qed.
Lemma included_conj' : ⊆ (Conj P Q) P.
Proof.
exact (prj1 _ P Q).
Qed.
Lemma included_conj'' : ⊆ (Conj P Q) Q.
Proof.
exact (prj2 _ P Q).
Qed.
Lemma included_conj_lft : ⊆ R (Conj P Q) → ⊆ R P.
Proof.
red in |- ×.
unfold conjP.
intros H1 x H2.
elim (H1 x); auto.
Qed.
Lemma included_conj_rht : ⊆ R (Conj P Q) → ⊆ R Q.
Proof.
red in |- ×. unfold conjP.
intros H1 x H2.
elim (H1 x); auto.
Qed.
Lemma included_extend : ∀ (H : ∀ x, P x → CProp),
⊆ R (extend P H) → ⊆ R P.
Proof.
intros H0 H1.
red in |- ×.
unfold extend in H1.
intros.
elim (H1 x); auto.
Qed.
End Basics.
Variables F G : (PartFunct S).
Variable R : S → CProp.
Lemma included_FComp : ⊆ R P → (∀ x Hx, (R x) → Q (F x Hx)) → ⊆ R (Dom (G[o]F)).
Proof.
intros HP HQ.
simpl in |- ×.
red in |- *; intros x Hx.
∃ (HP x Hx).
apply HQ.
assumption.
Qed.
Lemma included_FComp' : ⊆ R (Dom (G[o]F)) → ⊆ R P.
Proof.
intro H; simpl in H; red in |- *; intros x Hx.
elim (H x Hx); auto.
Qed.
End inclusion.
Implicit Arguments ⊆ [S].
Hint Resolve included_refl included_FComp : ⊆.
Hint Immediate included_trans included_FComp' : ⊆.