proposition: Lemma refine_EnsembleListEquivalenceAdd {T} ls a : refine {ls' : list T | EnsembleListEquivalence (elements (a::ls)) ls'} (ls' <- {ls' : list T | EnsembleListEquivalence (elements ls) 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 | _ => assumption | _ => right; assumption | _ => intro | [ 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 | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl) | _ => progress subst | _ => progress destruct_head_hnf bool | _ => progress destruct_head_hnf or | _ => progress inversion_by computes_to_inv | _ => progress split_iff | _ => apply PickComputes | [ H : ?T -> false = true |- _ ] => assert (~T) by (let H' := fresh in intro H'; specialize (H H'); inversion H); clear H | [ |- EnsembleListEquivalence _ _ ] => eapply EnsembleListEquivalence_Same_set; try eassumption; [] | [ |- Same_set _ _ _ ] => split; repeat intro; hnf in * | [ |- EnsembleListEquivalence _ _ ] => destruct_head_hnf and; split | _ => progress unfold elements, Ensembles.In in * | [ |- NoDup (_::_) ] => constructor | _ => solve [ eauto ] | [ |- _ <-> _ ] => split 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