(* * Copyright (c) 2009, Andrew Appel, Robert Dockins and Aquinas Hobor. * *) Require Import base. Require Import sepalg. Require Import sepalg_generators. Require Import sepalg_functors. Require Import age_sepalg. Require Import predicates_hered. Require Import predicates_rec. Require Import subtypes. Local Open Scope pred. Lemma conj_nonexpansive `{ASA A} : forall F G, nonexpansive F -> nonexpansive G -> nonexpansive (fun x => F x && G x). Proof. unfold nonexpansive; intros. apply sub_equ. apply sub_conj; apply equ_sub; auto. apply sub_conj; apply equ_sub2; auto. Qed. Lemma conj_contractive `{ASA A} : forall F G, contractive F -> contractive G -> contractive (fun x => F x && G x). Proof. unfold contractive; intros. apply sub_equ. apply sub_conj; apply equ_sub; auto. apply sub_conj; apply equ_sub2; auto. Qed. Lemma impl_contractive `{ASA A} : forall F G, contractive F -> contractive G -> contractive (fun x => F x --> G x). Proof. unfold contractive; intros. apply sub_equ. apply sub_impl. apply equ_sub2; auto. apply equ_sub; auto. apply sub_impl. apply equ_sub; auto. apply equ_sub2; auto. Qed. Lemma impl_nonexpansive `{ASA A} : forall F G, nonexpansive F -> nonexpansive G -> nonexpansive (fun x => F x --> G x). Proof. unfold nonexpansive; intros. apply sub_equ. apply sub_impl. apply equ_sub2; auto. apply equ_sub; auto. apply sub_impl. apply equ_sub; auto. apply equ_sub2; auto. Qed. Lemma forall_contractive `{ASA A} : forall B (X : pred A -> B -> pred A), (forall x, (contractive (fun y => X y x))) -> contractive (fun x => (universal (X x))). Proof. unfold contractive; intros. apply sub_equ. apply sub_forall; intros. apply equ_sub; auto. apply sub_forall; intros. apply equ_sub2; auto. Qed. Lemma forall_nonexpansive `{ASA A} : forall B (X : pred A -> B -> pred A), (forall x, (nonexpansive (fun y => X y x))) -> nonexpansive (fun x => (universal (X x))). Proof. unfold nonexpansive; intros. apply sub_equ. apply sub_forall; intros. apply equ_sub; auto. apply sub_forall; intros. apply equ_sub2; auto. Qed. Lemma exists_contractive `{ASA A} : forall B (X : pred A -> B -> pred A), (forall x, (contractive (fun y => X y x))) -> contractive (fun x => (existential (X x))). Proof. unfold contractive; intros. apply sub_equ; apply sub_exists; intros. apply equ_sub; auto. apply equ_sub2; auto. Qed. Lemma exists_nonexpansive `{ASA A} : forall B (X : pred A -> B -> pred A), (forall x, (nonexpansive (fun y => X y x))) -> nonexpansive (fun x => (existential (X x))). Proof. unfold nonexpansive; intros. apply sub_equ; apply sub_exists; intros. apply equ_sub; auto. apply equ_sub2; auto. Qed. Lemma later_contractive `{ASA A} : forall F, nonexpansive F -> contractive (fun X => (|>(F X))). Proof. unfold nonexpansive, contractive; intros. apply sub_equ. rewrite <- sub_later. apply box_positive; auto. apply equ_sub; auto. rewrite <- sub_later. apply box_positive; auto. apply equ_sub2; auto. Qed. Lemma box_contractive `{ASA A} : forall F (M:modality), inclusion _ M fashionable -> contractive F -> contractive (fun X => box M (F X)). Proof. unfold contractive; intros. apply sub_equ. apply sub_box; auto. apply equ_sub; auto. apply sub_box; auto. apply equ_sub2; auto. Qed. Lemma box_nonexpansive `{ASA A} : forall F (M:modality), inclusion _ M fashionable -> nonexpansive F -> nonexpansive (fun X => box M (F X)). Proof. unfold nonexpansive; intros. apply sub_equ. apply sub_box; auto. apply equ_sub; auto. apply sub_box; auto. apply equ_sub2; auto. Qed. Lemma diamond_contractive `{ASA A} : forall F (M:modality), inclusion _ M fashionable -> contractive F -> contractive (fun X => diamond M (F X)). Proof. unfold contractive; intros. apply sub_equ. apply sub_diamond; auto. apply equ_sub; auto. apply sub_diamond; auto. apply equ_sub2; auto. Qed. Lemma diamond_nonexpansive `{ASA A} : forall F (M:modality), inclusion _ M fashionable -> nonexpansive F -> nonexpansive (fun X => diamond M (F X)). Proof. unfold nonexpansive; intros. apply sub_equ. apply sub_diamond; auto. apply equ_sub; auto. apply sub_diamond; auto. apply equ_sub2; auto. Qed. Lemma contractive_nonexpansive `{ASA A} : forall F, contractive F -> nonexpansive F. Proof. unfold contractive, nonexpansive; intros. apply derives_cut with (|>(P <=>Q)); auto. apply now_later. Qed. Lemma sep_con_contractive `{ASA A} : forall F G, contractive F -> contractive G -> contractive (fun x => F x * G x). Proof. unfold contractive; intros. apply sub_equ. apply sub_con; apply equ_sub; auto. apply sub_con; apply equ_sub2; auto. Qed. Lemma sep_con_nonexpansive `{ASA A} : forall F G, nonexpansive F -> nonexpansive G -> nonexpansive (fun x => F x * G x). Proof. unfold nonexpansive; intros. apply sub_equ. apply sub_con; apply equ_sub; auto. apply sub_con; apply equ_sub2; auto. Qed. Lemma wand_contractive `{ASA A} : forall F G, contractive F -> contractive G -> contractive (fun x => F x -* G x). Proof. unfold contractive; intros. apply sub_equ. apply sub_wand. apply equ_sub2; auto. apply equ_sub; auto. apply sub_wand. apply equ_sub; auto. apply equ_sub2; auto. Qed. Lemma wand_nonexpansive `{ASA A} : forall F G, nonexpansive F -> nonexpansive G -> nonexpansive (fun x => F x -* G x). Proof. unfold nonexpansive; intros. apply sub_equ. apply sub_wand. apply equ_sub2; auto. apply equ_sub; auto. apply sub_wand. apply equ_sub; auto. apply equ_sub2; auto. Qed. Lemma prove_contractive `{ASA A} : forall F, (forall P Q, |>(P >=> Q) |-- F P >=> F Q) -> contractive F. Proof. intros. unfold contractive. intros. apply sub_equ. apply derives_cut with (|>(P >=> Q)). apply box_positive. apply equ_sub. hnf; auto. auto. apply derives_cut with (|>(Q >=> P)). apply box_positive. apply equ_sub2. hnf; auto. auto. Qed. Lemma prove_HOcontractive `{ASA A} : forall X F, (forall P Q, (All_ x:X, |>(P x >=> Q x) |-- All_ x:X, F P x >=> F Q x)) -> HOcontractive F. Proof. unfold HOcontractive. repeat intro. split. eapply H0; eauto. repeat intro; eapply H1; eauto. eapply H0; eauto. repeat intro; eapply H1; eauto. Qed. Lemma Rec_sub `{ASA A} : forall G (F : pred A -> pred A -> pred A) (HF1 : forall X, contractive (F X)) (HF2 : forall R P Q, P >=> Q |-- F P R >=> F Q R) (HF3 : forall P Q X, |>(P >=> Q) |-- F X P >=> F X Q), forall P Q, G |-- P >=> Q -> G |-- Rec (HF1 P) >=> Rec (HF1 Q). Proof. intros. apply derives_cut with (P >=> Q); auto. clear H0. apply goedel_loeb; repeat intro. destruct H0. rewrite Rec_fold_unfold. spec HF2 (Rec (HF1 Q)) P Q. spec HF2 a H0. spec HF2 a' H1. eapply HF2; auto. rewrite Rec_fold_unfold in H3. generalize (HF3 (Rec (HF1 P)) (Rec (HF1 Q)) P); intros. spec H5 a H4. spec H5 a' H1. eapply H5; auto. Qed. Lemma HORec_sub `{ASA A} : forall G B (F : pred A -> (B -> pred A) -> B -> pred A) (HF1 : forall X, HOcontractive (F X)) (HF2 : forall R a P Q, P >=> Q |-- F P R a >=> F Q R a) (HF3 : forall P Q X, All_ b:B, |>(P b >=> Q b) |-- All_ b:B, F X P b >=> F X Q b), forall P Q, G |-- P >=> Q -> G |-- All_ b:B, HORec (HF1 P) b >=> HORec (HF1 Q) b. Proof. intros. apply derives_cut with (P>=>Q); auto. clear H0. apply goedel_loeb; repeat intro. destruct H0. rewrite HORec_fold_unfold. spec HF2 (HORec (HF1 Q)). spec HF2 b P Q a H0. spec HF2 a' H1. apply HF2; auto. rewrite HORec_fold_unfold in H3. rewrite box_all in H4. spec HF3 (HORec (HF1 P)) (HORec (HF1 Q)). spec HF3 P a H4 b. spec HF3 a' H1. apply HF3; auto. Qed. Lemma Rec_contractive `{ASA A} : forall (F : pred A -> pred A -> pred A) (HF1 : forall X, contractive (F X)) (HF2 : forall R, contractive (fun X => F X R)), contractive (fun X => Rec (HF1 X)). Proof. intros; hnf; intros. simpl. apply goedel_loeb; repeat intro. destruct H0. split; repeat intro. rewrite Rec_fold_unfold. spec HF2 (Rec (HF1 Q)). spec HF2 P Q a H0. spec HF2 a' H1. destruct HF2. eapply H5; auto. rewrite Rec_fold_unfold in H4. generalize (HF1 P (Rec (HF1 P)) (Rec (HF1 Q))); intros. spec H7 a. detach H7; auto. spec H7 a' H1. destruct H7; eauto. rewrite Rec_fold_unfold. spec HF2 (Rec (HF1 P)). spec HF2 P Q a H0. spec HF2 a' H1. destruct HF2. eapply H6; auto. rewrite Rec_fold_unfold in H4. generalize (HF1 Q (Rec (HF1 P)) (Rec (HF1 Q))); intros. spec H7 a. detach H7; auto. spec H7 a' H1. destruct H7; eauto. Qed. Lemma Rec_nonexpansive `{ASA A} : forall (F : pred A -> pred A -> pred A) (HF1 : forall X, contractive (F X)) (HF2 : forall R, nonexpansive (fun X => F X R)), nonexpansive (fun X => Rec (HF1 X)). Proof. intros; hnf; intros. simpl. apply goedel_loeb; repeat intro. destruct H0. split; repeat intro. rewrite Rec_fold_unfold. spec HF2 (Rec (HF1 Q)). spec HF2 P Q a H0. spec HF2 a' H1. destruct HF2. eapply H5; auto. rewrite Rec_fold_unfold in H4. generalize (HF1 P (Rec (HF1 P)) (Rec (HF1 Q))); intros. spec H7 a. detach H7; auto. spec H7 a' H1. destruct H7; eauto. rewrite Rec_fold_unfold. spec HF2 (Rec (HF1 P)). spec HF2 P Q a H0. spec HF2 a' H1. destruct HF2. eapply H6; auto. rewrite Rec_fold_unfold in H4. generalize (HF1 Q (Rec (HF1 P)) (Rec (HF1 Q))); intros. spec H7 a. detach H7; auto. spec H7 a' H1. destruct H7; eauto. Qed. Lemma HORec_contractive `{ASA A} : forall B (F : pred A -> (B -> pred A) -> B -> pred A) (HF1 : forall X, HOcontractive (F X)) (HF2 : forall R a, contractive (fun X => F X R a)), forall a, contractive (fun X => HORec (HF1 X) a). Proof. intros; hnf; intros. simpl. cut (|>(P <=> Q) |-- All_ a:B, HORec (HF1 P) a <=> HORec (HF1 Q) a). repeat intro. eapply H0; eauto. clear a. apply goedel_loeb. repeat intro. destruct H0. split; repeat intro. rewrite HORec_fold_unfold. spec HF2 (HORec (HF1 Q)) b. spec HF2 P Q a H0. spec HF2 a' H1. destruct HF2. eapply H5; auto. rewrite HORec_fold_unfold in H4. generalize (HF1 P (HORec (HF1 P)) (HORec (HF1 Q))); intros. spec H7 a. detach H7. spec H7 b a' H1. destruct H7; eauto. rewrite <- box_all. auto. rewrite HORec_fold_unfold. spec HF2 (HORec (HF1 P)) b. spec HF2 P Q a H0. spec HF2 a' H1. destruct HF2. eapply H6; auto. rewrite HORec_fold_unfold in H4. generalize (HF1 Q (HORec (HF1 P)) (HORec (HF1 Q))); intros. spec H7 a. detach H7. spec H7 b a' H1. destruct H7; eauto. rewrite <- box_all. auto. Qed. Lemma HORec_nonexpansive `{ASA A} : forall B (F : pred A -> (B -> pred A) -> B -> pred A) (HF1 : forall X, HOcontractive (F X)) (HF2 : forall R a, nonexpansive (fun X => F X R a)), forall a, nonexpansive (fun X => HORec (HF1 X) a). Proof. intros; hnf; intros. simpl. cut (P <=> Q |-- All_ a:B, HORec (HF1 P) a <=> HORec (HF1 Q) a). repeat intro. eapply H0; eauto. clear a. apply goedel_loeb. repeat intro. destruct H0. split; repeat intro. rewrite HORec_fold_unfold. spec HF2 (HORec (HF1 Q)) b. spec HF2 P Q a H0. spec HF2 a' H1. destruct HF2. eapply H5; auto. rewrite HORec_fold_unfold in H4. generalize (HF1 P (HORec (HF1 P)) (HORec (HF1 Q))); intros. spec H7 a. detach H7. spec H7 b a' H1. destruct H7; eauto. rewrite <- box_all. auto. rewrite HORec_fold_unfold. spec HF2 (HORec (HF1 P)) b. spec HF2 P Q a H0. spec HF2 a' H1. destruct HF2. eapply H6; auto. rewrite HORec_fold_unfold in H4. generalize (HF1 Q (HORec (HF1 P)) (HORec (HF1 Q))); intros. spec H7 a. detach H7. spec H7 b a' H1. destruct H7; eauto. rewrite <- box_all. auto. Qed.