proposition: Lemma find_minimum_Key_correct : forall indices kv, find_minimum_Key indices = Some kv -> forall k v, StringIndexedMap.find k indices = Some v -> snd kv <= v.
proof: Proof. intros. unfold find_minimum_Key in H. rewrite StringIndexedMap.fold_1 in H. apply StringIndexedMap.find_2 in H0. apply StringIndexedMap.elements_1 in H0. unfold StringIndexedMap.eq_key_elt in H0. unfold StringIndexedMap.Raw.Proofs.PX.eqke in H0. assert ( forall (k0 : StringIndexedMap.key) (v0 : nat) p', fold_left (fun (a : option (StringIndexedMap.key * nat)) (p : StringIndexedMap.key * nat) => Ifopt a as sv' Then if lt_dec (snd p) (snd sv') then Some (fst p, snd p) else Some sv' Else Some p) (StringIndexedMap.elements (elt:=nat) indices) (Some p') = Some kv -> SetoidList.InA (fun p p' : string * nat => fst p = fst p' /\ snd p = snd p') (k0, v0) (StringIndexedMap.elements (elt:=nat) indices) -> ((snd kv <= snd p') /\( snd kv <= v0 ))). { clear; induction (StringIndexedMap.elements (elt:=nat) indices); simpl; intros; subst; eauto. destruct p'; simpl in H. inversion H0; subst; intuition; simpl in *; subst; eauto. destruct (lt_dec (snd a) (snd p')). inversion H0; subst. intuition; simpl in *; intros; subst. destruct (fold_left_In _ _ H); injections; simpl; auto with arith. destruct kv. destruct (IHl _ _ _ H H1); simpl in *. eauto with arith. destruct (fold_left_In _ _ H); injections; simpl; auto with arith. destruct kv. destruct (IHl _ _ _ H H1); simpl in *; eauto with arith. intuition. destruct (IHl _ _ _ H H2); simpl in *. omega. destruct (IHl _ _ _ H H2); simpl in *; eauto. inversion H0; subst. destruct (fold_left_In _ _ H); injections; simpl; intuition; simpl in *; subst. apply not_gt. auto with arith. destruct kv. destruct (IHl _ _ _ H H1); simpl in *; eauto. destruct kv. destruct (IHl _ _ _ H H1); simpl in *; eauto. eapply le_trans. eapply H2. apply not_gt; auto with arith. destruct (IHl _ _ _ H H2); eauto. } destruct ((StringIndexedMap.elements (elt:=nat) indices)). simpl in H; discriminate. simpl in H. eapply H1 with (p' := p); eauto. simpl. destruct (lt_dec (snd p) (snd p)); eauto. exfalso. omega. rewrite <- H; f_equal. repeat (apply functional_extensionality; intros); f_equal. destruct x0; reflexivity. destruct p; 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