CoRN.algebra.CSetoidInc

Require Export CSetoidFun.

Section inclusion.

Inclusion

Let S be a setoid, and P, Q, R be predicates on S.

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.

Let I,R:S→CProp and F G:(PartFunct S), and denote by P and Q, respectively, the domains of F and G.

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' : ⊆.