proposition: Lemma refine_ReplaceUsedKeyAdd : forall (kv : Key * Value) (r : Ensemble (Key * Value)), refine { r' | (SubEnsembleInsert kv r (fst r')) /\ ((usedKey r (fst kv) /\ snd r' = false) \/ (~ usedKey r (fst kv) /\ snd r' = true))} (b <- {b | decides b (usedKey r (fst kv))}; r' <- If b Then (ret (EnsembleReplace kv r)) Else { r' | SubEnsembleInsert kv r r' }; ret (r', negb b)).
proof: Proof. etransitivity. apply refine_pick_decides with (P := usedKey r (fst kv)); intros; refine pick pair; (apply refine_bind; [reflexivity | unfold pointwise_relation; intros; refine pick val _; [simplify with monad laws; higher_order_1_reflexivity | intuition ]]). f_equiv; unfold pointwise_relation; intros. destruct a; simpl. - refine pick val _; try reflexivity. apply SubEnsembleInsertReplace. - reflexivity. 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