proposition: Lemma In_flatten_CompList {A} : forall (P : Ensemble A) (P_dec : forall a, P a \/ ~ P a) (il : list (@IndexedElement A)) (l : list A) (a : A), List.In a l -> flatten_CompList (map (fun x1 : IndexedElement => Where (P (indexedElement x1)) Return (indexedElement x1) ) il) ↝ l -> exists a', List.In a' il /\ indexedElement a' = a.
proof: Proof. induction il; simpl; intros; computes_to_inv; subst; simpl in *; intuition. apply in_app_or in H; intuition. unfold Query_Where in H0; computes_to_inv; intuition. destruct (P_dec (indexedElement a)). apply H in H0; unfold Query_Return in *; computes_to_inv; subst; simpl in H; exists a; simpl in H1; intuition; eauto. apply H2 in H0; subst; simpl in *; contradiction. destruct (IHil _ _ H1 H0') as [a' [In_a' a'_eq] ]; exists a'; split; eauto. Qed.
imports: Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Specification.Operations.Query Coq.Lists.List Coq.Arith.Compare_dec Coq.Bool.Bool Coq.Strings.String Fiat.Common.BoolFacts Fiat.Common.List.PermutationFacts Fiat.Common.List.ListMorphisms Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.Common.Ensembles.EnsembleListEquivalence Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.Common.IterateBoundedIndex Fiat.Common.List.ListFacts Fiat.Common.LogicFacts Fiat.Common.DecideableEnsembles Fiat.Computation.Refinements.Iterate_Decide_Comp Fiat.Computation.Refinements.General Fiat.QueryStructure.Specification.Constraints.tupleAgree Fiat.QueryStructure.Specification.Operations.Mutate