proposition: Lemma rt_closure_aux_spec: forall f (Hwf: terminates f) i acc acc' p, approx f acc -> rt_closure_aux Hwf i acc = (acc',p) -> StateMap.MapsTo i p acc' /\ approx f acc' /\ (forall j, StateMap.In j acc -> StateMap.In j acc').
proof: Proof. intros f Hwf. refine (Fix_induction Hwf (P:=fun i (g: statemap stateset -> _) => forall acc acc' p, approx f acc -> g acc = (acc',p) -> StateMap.MapsTo i p acc' /\ approx f acc' /\ (forall j, StateMap.In j acc -> StateMap.In j acc')) _). intros i G IH acc acc' p Hacc Hcall. StateMapProps.find_analyse. dependent destruction Hcall. auto. clear H. simpl in Hcall. destruct_fold_pair Hcall. apply add_valid. match type of H with stateset_fold _ ?f _ = _ => set (g:=f) in * end. pose (stateset_fold_rec_bis (f:=g) (P:=fun x' accy => let '(acc',y) := accy in approx f acc' /\ (forall j, StateSet.In j y -> steps f i j) /\ (forall j, steps f i j -> StateSet.In j y \/ exists2 k, StateSet.In k (StateSet.diff (f i) x') & steps f k j) /\ (forall j, StateMap.In j acc -> StateMap.In j acc') ) (i:=(acc,StateSet.singleton i)) (p:=f i) ) as H'. rewrite H in H'. clear H. apply apply in H'. apply apply in H'. apply apply in H'. intuition. intro j. intuition. destruct (H0 _ H2) as [? | [k ? ?]]; trivial. clear - H4. revert H4. StateSetProps.set_iff. tauto. StateMapProps.map_iff. auto. clear - IH. intros j [acc' p] y Hij Hnjy IHx. simpl. intuition. unfold g in *; clear g. case_eq (G j Hij acc'). intros acc'' pj Heq. apply IH in Heq; trivial; clear IH. intuition. revert H4. StateSetProps.set_iff. intros [H4|H4]. apply H5 in H2. apply H2 in H4. clear - Hij H4. econstructor 2; eassumption. apply H1 in H4. trivial. destruct (H0 _ H4) as [H8 | [k H9 H10]]. left. clear - H8. StateSetProps.set_iff. auto. destruct (eq_num_dec k j). subst. left. apply H5 in H2. apply H2 in H10. revert H10. clear. StateSetProps.set_iff. auto. right. exists k; trivial. revert H9. clear -n. StateSetProps.set_iff. intuition. clear - Hacc. intuition. revert H. StateSetProps.set_iff. intro H. subst. constructor 1. inversion_clear H. left. auto with set. right. exists y; trivial. StateSetProps.set_iff; auto with set. clear. intros u v [acc' y] Hu H. intuition. destruct (H1 j H2) as [?|[k ? ?]]; auto. right. exists k; auto. rewrite <- Hu. trivial. Qed.
imports: ATBR(Common) ATBR(Classes) ATBR(Graph) ATBR(Monoid) ATBR(SemiLattice) ATBR(SemiRing) ATBR(KleeneAlgebra) ATBR(MxGraph) ATBR(MxSemiLattice) ATBR(MxSemiRing) ATBR(MxKleeneAlgebra) ATBR(DKA_Definitions) ATBR(Utils_WF) Coq(Relations) Coq(Eqdep_dec)