proposition: Lemma refine_pick_oldest {V} : forall spec_indices impl_indices spec_values impl_values, EnsembleFMapEquivalence spec_indices impl_indices /\ EnsembleFMapEquivalence spec_values impl_values /\ FMapCommonKeys impl_values impl_indices -> refine {k_opt | forall k' : string, k_opt = Some k' -> ((exists v' : V, spec_values (k', v')) /\ (forall (idx : nat) (ki : string * nat), spec_indices (k', idx) -> spec_indices ki -> idx <= snd ki))} (ret (option_map fst (find_minimum_Key impl_indices))).
proof: Proof. unfold refine; intros; inversion_by computes_to_inv; subst. econstructor; intros. caseEq (find_minimum_Key impl_indices); rewrite H2 in *; simpl in *; try discriminate; injections. unfold EnsembleFMapEquivalence in *. pose proof (find_minimum_Key_correct _ H2). pose proof (find_minimum_Key_In _ H2). split; intros. unfold FMapCommonKeys in H3. destruct (H3 (fst p)). destruct (H6 (snd p)); eauto. destruct (H (fst p)); eexists; eauto. eapply H8. eauto using StringIndexedMap.find_1. apply H1 in H5; destruct ki; eapply H1 in H6. destruct_ex; simpl in *. eapply StringIndexedMap.find_1 in H4; rewrite H5 in H4. injection H4; intros; subst; eauto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec CacheRefinements String_as_OT FMapAVL