proposition: Lemma refine_EnsembleListEquivalenceAdd_iff {T} ls a : refine (S <- {S : Ensemble T | forall x, Ensembles.In T S x <-> a = x \/ List.In x ls}; {ls' : list T | EnsembleListEquivalence S ls'}) (S <- {S : Ensemble T | forall x, Ensembles.In T S x <-> List.In x ls}; ls' <- {ls' : list T | EnsembleListEquivalence S ls'}; b <- { b : bool | b = true <-> List.In a ls }; ret (if b then ls' else a::ls')).
proof: Proof. repeat intro. repeat match goal with | [ H : computes_to (Bind _ _) _ |- _ ] => apply computes_to_inv in H; destruct_head_hnf ex; destruct_head_hnf and | [ H : computes_to (ret _) _ |- _ ] => apply computes_to_inv in H | _ => progress subst | _ => progress inversion_by computes_to_inv | _ => progress split_iff end. let S := match goal with H : Ensemble _ |- _ => constr:(H) end in apply BindComputes with (comp_a_value := (Ensembles.Add _ S a)); constructor; repeat match goal with | _ => intro | _ => split | _ => progress destruct_head_hnf Union | _ => progress destruct_head_hnf Singleton | _ => progress destruct_head_hnf sumbool | _ => progress destruct_head_hnf or | _ => progress destruct_head_hnf and | _ => progress destruct_head_hnf bool | _ => progress split_iff | _ => progress subst | _ => solve [ left; eauto ] | _ => solve [ right; eauto ] | [ H : forall x, Ensembles.In _ _ _ -> _, H' : Ensembles.In _ _ _ |- _ ] => specialize (H _ H') | _ => solve [ eauto ] | _ => solve [ constructor; intuition ] 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