proposition: Lemma refine_MaxPrefix {resultT} : forall (f : resultT -> string) (l : Comp (list resultT)), refine (MaxElements (fun s s' => prefix (f s) (f s')) l) (results <- l; ret (snd (@fold_left (prod string (list resultT)) resultT (fun maxes s => If prefix (fst maxes) (f s) Then (If prefix (f s) (fst maxes) Then (fst maxes, s :: (snd maxes)) Else (f s, [s])) Else maxes) results ("", [ ])))).
proof: Proof. Admitted. Ltac implement_Count find_search_term ::= match goal with [ H : @DelegateToBag_AbsR ?qs_schema ?indices ?r_o ?r_n |- refine (Bind (Count For (UnConstrQuery_In _ ?idx (fun tup => Where (@?P tup) Return (@?f tup)))) _) _ ] => let filter_dec := eval simpl in (@DecideableEnsembles.dec _ P _) in let idx_search_update_term := eval simpl in (ith3 indices idx) in let search_term_type' := eval simpl in (BagSearchTermType idx_search_update_term) in let search_term_matcher := eval simpl in (BagMatchSearchTerm idx_search_update_term) in makeEvar search_term_type' ltac: (fun search_term => let eqv := fresh in assert (ExtensionalEq filter_dec (search_term_matcher search_term)) as eqv; [ find_search_term qs_schema idx filter_dec search_term | let H' := fresh in pose proof (@refine_BagFindBagCount _ qs_schema indices idx r_o r_n search_term P f H eqv) as H'; fold_string_hyps_in H'; fold_heading_hyps_in H'; rewrite H'; clear H' eqv ]) | [ H : @DelegateToBag_AbsR ?qs_schema ?indices ?r_o ?r_n |- refine (Bind (Count For (UnConstrQuery_In _ ?idx (fun tup => Where (@?P tup) Return _))) _) _ ] => let filter_dec := eval simpl in (@DecideableEnsembles.dec _ P _) in let idx_search_update_term := eval simpl in (ith3 indices idx) in let search_term_type' := eval simpl in (BagSearchTermType idx_search_update_term) in let search_term_matcher := eval simpl in (BagMatchSearchTerm idx_search_update_term) in makeEvar search_term_type' ltac: (fun search_term => let eqv := fresh in assert (ExtensionalEq filter_dec (search_term_matcher search_term)) as eqv; [ find_search_term qs_schema idx filter_dec search_term | let H' := fresh in pose proof (@refine_BagFindBagCount unit qs_schema indices idx r_o r_n search_term P (fun _ => tt) _ H eqv) as H'; fold_string_hyps_in H'; fold_heading_hyps_in H'; rewrite H'; clear H' eqv ]) end. Ltac implement_insert''' := first [ implement_simple_For ltac:(find_simple_search_term ltac:(CombineCase5 StringPrefixIndexUse EqIndexUse) ltac:(CombineCase10 createEarlyStringPrefixTerm createEarlyEqualityTerm) ltac:(CombineCase7 createLastStringPrefixTerm createLastEqualityTerm)) | implement_Count ltac:(find_simple_search_term ltac:(CombineCase5 StringPrefixIndexUse EqIndexUse) ltac:(CombineCase10 createEarlyStringPrefixTerm createEarlyEqualityTerm) ltac:(CombineCase7 createLastStringPrefixTerm createLastEqualityTerm)) | implement_insert'']. Ltac simplify_Query_Where ::= match goal with |- context [UnConstrQuery_In ?r_n ?Ridx (fun tup => Query_Where (@?P tup) _)] => rewrite (fun ResultT => @refine_UnConstrQuery_In_Query_Where_Cond _ r_n Ridx ResultT P); [ | intros; match goal with |- context [RDataTypeToRRecordType (SumType.inj_SumType ?y ?z ?x) <> ?q] => case_eq (fin_eq_dec z q); simpl; intros ? ?; try discriminate; first [let H' := fresh in assert (RDataTypeToRRecordType (SumType.inj_SumType y z x) <> q <-> True) as H' by (rewrite RDataTypeToRRecordType_inj; intuition eauto); set_evars; rewrite ?H', ?and_True_l, ?and_True_r, ?and_False_r, ?and_False_l | let H' := fresh in assert (RDataTypeToRRecordType (SumType.inj_SumType y z x) <> q <-> False) as H' by (rewrite RDataTypeToRRecordType_inj; eauto; intuition eauto); set_evars; rewrite ?H', ?and_True_l, ?and_True_r, ?and_False_r, ?and_False_l]; finish honing | |- context [RDataTypeToRRecordType (SumType.inj_SumType ?y ?z ?x) = ?q] => case_eq (fin_eq_dec z q); simpl; intros ? ?; try discriminate; first [let H' := fresh in assert (RDataTypeToRRecordType (SumType.inj_SumType y z x) = q <-> True) as H' by (rewrite RDataTypeToRRecordType_inj; intuition eauto); set_evars; rewrite ?H', ?and_True_l, ?and_True_r, ?and_False_r, ?and_False_l | let H' := fresh in assert (RDataTypeToRRecordType (SumType.inj_SumType y z x) = q <-> False) as H' by (rewrite RDataTypeToRRecordType_inj; eauto; intuition eauto); set_evars; rewrite ?H', ?and_True_l, ?and_True_r, ?and_False_r, ?and_False_l | rewrite RDataTypeToRRecordType_inj; eauto]; finish honing | |- context [RDataTypeToRRecordType (SumType.inj_SumType ?y ?z ?x)] => set_evars; rewrite !RDataTypeToRRecordType_inj; eauto; finish honing end] end. Ltac simplify_Query_Where' := match goal with H : DelegateToBag_AbsR ?r_o ?r_n |- refine (Bind (For (UnConstrQuery_In ?r_o ?idx (fun tup => Where False (@?body tup)))) _) _ => rewrite (@refine_Query_In_Where_False _ _ _ r_o r_n idx body H) | H : DelegateToBag_AbsR ?r_o ?r_n |- refine (Bind (For (UnConstrQuery_In (qsSchema := ?qs_schema) ?r_o ?idx (fun tup => Where (?a = ?b /\ @?Q tup) (@?body tup)))) _) _ => rewrite (@refine_Query_In_Where_Const qs_schema _ _ _ _ r_o _ idx body Q a b H) | H : DelegateToBag_AbsR ?r_o ?r_n |- refine (Bind (For (UnConstrQuery_In (qsSchema := ?qs_schema) ?r_o ?idx (fun tup => Where (?a <> ?b /\ @?Q tup) (@?body tup)))) _) _ => rewrite (@refine_Query_In_Where_Const_neq qs_schema _ _ _ _ r_o _ idx body Q a b H) | H : DelegateToBag_AbsR ?r_o ?r_n |- refine (Bind (Count (For (UnConstrQuery_In ?r_o ?idx (fun tup => Where False (@?body tup))))) _) _ => rewrite (@refine_Count_Query_In_Where_False _ _ _ r_o r_n idx body H) | H : DelegateToBag_AbsR ?r_o ?r_n |- refine (Bind (Count (For (UnConstrQuery_In (qsSchema := ?qs_schema) ?r_o ?idx (fun tup => Where (?a = ?b /\ @?Q tup) (@?body tup))))) _) _ => rewrite (@refine_Count_Query_In_Where_Const qs_schema _ _ _ _ r_o _ idx body Q a b H) | H : DelegateToBag_AbsR ?r_o ?r_n |- refine (Bind (Count (For (UnConstrQuery_In (qsSchema := ?qs_schema) ?r_o ?idx (fun tup => Where (?a <> ?b /\ @?Q tup) (@?body tup))))) _) _ => rewrite (@refine_Count_Query_In_Where_Const_neq qs_schema _ _ _ _ r_o _ idx body Q a b H) end. Lemma refine_LetIn {A B} : forall (a : A) (k k' : A -> Comp B), (forall a', a' = a -> refine (k a') (k' a')) -> refine (LetIn a k) (LetIn a k'). Proof. unfold LetIn; intros; 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.Tactics.CacheStringConstant Fiat.Computation.Decidable Fiat.Computation.IfDec Fiat.Computation.FoldComp Fiat.Computation.FueledFix Fiat.Computation.ListComputations Fiat.QueryStructure.Automation.Common Fiat.QueryStructure.Automation.MasterPlan Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindStringPrefixSearchTerms Fiat.QueryStructure.Automation.QSImplementation Bedrock.Word Fiat.Narcissus.Formats.DomainNameOpt Fiat.Narcissus.Examples.DNS.SimpleDnsOpt Fiat.Narcissus.Examples.DNS.SimpleDNSPacket Fiat.Narcissus.Stores.Cache Fiat.Narcissus.Stores.DomainNameStore Fiat.Narcissus.BinLib.AlignedDomainName Fiat.Narcissus.BinLib.AlignedByteString Fiat.Examples.DnsServer.DecomposeSumField Fiat.Examples.DnsServer.SimpleDnsLemmas Fiat.Examples.DnsServer.DnsAutomation Fiat.Examples.DnsServer.SimpleAuthoritativeDNSSchema