proposition: Lemma tuples_in_relation_satisfy_constraint {qs_schema}: forall (r_n : QueryStructure qs_schema) Ridx P l (P_dec : DecideableEnsemble P), For (Query_In r_n Ridx (fun r => Where (P r) Return r )) ↝ l -> forall (t t' : _ ) (n0 n' : nat), n0 <> n' -> nth_error l n0 = Some t -> nth_error l n' = Some t' -> SatisfiesTupleConstraints Ridx t t'.
proof: Proof. intros. apply refine_For_List' in H; computes_to_inv. assert (forall l', computes_to (let qs_schema := DnsSchema in let r' := r_n in Query_In r' Ridx (fun r : RawTuple => Return r )) l' -> List.incl l l'). { intros. unfold Query_In, QueryResultComp, In in *; computes_to_inv. unfold incl; intros. apply flatten_CompList_Return' in H3'; computes_to_inv; subst. pose proof (Permutation_UnIndexedEnsembleListEquivalence' H H3). rewrite <- H5. eapply flatten_CompList_Subset in H'0; eauto. rewrite H'; assumption. } assert (Permutation l v) by (symmetry; apply H'). assert (forall l', In (list RawTuple) (let qs_schema := DnsSchema in let r' := r_n in Query_In r' Ridx (fun r : RawTuple => Return r)) l' -> incl l l'). { intros allTuplesInRelation inRelation. unfold incl. intros aTuple inA. unfold incl in H4. eapply (H3 allTuplesInRelation inRelation aTuple); eauto. } assert (List.In t l). { apply exists_in_list. exists n0. auto. } assert (List.In t' l). { apply exists_in_list. exists n'. auto. } simpl in H5. eapply refine_Intersection_Where in H. unfold QueryResultComp in H; computes_to_inv. destruct H as [x' [Equiv [Equiv' Equiv''] ] ]. rewrite <- Equiv in *. eapply flatmap_permutation in H'0; rewrite H'0 in H4. destruct (unindexed_OK_exists_index' _ H0 H1 H2 H4) as [m [m' [idx [idx' ?] ] ] ]; intuition. pose proof (rawTupleconstr (ith2 (rawRels r_n) (Ridx ))) as constraint_in_relation_OK; simpl in *. unfold GetNRelSchema. destruct (tupleConstraints (Vector.map schemaRaw (QSschemaSchemas qs_schema))[@Ridx]); eauto; apply (constraint_in_relation_OK {| elementIndex := idx; indexedElement := t |} {| elementIndex := idx'; indexedElement := t' |}); simpl; try eassumption. eapply map_nth_error with (f := elementIndex) in H. eapply map_nth_error with (f := elementIndex) in H10. { revert m m' H H10 H8 Equiv''; clear; unfold Tuple; simpl; induction (map elementIndex x'). - destruct m; destruct m'; simpl; intros; try discriminate. - destruct m; destruct m'; simpl; intros; try discriminate. + intuition. + inversion Equiv''; subst. intro; subst; apply H2; injections; apply exists_in_list; eauto. + inversion Equiv''; subst. intro; subst; apply H2; injections; apply exists_in_list; eauto. + inversion Equiv''; eauto. } assert (List.In {| elementIndex := idx; indexedElement := t |} x'). { eapply exists_in_list; eauto. } apply Equiv' in H9; destruct H9; apply H9. assert (List.In {| elementIndex := idx'; indexedElement := t' |} x'). { eapply exists_in_list; eauto. } apply Equiv' in H9; destruct H9; apply H9. eauto. Qed.
imports: Coq.Vectors.Vector Coq.Strings.Ascii Coq.Bool.Bool Coq.Bool.Bvector Coq.Lists.List Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Examples.DnsServer.DecomposeSumField Fiat.Computation.FoldComp Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema