proposition: Lemma refine_Query_In_Enumerate (ResultT : Type) : forall r_o (r_n : IndexedQueryStructure qs_schema BagIndexKeys), DelegateToBag_AbsR r_o r_n -> forall (idx : Fin.t _) (resultComp : RawTuple -> Comp (list ResultT)), refine (UnConstrQuery_In r_o idx resultComp) (l <- Join_Comp_Lists [ inil2 ] (fun _ => l <- CallBagEnumerate idx r_n; (ret (snd l))); (List_Query_In l (fun tup : ilist2 (B := @RawTuple) [ _ ]=> resultComp (ilist2_hd tup)))) .
proof: Proof. unfold UnConstrQuery_In, QueryResultComp, CallBagEnumerate, CallBagMethod; intros; simpl. setoid_rewrite refineEquiv_bind_bind; setoid_rewrite refineEquiv_bind_unit; simpl. unfold List_Query_In. intros v Comp_v; computes_to_inv; unfold EnsembleIndexedListEquivalence, UnIndexedEnsembleListEquivalence in *. destruct (H idx); intuition; destruct_ex; intuition; subst. unfold EnsembleIndexedListEquivalence, UnIndexedEnsembleListEquivalence in *; intuition; destruct_ex; intuition; subst. computes_to_econstructor. instantiate (1 := map indexedElement x0); computes_to_econstructor; eauto. setoid_rewrite H0 in H8. setoid_rewrite H4. revert H6 H8 H11 H5 H10; clear; intros. apply NoDup_Permutation in H8; eauto using NoDup_IndexedElement. destruct (@permu_exists _ (map indexedElement x0) x4); intuition. simpl in *; unfold GetNRelSchema in *; rewrite <- H5. eapply Permutation_map; eauto. setoid_rewrite <- H1. eexists x; intuition eauto. eapply Permutation_map in H1. symmetry in H1. eapply NoDup_Permutation_rewrite; eauto. rewrite map_map. first [ rewrite !map_app, !map_map, !app_nil_r in Comp_v''; simpl in *; rewrite map_map in Comp_v''; eauto | repeat setoid_rewrite map_app in Comp_v''; repeat setoid_rewrite map_map in Comp_v''; simpl in *; rewrite app_nil_r in Comp_v''; eauto ]. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Lists.List Coq.Program.Program Fiat.QueryStructure.Specification.Representation.Tuple Fiat.QueryStructure.Specification.Representation.Heading Fiat.Common.ilist2 Fiat.Common.i2list Fiat.Common.ilist3 Fiat.Common.i3list Coq.Bool.Bool Coq.Strings.String Coq.Structures.OrderedTypeEx Coq.Arith.Arith Fiat.Common.String_as_OT Fiat.Common.Ensembles.IndexedEnsembles Fiat.Common.DecideableEnsembles Fiat.Common.List.ListFacts Fiat.QueryStructure.Specification.Operations.FlattenCompList Fiat.QueryStructure.Implementation.Operations.General.QueryRefinements Fiat.QueryStructure.Implementation.Operations.General.InsertRefinements Fiat.QueryStructure.Implementation.Operations.General.EmptyRefinements Fiat.QueryStructure.Specification.Representation.QueryStructureNotations Fiat.QueryStructure.Implementation.ListImplementation Fiat.Common.List.PermutationFacts Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Implementation.DataStructures.BagADT.QueryStructureImplementation Fiat.QueryStructure.Implementation.DataStructures.BagADT.IndexSearchTerms Fiat.QueryStructure.Implementation.Operations.General.DeleteRefinements