proposition: Lemma refine_ELE_filter_by_and {T} (P : T -> Prop) (S0 : Ensemble T) : refine {ls : list T | EnsembleListEquivalence (fun x : T => Ensembles.In T S0 x /\ P x) ls } (filter_pred P S0).
proof: Proof. unfold filter_pred, fold_right, to_list; repeat intro; try inversion_by computes_to_inv. repeat match goal with | _ => intro | [ H : computes_to (Bind _ _) _ |- _ ] => apply computes_to_inv in H | _ => progress destruct_head ex | _ => progress destruct_head_hnf and | _ => progress split_iff | _ => progress inversion_by computes_to_inv | [ |- computes_to (Pick _) _ ] => constructor | [ |- EnsembleListEquivalence _ _ ] => split end. { match goal with | [ H : NoDup ?ls, H' : computes_to (List.fold_right _ _ _) ?v |- _ ] => revert H H'; clear; intros H H'; generalize dependent v; induction ls end; repeat match goal with | _ => intro | _ => progress subst | _ => progress simpl in * | [ H : computes_to (Bind _ _) _ |- _ ] => apply computes_to_inv in H | [ H : computes_to (ret _) _ |- _ ] => apply computes_to_inv in H | _ => progress destruct_head ex | _ => progress destruct_head_hnf and | _ => progress destruct_head_hnf bool | _ => progress split_iff | _ => progress inversion_by computes_to_inv | [ |- computes_to (Pick _) _ ] => constructor | [ |- EnsembleListEquivalence _ _ ] => split | [ |- NoDup nil ] => constructor | [ |- NoDup (_::_) ] => constructor | [ H : NoDup (_::_) |- _ ] => inversion H; clear H | [ H : ?T -> ?U, H' : ?T |- _ ] => specialize (H H') | [ IH : forall v, computes_to (List.fold_right _ _ _) v -> _, H : computes_to (List.fold_right _ _ _) _ |- _ ] => pose proof (@list_filter_pred_In _ _ _ _ H); apply IH in H; clear IH | [ H : true = true -> _ |- _ ] => specialize (H eq_refl) | _ => solve [ eauto ] end. } { unfold Ensembles.In in *. let H := match goal with H : computes_to _ _ |- _ => constr:(H) end in rewrite (@list_filter_pred_In_iff _ _ _ _ H). intuition. } 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