proposition: Lemma In_check_impl (S0 : Ensemble W) {T} (f : (W -> Prop) -> Comp T) `{fR : Proper _ (respectful (pointwise_relation _ iff) refine) f} : refine (f (Ensembles.In _ S0)) (ls <- to_list S0; let fs_S0 := FiniteSetOfList ls in (f (fun x => (snd (CallMethod (projT1 FiniteSetImpl) sIn fs_S0 x) : bool) = true))).
proof: Proof. intros v H'. apply computes_to_inv in H'. destruct H' as [ls [Hls H']]. revert v H'. hnf in fR. apply fR; clear fR. unfold to_list in *. inversion_by computes_to_inv. intro. handle_calls_then' ltac:(fun H => first [ specialize (H _ (AbsR_EnsembleOfList_FiniteSetOfListOfFiniteSetAndListOfList _)) | specialize (H _ (AbsR_EnsembleOfList_FiniteSetOfList _)) ]); inversion_by computes_to_inv. repeat match goal with | _ => progress subst | _ => progress simpl in * | [ H : (_, _) = (_, _) |- _ ] => inversion H; clear H | [ H : (_, _) = ?x |- context[?x] ] => destruct x end. rewrite EnsembleOfList_In in *. match goal with | [ H : ?T <-> _ |- _ <-> ?T ] => rewrite H; clear H end. destruct_head_hnf and; auto. 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