proposition: Theorem abstract_i_sound : forall i e i' e', abstract_i i e = (i', e') -> forall g, i_lc m g (vcg i' (to_a' e')).
proof: Proof. induction i. simpl; intros e i' e' Heq; injection Heq; intros; subst i' e'; simpl; split; auto. intros Hyp; apply i_a_ab_update; auto. apply ab_eval_i_a; auto. simpl; intros e i' e'. assert (IHi1' := IHi1 e); clear IHi1. destruct (abstract_i i1 e) as [i'1 [l' | ]]. assert (Hpc:= abstract_i_pre_condition i2 l'). assert (IHi2' := IHi2 l'); clear IHi2. destruct (abstract_i i2 l') as [i'2 [l'' | ]]. intros Heq; injection Heq; do 2 intro; subst i' e'; simpl. intros g; simpl; apply app_i_lc. apply (IHi2' i'2 (Some l'')); auto. simpl in Hpc; rewrite Hpc; apply (IHi1' i'1 (Some l')); auto. intros Heq; injection Heq; intros Hi' He'; subst i' e'. intros g; simpl; apply app_i_lc. apply IHi2' with (i':=i'2)(e':= (@None ab_env)); auto. simpl in Hpc; rewrite Hpc; apply (IHi1' i'1 (Some l')); auto. intros Heq; injection Heq; intros Hi' He'; subst i' e'. intros g; simpl; split. rewrite f_p_lookup; rewrite false_top; intuition. apply app_i_lc. apply mark_sound. apply (IHi1' i'1 (@None ab_env)); auto. simpl; intros e i' e'. case_eq (intersect_env true e b). intros l Hl. case_eq (fp e b i (abstract_i i)). intros i2 [l' | ] Hfp. case_eq (intersect_env false l' b). intros l'' Hneg Heq; injection Heq; do 2 intro; subst i' e'; intros g. simpl. split. apply fp_monotonic_entry with (1:= Hfp). split. intros [Hb Hl']; change (to_a l'') with (to_a' (Some l'')). rewrite <- Hneg; apply intersect_env_false_i_a; auto. split. exact (fp_precondition e b i i i2 l' Hfp g). assert(Hel':=fp_thinner (abstract_i i)(abstract_i_compatible i) _ _ _ _ _ Hfp). destruct (intersect_env_true_accept e l' Hel' b l Hl) as [l0 [Hl0 Hthl0]]. destruct (fp_abstract_i_body_accept _ _ _ _ _ l' l0 Hfp Hl0) as [l1 Hl1]. assert (IHi' := IHi l0 i2 (Some l1) Hl1). assert (Hl1l' := fp_abstract_i_body_imp_invariant e b i i2 i2 _ _ _ (abstract_i i) (abstract_i_compatible i) Hl0 Hfp Hl1). assert (Hl1l'_c : forall g, i_c Ab.m g (c_imp (to_a l1)(to_a l'))) by exact (thinner_env_prop _ _ Hl1l'). destruct (vcg_shift _ _ (to_a l1)(to_a l') IHi' Hl1l'_c g); auto. intros Hinter Heq; injection Heq; do 2 intro; subst i' e'. simpl; intros g; split. apply (fp_monotonic_entry g e b i i i2 l');auto. split. intros [Hnt Hia]; change (i_a m g (to_a' None)); rewrite <- Hinter. apply intersect_env_false_i_a; auto. split. intros [Hb Hia]; apply fp_precondition with (1:=Hfp); simpl; auto. assert(Hel':=fp_thinner (abstract_i i)(abstract_i_compatible i) _ _ _ _ _ Hfp). destruct (intersect_env_true_accept e l' Hel' b l Hl) as [l0 [Hl0 Hthl0]]. destruct (fp_abstract_i_body_accept _ _ _ _ _ l' l0 Hfp Hl0) as [l1 Hl1]. assert (IHi' := IHi l0 i2 (Some l1) Hl1). assert (Hl1l' := fp_abstract_i_body_imp_invariant e b i i2 i2 _ _ _ (abstract_i i) (abstract_i_compatible i) Hl0 Hfp Hl1). assert (Hl1l'_c : forall g, i_c Ab.m g (c_imp (to_a l1)(to_a l'))) by exact (thinner_env_prop _ _ Hl1l'). destruct (vcg_shift m i2 (to_a l1)(to_a l') IHi' Hl1l'_c g); auto. intros Heq; injection Heq; do 2 intros; subst i' e'; clear Heq. simpl. split; auto. split. intros [Hnt Hia]; apply intersect_env_false_i_a; auto. elim fp_none_start with (1:= Hfp). intros e' [e2 [Hai [Hth Hinter]]]. assert (Hpc := abstract_i_pre_condition i e2 (to_a e)). rewrite Hai in Hpc; simpl in Hpc; rewrite Hpc. change (to_a e2) with (to_a' (Some e2)). rewrite <- Hinter. split. intros [Hb Hia]. apply intersect_env_true_i_a. apply thinner_env_prop with e; auto. exact Hb. assert (HFalse_e: forall g, i_c Ab.m g (c_imp (to_a' None) (to_a e))) by (simpl; rewrite f_p_lookup; rewrite false_top; intuition). assert (IHi' := IHi e2 i2 None Hai). destruct (vcg_shift m i2 (to_a' None)(to_a e) IHi' HFalse_e g); auto. intros Hinter Heq; injection Heq; do 2 intro; subst e' i'; simpl. intros g. split. intros Hyp; split; auto. intros Habs. assert (Habs' : i_a Ab.m g (a_b b)) by exact Habs. assert (i_a Ab.m g (to_a' None)). rewrite <- Hinter; apply intersect_env_true_i_a; auto. elim intersect_env_true_none with (1:=Hinter)(2:=Hyp);auto. split. intuition. split. intuition. assert (Hi := fun g => i_lc_vcg_mark g i). assert (Ha : forall g, i_c Ab.m g (c_imp false_assert (a_conj (a_not (a_b b))(to_a e)))). simpl; intros g'; rewrite f_p_lookup; intros Hf. rewrite Ab.false_top in Hf; intuition. destruct (vcg_shift Ab.m (mark i) false_assert (a_conj (a_not (a_b b))(to_a e)) Hi Ha g) as [Hv1 Hv2]; auto. simpl; intros e i' e' Heq; injection Heq; do 2 intro; subst i' e'; simpl; auto. Qed.
imports: syntax little denot Bool List String ZArith axiom