proposition: Lemma For_computes_to_In : forall {heading} P, (forall a, P a \/ ~ P a) -> forall seq ens, computes_to (For (QueryResultComp (heading := heading) ens (fun tup => Where (P tup) Return tup))) seq -> forall x, List.In x seq -> (P x /\ (exists x0, ens x0 /\ indexedRawTuple x0 = x)).
proof: Proof. unfold refine, decides; unfold Query_For, QueryResultComp; intros * excl; induction seq as [ | head seq' IH ]; intros. exfalso; intuition. computes_to_inv. pose proof (permutation_cons_in H') as in_x0. apply in_split in in_x0. destruct in_x0 as [ x0_before [ x0_after ? ] ]; subst. symmetry in H'. apply Permutation_cons_app_inv in H'. unfold UnIndexedEnsembleListEquivalence in H; destruct_ex; intuition; subst. rewrite map_map in H'0. destruct (flatten_CompList_app_cons_inv _ excl _ _ _ _ H'0) as [ x1_before [ x1_middle [ head' [ x1_after (_eq & in_orig & before & middle & after) ] ] ] ]; subst. unfold boxed_option in middle; simpl in middle. eapply Bind_inv in middle. destruct middle as [head'' (middle1 & middle2)]. apply Pick_inv in middle1. apply Bind_inv in middle2. destruct middle1 as ( spec1 & spec2 ). destruct middle2 as [ nil' (ret_nil & ret_cons) ]. apply Return_inv in ret_nil; subst. rewrite app_nil_r in *; subst. apply Return_inv in ret_cons; subst. rewrite singleton_neq_nil in spec2. destruct (excl (indexedRawTuple head')) as [ H'' | H'' ]; try solve [exfalso; intuition]. specialize (spec1 H''). apply Return_inv in spec1. injection spec1; intros; subst. destruct H0. - subst x; eauto. - pose proof (flatten_CompList_app _ _ _ _ before after) as flatten_app. eapply IH; try assumption. computes_to_econstructor; [ | computes_to_constructor; symmetry; eassumption ]. computes_to_econstructor. pose proof (EnsembleListEquivalence_slice x1_before x1_middle x1_after). instantiate (2 := (fun x0 : IndexedRawTuple => ens x0 /\ ~ List.In x0 x1_middle)). eapply PickComputes with (a := map indexedElement (x1_before ++ x1_after)). econstructor; split; eauto; intuition. destruct (H1 ens). unfold EnsembleListEquivalence; split; eauto using NoDup_IndexedElement. eapply H5; eauto. unfold Ensembles.In; split. eapply H; apply in_app_or in H2; intuition. intros; apply NoDup_IndexedElement in H3; eapply NoDup_app_inv'; eauto using in_app_or. repeat rewrite map_app in *; eauto using NoDup_slice. unfold boxed_option in *. rewrite !map_app, !map_map. apply flatten_app. - rewrite map_map in H'0. destruct (In_flatten_CompList P excl x0 (x0_before ++ head :: x0_after) x) as [x1 [In_x1 x1_eq] ]; eauto. eapply Permutation_in with (l := head :: (x0_before ++ x0_after)). eapply Permutation_middle. simpl in *; intuition; right; eauto using Permutation_in. exists x1; split; eauto. apply H; 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