proposition: Lemma fp1_precondition : forall e l b i1 i2 i3 l', compatible e l -> fp1 e l b i1 (abstract_i i2) = (i3, Some l') -> forall g, i_a Ab.m g (a_conj (a_b b)(to_a l)) -> i_a Ab.m g (pc i3 (to_a l')).
proof: Proof. intros e l b i1 i2 i3 l' Hcel. unfold fp1. case_eq (intersect_env true l b). intros l0 Hi. assert (Hcll0 : compatible l l0) by (apply compatible_intersect_env with true b; auto). case_eq (abstract_i i2 l0); intros i' [l'' | ] Hai Heq. assert (Hcl0l'': compatible l0 l'') by (apply (abstract_i_compatible i2); rewrite Hai; auto). injection Heq; do 2 intro; subst i3 l'. intros g; simpl; intros [Hb Hl]. assert (Has_i : i_a Ab.m g (to_a' (Some l0))) by (rewrite <- Hi; apply intersect_env_true_i_a; auto). simpl in Has_i. apply precondition_shift with (to_a l0); auto. intros g0 Hal0. apply join_env_prop_right. apply compatible_sym; apply compatible_trans with l0. apply compatible_trans with l; auto. apply compatible_join_env_left; auto. apply thinner_env_prop with l0; auto. apply thinner_join_env_left; auto. change i' with (fst (i', Some l'')). rewrite <- Hai; rewrite abstract_i_pre_condition; auto. discriminate. intros Hi Heq; injection Heq; do 2 intro; subst i3 l'; clear Heq. simpl; intros g [Hb Hl]. case (intersect_env_true_none l b Hi g); auto. Qed.
imports: syntax little denot Bool List String ZArith axiom