proposition: Lemma FiniteSetAndFunctionOfList_pull_ret {A} (f : W -> A -> A) (a : A) (ls : list W) : refineEquiv (snd (FiniteSetAndFunctionOfList (fun w acc => a' <- acc; ret (f w a')) (ret a) ls)) (ret (snd (FiniteSetAndFunctionOfList f a ls))).
proof: Proof. revert a; induction ls; simpl. { reflexivity. } { intro; simpl in *. rewrite !NoFunctionJustFiniteSetOfFunction. match goal with | [ |- context[if ?E then _ else _] ] => destruct E end. { rewrite <- IHls; reflexivity. } { rewrite IHls; autorewrite with refine_monad; reflexivity. } } Qed.
imports: Coq.Strings.String Coq.Sets.Ensembles Coq.Sets.Finite_sets Coq.Lists.List Coq.Sorting.Permutation Coq.Classes.RelationPairs Fiat.ADT Fiat.ADT.ComputationalADT Fiat.ADTRefinement.Core Fiat.ADTNotation Fiat.ADTRefinement.GeneralRefinements Fiat.Computation Fiat.Common Fiat.Common.Ensembles Fiat.Common.Ensembles.Tactics Fiat.ComputationalEnsembles Fiat.FiniteSetADTs.FiniteSetADTMethodLaws Fiat.FiniteSetADTs.FiniteSetADT