Require Import Classical. Require Import util. Require Import applpi. Require Import redseq. Require Import logic. Require Import logic_prop. Require Import logic_tactic2. Require Import logic_extensions. Set Implicit Arguments. (** fixpoint theory *) Definition imply_pred p q : Prop := forall P, P |=t p -> P |=t q. Definition is_monotonic F : Prop := forall p q, imply_pred p q -> imply_pred (F p) (F q). Lemma MU_is_least : forall F, is_monotonic F -> forall X, (forall P, tsat (F X) P -> tsat X P) -> forall Q, Q |=t (MU F) -> Q |=t X. intros. generalize (MU_sat_inv H1); intro. apply H2. intros. apply H0. auto. Qed. Lemma MU_is_prefixedpoint : forall F, is_monotonic F -> imply_pred (F (MU F)) (MU F). intros. red in H. red in |- *. intros. apply MU_sat. intros. apply H1. cut (imply_pred (F (MU F)) (F p)). intro. unfold imply_pred in H2. apply H2. auto. (* prove cut *) apply H. red. apply MU_is_least. unfold is_monotonic in |- *; auto. auto. Qed. Definition eq_pred p q := forall P, (tsat p P -> tsat q P) /\ (tsat q P -> tsat p P). Lemma MU_is_fix : forall F, is_monotonic F -> eq_pred (MU F) (F (MU F)). intros. unfold eq_pred in |- *. intro. split. (* (MU F) <= (F (MU F)) *) intro. (* we have (Mu F), we want to prove (F (Mu F)) *) generalize (MU_sat_inv H0); intro. (* by definition of (Mu F), it is enough to prove that (F (Mu F)) contains its image by F *) apply (H1 (F (MU F))). (* we have to prove (F (F (Mu F)))->(F (Mu F)), i.e. (F (Mu F))->(Mu F) by monotonicity, true since (Mu F) is a pre-fixed point *) intro. apply H. apply MU_is_prefixedpoint. auto. (* (F (MU F)) <= (MU F)*) apply MU_is_prefixedpoint. auto. Qed. Unset Implicit Arguments. Lemma contra : forall (T : Type) (p q : T -> Prop), (forall Q : T, p Q -> q Q) -> forall Q : T, ~ q Q -> ~ p Q. intros. intro. apply H0. apply H. auto. Qed. Inductive Redsp (phi : state -> Prop) : state -> state -> Type := | redsp_b : forall P Q : state, Red P Q /\ phi P /\ phi Q -> Redsp phi P Q | redsp_i : forall P Q R : state, Redsp phi P Q -> Red Q R /\ phi R -> Redsp phi P R. Inductive Redsp' (phi : state -> Prop) : state -> state -> Type := | redsp_b' : forall P Q : state, Red P Q /\ phi P /\ phi Q -> Redsp' phi P Q | redsp_i' : forall P Q R : state, Red P Q /\ phi P -> Redsp' phi Q R -> Redsp' phi P R. Lemma redsp'_trans : forall (phi : state -> Prop) (P Q R : state), Redsp' phi P Q -> Redsp' phi Q R -> Redsp' phi P R. intros. induction X. apply redsp_i' with (Q := Q). decompose [and] a; clear a. auto. auto. apply redsp_i' with (Q := Q). auto. apply IHX. auto. Qed. Lemma redsp_redsp' : forall (phi : state -> Prop) (P Q : state), Redsp phi P Q -> Redsp' phi P Q. intros. elim X. intros. decompose [and] a;clear a. apply redsp_b'. auto. intros. inversion r. clear H0 H1 P1 Q1. decompose [and] H;clear H. apply redsp_i' with (Q:=Q0). auto. apply redsp_b'. inversion_clear a. auto. clear H0 H1 P1 R0. assert (Redsp' phi Q0 R). apply redsp_b'. inversion_clear a. inversion_clear H. auto. apply redsp'_trans with (Q:=Q0). auto. auto. Qed. (** equivalence between the native mustev predicate and the fixpoint version *) Lemma mustev_mu : forall (p : tform) (P : state), tsat (MUSTEV p) P -> tsat (MUSTEV_ALT p) P. intros. unfold MUSTEV_ALT in |- *. apply MU_sat. intros. apply NNPP. intro. (* given the hypothesis ~(sat p0 P) and the hypothesis H0, we show ~(sat p P) and (NEXT (NEG p0) P) *) generalize (contra state (fun Q : state => tsat (ORT p (ANDT (NEGT STABLE) (MUST_NEXT p0))) Q) (fun Q : state => tsat p0 Q) H0); intro. generalize (H2 _ H1); clear H2; intro. generalize (not_ORT_ANDT H2); clear H2; intro. generalize (ANDT_sat_inv H2); clear H2; intro. inversion_clear H2. generalize (NEGT_ANDT_ORT H4); clear H4; intro. generalize (ORT_sat_inv H2); clear H2; intro. inversion_clear H2. generalize (NEGT_NEGT H4); clear H4; intro. generalize (MUSTEV_sat_inv H); intro. generalize (H4 (fun x : nat => match x with | O => SomeT _ P | _ => NoneT state end) (refl_equal (SomeT _ P))); intro. cut (isMaxRedSeq (fun x : nat => match x with | O => SomeT state P | S _ => NoneT state end)). intro. generalize (H5 H6); clear H5 H6; intro. inversion_clear H5. inversion_clear H6. inversion_clear H5. induction x0. injection H6; intro. rewrite <- H5 in H7. generalize (NEGT_sat_inv H3); intro. apply H8; auto. discriminate H6. red in |- *. split. red in |- *. split. case n. intros. auto. intros. discriminate H6. auto. intros. induction n. injection H6; intro. rewrite <- H8. generalize (STABLE_sat_inv H2); intro. auto. discriminate H6. generalize (NEGT_sat_inv H4); clear H4; intro. apply H2; clear H2. apply MUST_NEXT_sat. intros. apply NNPP; intro. generalize (conj H2 H4); clear H2 H4; intro. rename Q into P'. (* to solve the probleme it is enough to find an infinite sequence of processes such that p0 nevers holds *) cut (exists PS : stateSeq, PS 0 = SomeT _ P /\ (forall n : nat, exists Q0 : state, (exists Q : state, PS n = SomeT _ Q0 /\ PS (S n) = SomeT _ Q /\ Red Q0 Q /\ ~ tsat p0 Q0))). intro. inversion_clear H4. inversion_clear H5. generalize (MUSTEV_sat_inv H); clear H; intro. generalize (H x); intro. assert (isMaxRedSeq x). red in |- *. split. red in |- *. split. intros. generalize (H6 n); intro. inversion_clear H8. inversion_clear H9. decompose [and] H8; clear H8. left. exists x1. rewrite H7 in H9; injection H9; intro. rewrite H8; auto. intro. generalize (H6 n). intro X; inversion_clear X. inversion_clear H8. decompose [and] H9; clear H9. rewrite H8 in H7; discriminate H7. intros. generalize (H6 n). intro X; inversion_clear X. inversion_clear H9. decompose [and] H10; clear H10. rewrite H8 in H12; discriminate H12. generalize (H5 H4 H7); intro. inversion_clear H8. inversion_clear H9. inversion_clear H8. generalize (H6 x1); intro. inversion_clear H8. inversion_clear H11. decompose [and] H8; clear H8. (* comme dans le preambule, on derive ~(p x3) de ~(p0 x3) *) generalize (contra state (fun Q : state => tsat (ORT p (ANDT (NEGT STABLE) (MUST_NEXT p0))) Q) (fun Q : state => tsat p0 Q) H0); intro. generalize (H8 x2 H15); clear H8; intro. generalize (not_ORT_ANDT H8); clear H8; intro. generalize (ANDT_sat_inv H8); clear H8; intro. inversion_clear H8. rewrite H9 in H11; injection H11; intros. rewrite H8 in H10. generalize (NEGT_sat_inv H14); clear H14; intro. apply H14; auto. cut (ex (fun PS : nat -> state => PS 0 = P /\ (forall n : nat, Red (PS n) (PS (S n)) /\ ~ tsat p0 (PS (S n))))). intros X. elim X. intros x p1. exists (fun k : nat => SomeT _ (x k)). split. inversion_clear p1. rewrite H4; auto. intro. exists (x n). exists (x (S n)). split; auto. split; auto. induction n. inversion_clear p1. generalize (H5 0); intro. inversion_clear H6. split; auto. rewrite H4; auto. inversion_clear p1. generalize (H5 (S n)); intro. split. inversion_clear H6. auto. generalize (H5 n); intro. inversion_clear H7. auto. (* on peut ecrire une fonction correspondant a la reduction sequence desiree a partir d'une preuve de l'existence d'un successeur adequat pour tout etat x atteint vie une reduction sequence adequate *) Fixpoint mustev_mu_g (phi : state -> Prop) (seed0 seed1 : state) (H : Redsp phi seed0 seed1) (X0 : forall (x : state) (Px : Redsp phi seed0 x), sigT (fun y : state => Red x y /\ phi y)) (k : nat) {struct k} : sigT (fun y : state => Redsp phi seed0 y) := match k with | O => existT (fun x => Redsp phi seed0 x) seed1 H | S n => match mustev_mu_g phi seed0 seed1 H X0 n with | existT m M => match X0 m M with | existT l L => existT (fun x => Redsp phi seed0 x) l (redsp_i _ _ _ _ M L) end end end. Definition mustev_mu_h (phi : state -> Prop) (seed0 seed1 : state) (H : Redsp phi seed0 seed1) (X0 : forall (x : state) (Px : Redsp phi seed0 x), sigT (fun y : state => Red x y /\ phi y)) (n : nat) : state := match mustev_mu_g _ _ _ H X0 n with | existT m _ => m end. cut (forall (x : state) (H : Redsp (fun x : state => ~ tsat p0 x) P x), sigT (fun y : state => Red x y /\ ~ tsat p0 y)). intro. assert (Redsp (fun x : state => ~ tsat p0 x) P P'). apply redsp_b. inversion_clear H2. auto. exists (fun j : nat => match j with | O => P | S t => mustev_mu_h (fun x : state => ~ tsat p0 x) P P' X0 X t end). split. auto. intro. induction n. unfold mustev_mu_h in |- *; simpl in |- *. auto. unfold mustev_mu_h in |- *; simpl in |- *. elim (mustev_mu_g (fun x : state => ~ tsat p0 x) P P' X0 X n); intro. intro. elim (X x p1); intro. tauto. (* maintenant on doit prouver que tout etat atteint par une sequence d'etat ne verifiant pas p0 peut encore se prolonger *) intros. assert (Redsp (fun x : state => ~ tsat p x) P x). induction H4. apply redsp_b. split. decompose [and] a; clear a. auto. split. apply (NEGT_sat_inv H3). decompose [and] a; clear a. generalize (contra state (fun Q : state => tsat (ORT p (ANDT (NEGT STABLE) (MUST_NEXT p0))) Q) (fun Q : state => tsat p0 Q) H0); intro. generalize (H5 Q H7); clear H5; intro. generalize (not_ORT_ANDT H5); clear H5; intro. generalize (ANDT_sat_inv H5); clear H5; intro. inversion_clear H5. apply (NEGT_sat_inv H8). generalize (IHRedsp H H1 H3 H2); intro. apply redsp_i with (Q := Q). auto. assert (tsat p R \/ ~ tsat p R). apply classic. inversion_clear H5. generalize (H0 R); intro. assert (tsat (ORT p (ANDT (NEGT STABLE) (MUST_NEXT p0))) R). apply ORT_sat. left; auto. generalize (H5 H7); intro. inversion_clear a. generalize (H10 H8); contradiction. inversion_clear a. auto. assert (exists y : state, Red x y /\ ~ tsat p0 y). apply NNPP. intro. generalize (not_ex_all_not _ (fun y => Red x y /\ ~ tsat p0 y) H5); clear H5; intro. assert (forall n : state, Red x n -> tsat p0 n). intro. generalize (H5 n); intro. generalize (not_and_or _ _ H6); intro. generalize (or_to_imply _ _ H7); intro. intros. apply NNPP. tauto. cut (~ tsat STABLE x). intro. assert (~ tsat STABLE x /\ tsat (MUST_NEXT p0) x). split. auto. apply MUST_NEXT_sat. auto. assert (tsat (ORT p (ANDT (NEGT STABLE) (MUST_NEXT p0))) x). apply ORT_sat. right. apply ANDT_sat. split. apply NEGT_sat. intuition. intuition. generalize (H0 _ H9); intro. inversion H4. decompose [and] H11; clear H11. apply H17. auto. inversion_clear H11. apply H15. auto. intro. (* on montre par contradiction que x ne peut etre stable parce sinon on peut construire une sequence le long de laquelle p n'est jamais verifie *) Fixpoint mustev_mu_f (phi : state -> Prop) (P R : state) (H : Redsp' (fun x : state => ~ phi x) P R) (n : nat) {struct H} : optionT state := match H with | redsp_b' p q redpq => match n with | O => SomeT _ p | S O => SomeT _ q | S (S _) => NoneT state end | redsp_i' p q r redpq redqr => match n with | O => SomeT _ p | S O => SomeT _ q | S (S n) => mustev_mu_f phi _ _ redqr (S n) end end. generalize (MUSTEV_sat_inv H); clear H; intro. assert (Redsp' (fun x : state => ~ tsat p x) P x). apply redsp_redsp'. auto. generalize (H (mustev_mu_f (fun w : state => tsat p w) _ _ X0)); intro. assert (mustev_mu_f (fun w : state => tsat p w) _ _ X0 0 = SomeT state P). elim X0. simpl in |- *. auto. simpl in |- *. auto. assert (isRedSeq (mustev_mu_f (fun w : state => tsat p w) _ _ X0)). elim X0. simpl in |- *. intros. red in |- *. intro. case n. split. intros. left; exists Q. split; auto. injection H10; intros. rewrite <- H11. decompose [and] a; clear a. induction Q. auto. intro Z; discriminate Z. intros. split. intros. auto. auto. intros. assert (exists f0 : state, mustev_mu_f (fun w : state => tsat p w) _ _ r 0 = SomeT _ f0 /\ Red P0 f0). exists Q. split. elim r. simpl in |- *. auto. simpl in |- *. auto. inversion_clear a. auto. generalize (lem_RedSeq_is_prefix _ H10 _ H11); intros. assert (forall n : nat, mustev_mu_f (fun w : state => tsat p w) _ _ (redsp_i' (fun x0 : state => ~ tsat p x0) P0 Q R a r) n = (fun j : nat => match j with | O => SomeT state P0 | S k => mustev_mu_f (fun w : state => tsat p w) Q R r k end) n). intro. induction n. simpl in |- *. auto. induction n. simpl in |- *. elim r. simpl in |- *. auto. simpl in |- *. auto. simpl in |- *. auto. generalize (extension _ _ _ (fun j : nat => match j with | O => SomeT state P0 | S k => mustev_mu_f (fun w : state => tsat p w) Q R r k end) H13); intro. rewrite H14. auto. assert (exists n : nat, (exists x' : state, mustev_mu_f (fun w : state => tsat p w) P x X0 n = SomeT _ x' /\ Stable x' /\ (forall m : nat, n < m -> mustev_mu_f (fun w : state => tsat p w) P x X0 m = NoneT _))). assert (exists n : nat, mustev_mu_f (fun w : state => tsat p w) P x X0 n = SomeT state x). elim X0. simpl in |- *. intros. exists 1. auto. simpl in |- *. intros. inversion_clear H11. exists (S x0). induction x0. generalize H12; clear H12. elim r. simpl in |- *. auto. simpl in |- *. auto. auto. inversion_clear H11. exists x0. exists x. split; auto. split. apply (STABLE_sat_inv H7). intros. red in H11. generalize (STABLE_sat_inv H7); clear H7; intro. generalize (isRedSeq_stable_none _ H10 _ _ (conj H12 H7)); intro. assert (x0 < m). red in |- *. auto. apply H13. auto. generalize (redseq_is_maxredseq _ H10 H11); intro. generalize (H _ H9 H12); intro. inversion_clear H13. inversion_clear H14. inversion_clear H13. assert (forall (w : nat) (W : state), mustev_mu_f (fun w : state => tsat p w) P x X0 w = SomeT state W -> ~ tsat p W). elim X0. simpl in |- *. intros. induction w. injection H13; intro. rewrite <- H16. decompose [and] a; clear a. auto. induction w. injection H13; intros. rewrite <- H16; decompose [and] a; clear a. auto. discriminate H13. simpl in |- *. intros. induction w. injection H16; intros. rewrite <- H17. inversion_clear a. auto. induction w. assert (mustev_mu_f (fun w : state => tsat p w) Q R r 0 = SomeT state Q). elim r. simpl in |- *. auto. simpl in |- *. auto. generalize (H13 _ _ H17); intro. injection H16; intros. rewrite <- H19; auto. apply (H13 _ _ H16). generalize (H13 _ _ H14); intro. apply H16. auto. (* il existe forcement un y qui suit x et qui ne verifie pas p0 *) apply EXT_sigT with (P := fun y : state => Red x y /\ ~ tsat p0 y). auto. Qed.