proposition: Lemma AssignablePivotTargets_Correct: forall p st a1 a2 pivot, CorrectBacklinks p st -> (fst a1) [=] (fst a2) -> (snd a1) [=] (snd a2) -> Rac2.AssignablePivotTargets p st@h pivot a1 [=] AssignablePivotTargets p st@bl pivot a2.
proof: Proof. intros. unfold CorrectBacklinks in H. split; intros. destruct a1. destruct a2. simpl in *. rewrite Rac2.AssignablePivotTargets_def in H2. destruct H2 as (dg', H2). destruct H2. destruct H3 as (dg, H3). destruct H3. unfold AssignablePivotTargets. apply list2LocSet_1. apply filter_In. apply H in H2. destruct H2 as (dgs, H2). destruct H2. split. apply Backlinks.keys_1. intro. apply LocDict_get_some in H2. destruct H2. rewrite H2 in H6. inversion H6. rewrite H2. case_eq (LocSet.fold (fun (elem : LocSet.elt) (b : bool) => Assignable p st @bl elem (t1, t2) || b) dgs false); intro. trivial. rewrite <- not_true_iff_false in H6. rewrite LocSet_fold_orb in H6. elim H6. clear H6. exists dg'. split; trivial. unfold Assignable. simpl. rewrite LocSet_fold_orb. exists dg. split; trivial. rewrite <- H1; trivial. rewrite <- FieldInDg_rac3_Correct. rewrite <- FieldInDg_rac2_Correct with (ep1 := t); trivial. auto with *. destruct a1. destruct a2. simpl in *. rewrite Rac2.AssignablePivotTargets_def. unfold AssignablePivotTargets in H2. apply list2LocSet_1 in H2. apply filter_In in H2. destruct H2 as (H', H2). case_eq (LocDict.get (get_backlinks st @bl a) pivot); intros. rewrite H3 in H2. case_eq (LocSet.fold (fun (dg : LocSet.elt) (b : bool) => Assignable p st @bl dg (t1, t2) || b) v false); intros. apply LocSet_fold_orb in H4. destruct H4. destruct H4. exists x. split. apply H. exists v. auto. unfold Assignable in H5. apply LocSet_fold_orb in H5. simpl in H5. destruct H5 as (dg, H5). exists dg. rewrite H1. rewrite FieldInDg_rac2_Correct with (ep2 := t1); trivial. rewrite FieldInDg_rac3_Correct; trivial. destruct H5. auto. rewrite H4 in H2. inversion H2. rewrite H3 in H2. inversion H2. Qed.
imports: Coq(List) JML(Stack) Coq(ListSet) Coq(Bool) Coq(ZArith) Coq(Relation_Operators) JML(ListHelpers) Coq(Classical) Coq(DecidableType) Coq(FSetInterface) Coq(FSetProperties) Coq(FSetEqProperties) Coq(FSetFacts) Coq(Sumbool) Coq(Lia)