Library Pow
Require Export Poset.
Section Pow.
Variable A : Set.
Definition PowPoset : Poset (A->Prop).
refine
(poset_constr (A->Prop)
(fun P Q => forall x, (P x) <-> (Q x)) _ _ _
(fun P Q => forall x, (P x) -> (Q x)) _ _ _); intuition.
elim (H x0); auto.
elim (H x0); auto.
elim (H x0); elim (H0 x0); auto.
elim (H x0); elim (H0 x0); auto.
elim (H x0); auto.
Defined.
End Pow.
Notation "S1 <=< S2" := (order (PowPoset _) S1 S2) (at level 0).
Inductive Post (A B:Set) (f:A->B->Prop) (S:A->Prop) (b:B) : Prop :=
Post_def : forall a, f a b -> S a -> Post A B f S b.
Implicit Arguments Post [A B].
Inductive Post2 (A B C:Set) (f:A->B->C->Prop) (S1:A->Prop) (S2:B->Prop) (c:C) : Prop :=
Post2_def : forall a b, f a b c -> S1 a -> S2 b -> Post2 A B C f S1 S2 c.
Implicit Arguments Post2 [A B C].
Inductive Post2' (A B C:Set) (f:A->B->C->Prop) (S1:A->Prop) (S2:(A*B)->Prop) (c:C) : Prop :=
Post2'_def : forall a b, f a b c -> S1 a -> S2 (a,b) -> Post2' A B C f S1 S2 c.
Implicit Arguments Post2' [A B C].
Inductive Post3 (A B C D:Set) (f:A->B->C->D->Prop) (S1:A->Prop) (S2:B->Prop) (S3:C->Prop) (d:D) : Prop :=
Post3_def : forall a b c, f a b c d -> S1 a -> S2 b -> S3 c -> Post3 A B C D f S1 S2 S3 d.
Implicit Arguments Post3 [A B C D].
Inductive Post3' (A B C D:Set) (f:A->B->C->D->Prop) (S1:A->Prop) (S2:(A*B)->Prop) (S3:C->Prop) (d:D) : Prop :=
Post3'_def : forall a b c, f a b c d -> S1 a -> S2 (a,b) -> S3 c -> Post3' A B C D f S1 S2 S3 d.
Implicit Arguments Post3' [A B C D].
Set Implicit Arguments.
Section A.
Variable A B C D : Set.
Inductive compose (A B C:Set) (R2:B->C->Prop) (R1:A->B->Prop) : A -> C -> Prop :=
compose_def : forall a b c,
R1 a b -> R2 b c -> compose R2 R1 a c.
Inductive compose2 (A B C D:Set) (R3:B->C->D->Prop) (R1:A->B->Prop) (R2:A->C->Prop) : A -> D -> Prop :=
compose2_def : forall a b c d,
R1 a b -> R2 a c -> R3 b c d -> compose2 R3 R1 R2 a d.
Definition Fcompose (A B C:Set) (f2:B->C) (f1:A->B) (a:A) : C :=
f2 (f1 a).
Definition Fcompose2 (A B C D:Set) (f:B->C->D) (f1:A->B) (f2:A->C) (a:A) : D :=
f (f1 a) (f2 a).
Lemma post_compose_1 : forall (R1:A->B->Prop) (R2:B->C->Prop) (PA:A->Prop),
(Post (compose R2 R1) PA) <=< (Post R2 (Post R1 PA)).
Proof.
intros; intros c H.
inversion_clear H.
inversion_clear H0.
constructor 1 with b; auto.
constructor 1 with a; auto.
Qed.
Lemma post_compose_2 : forall (R1:A->B->Prop) (R2:B->C->Prop) (PA:A->Prop),
(Post R2 (Post R1 PA)) <=< (Post (compose R2 R1) PA).
Proof.
intros; intros c H.
inversion_clear H.
inversion_clear H1.
constructor 1 with a0; auto.
constructor 1 with a; auto.
Qed.
Lemma post2_compose_1 : forall (R1:A->B->Prop) (R2:A->C->Prop) (R3:B->C->D->Prop) (PA:A->Prop),
(Post (compose2 R3 R1 R2) PA) <=< (Post2 R3 (Post R1 PA) (Post R2 PA)).
Proof.
intros; intros c H.
inversion_clear H.
inversion_clear H0.
constructor 1 with b c0; auto.
constructor 1 with a; auto.
constructor 1 with a; auto.
Qed.
Lemma post_monotone : forall (R:A->B->Prop) P1 P2,
P1 <=< P2 -> (Post R P1) <=< (Post R P2).
Proof.
intros; intros b Hb.
inversion_clear Hb.
constructor 1 with a; auto.
Qed.
Lemma post2_monotone : forall (R:A->B->C->Prop) P1 P2 S1 S2,
P1 <=< P2 -> S1 <=< S2 ->
(Post2 R P1 S1) <=< (Post2 R P2 S2).
Proof.
intros; intros c Hc.
inversion_clear Hc.
constructor 1 with a b; auto.
Qed.
End A.
Section correct.
Variable A AbA B AbB : Set.
Variable gammaA : AbA -> A -> Prop.
Variable gammaB : AbB -> B -> Prop.
Variable R : A -> B -> Prop.
Variable f : AbA -> AbB.
Definition correct1 : Prop :=
forall a, (Post R (gammaA a)) <=< (gammaB (f a)).
End correct.
Definition correct2
(A B C AbA AbB AbC : Set)
(gammaA : AbA -> A -> Prop)
(gammaB : AbB -> B -> Prop)
(gammaC : AbC -> C -> Prop)
(R : A -> B -> C -> Prop)
(f : AbA -> AbB -> AbC) : Prop :=
forall a b, (Post2 R (gammaA a) (gammaB b)) <=< (gammaC (f a b)).
Lemma criterium1 :
forall (A B C AbA AbB AbC : Set)
(gammaA : AbA -> A -> Prop)
(gammaB : AbB -> B -> Prop)
(gammaC : AbC -> C -> Prop)
R1 f1 R2 f2,
correct1 gammaA gammaB R1 f1 ->
correct1 gammaB gammaC R2 f2 ->
correct1 gammaA gammaC (compose R2 R1) (Fcompose f2 f1).
Proof.
intros; intros a c Hac; unfold Fcompose.
apply H0.
apply post_monotone with (P1:=(Post R1 (gammaA a))); auto.
apply post_compose_1; auto.
Qed.
Lemma criterium2 :
forall (A B C D AbA AbB AbC AbD : Set)
(gammaA : AbA -> A -> Prop)
(gammaB : AbB -> B -> Prop)
(gammaC : AbC -> C -> Prop)
(gammaD : AbD -> D -> Prop)
R1 f1 R2 f2 R f,
correct1 gammaA gammaB R1 f1 ->
correct1 gammaA gammaC R2 f2 ->
correct2 gammaB gammaC gammaD R f ->
correct1 gammaA gammaD (compose2 R R1 R2) (Fcompose2 f f1 f2).
Proof.
intros; intros a c Hac; unfold Fcompose2.
apply H1.
apply post2_monotone with (P1:=(Post R1 (gammaA a)))
(S1:=(Post R2 (gammaA a))); auto.
apply post2_compose_1; auto.
Qed.
Index
This page has been generated by coqdoc