proposition: Lemma pred_sepcon_ramif_1Q: forall {T: Type} (Pure: T -> Prop) (P: B -> Prop) (P': T -> B -> Prop) (p: B -> A) (p': T -> B -> A) (x: B) (x' : T -> B), (exists Pf, Prop_join (eq x) Pf P /\ (forall a, Pure a -> Prop_join (eq (x' a)) Pf (P' a)) /\ (forall a, Pure a -> (forall y, Pf y -> p y = (p' a) y))) -> pred_sepcon P p |-- p x * (ALL a: T, !! Pure a --> ((p' a) (x' a) -* pred_sepcon (P' a) (p' a))).
proof: Proof. intros. unfold pred_sepcon. normalize; intros; normalize; rename x0 into g. destruct H as [Pf [? [? ?]]]. destruct (Permutation_spec_Prop_join g P Pf x H (conj H0 H1)) as [f [? [? ?]]]. evar (pp : T -> A). evar (ll: T -> A). evar (gg: list B -> T -> A). assert ((fun a : T => !! Pure a --> (p' a (x' a) -* (EX l : list B, !! (forall x0 : B, In x0 l <-> P' a x0) && !! NoDup l && iter_sepcon l (p' a)))) = (pp --> (ll -* exp gg))). { extensionality x0. super_pattern (!! Pure x0) x0. super_pattern (p' x0 (x' x0)) x0. super_pattern (fun l => !! (forall x1 : B, In x1 l <-> P' x0 x1) && !! NoDup l && iter_sepcon l (p' x0)) x0. instantiate (1 := (fun t : T => !! Pure t)) in (value of pp). instantiate (1 := (fun t : T => p' t (x' t))) in (value of ll). instantiate (1 := (fun (l : list B) (t : T) => !! (forall x1 : B, In x1 l <-> P' t x1) && !! NoDup l && iter_sepcon l (p' t))) in (value of gg). subst pp gg ll. reflexivity. } subst pp gg ll. rewrite H7. clear H7. apply (RAMIF_Q'.exp_right (fun a => x' a :: f)); [simpl; auto |]. pose proof iter_sepcon_ramif_1Q Pure p p' g (fun a => x' a :: f) x x'. spec H7; [clear H7 |]. + exists f. split; auto. split; intros. - reflexivity. - apply (H3 _ H7). rewrite <- H5; auto. + eapply derives_trans; [exact H7 |]; clear H7. apply sepcon_derives; auto. apply allp_right; intros a. apply (allp_left _ a). simpl. apply imp_andp_adjoint; normalize. unfold TT; rewrite prop_imp by auto. apply wand_derives; auto. apply andp_right; auto. specialize (H2 _ H7). specialize (H3 _ H7). apply andp_right; apply prop_right. - intro y. rewrite H5. destruct H2 as [? _]. symmetry; apply H2. - apply NoDup_cons; auto. destruct H2 as [_ ?]. specialize (H2 (x' a) eq_refl). rewrite H5; auto. Qed.
imports: CertiGraph.msl_ext.log_normalize CertiGraph.msl_ext.iter_sepcon CertiGraph.lib.Coqlib CertiGraph.lib.EquivDec_ext CertiGraph.lib.EnumEnsembles CertiGraph.lib.List_ext VST.msl.base VST.msl.simple_CCC VST.msl.seplog VST.msl.log_normalize VST.msl.Coqlib2 VST.msl.ramification_lemmas