proposition: Lemma finite_set_handle_EnsembleListEquivalence (ls : list W) : refine { ls' : _ | EnsembleListEquivalence (elements ls) ls' } (ret (snd (FiniteSetAndListOfList ls))).
proof: Proof. simpl. induction ls; simpl. { autosetoid_rewrite with refine_monad. repeat first [ intro | progress simpl | rewrite <- refine_skip | progress autosetoid_rewrite with refine_monad | progress inversion_by computes_to_inv | progress subst ]. econstructor; repeat constructor; eauto; simpl; eauto. } { rewrite refine_EnsembleListEquivalenceAdd. rewrite IHls; clear IHls. autorewrite with refine_monad. rewrite NoListJustFiniteSetOfList. match goal with | [ |- context[if ?E then _ else _] ] => case_eq E; intro end; handle_calls_then' ltac:(fun H => specialize (H _ (AbsR_EnsembleOfList_FiniteSetOfList _))); inversion_by computes_to_inv; t. { match goal with | [ H : Ensembles.In _ (EnsembleOfList _) _ |- _ ] => apply EnsembleOfList_In in H end. apply BindComputes with (comp_a_value := true); repeat constructor; eauto. } { apply BindComputes with (comp_a_value := false); repeat constructor; intros; eauto. match goal with | [ H : Ensembles.In _ (EnsembleOfList _) _ -> ?T |- ?T ] => apply H, EnsembleOfList_In; trivial end. } } 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