proposition: Lemma refine_SubEnsembleInsert : forall (kv : Key * Value) (r : Ensemble (Key * Value)), refine { r' | (SubEnsembleInsert kv r r')} (k_opt <- {k_opt | forall k', k_opt = Some k' -> exists v', r (k', v')}; Ifopt k_opt as k' Then ret (EnsembleInsert kv (EnsembleRemoveKey k' r)) Else ret (EnsembleInsert kv r)).
proof: Proof. intros; rewrite refine_Pick_If_Then_Opt with (P := fun k' => exists v', r (k', v')). f_equiv; unfold pointwise_relation; intros; simpl. destruct a; [ higher_order_1_reflexivity | reflexivity ]. simpl; intros; apply refine_pick_val; unfold Same_set, Included, In, SubEnsembleInsert, EnsembleInsert, EnsembleRemoveKey in *; simpl; intros; intuition. simpl; intros; apply refine_pick_val; unfold Same_set, Included, In, SubEnsembleInsert, EnsembleInsert, EnsembleRemoveKey in *; simpl; intros; intuition. Qed.
imports: Coq.Strings.String Coq.ZArith.ZArith Coq.Lists.List Coq.Logic.FunctionalExtensionality Coq.Sets.Ensembles Computation ADT ADTRefinement ADTNotation BuildADTRefinements KVEnsembles CacheSpec