proposition: Lemma refine_IgnoreUnusedKeyUpdate : forall (kv : Key * (Value -> Value)) (r : Ensemble (Key * Value)), refine { r' | (Same_set _ (fst r') (EnsembleUpdate (fst kv) r (snd kv))) /\ ((usedKey r (fst kv) /\ snd r' = true) \/ (~ usedKey r (fst kv) -> snd r' = false))} (b <- {b | decides b (usedKey r (fst kv))}; r' <- ret (EnsembleUpdate (fst kv) r (snd kv)); ret (r', 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 ]]). apply refine_under_bind. destruct a; simpl; intros. - refine pick val _; [reflexivity | intuition ]. - inversion_by computes_to_inv; simpl in H. f_equiv. apply refine_pick_val. unfold Same_set, Included; intuition; unfold In in *. 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