proposition: Lemma refine_UnIndexedEnsembleListEquivalence_Iterate_Equiv_QueryResultComp m (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) (distinctIndexes : forall idx idx' tup tup', idx <> idx' -> Ensembles idx tup -> Ensembles idx' tup' -> elementIndex tup <> elementIndex tup') : refine {queriedList : list RawTuple | UnIndexedEnsembleListEquivalence (fun tup => exists idx tup', tup = {| elementIndex := elementIndex tup'; indexedElement := inj_Tuple idx (indexedElement tup') |} /\ In _ (Ensembles idx) tup') queriedList} (Iterate_Equiv_QueryResultComp heading headings Ensembles inj_Tuple).
proof: Proof. revert heading headings Ensembles inj_Tuple distinctIndexes. induction m; simpl; intros; intros ? ?. - computes_to_inv; subst; computes_to_econstructor. unfold UnIndexedEnsembleListEquivalence; eexists nil; simpl; intuition eauto. unfold In in H; destruct_ex; intuition subst. inversion x0. constructor. - unfold QueryResultComp in H. computes_to_inv; subst. eapply IHm in H'; computes_to_inv; clear IHm. apply flatten_CompList_ret in H'0; computes_to_inv; subst. computes_to_econstructor. unfold UnIndexedEnsembleListEquivalence in *; destruct_ex; intuition; subst. rewrite map_map. replace (fun x1 : IndexedElement => inj_Tuple Fin.F1 (indexedElement x1)) with (fun x1 : IndexedElement => indexedElement {| elementIndex := elementIndex x1; indexedElement := inj_Tuple Fin.F1 (indexedElement x1) |}) by (apply functional_extensionality; reflexivity). rewrite <- map_map. eexists (_ ++ _)%list. rewrite map_app; intuition eauto. + unfold In in *; destruct_ex; intuition subst. revert headings Ensembles inj_Tuple distinctIndexes x0 x H0 H4 H2 H5 x3 H3. pattern m, x2. eapply Fin.caseS; clear m x2; intros. * simpl in *; apply H0 in H3; apply in_or_app; left. eapply in_map with (f := (fun x1 : IndexedElement => {| elementIndex := elementIndex x1; indexedElement := inj_Tuple Fin.F1 (indexedElement x1) |})) in H3. apply H3. * apply in_or_app; right. eapply H2; eexists _,_; intuition eauto. + apply in_app_or in H; unfold In in *; destruct_ex; intuition subst. * apply in_map_iff in H1; destruct_ex; intuition subst. eexists _, _; intuition eauto. eapply H0; eauto. * eapply H2 in H1. destruct_ex; intuition subst. eexists _, _; intuition eauto. + rewrite map_app. eapply NoDup_app_in_iff; intuition. revert H4; clear; induction x0; simpl; intros; econstructor; inversion H4; subst; eauto. intro; apply H1; revert H; clear; induction x0; simpl; intuition auto. rewrite map_map in H1. apply in_map_iff in H; apply in_map_iff in H1. destruct_ex; intuition; subst. eapply H2 in H6; eapply H0 in H7. destruct H6 as [? [? [? ?] ] ]; simpl in *; subst; simpl in *. eapply (distinctIndexes Fin.F1 (Fin.FS x1)); eauto. intros; discriminate. + intros; eapply distinctIndexes; eauto. intro; apply H0. apply Fin.FS_inj; eauto. 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