proposition: Lemma fp_abstract_i_body_imp_invariant : forall e b i1 i3 i4 l' l'' l''' f, (forall l l', snd (f l) = Some l' -> compatible l l') -> intersect_env true l' b = Some l'' -> fp e b i1 f = (i3,Some l') -> f l'' = (i4, Some l''') -> thinner_env l''' l'.
proof: Proof. intros e b i1 i3 i4 l' l'' l''' f Hf Hi. unfold fp. case_eq (fp2 e e b i1 f); [intros i' [l1 | ] Hfp2 Heq Hai| intros l1 Hfp2]. injection Heq; do 2 intro; subst i3 l'. apply fp2_abstract_i_body_imp_invariant with (3:= Hfp2)(4:=Hi)(5:=Hai);auto. apply compatible_refl. discriminate. case_eq (fp2 e l1 b i1 f); [intros i2' [l2 | ] Hfp2' Heq Hai | intros l2 Hfp2']. injection Heq; do 2 intro; subst i3 l'. apply fp2_abstract_i_body_imp_invariant with (3:= Hfp2')(4:=Hi)(5:=Hai);auto. apply fp2_compatible2 with (2 := Hfp2); auto. apply compatible_refl. intros; discriminate. case_eq (fp1 (widen2 e) (widen2 e) b i1 f); intros i' [_l | ] Hfp1 Heq Hai. injection Heq; do 2 intro; subst i3 l'. apply compatible_thinner_widen2. apply compatible_sym; apply compatible_trans with (widen2 e). apply compatible_widen2. apply compatible_trans with l''. apply compatible_intersect_env with true b; auto. apply Hf; rewrite Hai; auto. discriminate. Qed.
imports: syntax little denot Bool List String ZArith axiom