proposition: Lemma refine_Iterate_Equiv_QueryResultComp_body m {ResultT : Type} (heading : RawHeading) (headings : Fin.t m -> RawHeading) (Ensembles : forall (idx : Fin.t m), @IndexedEnsemble (@RawTuple (headings idx))) (inj_Tuple : forall (idx : Fin.t m), @RawTuple (headings idx) -> @RawTuple heading) (body : @RawTuple heading -> Comp (list ResultT)) : refineEquiv (results <- Iterate_Equiv_QueryResultComp heading headings Ensembles inj_Tuple; FlattenCompList.flatten_CompList (map body results)) (Iterate_Equiv_QueryResultComp_body heading headings Ensembles inj_Tuple body).
proof: Proof. split. - induction m; simpl. + simplify with monad laws. simpl; reflexivity. + simplify with monad laws. setoid_rewrite <- IHm. repeat setoid_rewrite refineEquiv_bind_bind. f_equiv; intro. rewrite refineEquiv_swap_bind. rewrite (refineEquiv_swap_bind (FlattenCompList.flatten_CompList (map (fun tup : RawTuple => body (inj_Tuple Fin.F1 tup)) a))). f_equiv; intro. induction a; simpl; simplify with monad laws. * setoid_rewrite refineEquiv_bind_unit. simpl; setoid_rewrite refineEquiv_unit_bind. reflexivity. * repeat setoid_rewrite refineEquiv_bind_bind. simpl. rewrite refineEquiv_swap_bind. f_equiv; intro. rewrite <- refineEquiv_bind_bind, IHa. simplify with monad laws. setoid_rewrite refineEquiv_bind_unit. setoid_rewrite <- List.app_assoc. reflexivity. - induction m; simpl. + setoid_rewrite refineEquiv_bind_unit. simpl; reflexivity. + repeat setoid_rewrite refineEquiv_bind_bind. setoid_rewrite IHm. repeat setoid_rewrite refineEquiv_bind_bind. f_equiv; intro. rewrite refineEquiv_swap_bind. setoid_rewrite (refineEquiv_swap_bind _ (Iterate_Equiv_QueryResultComp heading (fun idx : Fin.t m => headings (Fin.FS idx)) (fun idx : Fin.t m => Ensembles (Fin.FS idx)) (fun (idx : Fin.t m) (tup : RawTuple) => inj_Tuple (Fin.FS idx) tup))). setoid_rewrite refineEquiv_bind_unit. f_equiv; intro. revert a0. induction a; simpl; intros; simplify with monad laws. * setoid_rewrite refineEquiv_bind_unit. reflexivity. * repeat setoid_rewrite refineEquiv_bind_bind. repeat setoid_rewrite refineEquiv_bind_unit. setoid_rewrite map_app. simpl. rewrite <- (refineEquiv_swap_bind (body (inj_Tuple Fin.F1 a))). f_equiv; intro. setoid_rewrite map_app in IHa. setoid_rewrite <- refineEquiv_bind_bind; rewrite <- IHa. repeat setoid_rewrite refineEquiv_bind_bind. setoid_rewrite refineEquiv_bind_unit. setoid_rewrite <- List.app_assoc. f_equiv; intro. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Fiat.Common.SumType Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Bedrock.Word Bedrock.Memory