proposition: Lemma EnsembleListEquivalence_Intersection_elements1_fold (ls : list W) (S0 : Ensemble W) : refine { ls' : _ | EnsembleListEquivalence (Intersection W (elements ls) S0) ls' } (ls_S0 <- to_list S0; let fs_S0 := FiniteSetOfList ls_S0 in ret (UniqueFilterOfList ls (fun x => snd (CallMethod (projT1 FiniteSetImpl) sIn fs_S0 x) : bool))).
proof: Proof. induction ls; simpl. { repeat match goal with | _ => intro | _ => inversion_by computes_to_inv | [ H : computes_to (Bind _ _) _ |- _ ] => apply computes_to_inv in H | [ H : computes_to (ret _) _ |- _ ] => apply computes_to_inv in H | _ => progress destruct_head_hnf ex | _ => progress destruct_head_hnf and | _ => progress destruct_head_hnf Intersection | _ => progress destruct_head_hnf False | _ => progress subst | [ |- computes_to (Pick _) _ ] => constructor | _ => progress unfold to_list in * | _ => split | _ => progress unfold FunctionOfList, UniqueFilterOfList in * | _ => progress simpl in * | [ |- NoDup nil ] => constructor | _ => solve [ eauto ] end. } { intros; simpl. setoid_rewrite Same_set__elements_cons__Union; simpl. setoid_rewrite Same_set_Intersection_Union'. rewrite refineEquivUnion; [ | let H := fresh in intros ? ? ? H; rewrite H; reflexivity ]. unfold to_list. setoid_rewrite EnsembleListEquivalence_Intersection_Singleton; simpl. setoid_rewrite IHls; clear IHls. simpl. autosetoid_rewrite with refine_monad. rewrite refine_bind_dedup. apply refine_under_bind; intros. inversion_by computes_to_inv. unfold UniqueFilterOfList, FunctionOfList; simpl. repeat setoid_rewrite NoFunctionJustFiniteSetOfFunction. rewrite finite_set_handle_EnsembleListEquivalence; rewrite !NoFiniteSetJustListOfList. rewrite !NoFiniteSetJustFilterFunctionOfList. rewrite if_app; simpl. rewrite (pull_if UniqueListOfList). rewrite UniuqeListOfList_cons_UniqueFilterOfList. rewrite !UniqueListOfUniqueFilterOfList. repeat handle_calls''. rewrite EnsembleOfList_In in *. destruct_head bool; simpl; trivial. } 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