proposition: Lemma EnsembleListEquivalence_Intersection_Singleton (x : W) (S0 : Ensemble W) : refine { ls' : _ | EnsembleListEquivalence (Intersection W (Singleton _ x) S0) ls' } (ls_S0 <- to_list S0; let fs_S0 := FiniteSetOfList ls_S0 in ret (if (snd (CallMethod (projT1 FiniteSetImpl) sIn fs_S0 x) : bool) then x::nil else nil)).
proof: Proof. simpl; unfold to_list; repeat intro; constructor. repeat match goal with | _ => intro | [ 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 subst | _ => progress inversion_by computes_to_inv | _ => handle_calls'' | [ H : _ |- _ ] => rewrite EnsembleOfList_In in H | _ => progress destruct_head_hnf and | _ => progress destruct_head_hnf or | _ => progress destruct_head_hnf bool | _ => progress destruct_head_hnf False | _ => progress destruct_head_hnf Union | _ => progress destruct_head_hnf Intersection | _ => progress destruct_head_hnf Singleton | _ => progress split_iff | _ => progress split_and | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) | [ |- EnsembleListEquivalence _ _ ] => split | [ |- NoDup (_::_) ] => constructor | [ |- NoDup nil ] => constructor | [ |- _ \/ False ] => left | [ |- _ <-> _ ] => split | _ => reflexivity | _ => progress unfold Ensembles.In in * | [ |- Intersection _ _ _ _ ] => constructor | _ => solve [ eauto ] | [ H : ?T -> false = true |- _ ] => assert (T -> False) by (let x := fresh in intro x; specialize (H x); inversion H); clear H 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