proposition: Lemma canonical_ram_reduce1: forall {A} QG RG QL RL s QL' RL' QG' RG' (Pure: A -> Prop) QG1' QG2', (forall a: A, exists TempG1 TempG2, split_by_closed s (QG' a) TempG1 TempG2 /\ QG1' a = TempG1 /\ QG2' a = TempG2) -> LOCALx QG TT |-- LOCALx QL TT -> (forall a: A, LOCALx QG TT |-- LOCALx (QG1' a) TT) -> (forall a: A, LOCALx (QL' a) TT |-- LOCALx (QG2' a) TT) -> SEPx RG |-- SEPx RL * ModBox s (ALL a: A, !! Pure a --> (SEPx (RL' a) -* SEPx (RG' a))) -> PROPx nil (LOCALx QG (SEPx RG)) |-- PROPx nil (LOCALx QL (SEPx RL)) * ModBox s (ALL a: A, !! Pure a --> (PROPx nil (LOCALx (QL' a) (SEPx (RL' a))) -* PROPx nil (LOCALx (QG' a) (SEPx (RG' a))))).
proof: Proof. intros. assert (forall a, EnvironStable (vars_relation (modifiedvars s)) (LOCALx (QG1' a) TT) /\ LOCALx (QG' a) TT = LOCALx (QG1' a) TT && LOCALx (QG2' a) TT). 1: { intro a; clear - H. destruct (H a) as [? [? [? [? ?]]]]. subst. apply split_by_closed_spec; auto. } pose proof (fun a => (proj1 (H4 a))). pose proof (fun a => (proj2 (H4 a))). clear H H4. rewrite !(PROPx_andp _ (LOCALx _ _)). rewrite !(LOCALx_andp _ (SEPx _)). rewrite corable_andp_sepcon1 by apply corable_PROP. apply andp_derives; auto. rewrite corable_andp_sepcon1 by apply corable_LOCAL. apply andp_right; [apply andp_left1; auto |]. eapply sepcon_EnvironBox_weaken with (allp ((fun a: A => LOCALx (QG1' a) TT) && (fun a: A => LOCALx (QL' a) TT --> LOCALx (QG2' a) TT) && (fun a: A => (!!Pure a --> (SEPx (RL' a) -* SEPx (RG' a)))))). 1: { apply allp_derives; intro a. change (((fun a0 : A => LOCALx (QG1' a0) TT) && (fun a0 : A => LOCALx (QL' a0) TT --> LOCALx (QG2' a0) TT) && (fun a0 : A => !!Pure a0 --> (SEPx (RL' a0) -* SEPx (RG' a0)))) a) with (LOCALx (QG1' a) TT && (LOCALx (QL' a) TT --> LOCALx (QG2' a) TT) && (!!Pure a --> (SEPx (RL' a) -* SEPx (RG' a)))). rewrite !(PROPx_andp _ (LOCALx _ _)). rewrite !(LOCALx_andp _ (SEPx _)). rewrite H6. unfold PROPx; simpl fold_right. fold (@TT (environ -> mpred) _); rewrite !TT_andp. rewrite <- imp_andp_adjoint. apply derives_extract_prop'; intro; rewrite prop_imp by auto. rewrite !andp_assoc. eapply derives_trans; [| apply wand_corable_andp; apply corable_LOCAL]. apply andp_derives; auto. apply corable_andp_wand_corable_andp; apply corable_LOCAL. } rewrite !allp_andp. rewrite !@EnvironBox_andp. rewrite andp_assoc, corable_sepcon_andp1 by (apply EnvironBox_corable, @corable_allp; intro; apply corable_LOCAL). apply andp_derives. 1: { rewrite @EnvironStable_EnvironBox. + apply allp_right; intro a; auto. + apply vars_relation_Equivalence. + apply EnvironStable_allp; auto. } rewrite corable_sepcon_andp1 by (apply EnvironBox_corable, @corable_allp; intro; apply corable_imp; apply corable_LOCAL). apply andp_right. 1: { apply derives_trans with TT; [apply TT_right |]. rewrite <- (@EnvironBox_TT _ _ _ (vars_relation (modifiedvars s))) at 1. apply EnvironBox_derives. apply allp_right; intro a. apply imp_andp_adjoint. apply andp_left2; auto. } auto. Qed.
imports: VST.floyd.base VST.floyd.canon VST.floyd.assert_lemmas VST.floyd.client_lemmas VST.floyd.reptype_lemmas VST.floyd.semax_tactics VST.floyd.local2ptree_denote VST.floyd.local2ptree_eval VST.floyd.call_lemmas VST.floyd.diagnosis VST.floyd.forward CertiGraph.lib.Coqlib CertiGraph.veric_ext.SeparationLogic CertiGraph.floyd_ext.ramification CertiGraph.floyd_ext.semax_ram_lemmas CertiGraph.floyd_ext.exists_trick CertiGraph.floyd_ext.closed_lemmas